Démonstration du théorème l10_12
Enoncé
∀ A B C A' B' C', Δ A B C → Δ A' B' C' → AB ≡ A'B' → BC ≡ B'C' → AC ≡ A'C'
Deux cas de figure sont possibles selon que A B C et A' B' C' aient la même orientation ou non :
isométrie négative
isométrie positive
| Hypothèses | Conclusion |
|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' |
AC ≡ A'C' |
On traite dans un premier temps les cas dégénérés : A = B ou B = C
Cas dégénéré : A = B
|
A = B → AA≡A'B' AA ≡ A'B' → A'B' ≡ AA A'B' ≡ AA → A' = B' BC ≡ B'C' → AC ≡ A'C' |
HC1 (B/A) HC2 (B/A , B'/A') |
Cas dégénéré : B = C
|
B = C → BB≡B'C' BB ≡ B'C' → B'C' ≡ BB B'C' ≡ BB → B' = C' AB ≡ A'B' → AC ≡ A'C' |
HC2 (C/B) HC1 (B/C , B'/C') |
Cas A ≠ B /\ B ≠ C
| Hypothèses | Conclusion |
|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C |
AC ≡ A'C' |
On construit le milieu X de B et B' dont l'existence est assurée par le théorème "midpoint_existence"
On construit le point A1 symétrique de A' par rapport à X (ax : segment_construction)
On construit le point C1 symétrique de C' par rapport à X (ax : segment_construction)
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 |
AC ≡ A'C' |
En utilisant le théorème l7_13 qui assure qu'une symétrie centrale conserve les distances :
l7_13 : ∀ M P Q P' Q' , M milieu de P' P → M est milieu de Q' Q → PQ ≡ P'Q'
on montre (A' B' C') ≡ (A1 B C1)
- A'B' ≡ A1B
- B'C' ≡ BC1
- A'C' ≡ A1C1
|
X milieu de A' A1 → X milieu de B' B → A'B' ≡ A1B X milieu de B' B → X milieu de C' C1 → B'C' ≡ BC1 X milieu de A' A1 → X milieu de C' C1 → A'C' ≡ A1C1 |
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) |
AC ≡ A'C' |
Du théorème l8_10 :
l8_10 : ∀ A B C A' B' C', Δ A B C → (A B C) ≡ (A' B' C') → Δ A' B' C'
on déduit : Δ A1 B C1 puisque :
- Δ A' B' C' (hyp : HP2)
- (A' B' C') ≡ (A1 B C1) (hyp : H3)
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HP3 : Δ A1 B C1 |
AC ≡ A'C' |
Par transitivité de la relation de congruence ≡ :
cong_transitivity : ∀ A B C D E F , AB ≡ CD → CD ≡ EF → AB ≡ EF
on montre que :
- AB ≡ A1B puisque AB ≡ A'B' (HC1) et A'B' ≡ A1B(H3)
- BC ≡ BC1 puisque BC ≡ B'C'(HC2) et B'C' ≡ BC1(H3)
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HP3 : Δ A1 B C1 HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
AC ≡ A'C' |
sachant que A'C' ≡ A1C1 (H3), pour prouver AC ≡ A'C' il suffit de prouver AC ≡ A1C1 (transitivité de ≡ )
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HP3 : Δ A1 B C1 HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
AC ≡ A1C1 |
On construit Y le milieu de C C1 (th : midpoint_existence)
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HP3 : Δ A1 B C1 HC3 : AB ≡ A1B HC4 : BC ≡ BC1 HY : Y est milieu de C C1 |
AC ≡ A1C1 |
On distingue deux cas : B = Y et B ≠ Y
Cas B = Y
-
si A = A1 (cas d'une isométrie négative)
Hypothèses Hypothèses Conclusion HP1 : Δ A B C
HP2 : Δ A' B' C'
HC1 : AB ≡ A'B'
HC2 : BC ≡ B'C'
HD1 : A ≠ B
HD2 : B ≠ C
HXB : X milieu de B' B
HXA : X milieu de A' A
HXC : X milieu de C' C1
H3 : (A' B' C') ≡ (A B C1)
HP3 : Δ A B C1
HC3 : AB ≡ AB
HC4 : BC ≡ BC1
HY : B est milieu de C C1
AC ≡ AC1
Par définition (HP3) : Δ A B C1 := ∃ C2, B milieu de C1 C2 /\ AC1 ≡ AC2
Hypothèses Hypothèses Conclusion HP1 : Δ A B C
HP2 : Δ A' B' C'
HC1 : AB ≡ A'B'
HC2 : BC ≡ B'C'
HD1 : A ≠ B
HD2 : B ≠ C
HXB : X milieu de B' B
HXA : X milieu de A' A
HXC : X milieu de C' C1
H3 : (A' B' C') ≡ (A B C1)
HP3_1 : B milieu de C1 C2
HP3_2 : AC1 ≡ AC2
HC3 : AB ≡ AB
HC4 : BC ≡ BC1
HY : B est milieu de C C1
AC ≡ AC1
De l'hypothèse HP3_1 et HY en utilisant le théorème l7_9 on déduit que C = C2
l7_9 : ∀ P Q A X : A milieu de P X -> A milieu de Q X → P = Q
HP3_1 : B milieu de C1 C2 → B milieu C2 C1 (th l7_2)
HY : B milieu de C C1
→ C = C2 (th l7_9)
En remplaçant C2 par C dans l'hypothèse HP3_2 on obtient AC1 ≡ AC qui est le but à prouver à la symetrie près de la congruence (th : cong_symmetry)
-
si A ≠ A1 (cas d'une isométrie positive)
Hypothèses Hypothèses Conclusion HP1 : Δ A B C
HP2 : Δ A' B' C'
HC1 : AB ≡ A'B'
HC2 : BC ≡ B'C'
HD1 : A ≠ B
HD2 : B ≠ C
HD3 : A ≠ A1
HXB : X milieu de B' B
HXA : X milieu de A' A
HXC : X milieu de C' C1
H3 : (A' B' C') ≡ (A1 B C1)
HP3 : Δ A1 B C1
HC3 : AB ≡ A1B
HC4 : BC ≡ BC1
HY : B est milieu de C C1
AC ≡ A1C1
C1 ≠ B car si C1 = B alors
- d'après HY (B milieu de C B) on a B milieu de B C (th l7_2)
- en appliquant le théorème is_midpoint_id on obtient B = C qui est contradictoire avec HD2
is_midpoint_id : ∀ A B , A milieu de A B → A = B
donc C1 ≠ B
Hypothèses Hypothèses Conclusion HP1 : Δ A B C
HP2 : Δ A' B' C'
HC1 : AB ≡ A'B'
HC2 : BC ≡ B'C'
HD1 : A ≠ B
HD2 : B ≠ C
HD3 : A ≠ A1
HD4 : C1 ≠ B
HXB : X milieu de B' B
HXA : X milieu de A' A
HXC : X milieu de C' C1
H3 : (A' B' C') ≡ (A1 B C1)
HP3 : Δ A1 B C1
HC3 : AB ≡ A1B
HC4 : BC ≡ BC1
HY : B est milieu de C C1
AC ≡ A1C1
Le théorème l8_3
l8_3 : ∀ A B C A' , Δ A B C → A ≠ B → Col B A A' → Δ A' B C
appliqué aux points : C1 B A1 C devient :
Δ C1 B A1 → C1 ≠ B → Col B C1 C → Δ C B A1
or les trois hypotèses ci-dessus étant vérifiées :
- (HP3) : Δ A1 B C1 → Δ C1 B A1 (th l8_2)
- (HD4) : C1 ≠ B
- (HY) : B est milieu de C C1 → B milieu de C1 C (th l7_2)
→ Col B C1 C (th midpoint_col)midpoint_col : ∀ A M B , M milieu de A B → Col M A B
on en déduit : Δ C B A1
Hypothèses Hypothèses Conclusion HP1 : Δ A B C
HP2 : Δ A' B' C'
HC1 : AB ≡ A'B'
HC2 : BC ≡ B'C'
HD1 : A ≠ B
HD2 : B ≠ C
HD3 : A ≠ A1
HD4 : C1 ≠ B
HXB : X milieu de B' B
HXA : X milieu de A' A
HXC : X milieu de C' C1
H3 : (A' B' C') ≡ (A1 B C1)
HP3 : Δ A1 B C1
HP4 : Δ C B A1
HC3 : AB ≡ A1B
HC4 : BC ≡ BC1
HY : B est milieu de C C1
AC ≡ A1C1
On montre que A A1 et B sont colinéaires en appliquant le lemme perp_per_col :
perp_per_col : ∀ A B C X , Δ A X C → X ≠ C → Δ B X C → Col A B X
perp_per_col A A1 C B : Δ A B C → B ≠ C → Δ A1 B C → Col A A1 B
- (HP1) : Δ A B C
- (HD2) : B ≠ C
- (HP4) : Δ C B A1 → Δ A1 B C (th l_8_2)
Hypothèses Hypothèses Conclusion HP1 : Δ A B C
HP2 : Δ A' B' C'
HC1 : AB ≡ A'B'
HC2 : BC ≡ B'C'
HD1 : A ≠ B
HD2 : B ≠ C
HD3 : A ≠ A1
HD4 : C1 ≠ B
HXB : X milieu de B' B
HXA : X milieu de A' A
HXC : X milieu de C' C1
H3 : (A' B' C') ≡ (A1 B C1)
HP3 : Δ A1 B C1
HP4 : Δ C B A1
HC3 : AB ≡ A1B
HC4 : BC ≡ BC1
HY : B milieu de C C1
HCL : Col A A1 B
AC ≡ A1C1
l7_20 : ∀ M A B , Col A M B → MA ≡ MB → A = B \/ M milieu de A B
l7_20 B A A1 : Col A B A1 → BA ≡ BA1 → A = A1 \/ B milieu de A A1
permet de prouver : A = A1 \/ B milieu de A A1
En effet
- (HCl) : Col A A1 B → Col A B A1 (th col_permutation_5)
- (HC3) : AB ≡ A1B → BA ≡ BA1 (th cong_commutativity)
Comme (A = A1 \/ B milieu de A A1) /\ (A ≠ A1) (HD3) on a B milieu de A A1
Hypothèses Hypothèses Conclusion HP1 : Δ A B C
HP2 : Δ A' B' C'
HC1 : AB ≡ A'B'
HC2 : BC ≡ B'C'
HD1 : A ≠ B
HD2 : B ≠ C
HD3 : A ≠ A1
HD4 : C1 ≠ B
HXB : X milieu de B' B
HXA : X milieu de A' A
HXC : X milieu de C' C1
H3 : (A' B' C') ≡ (A1 B C1)
HP3 : Δ A1 B C1
HP4 : Δ C B A1
HC3 : AB ≡ A1B
HC4 : BC ≡ BC1
HY : B milieu de C C1
HCL : Col A A1 B
HB : B milieu de A A1
AC ≡ A1C1
En utilisant le théorème l7_13 qui assure qu'une symétrie centrale conserve les distances :
l7_13 : ∀ M P Q P' Q' , M milieu de P' P → M est milieu de Q' Q → PQ ≡ P'Q'
- (HB) : B mileu de A A1
- (HY) : B milieu de C C1
on montre que AC ≡ A1C1 qui est le but à démontrer
Cas B ≠ Y
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HP3 : Δ A1 B C1 HC3 : AB ≡ A1B HC4 : BC ≡ BC1 HY : Y est milieu de C C1 |
AC ≡ A1C1 |
On montre que C1 est le symétrique de C par rapport à BY : is_image C1 C B Y
is_image C1 C B Y := (exists Z , Z milieu C C1 /\ Col B Y Z) /\ (BY ⊥ CC1 \/ C = C1)
- (HY) : Y milieu C C1
- (th col_trivial_2) : Col B Y Y
Y est bien un témoin de l'existence du Z de la première assertion
Il reste à prouver HH : BY ⊥ CC1 \/ C = C1
si C = C1 alors HH est trivialement prouvée
si C ≠ C1 on prouve HH en montrant CC1 ⊥ BY (th perp_sym)
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HD4 : C ≠ C1 |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HP3 : Δ A1 B C1 HC3 : AB ≡ A1B HC4 : BC ≡ BC1 HY : Y milieu de C C1 |
CC1 ⊥ BY |
On déduit de (HY) et (HD4) que C ≠ Y /\ C1 ≠ Y (midpoint_diff)
midpoint_diff : ∀ A M B : A ≠ B → M milieu de A B → A ≠ M /\ B ≠ M
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HD4 :C ≠ C1 HD5 :C ≠ Y HD6 :C1 ≠ Y |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HP3 : Δ A1 B C1 HC3 : AB ≡ A1B HC4 : BC ≡ BC1 HY : Y milieu de C C1 |
CC1 ⊥ BY |
En utilisant le lemme per_perp de circonstance :
per_perp : ∀ A B C D, A ≠ B → B ≠ C → D ≠ B → D ≠ C → Col B C D →ΔA B C
→ Perp C D A B
per_perp B Y C C1 : B ≠ Y → Y ≠ C → C1 ≠ Y → C1 ≠ C → Col Y C C1 → Δ B Y C → Perp CC1 ⊥ BY
- (HD3) : B ≠ Y
- (HD5) : C ≠ Y → Y ≠ C (th diff_sym)
- (HD6) : C1 ≠ Y
- (HD4) : C ≠ C1 → C1 ≠ C (th diff_sym)
- (HY) : Y milieu de C C1 → Col Y C C1(th midpoint_col)
-
- (HY) : Y milieu de C C1
- (HC4) : BC ≡ BC1
→ Δ B Y C := ∃ Z , Y milieu de C Z /\ BC ≡ BZ (C1 témoin)
on a donc prouvé CC1 ⊥ BY et donc HH et donc que C1 est le symétrique de C par rapport à BY (is_image C1 C B Y)
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HP3 : Δ A1 B C1 HC3 : AB ≡ A1B HC4 : BC ≡ BC1 HY : Y milieu de C C1 HIC : is_image C1 C B Y |
AC ≡ A1C1 |
Deux configurations sont possibles selon que A B C et A' B' C' aient la même orientation ou non :
isométrie négative
isométrie positive
Dans le cas d'une isométrie négative A1 est le symétrique orthogonal de A par rapport à BY
En conséquence on distingue le cas où A1 est le symétrique orthogonal de A et le cas contraire
Cas : A1 est le symétrique de A
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HP3 : Δ A1 B C1 HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HY : Y milieu de C C1 HIC : is_image C1 C B Y HIA : is_image A1 A B Y |
AC ≡ A1C1 |
On peut dès lors appliquer le théorème l10_10 qui affirme que la projection orthogonale préserve les distances :
l10_10 : ∀ A B P Q P' Q' , A ≠ B → is_image P' P A B → is_image Q' Q A B → PQ ≡ P'Q'
- HIC : is_image C1 C B Y
- HIA : is_image A1 A B Y
→ AC ≡ A1C1 qui est le but à prouver
Cas : A1 n'est pas le symétrique de A par rapport à BY
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HP3 : Δ A1 B C1 HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HY : Y milieu de C C1 HIC : is_image C1 C B Y HNI : ¬ is_image A1 A B Y |
AC ≡ A1C1 |
On construit le point A2 symétrique de A1 par rapport à BY dont l'existence est assurée par le théorème l10_6_existence
l10_6_existence : ∀ A B P', A ≠ B → ∃ P , is_image P' P A B
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HP3 : Δ A1 B C1 HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HY : Y milieu de C C1 HIC : is_image C1 C B Y HNI : ¬ is_image A1 A1 B Y HIA : is_image A2 A1 B Y |
AC ≡ A1C1 |
En appliquant le théorème l10_10 qui affirme que la projection orthogonale préserve les distances :
l10_10 : ∀ A B P Q P' Q' , A ≠ B → is_image P' P A B → is_image Q' Q A B
→ PQ ≡ P'Q'
on montre que CA2 ≡ C1A1
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HP3 : Δ A1 B C1 HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HY : Y milieu de C C1 HIC : is_image C1 C B Y HNI : ¬ is_image A1 A1 B Y HIA : is_image A2 A1 B Y HC5 : CA2 ≡ C1A1 |
AC ≡ A1C1 |
On montre que B est son propre symétrique par rapport à BY par application du lemme image_col
image_col : ∀ A B X , Col A B X → is_image X X A B
image_col B Y B : Col B Y B → is_image B B B Y
Comme on a trivialement : Col B Y B (Col_trivial_3) on en déduit is_image B B B Y
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HP3 : Δ A1 B C1 HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HY : Y milieu de C C1 HIC : is_image C1 C B Y HNI : ¬ is_image A1 A1 B Y HIA : is_image A2 A1 B Y HC5 : CA2 ≡ C1A1 HIB : is_image B B B Y |
AC ≡ A1C1 |
On prouve Δ A2 B C par application du théorème image_preserves_per qui assure qu'une symétrie orthogonale préserve la perpendicularité :
image_preserves_per : ∀ A B C A' B' C' X Y , X ≠ Y →
is_image A A' X Y → is_image B B' X Y → is_image C C' X Y →
Per A B C →ΔA' B' C'
- (HD3) : B ≠ Y
- (HIA) : is_image A2 A1 B Y → is_image A1 A2 B Y (l10_4)
- (HIB) : is_image B B B Y
- (HIC) : is_image C1 C B Y
- (HP3) : Δ A1 B C1
→ Δ A2 B C
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HP3 : Δ A1 B C1 HP4 : Δ A2 B C HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HY : Y milieu de C C1 HIC : is_image C1 C B Y HNI : ¬ is_image A1 A1 B Y HIA : is_image A2 A1 B Y HC5 : CA2 ≡ C1A1 HIB : is_image B B B Y |
AC ≡ A1C1 |
en appliquant le theoreme image_col_cong :
image_col_cong : ∀ A B P P' X, is_image P P' A B → Col A B X → PX ≡ P'X
image_col_cong B Y A1 A2 B :
is_image A1 A2 B Y → Col B Y B → A1 B ≡ A2 B
On montre que A1B ≡ A2B
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HP3 : Δ A1 B C1 HP4 : Δ A2 B C HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HY : Y milieu de C C1 HIC : is_image C1 C B Y HNI : ¬ is_image A1 A1 B Y HIA : is_image A2 A1 B Y HC5 : CA2 ≡ C1A1 HIB : is_image B B B Y HC6 : A1B ≡ A2B |
AC ≡ A1C1 |
On montre que A A2 B sont colinéaires en utilisant le lemme per_per_col
per_per_col : ∀ A B C X , ΔA X C → X <> C → Δ B X C → Col A B X
per_per_col A A2 C B : Δ A B C → B ≠ C → Δ A2 B C → Col A A2 B
- (HP1) : Δ A B C
- (HHD2) : B ≠ C
- (HP4) : Δ A2 B C
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HP3 : Δ A1 B C1 HP4 : Δ A2 B C HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HY : Y milieu de C C1 HIC : is_image C1 C B Y HNI : ¬ is_image A1 A1 B Y HIA : is_image A2 A1 B Y HC5 : CA2 ≡ C1A1 HIB : is_image B B B Y HC6 : A1B ≡ A2B HCL : Col A A2 B |
AC ≡ A1C1 |
l7_20 : ∀ M A B , Col A M B → MA ≡ MB → A = B \/ M milieu de A B
permet de prouver : (A = A2) \/ (B milieu de A A2)
l7_20 B A A2 : Col A B A2 → BA ≡ BA2 → A = A2 \/ B milieu de A A2
En effet :
- (HCL) : Col A A2 B → Col A B A2 (th col_permutation_1)
- (par transitivité et commutativité de ≡ (HC3 HC6)) : (BA ≡ BA2)
si A = A2
HC5 devient CA ≡ C1A1 → AC ≡ A1C1 qui est le but à prouver
B milieu de A A2
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HP3 : Δ A1 B C1 HP4 : Δ A2 B C HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HY : Y milieu de C C1 HIC : is_image C1 C B Y HNI : ¬ is_image A1 A1 B Y HIA : is_image A2 A1 B Y HC5 : CA2 ≡ C1A1 HIB : is_image B B B Y HC6 : A1B ≡ A2B HCL : Col A A2 B HB2 : B milieu de A A2 |
AC ≡ A1C1 |
De l'hypotèse HP1 : Δ A B C on déduit Δ C B A (th l8_2)
Δ C B A := ∃ A3, B milieu de A A3 /\ CA ≡ CA3
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HP3 : Δ A1 B C1 HP4 : Δ A2 B C HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HY : Y milieu de C C1 HIC : is_image C1 C B Y HNI : ¬ is_image A1 A1 B Y HIA : is_image A2 A1 B Y HC5 : CA2 ≡ C1A1 HIB : is_image B B B Y HC6 : A1B ≡ A2B HCL : Col A A2 B HB2 : B milieu de A A2 HB3 : B milieu de A A3 HC7 : CA ≡ CA3 |
AC ≡ A1C1 |
Des l'hypothèses HB2 et HB3 on déduit que A2 = A3 (th midpoint_id)
midpoint_id : ∀ A B C C', A milieu de B C → A milieu de B C' → C = C'
| Hypothèses | Hypothèses | Conclusion |
|---|---|---|
|
HP1 : Δ A B C HP2 : Δ A' B' C' HP3 : Δ A1 B C1 HP4 : Δ A2 B C HC1 : AB ≡ A'B' HC2 : BC ≡ B'C' HD1 : A ≠ B HD2 : B ≠ C HD3 : B ≠ Y HC3 : AB ≡ A1B HC4 : BC ≡ BC1 |
HXB : X milieu de B' B HXA : X milieu de A' A1 HXC : X milieu de C' C1 H3 : (A' B' C') ≡ (A1 B C1) HY : Y milieu de C C1 HIC : is_image C1 C B Y HNI : ¬ is_image A1 A1 B Y HIA : is_image A2 A1 B Y HC5 : CA2 ≡ C1A1 HIB : is_image B B B Y HC6 : A1B ≡ A2B HCL : Col A A2 B HB2 : B milieu de A A2 HB3 : B milieu de A A2 HC7 : CA ≡ CA2 |
AC ≡ A1C1 |
puisque
- (HC7) : CA ≡ CA2
- (HC5) : CA2 ≡ C1A1
on on en déduit CA ≡ C1A1 (cong_transitivity)
et donc AC ≡ A1C1 (cong_commutativity)
En coq la démonstration nécéssite 192 pas