Construction du projeté orthogonal
Les outils
Le prolongement
Le prolongement est assuré par l'axiome segment_construction
segment_construction : ∀ A B C D : Point, ∃ E : Point, Bet A B E /\ B E ≡ C D
Le milieu sous condition
Le théorème l7_25 assure l'existence du mileu de deux points équidistants d'un troisième point
l7_25 : ∀ A B C, CA ≡ CB → ∃ X, X milieu de A B
La construction
Dans le cadre de la démonstration du théorème l8_18_existence :
l8_18_existence : ∀ A B C, ¬Col A B C → ∃ X, Col A B X /\ Perp A B C X
il est nécéssaire de construire le point X en utilisant exclusivement le prolongement et le milieu sous condition présentés plus haut
Etape 0
Hypothèse : ¬ Col A B C
Etape 1
on prolonge BA par Y de sorte que AY ≡ AC
Etape 2
puisque par construction AY ≡ AC on peut construire le milieu P de C Y
Etape 3
On prolonge AY par Z de sorte que AY ≡ PY
Etape 4
On prolonge CY par Q de sorte que YQ ≡ AY
Etape 5
On prolonge QZ par Q' de sorte que ZQ' ≡ QZ
Etape 6
On prolonge QY par C' de sorte que YC' ≡ YC
Etape 7
puisque par construction YC ≡ YC' on peut construire le milieu X de C C'
Il reste a prouver que X est bien le projeté orthogonal de C sur A B (500 pas de démonstration)