Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
2 | | simp2l 1200 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
3 | | simp3r 1203 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
4 | | simp3 1139 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) |
5 | | axsegcon 26875 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∃𝑐 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉)) |
6 | 1, 2, 3, 4, 5 | syl121anc 1376 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∃𝑐 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉)) |
7 | | simp3l 1202 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
8 | | axsegcon 26875 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∃𝑑 ∈ (𝔼‘𝑁)(𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) |
9 | 1, 2, 7, 4, 8 | syl121anc 1376 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∃𝑑 ∈ (𝔼‘𝑁)(𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) |
10 | | reeanv 3270 |
. . . 4
⊢
(∃𝑐 ∈
(𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ↔ (∃𝑐 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ ∃𝑑 ∈ (𝔼‘𝑁)(𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) |
11 | 6, 9, 10 | sylanbrc 586 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) |
12 | 11 | adantr 484 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) → ∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) |
13 | | simpl1 1192 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
14 | | simpl2l 1227 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
15 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → 𝑐 ∈ (𝔼‘𝑁)) |
16 | | simpl3l 1229 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
17 | | simpl2r 1228 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
18 | | axsegcon 26875 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ∃𝑏 ∈ (𝔼‘𝑁)(𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉)) |
19 | 13, 14, 15, 16, 17, 18 | syl122anc 1380 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → ∃𝑏 ∈ (𝔼‘𝑁)(𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉)) |
20 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → 𝑑 ∈ (𝔼‘𝑁)) |
21 | | simpl3r 1230 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
22 | | axsegcon 26875 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉)) |
23 | 13, 14, 20, 21, 17, 22 | syl122anc 1380 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉)) |
24 | 19, 23 | jca 515 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → (∃𝑏 ∈ (𝔼‘𝑁)(𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ ∃𝑥 ∈ (𝔼‘𝑁)(𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉))) |
25 | 24 | adantr 484 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → (∃𝑏 ∈ (𝔼‘𝑁)(𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ ∃𝑥 ∈ (𝔼‘𝑁)(𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉))) |
26 | | reeanv 3270 |
. . . . . . . 8
⊢
(∃𝑏 ∈
(𝔼‘𝑁)∃𝑥 ∈ (𝔼‘𝑁)((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉)) ↔ (∃𝑏 ∈ (𝔼‘𝑁)(𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ ∃𝑥 ∈ (𝔼‘𝑁)(𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉))) |
27 | 25, 26 | sylibr 237 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → ∃𝑏 ∈ (𝔼‘𝑁)∃𝑥 ∈ (𝔼‘𝑁)((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉))) |
28 | 13, 14, 17 | 3jca 1129 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → (𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) |
29 | 28 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) |
30 | 16, 21, 15 | 3jca 1129 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁))) |
31 | 30 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁))) |
32 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → 𝑑 ∈ (𝔼‘𝑁)) |
33 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → 𝑏 ∈ (𝔼‘𝑁)) |
34 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → 𝑥 ∈ (𝔼‘𝑁)) |
35 | 32, 33, 34 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) |
36 | 29, 31, 35 | 3jca 1129 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)))) |
37 | | simpll 767 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉))) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) |
38 | | simplr 769 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉))) → ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) |
39 | | simpr 488 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉))) → ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉))) |
40 | 37, 38, 39 | 3jca 1129 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉))) → (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉)))) |
41 | | btwnconn1lem2 34035 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉)))) → 𝑥 = 𝑏) |
42 | 36, 40, 41 | syl2an 599 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
(𝑐 ∈
(𝔼‘𝑁) ∧
𝑑 ∈
(𝔼‘𝑁))) ∧
(𝑏 ∈
(𝔼‘𝑁) ∧
𝑥 ∈
(𝔼‘𝑁))) ∧
((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉)))) → 𝑥 = 𝑏) |
43 | | opeq2 4761 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑏 → 〈𝐴, 𝑥〉 = 〈𝐴, 𝑏〉) |
44 | 43 | breq2d 5042 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑏 → (𝑑 Btwn 〈𝐴, 𝑥〉 ↔ 𝑑 Btwn 〈𝐴, 𝑏〉)) |
45 | | opeq2 4761 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑏 → 〈𝑑, 𝑥〉 = 〈𝑑, 𝑏〉) |
46 | 45 | breq1d 5040 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑏 → (〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉 ↔ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉)) |
47 | 44, 46 | anbi12d 634 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑏 → ((𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉) ↔ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) |
48 | 47 | anbi2d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑏 → (((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉)) ↔ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉)))) |
49 | 48 | anbi2d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑏 → (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉))) ↔ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))))) |
50 | 49 | biimpac 482 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉))) ∧ 𝑥 = 𝑏) → ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉)))) |
51 | 32, 33 | jca 515 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁))) |
52 | 29, 31, 51 | jca32 519 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁))))) |
53 | | simpll 767 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) |
54 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) → ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) |
55 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) → ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) |
56 | 53, 54, 55 | 3jca 1129 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) → (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉)))) |
57 | | btwnconn1lem13 34046 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁)) ∧ (𝑑 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉)))) → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑)) |
58 | 52, 56, 57 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
(𝑐 ∈
(𝔼‘𝑁) ∧
𝑑 ∈
(𝔼‘𝑁))) ∧
(𝑏 ∈
(𝔼‘𝑁) ∧
𝑥 ∈
(𝔼‘𝑁))) ∧
((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉)))) → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑)) |
59 | 58 | ex 416 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑑, 𝑏〉Cgr〈𝐷, 𝐵〉))) → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑))) |
60 | 50, 59 | syl5 34 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉))) ∧ 𝑥 = 𝑏) → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑))) |
61 | 60 | expdimp 456 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
(𝑐 ∈
(𝔼‘𝑁) ∧
𝑑 ∈
(𝔼‘𝑁))) ∧
(𝑏 ∈
(𝔼‘𝑁) ∧
𝑥 ∈
(𝔼‘𝑁))) ∧
((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉)))) → (𝑥 = 𝑏 → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑))) |
62 | 42, 61 | mpd 15 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
(𝑐 ∈
(𝔼‘𝑁) ∧
𝑑 ∈
(𝔼‘𝑁))) ∧
(𝑏 ∈
(𝔼‘𝑁) ∧
𝑥 ∈
(𝔼‘𝑁))) ∧
((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉)))) → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑)) |
63 | 62 | an4s 660 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
(𝑐 ∈
(𝔼‘𝑁) ∧
𝑑 ∈
(𝔼‘𝑁))) ∧
(((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) ∧ ((𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉)))) → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑)) |
64 | 63 | exp32 424 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → ((𝑏 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉)) → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑)))) |
65 | 64 | rexlimdvv 3203 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → (∃𝑏 ∈ (𝔼‘𝑁)∃𝑥 ∈ (𝔼‘𝑁)((𝑐 Btwn 〈𝐴, 𝑏〉 ∧ 〈𝑐, 𝑏〉Cgr〈𝐶, 𝐵〉) ∧ (𝑑 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝑑, 𝑥〉Cgr〈𝐷, 𝐵〉)) → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑))) |
66 | 27, 65 | mpd 15 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → (𝐶 = 𝑐 ∨ 𝐷 = 𝑑)) |
67 | | orcom 869 |
. . . . . . 7
⊢ ((𝐶 = 𝑐 ∨ 𝐷 = 𝑑) ↔ (𝐷 = 𝑑 ∨ 𝐶 = 𝑐)) |
68 | | simprrl 781 |
. . . . . . . . . 10
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) → 𝐶 Btwn 〈𝐴, 𝑑〉) |
69 | 68 | adantl 485 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → 𝐶 Btwn 〈𝐴, 𝑑〉) |
70 | | opeq2 4761 |
. . . . . . . . . 10
⊢ (𝐷 = 𝑑 → 〈𝐴, 𝐷〉 = 〈𝐴, 𝑑〉) |
71 | 70 | breq2d 5042 |
. . . . . . . . 9
⊢ (𝐷 = 𝑑 → (𝐶 Btwn 〈𝐴, 𝐷〉 ↔ 𝐶 Btwn 〈𝐴, 𝑑〉)) |
72 | 69, 71 | syl5ibrcom 250 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → (𝐷 = 𝑑 → 𝐶 Btwn 〈𝐴, 𝐷〉)) |
73 | | simprll 779 |
. . . . . . . . . 10
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉))) → 𝐷 Btwn 〈𝐴, 𝑐〉) |
74 | 73 | adantl 485 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → 𝐷 Btwn 〈𝐴, 𝑐〉) |
75 | | opeq2 4761 |
. . . . . . . . . 10
⊢ (𝐶 = 𝑐 → 〈𝐴, 𝐶〉 = 〈𝐴, 𝑐〉) |
76 | 75 | breq2d 5042 |
. . . . . . . . 9
⊢ (𝐶 = 𝑐 → (𝐷 Btwn 〈𝐴, 𝐶〉 ↔ 𝐷 Btwn 〈𝐴, 𝑐〉)) |
77 | 74, 76 | syl5ibrcom 250 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → (𝐶 = 𝑐 → 𝐷 Btwn 〈𝐴, 𝐶〉)) |
78 | 72, 77 | orim12d 964 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → ((𝐷 = 𝑑 ∨ 𝐶 = 𝑐) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉))) |
79 | 67, 78 | syl5bi 245 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → ((𝐶 = 𝑐 ∨ 𝐷 = 𝑑) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉))) |
80 | 66, 79 | mpd 15 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁))) ∧ (((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉)) |
81 | 80 | an4s 660 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) ∧ ((𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁)) ∧ ((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)))) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉)) |
82 | 81 | exp32 424 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) → ((𝑐 ∈ (𝔼‘𝑁) ∧ 𝑑 ∈ (𝔼‘𝑁)) → (((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉)))) |
83 | 82 | rexlimdvv 3203 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) → (∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)((𝐷 Btwn 〈𝐴, 𝑐〉 ∧ 〈𝐷, 𝑐〉Cgr〈𝐶, 𝐷〉) ∧ (𝐶 Btwn 〈𝐴, 𝑑〉 ∧ 〈𝐶, 𝑑〉Cgr〈𝐶, 𝐷〉)) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉))) |
84 | 12, 83 | mpd 15 |
1
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐷〉))) → (𝐶 Btwn 〈𝐴, 𝐷〉 ∨ 𝐷 Btwn 〈𝐴, 𝐶〉)) |