Proof of Theorem btwnconn1lem1
Step | Hyp | Ref
| Expression |
1 | | simp11 1091 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
2 | | simp13 1093 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
3 | | simp22 1095 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
4 | | simp23 1096 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) → 𝑐 ∈ (𝔼‘𝑁)) |
5 | | simp33 1099 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) → 𝑋 ∈ (𝔼‘𝑁)) |
6 | | simp31 1097 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) → 𝑑 ∈ (𝔼‘𝑁)) |
7 | | simp21 1094 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
8 | | simp12 1092 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
9 | | simp1rr 1127 |
. . . 4
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉))) → 𝐵 Btwn 〈𝐴, 𝐷〉) |
10 | 9 | adantl 482 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 𝐵 Btwn 〈𝐴, 𝐷〉) |
11 | | simp2ll 1128 |
. . . 4
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉))) → 𝐷 Btwn 〈𝐴, 𝑐〉) |
12 | 11 | adantl 482 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 𝐷 Btwn 〈𝐴, 𝑐〉) |
13 | 1, 8, 2, 3, 4, 10,
12 | btwnexch3and 32128 |
. 2
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 𝐷 Btwn 〈𝐵, 𝑐〉) |
14 | | simp2rl 1130 |
. . . . 5
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉))) → 𝐶 Btwn 〈𝐴, 𝑑〉) |
15 | 14 | adantl 482 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 𝐶 Btwn 〈𝐴, 𝑑〉) |
16 | | simp3rl 1134 |
. . . . 5
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉))) → 𝑑 Btwn 〈𝐴, 𝑋〉) |
17 | 16 | adantl 482 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 𝑑 Btwn 〈𝐴, 𝑋〉) |
18 | 1, 8, 7, 6, 5, 15,
17 | btwnexch3and 32128 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 𝑑 Btwn 〈𝐶, 𝑋〉) |
19 | 1, 6, 7, 5, 18 | btwncomand 32122 |
. 2
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 𝑑 Btwn 〈𝑋, 𝐶〉) |
20 | | simp3rr 1135 |
. . . . 5
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉))) → 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉) |
21 | 20 | adantl 482 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉) |
22 | 1, 6, 5, 3, 2, 21 | cgrcomand 32098 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 〈𝐷, 𝐵〉Cgr〈𝑑, 𝑋〉) |
23 | 1, 3, 2, 6, 5, 22 | cgrcomlrand 32108 |
. 2
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 〈𝐵, 𝐷〉Cgr〈𝑋, 𝑑〉) |
24 | | simp2lr 1129 |
. . . 4
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉))) → 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) |
25 | 24 | adantl 482 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) |
26 | | simp2rr 1131 |
. . . . 5
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉))) → 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉) |
27 | 26 | adantl 482 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉) |
28 | 1, 7, 6, 7, 3, 27 | cgrcomland 32106 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 〈𝑑, 𝐶〉Cgr〈𝐶, 𝐷〉) |
29 | 1, 3, 4, 6, 7, 7, 3, 25, 28 | cgrtr3and 32102 |
. 2
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 〈𝐷, 𝑐〉Cgr〈𝑑, 𝐶〉) |
30 | 1, 2, 3, 4, 5, 6, 7, 13, 19, 23, 29 | cgrextendand 32116 |
1
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑋〉 ∧ 〈𝑑, 𝑋〉Cgr〈𝐷, 𝐵〉)))) → 〈𝐵, 𝑐〉Cgr〈𝑋, 𝐶〉) |