Library GeoCoq.Elements.OriginalProofs.proposition_46
Require Export GeoCoq.Elements.OriginalProofs.proposition_31short.
Require Export GeoCoq.Elements.OriginalProofs.lemma_triangletoparallelogram.
Require Export GeoCoq.Elements.OriginalProofs.lemma_equaltorightisright.
Require Export GeoCoq.Elements.OriginalProofs.lemma_samenotopposite.
Require Export GeoCoq.Elements.OriginalProofs.proposition_34.
Require Export GeoCoq.Elements.OriginalProofs.lemma_PGsymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_PGflip.
Section Euclid.
Context `{Ax:euclidean_euclidean}.
Lemma proposition_46 :
∀ A B R,
neq A B → nCol A B R →
∃ X Y, SQ A B X Y ∧ TS Y A B R ∧ PG A B X Y.
Proof.
intros.
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ F, (BetS B A F ∧ Cong A F A B)) by (conclude postulate_extension);destruct Tf as [F];spliter.
assert (nCol B A R) by (forward_using lemma_NCorder).
assert (Col B A F) by (conclude_def Col ).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col B A B) by (conclude_def Col ).
assert (neq B F) by (forward_using lemma_betweennotequal).
assert (nCol B F R) by (conclude lemma_NChelper).
let Tf:=fresh in
assert (Tf:∃ C, (Per B A C ∧ TS C B F R)) by (conclude proposition_11B);destruct Tf as [C];spliter.
assert (nCol B F C) by (conclude_def TS ).
assert (Col B F A) by (forward_using lemma_collinearorder).
assert (Col B F B) by (conclude_def Col ).
assert (nCol B A C) by (conclude lemma_NChelper).
assert (nCol A B C) by (forward_using lemma_NCorder).
assert (neq A C) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:∃ D, (Out A C D ∧ Cong A D A B)) by (conclude lemma_layoff);destruct Tf as [D];spliter.
assert (Out A D C) by (conclude lemma_ray5).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A B A) by (conclude_def Col ).
let Tf:=fresh in
assert (Tf:∃ q, (BetS C q R ∧ Col B F q ∧ nCol B F C)) by (conclude_def TS );destruct Tf as [q];spliter.
assert (Col F B q) by (forward_using lemma_collinearorder).
assert (Col F B A) by (forward_using lemma_collinearorder).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col F B B) by (conclude_def Col ).
assert (nCol A B C) by (conclude lemma_NChelper).
assert (Col A B F) by (forward_using lemma_collinearorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col F B A) by (forward_using lemma_collinearorder).
assert (neq B F) by (forward_using lemma_betweennotequal).
assert (neq F B) by (conclude lemma_inequalitysymmetric).
assert (Col B A q) by (conclude lemma_collinear4).
assert (Col A B q) by (forward_using lemma_collinearorder).
assert (TS C A B R) by (conclude_def TS ).
assert (TS D A B R) by (conclude lemma_9_5).
assert (Col A D C) by (conclude lemma_rayimpliescollinear).
assert (Col A C D) by (forward_using lemma_collinearorder).
assert (nCol C A B) by (forward_using lemma_NCorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col C A A) by (conclude_def Col ).
assert (Col A C D) by (conclude lemma_rayimpliescollinear).
assert (Col C A D) by (forward_using lemma_collinearorder).
assert (neq A D) by (conclude lemma_ray2).
assert (nCol C A B) by (forward_using lemma_NCorder).
assert (nCol A D B) by (conclude lemma_NChelper).
assert (nCol A B D) by (forward_using lemma_NCorder).
assert (BetS F A B) by (conclude axiom_betweennesssymmetry).
assert (Col A B B) by (conclude_def Col ).
assert (nCol F B D) by (conclude lemma_NChelper).
let Tf:=fresh in
assert (Tf:∃ G e M, (BetS G D e ∧ CongA G D A D A B ∧ Par G e F B ∧ BetS G M B ∧ BetS D M A)) by (conclude proposition_31short);destruct Tf as [G[e[M]]];spliter.
assert (Par G e A B) by (conclude lemma_collinearparallel).
assert (Par A B G e) by (conclude lemma_parallelsymmetric).
assert (Col G D e) by (conclude_def Col ).
assert (Col G e D) by (forward_using lemma_collinearorder).
let Tf:=fresh in
assert (Tf:∃ E, (PG D E B A ∧ Col G e E)) by (conclude lemma_triangletoparallelogram);destruct Tf as [E];spliter.
assert (Per C A B) by (conclude lemma_8_2).
assert (neq D A) by (conclude lemma_inequalitysymmetric).
assert (Per D A B) by (conclude lemma_collinearright).
assert (Per B A D) by (conclude lemma_8_2).
assert (Per G D A) by (conclude lemma_equaltorightisright).
let Tf:=fresh in
assert (Tf:∃ p, (BetS G D p ∧ Cong G D p D ∧ Cong G A p A ∧ neq D A)) by (conclude_def Per );destruct Tf as [p];spliter.
assert (BetS p D G) by (conclude axiom_betweennesssymmetry).
assert (Cong p D G D) by (conclude lemma_congruencesymmetric).
assert (Cong p A G A) by (conclude lemma_congruencesymmetric).
assert (Per p D A) by (conclude_def Per ).
assert (Par D A E B) by (conclude_def PG ).
assert (TP D A E B) by (conclude lemma_paralleldef2B).
assert (OS E B D A) by (conclude_def TP ).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (Col D A D) by (conclude_def Col ).
assert (nCol D A B) by (forward_using lemma_NCorder).
assert (BetS B M G) by (conclude axiom_betweennesssymmetry).
assert (Col D M A) by (conclude_def Col ).
assert (Col D A M) by (forward_using lemma_collinearorder).
assert (TS B D A G) by (conclude_def TS ).
assert (TS E D A G) by (conclude lemma_planeseparation).
assert (nCol D A E) by (conclude_def TS ).
assert (TS G D A E) by (conclude lemma_oppositesidesymmetric).
assert (nCol D A G) by (conclude_def TS ).
let Tf:=fresh in
assert (Tf:∃ d, (BetS E d G ∧ Col D A d ∧ nCol D A E)) by (conclude_def TS );destruct Tf as [d];spliter.
assert (neq E G) by (forward_using lemma_betweennotequal).
assert (neq G E) by (conclude lemma_inequalitysymmetric).
assert (neq G D) by (forward_using lemma_NCdistinct).
assert (neq D E) by (forward_using lemma_NCdistinct).
assert (¬ OS E G D A).
{
intro.
assert (¬ TS E D A G) by (conclude lemma_samenotopposite).
contradict.
}
assert (¬ BetS D G E).
{
intro.
assert (BetS E G D) by (conclude axiom_betweennesssymmetry).
assert (BetS E D e) by (conclude lemma_3_7a).
assert (OS E G D A) by (conclude_def OS ).
contradict.
}
assert (¬ BetS G E D).
{
intro.
assert (BetS D E G) by (conclude axiom_betweennesssymmetry).
assert (BetS E D e) by (conclude lemma_3_6a).
assert (OS E G D A) by (conclude_def OS ).
contradict.
}
assert (Col G D e) by (conclude_def Col ).
assert (Col e G D) by (forward_using lemma_collinearorder).
assert (Col e G E) by (forward_using lemma_collinearorder).
assert (nCol G e F) by (forward_using lemma_parallelNC).
assert (neq G e) by (forward_using lemma_NCdistinct).
assert (neq e G) by (conclude lemma_inequalitysymmetric).
assert (Col G D E) by (conclude lemma_collinear4).
assert ((eq G D ∨ eq G E ∨ eq D E ∨ BetS D G E ∨ BetS G D E ∨ BetS G E D)) by (conclude_def Col ).
assert (BetS G D E).
by cases on (eq G D ∨ eq G E ∨ eq D E ∨ BetS D G E ∨ BetS G D E ∨ BetS G E D).
{
assert (¬ ¬ BetS G D E).
{
intro.
contradict.
}
close.
}
{
assert (¬ ¬ BetS G D E).
{
intro.
contradict.
}
close.
}
{
assert (¬ ¬ BetS G D E).
{
intro.
contradict.
}
close.
}
{
assert (¬ ¬ BetS G D E).
{
intro.
contradict.
}
close.
}
{
close.
}
{
assert (¬ ¬ BetS G D E).
{
intro.
contradict.
}
close.
}
assert (Col G D E) by (conclude_def Col ).
assert (neq E D) by (conclude lemma_inequalitysymmetric).
assert (Per E D A) by (conclude lemma_collinearright).
assert ((Cong D A E B ∧ Cong D E A B ∧ CongA E D A A B E ∧ CongA D A B B E D ∧ Cong_3 E D A A B E)) by (conclude proposition_34).
assert (Cong A B D E) by (conclude lemma_congruencesymmetric).
assert (Cong A B E D) by (forward_using lemma_congruenceflip).
assert (Cong A B A D) by (conclude lemma_congruencesymmetric).
assert (Cong D E A D) by (conclude lemma_congruencetransitive).
assert (Cong A D E B) by (forward_using lemma_congruenceflip).
assert (Cong A B E B) by (conclude lemma_congruencetransitive).
assert (Cong A B B E) by (forward_using lemma_congruenceflip).
assert (Cong A B D A) by (forward_using lemma_congruenceflip).
assert (CongA B E D D A B) by (conclude lemma_equalanglessymmetric).
assert (CongA A B E E D A) by (conclude lemma_equalanglessymmetric).
assert (Per B E D) by (conclude lemma_equaltorightisright).
assert (Per A B E) by (conclude lemma_equaltorightisright).
assert (SQ A B E D) by (conclude_def SQ ).
assert (PG B A D E) by (conclude lemma_PGsymmetric).
assert (PG A B E D) by (conclude lemma_PGflip).
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.lemma_triangletoparallelogram.
Require Export GeoCoq.Elements.OriginalProofs.lemma_equaltorightisright.
Require Export GeoCoq.Elements.OriginalProofs.lemma_samenotopposite.
Require Export GeoCoq.Elements.OriginalProofs.proposition_34.
Require Export GeoCoq.Elements.OriginalProofs.lemma_PGsymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_PGflip.
Section Euclid.
Context `{Ax:euclidean_euclidean}.
Lemma proposition_46 :
∀ A B R,
neq A B → nCol A B R →
∃ X Y, SQ A B X Y ∧ TS Y A B R ∧ PG A B X Y.
Proof.
intros.
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ F, (BetS B A F ∧ Cong A F A B)) by (conclude postulate_extension);destruct Tf as [F];spliter.
assert (nCol B A R) by (forward_using lemma_NCorder).
assert (Col B A F) by (conclude_def Col ).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col B A B) by (conclude_def Col ).
assert (neq B F) by (forward_using lemma_betweennotequal).
assert (nCol B F R) by (conclude lemma_NChelper).
let Tf:=fresh in
assert (Tf:∃ C, (Per B A C ∧ TS C B F R)) by (conclude proposition_11B);destruct Tf as [C];spliter.
assert (nCol B F C) by (conclude_def TS ).
assert (Col B F A) by (forward_using lemma_collinearorder).
assert (Col B F B) by (conclude_def Col ).
assert (nCol B A C) by (conclude lemma_NChelper).
assert (nCol A B C) by (forward_using lemma_NCorder).
assert (neq A C) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:∃ D, (Out A C D ∧ Cong A D A B)) by (conclude lemma_layoff);destruct Tf as [D];spliter.
assert (Out A D C) by (conclude lemma_ray5).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A B A) by (conclude_def Col ).
let Tf:=fresh in
assert (Tf:∃ q, (BetS C q R ∧ Col B F q ∧ nCol B F C)) by (conclude_def TS );destruct Tf as [q];spliter.
assert (Col F B q) by (forward_using lemma_collinearorder).
assert (Col F B A) by (forward_using lemma_collinearorder).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col F B B) by (conclude_def Col ).
assert (nCol A B C) by (conclude lemma_NChelper).
assert (Col A B F) by (forward_using lemma_collinearorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col F B A) by (forward_using lemma_collinearorder).
assert (neq B F) by (forward_using lemma_betweennotequal).
assert (neq F B) by (conclude lemma_inequalitysymmetric).
assert (Col B A q) by (conclude lemma_collinear4).
assert (Col A B q) by (forward_using lemma_collinearorder).
assert (TS C A B R) by (conclude_def TS ).
assert (TS D A B R) by (conclude lemma_9_5).
assert (Col A D C) by (conclude lemma_rayimpliescollinear).
assert (Col A C D) by (forward_using lemma_collinearorder).
assert (nCol C A B) by (forward_using lemma_NCorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col C A A) by (conclude_def Col ).
assert (Col A C D) by (conclude lemma_rayimpliescollinear).
assert (Col C A D) by (forward_using lemma_collinearorder).
assert (neq A D) by (conclude lemma_ray2).
assert (nCol C A B) by (forward_using lemma_NCorder).
assert (nCol A D B) by (conclude lemma_NChelper).
assert (nCol A B D) by (forward_using lemma_NCorder).
assert (BetS F A B) by (conclude axiom_betweennesssymmetry).
assert (Col A B B) by (conclude_def Col ).
assert (nCol F B D) by (conclude lemma_NChelper).
let Tf:=fresh in
assert (Tf:∃ G e M, (BetS G D e ∧ CongA G D A D A B ∧ Par G e F B ∧ BetS G M B ∧ BetS D M A)) by (conclude proposition_31short);destruct Tf as [G[e[M]]];spliter.
assert (Par G e A B) by (conclude lemma_collinearparallel).
assert (Par A B G e) by (conclude lemma_parallelsymmetric).
assert (Col G D e) by (conclude_def Col ).
assert (Col G e D) by (forward_using lemma_collinearorder).
let Tf:=fresh in
assert (Tf:∃ E, (PG D E B A ∧ Col G e E)) by (conclude lemma_triangletoparallelogram);destruct Tf as [E];spliter.
assert (Per C A B) by (conclude lemma_8_2).
assert (neq D A) by (conclude lemma_inequalitysymmetric).
assert (Per D A B) by (conclude lemma_collinearright).
assert (Per B A D) by (conclude lemma_8_2).
assert (Per G D A) by (conclude lemma_equaltorightisright).
let Tf:=fresh in
assert (Tf:∃ p, (BetS G D p ∧ Cong G D p D ∧ Cong G A p A ∧ neq D A)) by (conclude_def Per );destruct Tf as [p];spliter.
assert (BetS p D G) by (conclude axiom_betweennesssymmetry).
assert (Cong p D G D) by (conclude lemma_congruencesymmetric).
assert (Cong p A G A) by (conclude lemma_congruencesymmetric).
assert (Per p D A) by (conclude_def Per ).
assert (Par D A E B) by (conclude_def PG ).
assert (TP D A E B) by (conclude lemma_paralleldef2B).
assert (OS E B D A) by (conclude_def TP ).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (Col D A D) by (conclude_def Col ).
assert (nCol D A B) by (forward_using lemma_NCorder).
assert (BetS B M G) by (conclude axiom_betweennesssymmetry).
assert (Col D M A) by (conclude_def Col ).
assert (Col D A M) by (forward_using lemma_collinearorder).
assert (TS B D A G) by (conclude_def TS ).
assert (TS E D A G) by (conclude lemma_planeseparation).
assert (nCol D A E) by (conclude_def TS ).
assert (TS G D A E) by (conclude lemma_oppositesidesymmetric).
assert (nCol D A G) by (conclude_def TS ).
let Tf:=fresh in
assert (Tf:∃ d, (BetS E d G ∧ Col D A d ∧ nCol D A E)) by (conclude_def TS );destruct Tf as [d];spliter.
assert (neq E G) by (forward_using lemma_betweennotequal).
assert (neq G E) by (conclude lemma_inequalitysymmetric).
assert (neq G D) by (forward_using lemma_NCdistinct).
assert (neq D E) by (forward_using lemma_NCdistinct).
assert (¬ OS E G D A).
{
intro.
assert (¬ TS E D A G) by (conclude lemma_samenotopposite).
contradict.
}
assert (¬ BetS D G E).
{
intro.
assert (BetS E G D) by (conclude axiom_betweennesssymmetry).
assert (BetS E D e) by (conclude lemma_3_7a).
assert (OS E G D A) by (conclude_def OS ).
contradict.
}
assert (¬ BetS G E D).
{
intro.
assert (BetS D E G) by (conclude axiom_betweennesssymmetry).
assert (BetS E D e) by (conclude lemma_3_6a).
assert (OS E G D A) by (conclude_def OS ).
contradict.
}
assert (Col G D e) by (conclude_def Col ).
assert (Col e G D) by (forward_using lemma_collinearorder).
assert (Col e G E) by (forward_using lemma_collinearorder).
assert (nCol G e F) by (forward_using lemma_parallelNC).
assert (neq G e) by (forward_using lemma_NCdistinct).
assert (neq e G) by (conclude lemma_inequalitysymmetric).
assert (Col G D E) by (conclude lemma_collinear4).
assert ((eq G D ∨ eq G E ∨ eq D E ∨ BetS D G E ∨ BetS G D E ∨ BetS G E D)) by (conclude_def Col ).
assert (BetS G D E).
by cases on (eq G D ∨ eq G E ∨ eq D E ∨ BetS D G E ∨ BetS G D E ∨ BetS G E D).
{
assert (¬ ¬ BetS G D E).
{
intro.
contradict.
}
close.
}
{
assert (¬ ¬ BetS G D E).
{
intro.
contradict.
}
close.
}
{
assert (¬ ¬ BetS G D E).
{
intro.
contradict.
}
close.
}
{
assert (¬ ¬ BetS G D E).
{
intro.
contradict.
}
close.
}
{
close.
}
{
assert (¬ ¬ BetS G D E).
{
intro.
contradict.
}
close.
}
assert (Col G D E) by (conclude_def Col ).
assert (neq E D) by (conclude lemma_inequalitysymmetric).
assert (Per E D A) by (conclude lemma_collinearright).
assert ((Cong D A E B ∧ Cong D E A B ∧ CongA E D A A B E ∧ CongA D A B B E D ∧ Cong_3 E D A A B E)) by (conclude proposition_34).
assert (Cong A B D E) by (conclude lemma_congruencesymmetric).
assert (Cong A B E D) by (forward_using lemma_congruenceflip).
assert (Cong A B A D) by (conclude lemma_congruencesymmetric).
assert (Cong D E A D) by (conclude lemma_congruencetransitive).
assert (Cong A D E B) by (forward_using lemma_congruenceflip).
assert (Cong A B E B) by (conclude lemma_congruencetransitive).
assert (Cong A B B E) by (forward_using lemma_congruenceflip).
assert (Cong A B D A) by (forward_using lemma_congruenceflip).
assert (CongA B E D D A B) by (conclude lemma_equalanglessymmetric).
assert (CongA A B E E D A) by (conclude lemma_equalanglessymmetric).
assert (Per B E D) by (conclude lemma_equaltorightisright).
assert (Per A B E) by (conclude lemma_equaltorightisright).
assert (SQ A B E D) by (conclude_def SQ ).
assert (PG B A D E) by (conclude lemma_PGsymmetric).
assert (PG A B E D) by (conclude lemma_PGflip).
close.
Qed.
End Euclid.