Step | Hyp | Ref
| Expression |
1 | | simp1 1135 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
2 | | simp3l 1200 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
3 | | simp2l 1198 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
4 | | simp3r 1201 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
5 | | btwncom 34316 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐷〉 ↔ 𝐶 Btwn 〈𝐷, 𝐴〉)) |
6 | 1, 2, 3, 4, 5 | syl13anc 1371 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐷〉 ↔ 𝐶 Btwn 〈𝐷, 𝐴〉)) |
7 | | simp2r 1199 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
8 | | btwncom 34316 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐴, 𝐶〉 ↔ 𝐵 Btwn 〈𝐶, 𝐴〉)) |
9 | 1, 7, 3, 2, 8 | syl13anc 1371 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐴, 𝐶〉 ↔ 𝐵 Btwn 〈𝐶, 𝐴〉)) |
10 | 6, 9 | anbi12d 631 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐶 Btwn 〈𝐴, 𝐷〉 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉) ↔ (𝐶 Btwn 〈𝐷, 𝐴〉 ∧ 𝐵 Btwn 〈𝐶, 𝐴〉))) |
11 | | axpasch 27309 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ((𝐶 Btwn 〈𝐷, 𝐴〉 ∧ 𝐵 Btwn 〈𝐶, 𝐴〉) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn 〈𝐶, 𝐶〉 ∧ 𝑥 Btwn 〈𝐵, 𝐷〉))) |
12 | 1, 4, 2, 3, 2, 7, 11 | syl132anc 1387 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐶 Btwn 〈𝐷, 𝐴〉 ∧ 𝐵 Btwn 〈𝐶, 𝐴〉) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn 〈𝐶, 𝐶〉 ∧ 𝑥 Btwn 〈𝐵, 𝐷〉))) |
13 | 10, 12 | sylbid 239 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐶 Btwn 〈𝐴, 𝐷〉 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn 〈𝐶, 𝐶〉 ∧ 𝑥 Btwn 〈𝐵, 𝐷〉))) |
14 | 13 | ancomsd 466 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐴, 𝐷〉) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn 〈𝐶, 𝐶〉 ∧ 𝑥 Btwn 〈𝐵, 𝐷〉))) |
15 | | simpl1 1190 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
16 | | simpr 485 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁)) |
17 | | simpl3l 1227 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁)) |
18 | | axbtwnid 27307 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝑥 Btwn 〈𝐶, 𝐶〉 → 𝑥 = 𝐶)) |
19 | 15, 16, 17, 18 | syl3anc 1370 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn 〈𝐶, 𝐶〉 → 𝑥 = 𝐶)) |
20 | | breq1 5077 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝑥 Btwn 〈𝐵, 𝐷〉 ↔ 𝐶 Btwn 〈𝐵, 𝐷〉)) |
21 | 20 | biimpd 228 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝑥 Btwn 〈𝐵, 𝐷〉 → 𝐶 Btwn 〈𝐵, 𝐷〉)) |
22 | 19, 21 | syl6 35 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn 〈𝐶, 𝐶〉 → (𝑥 Btwn 〈𝐵, 𝐷〉 → 𝐶 Btwn 〈𝐵, 𝐷〉))) |
23 | 22 | impd 411 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 Btwn 〈𝐶, 𝐶〉 ∧ 𝑥 Btwn 〈𝐵, 𝐷〉) → 𝐶 Btwn 〈𝐵, 𝐷〉)) |
24 | 23 | rexlimdva 3213 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn 〈𝐶, 𝐶〉 ∧ 𝑥 Btwn 〈𝐵, 𝐷〉) → 𝐶 Btwn 〈𝐵, 𝐷〉)) |
25 | 14, 24 | syld 47 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐴, 𝐷〉) → 𝐶 Btwn 〈𝐵, 𝐷〉)) |