Metamath Proof Explorer

Theorem btwnconn1lem13

Description: Lemma for btwnconn1 . Begin back-filling and eliminating hypotheses. (Contributed by Scott Fenton, 9-Oct-2013)

Ref Expression
Assertion btwnconn1lem13 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → C = c ∨ D = d

Proof

Step Hyp Ref Expression
1 df-ne ⊢ C ≠ c ↔ ¬ C = c
2 simp2rl ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → C Btwn A d
3 2 adantr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c → C Btwn A d
4 simp2ll ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → D Btwn A c
5 4 adantr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c → D Btwn A c
6 3 5 jca ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c → C Btwn A d ∧ D Btwn A c
7 simpl1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → N ∈ ℕ
8 simprl1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
9 simpl2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
10 simprrl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → d ∈ 𝔼 ⁡ N
11 btwncom ⊢ N ∈ ℕ ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → C Btwn A d ↔ C Btwn d A
12 7 8 9 10 11 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → C Btwn A d ↔ C Btwn d A
13 simprl2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
14 simprl3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → c ∈ 𝔼 ⁡ N
15 btwncom ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N → D Btwn A c ↔ D Btwn c A
16 7 13 9 14 15 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → D Btwn A c ↔ D Btwn c A
17 12 16 anbi12d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → C Btwn A d ∧ D Btwn A c ↔ C Btwn d A ∧ D Btwn c A
18 6 17 syl5ib ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c → C Btwn d A ∧ D Btwn c A
19 axpasch ⊢ N ∈ ℕ ∧ d ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C Btwn d A ∧ D Btwn c A → ∃ e ∈ 𝔼 ⁡ N e Btwn C c ∧ e Btwn D d
20 7 10 14 9 8 13 19 syl132anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → C Btwn d A ∧ D Btwn c A → ∃ e ∈ 𝔼 ⁡ N e Btwn C c ∧ e Btwn D d
21 18 20 syld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c → ∃ e ∈ 𝔼 ⁡ N e Btwn C c ∧ e Btwn D d
22 21 imp ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c → ∃ e ∈ 𝔼 ⁡ N e Btwn C c ∧ e Btwn D d
23 simpll1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → N ∈ ℕ
24 14 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → c ∈ 𝔼 ⁡ N
25 8 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
26 10 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → d ∈ 𝔼 ⁡ N
27 axsegcon ⊢ N ∈ ℕ ∧ c ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → ∃ p ∈ 𝔼 ⁡ N C Btwn c p ∧ C p Cgr C d
28 23 24 25 25 26 27 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → ∃ p ∈ 𝔼 ⁡ N C Btwn c p ∧ C p Cgr C d
29 simpr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → e ∈ 𝔼 ⁡ N
30 axsegcon ⊢ N ∈ ℕ ∧ d ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → ∃ r ∈ 𝔼 ⁡ N C Btwn d r ∧ C r Cgr C e
31 23 26 25 25 29 30 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → ∃ r ∈ 𝔼 ⁡ N C Btwn d r ∧ C r Cgr C e
32 reeanv ⊢ ∃ p ∈ 𝔼 ⁡ N ∃ r ∈ 𝔼 ⁡ N C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ↔ ∃ p ∈ 𝔼 ⁡ N C Btwn c p ∧ C p Cgr C d ∧ ∃ r ∈ 𝔼 ⁡ N C Btwn d r ∧ C r Cgr C e
33 28 31 32 sylanbrc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → ∃ p ∈ 𝔼 ⁡ N ∃ r ∈ 𝔼 ⁡ N C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e
34 33 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d → ∃ p ∈ 𝔼 ⁡ N ∃ r ∈ 𝔼 ⁡ N C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e
35 7 ad2antrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N → N ∈ ℕ
36 simprl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N → p ∈ 𝔼 ⁡ N
37 simprr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N → r ∈ 𝔼 ⁡ N
38 axsegcon ⊢ N ∈ ℕ ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N → ∃ q ∈ 𝔼 ⁡ N r Btwn p q ∧ r q Cgr r p
39 35 36 37 37 36 38 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N → ∃ q ∈ 𝔼 ⁡ N r Btwn p q ∧ r q Cgr r p
40 39 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e → ∃ q ∈ 𝔼 ⁡ N r Btwn p q ∧ r q Cgr r p
41 simp-4l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N → N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N
42 simplrl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N
43 42 ad2antrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N
44 10 ad3antrrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N → d ∈ 𝔼 ⁡ N
45 simprrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N → b ∈ 𝔼 ⁡ N
46 45 ad3antrrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N → b ∈ 𝔼 ⁡ N
47 simpllr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N → e ∈ 𝔼 ⁡ N
48 44 46 47 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N → d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N
49 43 48 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N
50 simplrl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N → p ∈ 𝔼 ⁡ N
51 simpr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N → q ∈ 𝔼 ⁡ N
52 simplrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N → r ∈ 𝔼 ⁡ N
53 50 51 52 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N → p ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N
54 41 49 53 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N → N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N
55 simp1ll ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → A ≠ B
56 55 ad3antrrr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e → A ≠ B
57 56 adantr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → A ≠ B
58 simp1lr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → B ≠ C
59 58 ad3antrrr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e → B ≠ C
60 59 adantr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → B ≠ C
61 simpllr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e → C ≠ c
62 61 adantr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → C ≠ c
63 57 60 62 3jca ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → A ≠ B ∧ B ≠ C ∧ C ≠ c
64 simpl1r ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c → B Btwn A C ∧ B Btwn A D
65 64 ad3antrrr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → B Btwn A C ∧ B Btwn A D
66 63 65 jca ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → A ≠ B ∧ B ≠ C ∧ C ≠ c ∧ B Btwn A C ∧ B Btwn A D
67 simpll2 ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d → D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D
68 67 ad2antrr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D
69 simpl3l ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c → c Btwn A b ∧ c b Cgr C B
70 69 ad3antrrr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → c Btwn A b ∧ c b Cgr C B
71 simpl3r ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c → d Btwn A b ∧ d b Cgr D B
72 71 ad3antrrr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → d Btwn A b ∧ d b Cgr D B
73 70 72 jca ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B
74 66 68 73 3jca ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → A ≠ B ∧ B ≠ C ∧ C ≠ c ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B
75 simpllr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → e Btwn C c ∧ e Btwn D d
76 simplrl ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → C Btwn c p ∧ C p Cgr C d
77 simplrr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → C Btwn d r ∧ C r Cgr C e
78 simpr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → r Btwn p q ∧ r q Cgr r p
79 76 77 78 3jca ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p
80 74 75 79 jca32 ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → A ≠ B ∧ B ≠ C ∧ C ≠ c ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p
81 btwnconn1lem12 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ C ≠ c ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → D = d
82 54 80 81 syl2an ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ q ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ r Btwn p q ∧ r q Cgr r p → D = d
83 82 an4s ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e ∧ q ∈ 𝔼 ⁡ N ∧ r Btwn p q ∧ r q Cgr r p → D = d
84 40 83 rexlimddv ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e → D = d
85 84 an4s ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d ∧ p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e → D = d
86 85 exp32 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d → p ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N → C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e → D = d
87 86 rexlimdvv ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d → ∃ p ∈ 𝔼 ⁡ N ∃ r ∈ 𝔼 ⁡ N C Btwn c p ∧ C p Cgr C d ∧ C Btwn d r ∧ C r Cgr C e → D = d
88 34 87 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e Btwn C c ∧ e Btwn D d → D = d
89 88 an4s ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c ∧ e ∈ 𝔼 ⁡ N ∧ e Btwn C c ∧ e Btwn D d → D = d
90 22 89 rexlimddv ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B ∧ C ≠ c → D = d
91 90 expr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → C ≠ c → D = d
92 1 91 syl5bir ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → ¬ C = c → D = d
93 92 orrd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → C = c ∨ D = d