Library GeoCoq.Elements.OriginalProofs.proposition_48
Require Export GeoCoq.Elements.OriginalProofs.proposition_47.
Require Export GeoCoq.Elements.OriginalProofs.lemma_squaresequal.
Require Export GeoCoq.Elements.OriginalProofs.proposition_48A.
Require Export GeoCoq.Elements.OriginalProofs.proposition_08.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_48 :
∀ A B C D E F G H K L M,
Triangle A B C → SQ A B F G → TS G B A C → SQ A C K H → TS H C A B → SQ B C E D → TS D C B A → BetS B M C → BetS E L D → EF A B F G B M L D → EF A C K H M C E L → RE B M L D → RE M C E L →
Per B A C.
Proof.
intros.
assert (nCol A B C) by (conclude_def Triangle ).
assert (neq A C) by (forward_using lemma_NCdistinct).
assert (neq A B) by (forward_using lemma_NCdistinct).
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ R, (BetS B A R ∧ Cong A R A B)) by (conclude postulate_extension);destruct Tf as [R];spliter.
assert (Col B A R) by (conclude_def Col ).
assert (Col A B R) by (forward_using lemma_collinearorder).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col A B B) by (conclude_def Col ).
assert (neq B R) by (forward_using lemma_betweennotequal).
assert (neq R B) by (conclude lemma_inequalitysymmetric).
assert (nCol R B C) by (conclude lemma_NChelper).
assert (nCol B R C) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ Q, (Per B A Q ∧ TS Q B R C)) by (conclude proposition_11B);destruct Tf as [Q];spliter.
assert (nCol B A Q) by (conclude lemma_rightangleNC).
assert (neq A Q) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:∃ c, (Out A Q c ∧ Cong A c A C)) by (conclude lemma_layoff);destruct Tf as [c];spliter.
assert (Per B A c) by (conclude lemma_8_3).
assert (nCol B A c) by (conclude lemma_rightangleNC).
assert (nCol A B c) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ f g, (SQ A B f g ∧ TS g A B c ∧ PG A B f g)) by (conclude proposition_46);destruct Tf as [f[g]];spliter.
assert (neq A c) by (forward_using lemma_NCdistinct).
assert (nCol A c B) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ k h, (SQ A c k h ∧ TS h A c B ∧ PG A c k h)) by (conclude proposition_46);destruct Tf as [k[h]];spliter.
assert (neq B c) by (forward_using lemma_NCdistinct).
assert (nCol B c A) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ e d, (SQ B c e d ∧ TS d B c A ∧ PG B c e d)) by (conclude proposition_46);destruct Tf as [e[d]];spliter.
assert (Triangle A B c) by (conclude_def Triangle ).
assert (TS g B A c) by (conclude lemma_oppositesideflip).
assert (TS h c A B) by (conclude lemma_oppositesideflip).
assert (TS d c B A) by (conclude lemma_oppositesideflip).
let Tf:=fresh in
assert (Tf:∃ m l, (PG B m l d ∧ BetS B m c ∧ PG m c e l ∧ BetS d l e ∧ EF A B f g B m l d ∧ EF A c k h m c e l)) by (conclude proposition_47);destruct Tf as [m[l]];spliter.
assert (Cong A C A c) by (conclude lemma_congruencesymmetric).
assert (EF A C K H A c k h) by (conclude lemma_squaresequal).
assert (Cong A B A B) by (conclude cn_congruencereflexive).
assert (EF A B F G A B f g) by (conclude lemma_squaresequal).
assert (EF A B F G B m l d) by (conclude axiom_EFtransitive).
assert (EF B M L D A B F G) by (conclude axiom_EFsymmetric).
assert (EF B M L D B m l d) by (conclude axiom_EFtransitive).
assert (EF M C E L A C K H) by (conclude axiom_EFsymmetric).
assert (EF M C E L A c k h) by (conclude axiom_EFtransitive).
assert (EF M C E L m c e l) by (conclude axiom_EFtransitive).
assert (BetS e l d) by (conclude axiom_betweennesssymmetry).
assert (EF B C E D B c e d) by (conclude axiom_paste5).
assert (Cong B C B c) by (conclude proposition_48A).
assert (Cong C B c B) by (forward_using lemma_congruenceflip).
assert (neq B C) by (forward_using lemma_NCdistinct).
assert (Cong A C A c) by (conclude lemma_congruencesymmetric).
assert (Triangle A B c) by (conclude_def Triangle ).
assert (CongA B A C B A c) by (apply (proposition_08 A B C A B c);auto).
assert (Per B A C) by (conclude lemma_equaltorightisright).
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.lemma_squaresequal.
Require Export GeoCoq.Elements.OriginalProofs.proposition_48A.
Require Export GeoCoq.Elements.OriginalProofs.proposition_08.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_48 :
∀ A B C D E F G H K L M,
Triangle A B C → SQ A B F G → TS G B A C → SQ A C K H → TS H C A B → SQ B C E D → TS D C B A → BetS B M C → BetS E L D → EF A B F G B M L D → EF A C K H M C E L → RE B M L D → RE M C E L →
Per B A C.
Proof.
intros.
assert (nCol A B C) by (conclude_def Triangle ).
assert (neq A C) by (forward_using lemma_NCdistinct).
assert (neq A B) by (forward_using lemma_NCdistinct).
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ R, (BetS B A R ∧ Cong A R A B)) by (conclude postulate_extension);destruct Tf as [R];spliter.
assert (Col B A R) by (conclude_def Col ).
assert (Col A B R) by (forward_using lemma_collinearorder).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col A B B) by (conclude_def Col ).
assert (neq B R) by (forward_using lemma_betweennotequal).
assert (neq R B) by (conclude lemma_inequalitysymmetric).
assert (nCol R B C) by (conclude lemma_NChelper).
assert (nCol B R C) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ Q, (Per B A Q ∧ TS Q B R C)) by (conclude proposition_11B);destruct Tf as [Q];spliter.
assert (nCol B A Q) by (conclude lemma_rightangleNC).
assert (neq A Q) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:∃ c, (Out A Q c ∧ Cong A c A C)) by (conclude lemma_layoff);destruct Tf as [c];spliter.
assert (Per B A c) by (conclude lemma_8_3).
assert (nCol B A c) by (conclude lemma_rightangleNC).
assert (nCol A B c) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ f g, (SQ A B f g ∧ TS g A B c ∧ PG A B f g)) by (conclude proposition_46);destruct Tf as [f[g]];spliter.
assert (neq A c) by (forward_using lemma_NCdistinct).
assert (nCol A c B) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ k h, (SQ A c k h ∧ TS h A c B ∧ PG A c k h)) by (conclude proposition_46);destruct Tf as [k[h]];spliter.
assert (neq B c) by (forward_using lemma_NCdistinct).
assert (nCol B c A) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ e d, (SQ B c e d ∧ TS d B c A ∧ PG B c e d)) by (conclude proposition_46);destruct Tf as [e[d]];spliter.
assert (Triangle A B c) by (conclude_def Triangle ).
assert (TS g B A c) by (conclude lemma_oppositesideflip).
assert (TS h c A B) by (conclude lemma_oppositesideflip).
assert (TS d c B A) by (conclude lemma_oppositesideflip).
let Tf:=fresh in
assert (Tf:∃ m l, (PG B m l d ∧ BetS B m c ∧ PG m c e l ∧ BetS d l e ∧ EF A B f g B m l d ∧ EF A c k h m c e l)) by (conclude proposition_47);destruct Tf as [m[l]];spliter.
assert (Cong A C A c) by (conclude lemma_congruencesymmetric).
assert (EF A C K H A c k h) by (conclude lemma_squaresequal).
assert (Cong A B A B) by (conclude cn_congruencereflexive).
assert (EF A B F G A B f g) by (conclude lemma_squaresequal).
assert (EF A B F G B m l d) by (conclude axiom_EFtransitive).
assert (EF B M L D A B F G) by (conclude axiom_EFsymmetric).
assert (EF B M L D B m l d) by (conclude axiom_EFtransitive).
assert (EF M C E L A C K H) by (conclude axiom_EFsymmetric).
assert (EF M C E L A c k h) by (conclude axiom_EFtransitive).
assert (EF M C E L m c e l) by (conclude axiom_EFtransitive).
assert (BetS e l d) by (conclude axiom_betweennesssymmetry).
assert (EF B C E D B c e d) by (conclude axiom_paste5).
assert (Cong B C B c) by (conclude proposition_48A).
assert (Cong C B c B) by (forward_using lemma_congruenceflip).
assert (neq B C) by (forward_using lemma_NCdistinct).
assert (Cong A C A c) by (conclude lemma_congruencesymmetric).
assert (Triangle A B c) by (conclude_def Triangle ).
assert (CongA B A C B A c) by (apply (proposition_08 A B C A B c);auto).
assert (Per B A C) by (conclude lemma_equaltorightisright).
close.
Qed.
End Euclid.