Metamath Proof Explorer

Theorem btwnconn1lem3

Description: Lemma for btwnconn1 . Establish the next congruence in the series. (Contributed by Scott Fenton, 8-Oct-2013)

Ref Expression
Assertion btwnconn1lem3 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑏 , 𝐷 ⟩ )

Proof

Step Hyp Ref Expression
1 simp11 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
2 simp13 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simp21 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
4 simp3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) )
5 simp3r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) )
6 simp23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) )
7 simp22 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
8 simp1rl ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
9 simp2rl ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ )
10 8 9 jca ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ) )
11 10 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ) )
12 simp12 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
13 btwnexch3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝑑 ⟩ ) )
14 1 12 2 3 4 13 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝑑 ⟩ ) )
15 14 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝑑 ⟩ ) )
16 11 15 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → 𝐶 Btwn ⟨ 𝐵 , 𝑑 ⟩ )
17 simp2ll ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ )
18 simp3ll ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ )
19 17 18 jca ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ) )
20 19 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ) )
21 btwnexch3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ) → 𝑐 Btwn ⟨ 𝐷 , 𝑏 ⟩ ) )
22 1 12 7 6 5 21 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ) → 𝑐 Btwn ⟨ 𝐷 , 𝑏 ⟩ ) )
23 22 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ) → 𝑐 Btwn ⟨ 𝐷 , 𝑏 ⟩ ) )
24 20 23 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → 𝑐 Btwn ⟨ 𝐷 , 𝑏 ⟩ )
25 1 6 7 5 24 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → 𝑐 Btwn ⟨ 𝑏 , 𝐷 ⟩ )
26 simp3lr ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ )
27 26 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ )
28 cgrcomlr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ↔ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
29 1 6 5 3 2 28 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ↔ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
30 cgrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑏 , 𝑐 ⟩ ) )
31 1 5 6 2 3 30 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑏 , 𝑐 ⟩ ) )
32 29 31 bitrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑏 , 𝑐 ⟩ ) )
33 32 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ( ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑏 , 𝑐 ⟩ ) )
34 27 33 mpbid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑏 , 𝑐 ⟩ )
35 simp2rr ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
36 35 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
37 simp2lr ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) → ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
38 37 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
39 1 7 6 3 7 38 cgrcomland ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ⟨ 𝑐 , 𝐷 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
40 1 3 4 6 7 3 7 36 39 cgrtr3and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝑐 , 𝐷 ⟩ )
41 1 2 3 4 5 6 7 16 25 34 40 cgrextendand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ ⟨ 𝐷 , 𝑐 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑑 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ( 𝑐 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑐 , 𝑏 ⟩ Cgr ⟨ 𝐶 , 𝐵 ⟩ ) ∧ ( 𝑑 Btwn ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝑑 , 𝑏 ⟩ Cgr ⟨ 𝐷 , 𝐵 ⟩ ) ) ) ) → ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑏 , 𝐷 ⟩ )