Library GeoCoq.Elements.OriginalProofs.lemma_diagonalsmeet
Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelsymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_paralleldef2B.
Require Export GeoCoq.Elements.OriginalProofs.lemma_planeseparation.
Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma lemma_diagonalsmeet :
∀ A B C D,
PG A B C D →
∃ X, BetS A X C ∧ BetS B X D.
Proof.
intros.
assert ((Par A B C D ∧ Par A D B C)) by (conclude_def PG ).
let Tf:=fresh in
assert (Tf:∃ a b c d m, (neq A B ∧ neq C D ∧ Col A B a ∧ Col A B b ∧ neq a b ∧ Col C D c ∧ Col C D d ∧ neq c d ∧ ¬ Meet A B C D ∧ BetS a m d ∧ BetS c m b)) by (conclude_def Par );destruct Tf as [a[b[c[d[m]]]]];spliter.
assert (Par C D A B) by (conclude lemma_parallelsymmetric).
assert (TP C D A B) by (conclude lemma_paralleldef2B).
assert (OS A B C D) by (conclude_def TP ).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (Col D C D) by (conclude_def Col ).
assert (¬ eq A D).
{
intro.
assert (Col D C A) by (conclude cn_equalitysub).
assert (Col C D A) by (forward_using lemma_collinearorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A B A) by (conclude_def Col ).
assert (Meet A B C D) by (conclude_def Meet ).
contradict.
}
let Tf:=fresh in
assert (Tf:∃ E, (BetS A D E ∧ Cong D E A D)) by (conclude postulate_extension);destruct Tf as [E];spliter.
assert (¬ Col D C A).
{
intro.
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A B A) by (conclude_def Col ).
assert (Col C D A) by (forward_using lemma_collinearorder).
assert (Meet A B C D) by (conclude_def Meet ).
assert (¬ Meet A B C D) by (conclude_def Par ).
contradict.
}
assert (TS A D C E) by (conclude_def TS ).
assert (OS B A D C) by (forward_using lemma_samesidesymmetric).
assert (TS B D C E) by (conclude lemma_planeseparation).
let Tf:=fresh in
assert (Tf:∃ F, (BetS B F E ∧ Col D C F ∧ nCol D C B)) by (conclude_def TS );destruct Tf as [F];spliter.
assert (BetS E F B) by (conclude axiom_betweennesssymmetry).
assert (BetS E D A) by (conclude axiom_betweennesssymmetry).
assert (Col E D A) by (conclude_def Col ).
assert (neq E D) by (forward_using lemma_betweennotequal).
assert (neq E A) by (forward_using lemma_betweennotequal).
assert (¬ Meet A D B C) by (conclude_def Par ).
assert (¬ eq B C).
{
intro.
assert (Col D B C) by (conclude_def Col ).
assert (Col D C B) by (forward_using lemma_collinearorder).
contradict.
}
let Tf:=fresh in
assert (Tf:∃ S, (BetS B C S ∧ Cong C S B C)) by (conclude postulate_extension);destruct Tf as [S];spliter.
assert (BetS S C B) by (conclude axiom_betweennesssymmetry).
assert (Col S C B) by (conclude_def Col ).
assert (neq S B) by (forward_using lemma_betweennotequal).
assert (neq C B) by (forward_using lemma_betweennotequal).
assert (¬ Meet E A S B).
{
intro.
let Tf:=fresh in
assert (Tf:∃ R, (neq E A ∧ neq S B ∧ Col E A R ∧ Col S B R)) by (conclude_def Meet );destruct Tf as [R];spliter.
assert (Col B C S) by (conclude_def Col ).
assert (Col S B C) by (forward_using lemma_collinearorder).
assert (Col B C R).
by cases on (eq B R ∨ neq B R).
{
assert (Col B C R) by (conclude_def Col ).
close.
}
{
assert (Col B R C) by (conclude lemma_collinear4).
assert (Col B C R) by (forward_using lemma_collinearorder).
close.
}
assert (Col A D E) by (conclude_def Col ).
assert (Col E A D) by (forward_using lemma_collinearorder).
assert (neq A D) by (forward_using lemma_betweennotequal).
assert (Col A D R) by (conclude lemma_collinear4).
assert (Meet A D B C) by (conclude_def Meet ).
contradict.
}
assert (Col D F C) by (forward_using lemma_collinearorder).
assert (BetS D F C) by (conclude lemma_collinearbetween).
assert (BetS C F D) by (conclude axiom_betweennesssymmetry).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (neq E A) by (conclude lemma_inequalitysymmetric).
assert (neq B S) by (forward_using lemma_betweennotequal).
assert (neq S B) by (conclude lemma_inequalitysymmetric).
assert (¬ Col E A C).
{
intro.
assert (Col B C S) by (conclude_def Col ).
assert (Col S B C) by (forward_using lemma_collinearorder).
assert (Meet E A S B) by (conclude_def Meet ).
contradict.
}
rename_H H;let Tf:=fresh in
assert (Tf:∃ H, (BetS C H A ∧ BetS E F H)) by (conclude postulate_Pasch_outer);destruct Tf as [H];spliter.
assert (Col E F H) by (conclude_def Col ).
assert (Col E F B) by (conclude_def Col ).
assert (neq E F) by (forward_using lemma_betweennotequal).
assert (neq F E) by (conclude lemma_inequalitysymmetric).
assert (Col F E H) by (forward_using lemma_collinearorder).
assert (Col F E B) by (forward_using lemma_collinearorder).
assert (Col E H B) by (conclude lemma_collinear4).
assert (BetS A H C) by (conclude axiom_betweennesssymmetry).
let Tf:=fresh in
assert (Tf:∃ R, (BetS A E R ∧ Cong E R A E)) by (conclude postulate_extension);destruct Tf as [R];spliter.
assert (Col A E R) by (conclude_def Col ).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (neq A R) by (forward_using lemma_betweennotequal).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ T, (BetS C B T ∧ Cong B T C B)) by (conclude postulate_extension);destruct Tf as [T];spliter.
assert (¬ Meet A R T C).
{
intro.
let Tf:=fresh in
assert (Tf:∃ p, (neq A R ∧ neq T C ∧ Col A R p ∧ Col T C p)) by (conclude_def Meet );destruct Tf as [p];spliter.
assert (Col A E R) by (conclude_def Col ).
assert (Col C B T) by (conclude_def Col ).
assert (Col A D E) by (conclude_def Col ).
assert (Col R A p) by (forward_using lemma_collinearorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A R A) by (conclude_def Col ).
assert (Col E A D) by (forward_using lemma_collinearorder).
assert (Col A E R) by (conclude_def Col ).
assert (Col E A R) by (forward_using lemma_collinearorder).
assert (neq A D) by (forward_using lemma_betweennotequal).
assert (Col A D R) by (conclude lemma_collinear4).
assert (Col A R D) by (forward_using lemma_collinearorder).
assert (Col A D p) by (conclude lemma_collinear5).
assert (Col B T C) by (forward_using lemma_collinearorder).
assert (Col T C B) by (forward_using lemma_collinearorder).
assert (neq C T) by (forward_using lemma_betweennotequal).
assert (neq T C) by (conclude lemma_inequalitysymmetric).
assert (Col C B p) by (conclude lemma_collinear4).
assert (Col B C p) by (forward_using lemma_collinearorder).
assert (Meet A D B C) by (conclude_def Meet ).
contradict.
}
assert (BetS T B C) by (conclude axiom_betweennesssymmetry).
assert (Col T B C) by (conclude_def Col ).
assert (neq T C) by (forward_using lemma_betweennotequal).
assert (neq B C) by (forward_using lemma_betweennotequal).
assert (Col E B H) by (forward_using lemma_collinearorder).
assert (BetS E H B) by (conclude lemma_collinearbetween).
assert (BetS B H E) by (conclude axiom_betweennesssymmetry).
assert (¬ Col B E A).
{
intro.
assert (Col A D E) by (conclude_def Col ).
assert (Col E A D) by (forward_using lemma_collinearorder).
assert (Col E A B) by (forward_using lemma_collinearorder).
assert (Col A D B) by (conclude lemma_collinear4).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col B C B) by (conclude_def Col ).
assert (Meet A D B C) by (conclude_def Meet ).
contradict.
}
let Tf:=fresh in
assert (Tf:∃ M, (BetS B M D ∧ BetS A M H)) by (conclude postulate_Pasch_inner);destruct Tf as [M];spliter.
assert (BetS A H C) by (conclude axiom_betweennesssymmetry).
assert (BetS A M C) by (conclude lemma_3_6b).
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.lemma_paralleldef2B.
Require Export GeoCoq.Elements.OriginalProofs.lemma_planeseparation.
Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma lemma_diagonalsmeet :
∀ A B C D,
PG A B C D →
∃ X, BetS A X C ∧ BetS B X D.
Proof.
intros.
assert ((Par A B C D ∧ Par A D B C)) by (conclude_def PG ).
let Tf:=fresh in
assert (Tf:∃ a b c d m, (neq A B ∧ neq C D ∧ Col A B a ∧ Col A B b ∧ neq a b ∧ Col C D c ∧ Col C D d ∧ neq c d ∧ ¬ Meet A B C D ∧ BetS a m d ∧ BetS c m b)) by (conclude_def Par );destruct Tf as [a[b[c[d[m]]]]];spliter.
assert (Par C D A B) by (conclude lemma_parallelsymmetric).
assert (TP C D A B) by (conclude lemma_paralleldef2B).
assert (OS A B C D) by (conclude_def TP ).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (Col D C D) by (conclude_def Col ).
assert (¬ eq A D).
{
intro.
assert (Col D C A) by (conclude cn_equalitysub).
assert (Col C D A) by (forward_using lemma_collinearorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A B A) by (conclude_def Col ).
assert (Meet A B C D) by (conclude_def Meet ).
contradict.
}
let Tf:=fresh in
assert (Tf:∃ E, (BetS A D E ∧ Cong D E A D)) by (conclude postulate_extension);destruct Tf as [E];spliter.
assert (¬ Col D C A).
{
intro.
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A B A) by (conclude_def Col ).
assert (Col C D A) by (forward_using lemma_collinearorder).
assert (Meet A B C D) by (conclude_def Meet ).
assert (¬ Meet A B C D) by (conclude_def Par ).
contradict.
}
assert (TS A D C E) by (conclude_def TS ).
assert (OS B A D C) by (forward_using lemma_samesidesymmetric).
assert (TS B D C E) by (conclude lemma_planeseparation).
let Tf:=fresh in
assert (Tf:∃ F, (BetS B F E ∧ Col D C F ∧ nCol D C B)) by (conclude_def TS );destruct Tf as [F];spliter.
assert (BetS E F B) by (conclude axiom_betweennesssymmetry).
assert (BetS E D A) by (conclude axiom_betweennesssymmetry).
assert (Col E D A) by (conclude_def Col ).
assert (neq E D) by (forward_using lemma_betweennotequal).
assert (neq E A) by (forward_using lemma_betweennotequal).
assert (¬ Meet A D B C) by (conclude_def Par ).
assert (¬ eq B C).
{
intro.
assert (Col D B C) by (conclude_def Col ).
assert (Col D C B) by (forward_using lemma_collinearorder).
contradict.
}
let Tf:=fresh in
assert (Tf:∃ S, (BetS B C S ∧ Cong C S B C)) by (conclude postulate_extension);destruct Tf as [S];spliter.
assert (BetS S C B) by (conclude axiom_betweennesssymmetry).
assert (Col S C B) by (conclude_def Col ).
assert (neq S B) by (forward_using lemma_betweennotequal).
assert (neq C B) by (forward_using lemma_betweennotequal).
assert (¬ Meet E A S B).
{
intro.
let Tf:=fresh in
assert (Tf:∃ R, (neq E A ∧ neq S B ∧ Col E A R ∧ Col S B R)) by (conclude_def Meet );destruct Tf as [R];spliter.
assert (Col B C S) by (conclude_def Col ).
assert (Col S B C) by (forward_using lemma_collinearorder).
assert (Col B C R).
by cases on (eq B R ∨ neq B R).
{
assert (Col B C R) by (conclude_def Col ).
close.
}
{
assert (Col B R C) by (conclude lemma_collinear4).
assert (Col B C R) by (forward_using lemma_collinearorder).
close.
}
assert (Col A D E) by (conclude_def Col ).
assert (Col E A D) by (forward_using lemma_collinearorder).
assert (neq A D) by (forward_using lemma_betweennotequal).
assert (Col A D R) by (conclude lemma_collinear4).
assert (Meet A D B C) by (conclude_def Meet ).
contradict.
}
assert (Col D F C) by (forward_using lemma_collinearorder).
assert (BetS D F C) by (conclude lemma_collinearbetween).
assert (BetS C F D) by (conclude axiom_betweennesssymmetry).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (neq E A) by (conclude lemma_inequalitysymmetric).
assert (neq B S) by (forward_using lemma_betweennotequal).
assert (neq S B) by (conclude lemma_inequalitysymmetric).
assert (¬ Col E A C).
{
intro.
assert (Col B C S) by (conclude_def Col ).
assert (Col S B C) by (forward_using lemma_collinearorder).
assert (Meet E A S B) by (conclude_def Meet ).
contradict.
}
rename_H H;let Tf:=fresh in
assert (Tf:∃ H, (BetS C H A ∧ BetS E F H)) by (conclude postulate_Pasch_outer);destruct Tf as [H];spliter.
assert (Col E F H) by (conclude_def Col ).
assert (Col E F B) by (conclude_def Col ).
assert (neq E F) by (forward_using lemma_betweennotequal).
assert (neq F E) by (conclude lemma_inequalitysymmetric).
assert (Col F E H) by (forward_using lemma_collinearorder).
assert (Col F E B) by (forward_using lemma_collinearorder).
assert (Col E H B) by (conclude lemma_collinear4).
assert (BetS A H C) by (conclude axiom_betweennesssymmetry).
let Tf:=fresh in
assert (Tf:∃ R, (BetS A E R ∧ Cong E R A E)) by (conclude postulate_extension);destruct Tf as [R];spliter.
assert (Col A E R) by (conclude_def Col ).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (neq A R) by (forward_using lemma_betweennotequal).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ T, (BetS C B T ∧ Cong B T C B)) by (conclude postulate_extension);destruct Tf as [T];spliter.
assert (¬ Meet A R T C).
{
intro.
let Tf:=fresh in
assert (Tf:∃ p, (neq A R ∧ neq T C ∧ Col A R p ∧ Col T C p)) by (conclude_def Meet );destruct Tf as [p];spliter.
assert (Col A E R) by (conclude_def Col ).
assert (Col C B T) by (conclude_def Col ).
assert (Col A D E) by (conclude_def Col ).
assert (Col R A p) by (forward_using lemma_collinearorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A R A) by (conclude_def Col ).
assert (Col E A D) by (forward_using lemma_collinearorder).
assert (Col A E R) by (conclude_def Col ).
assert (Col E A R) by (forward_using lemma_collinearorder).
assert (neq A D) by (forward_using lemma_betweennotequal).
assert (Col A D R) by (conclude lemma_collinear4).
assert (Col A R D) by (forward_using lemma_collinearorder).
assert (Col A D p) by (conclude lemma_collinear5).
assert (Col B T C) by (forward_using lemma_collinearorder).
assert (Col T C B) by (forward_using lemma_collinearorder).
assert (neq C T) by (forward_using lemma_betweennotequal).
assert (neq T C) by (conclude lemma_inequalitysymmetric).
assert (Col C B p) by (conclude lemma_collinear4).
assert (Col B C p) by (forward_using lemma_collinearorder).
assert (Meet A D B C) by (conclude_def Meet ).
contradict.
}
assert (BetS T B C) by (conclude axiom_betweennesssymmetry).
assert (Col T B C) by (conclude_def Col ).
assert (neq T C) by (forward_using lemma_betweennotequal).
assert (neq B C) by (forward_using lemma_betweennotequal).
assert (Col E B H) by (forward_using lemma_collinearorder).
assert (BetS E H B) by (conclude lemma_collinearbetween).
assert (BetS B H E) by (conclude axiom_betweennesssymmetry).
assert (¬ Col B E A).
{
intro.
assert (Col A D E) by (conclude_def Col ).
assert (Col E A D) by (forward_using lemma_collinearorder).
assert (Col E A B) by (forward_using lemma_collinearorder).
assert (Col A D B) by (conclude lemma_collinear4).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col B C B) by (conclude_def Col ).
assert (Meet A D B C) by (conclude_def Meet ).
contradict.
}
let Tf:=fresh in
assert (Tf:∃ M, (BetS B M D ∧ BetS A M H)) by (conclude postulate_Pasch_inner);destruct Tf as [M];spliter.
assert (BetS A H C) by (conclude axiom_betweennesssymmetry).
assert (BetS A M C) by (conclude lemma_3_6b).
close.
Qed.
End Euclid.