Proof of Theorem colinbtwnle
| Step | Hyp | Ref
| Expression |
| 1 | | btwnsegle 36118 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐴, 𝐶〉 → 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉)) |
| 2 | | 3anrev 1101 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ↔ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁))) |
| 3 | | btwnsegle 36118 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐶, 𝐴〉 → 〈𝐶, 𝐵〉 Seg≤ 〈𝐶, 𝐴〉)) |
| 4 | 2, 3 | sylan2b 594 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐶, 𝐴〉 → 〈𝐶, 𝐵〉 Seg≤ 〈𝐶, 𝐴〉)) |
| 5 | | 3ancoma 1098 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ↔ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) |
| 6 | | btwncom 36015 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐴, 𝐶〉 ↔ 𝐵 Btwn 〈𝐶, 𝐴〉)) |
| 7 | 5, 6 | sylan2b 594 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐴, 𝐶〉 ↔ 𝐵 Btwn 〈𝐶, 𝐴〉)) |
| 8 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 9 | | simpr2 1196 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
| 10 | | simpr3 1197 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 11 | 8, 9, 10 | cgrrflx2d 35985 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 〈𝐵, 𝐶〉Cgr〈𝐶, 𝐵〉) |
| 12 | | simpr1 1195 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 13 | 8, 12, 10 | cgrrflx2d 35985 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 〈𝐴, 𝐶〉Cgr〈𝐶, 𝐴〉) |
| 14 | | seglecgr12 36112 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁))) → ((〈𝐵, 𝐶〉Cgr〈𝐶, 𝐵〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐶, 𝐴〉) → (〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉 ↔ 〈𝐶, 𝐵〉 Seg≤ 〈𝐶, 𝐴〉))) |
| 15 | 8, 9, 10, 12, 10, 10, 9, 10, 12, 14 | syl333anc 1404 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((〈𝐵, 𝐶〉Cgr〈𝐶, 𝐵〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐶, 𝐴〉) → (〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉 ↔ 〈𝐶, 𝐵〉 Seg≤ 〈𝐶, 𝐴〉))) |
| 16 | 11, 13, 15 | mp2and 699 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉 ↔ 〈𝐶, 𝐵〉 Seg≤ 〈𝐶, 𝐴〉)) |
| 17 | 4, 7, 16 | 3imtr4d 294 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐴, 𝐶〉 → 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉)) |
| 18 | 1, 17 | jcad 512 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐴, 𝐶〉 → (〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉))) |
| 19 | 18 | adantr 480 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝐴 Colinear 〈𝐵, 𝐶〉) → (𝐵 Btwn 〈𝐴, 𝐶〉 → (〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉))) |
| 20 | | brcolinear 36060 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 ↔ (𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉))) |
| 21 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉)) → 𝐴 Btwn 〈𝐵, 𝐶〉) |
| 22 | 8, 12, 9, 10, 21 | btwncomand 36016 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉)) → 𝐴 Btwn 〈𝐶, 𝐵〉) |
| 23 | 16 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉) → 〈𝐶, 𝐵〉 Seg≤ 〈𝐶, 𝐴〉) |
| 24 | 23 | adantrl 716 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉)) → 〈𝐶, 𝐵〉 Seg≤ 〈𝐶, 𝐴〉) |
| 25 | | btwncom 36015 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐵, 𝐶〉 ↔ 𝐴 Btwn 〈𝐶, 𝐵〉)) |
| 26 | | 3anrot 1100 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ↔ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) |
| 27 | | btwnsegle 36118 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐶, 𝐵〉 → 〈𝐶, 𝐴〉 Seg≤ 〈𝐶, 𝐵〉)) |
| 28 | 26, 27 | sylan2br 595 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐶, 𝐵〉 → 〈𝐶, 𝐴〉 Seg≤ 〈𝐶, 𝐵〉)) |
| 29 | 25, 28 | sylbid 240 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐵, 𝐶〉 → 〈𝐶, 𝐴〉 Seg≤ 〈𝐶, 𝐵〉)) |
| 30 | 29 | imp 406 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝐴 Btwn 〈𝐵, 𝐶〉) → 〈𝐶, 𝐴〉 Seg≤ 〈𝐶, 𝐵〉) |
| 31 | 30 | adantrr 717 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉)) → 〈𝐶, 𝐴〉 Seg≤ 〈𝐶, 𝐵〉) |
| 32 | | segleantisym 36116 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁))) → ((〈𝐶, 𝐵〉 Seg≤ 〈𝐶, 𝐴〉 ∧ 〈𝐶, 𝐴〉 Seg≤ 〈𝐶, 𝐵〉) → 〈𝐶, 𝐵〉Cgr〈𝐶, 𝐴〉)) |
| 33 | 8, 10, 9, 10, 12, 32 | syl122anc 1381 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((〈𝐶, 𝐵〉 Seg≤ 〈𝐶, 𝐴〉 ∧ 〈𝐶, 𝐴〉 Seg≤ 〈𝐶, 𝐵〉) → 〈𝐶, 𝐵〉Cgr〈𝐶, 𝐴〉)) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉)) → ((〈𝐶, 𝐵〉 Seg≤ 〈𝐶, 𝐴〉 ∧ 〈𝐶, 𝐴〉 Seg≤ 〈𝐶, 𝐵〉) → 〈𝐶, 𝐵〉Cgr〈𝐶, 𝐴〉)) |
| 35 | 24, 31, 34 | mp2and 699 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉)) → 〈𝐶, 𝐵〉Cgr〈𝐶, 𝐴〉) |
| 36 | 8, 10, 9, 12, 22, 35 | endofsegidand 36087 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉)) → 𝐵 = 𝐴) |
| 37 | | btwntriv1 36017 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → 𝐴 Btwn 〈𝐴, 𝐶〉) |
| 38 | 37 | 3adant3r2 1184 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 𝐴 Btwn 〈𝐴, 𝐶〉) |
| 39 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝐵 = 𝐴 → (𝐵 Btwn 〈𝐴, 𝐶〉 ↔ 𝐴 Btwn 〈𝐴, 𝐶〉)) |
| 40 | 38, 39 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 = 𝐴 → 𝐵 Btwn 〈𝐴, 𝐶〉)) |
| 41 | 40 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉)) → (𝐵 = 𝐴 → 𝐵 Btwn 〈𝐴, 𝐶〉)) |
| 42 | 36, 41 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉)) → 𝐵 Btwn 〈𝐴, 𝐶〉) |
| 43 | 42 | expr 456 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝐴 Btwn 〈𝐵, 𝐶〉) → (〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉 → 𝐵 Btwn 〈𝐴, 𝐶〉)) |
| 44 | 43 | adantld 490 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝐴 Btwn 〈𝐵, 𝐶〉) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉) → 𝐵 Btwn 〈𝐴, 𝐶〉)) |
| 45 | 44 | ex 412 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐵, 𝐶〉 → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉) → 𝐵 Btwn 〈𝐴, 𝐶〉))) |
| 46 | 7 | biimprd 248 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐶, 𝐴〉 → 𝐵 Btwn 〈𝐴, 𝐶〉)) |
| 47 | 46 | a1dd 50 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐶, 𝐴〉 → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉) → 𝐵 Btwn 〈𝐴, 𝐶〉))) |
| 48 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐶 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉)) → 𝐶 Btwn 〈𝐴, 𝐵〉) |
| 49 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐶 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉)) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉) |
| 50 | | 3ancomb 1099 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ↔ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) |
| 51 | | btwnsegle 36118 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 〈𝐴, 𝐶〉 Seg≤ 〈𝐴, 𝐵〉)) |
| 52 | 50, 51 | sylan2b 594 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → 〈𝐴, 𝐶〉 Seg≤ 〈𝐴, 𝐵〉)) |
| 53 | 52 | imp 406 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝐶 Btwn 〈𝐴, 𝐵〉) → 〈𝐴, 𝐶〉 Seg≤ 〈𝐴, 𝐵〉) |
| 54 | 53 | adantrr 717 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐶 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉)) → 〈𝐴, 𝐶〉 Seg≤ 〈𝐴, 𝐵〉) |
| 55 | | segleantisym 36116 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉 Seg≤ 〈𝐴, 𝐵〉) → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉)) |
| 56 | 8, 12, 9, 12, 10, 55 | syl122anc 1381 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉 Seg≤ 〈𝐴, 𝐵〉) → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉)) |
| 57 | 56 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐶 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉)) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉 Seg≤ 〈𝐴, 𝐵〉) → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉)) |
| 58 | 49, 54, 57 | mp2and 699 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐶 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉)) → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉) |
| 59 | 8, 12, 9, 10, 48, 58 | endofsegidand 36087 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐶 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉)) → 𝐵 = 𝐶) |
| 60 | | btwntriv2 36013 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → 𝐶 Btwn 〈𝐴, 𝐶〉) |
| 61 | 60 | 3adant3r2 1184 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 𝐶 Btwn 〈𝐴, 𝐶〉) |
| 62 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝐵 = 𝐶 → (𝐵 Btwn 〈𝐴, 𝐶〉 ↔ 𝐶 Btwn 〈𝐴, 𝐶〉)) |
| 63 | 61, 62 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 = 𝐶 → 𝐵 Btwn 〈𝐴, 𝐶〉)) |
| 64 | 63 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐶 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉)) → (𝐵 = 𝐶 → 𝐵 Btwn 〈𝐴, 𝐶〉)) |
| 65 | 59, 64 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐶 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉)) → 𝐵 Btwn 〈𝐴, 𝐶〉) |
| 66 | 65 | expr 456 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝐶 Btwn 〈𝐴, 𝐵〉) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 → 𝐵 Btwn 〈𝐴, 𝐶〉)) |
| 67 | 66 | adantrd 491 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝐶 Btwn 〈𝐴, 𝐵〉) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉) → 𝐵 Btwn 〈𝐴, 𝐶〉)) |
| 68 | 67 | ex 412 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐴, 𝐵〉 → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉) → 𝐵 Btwn 〈𝐴, 𝐶〉))) |
| 69 | 45, 47, 68 | 3jaod 1431 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉) → 𝐵 Btwn 〈𝐴, 𝐶〉))) |
| 70 | 20, 69 | sylbid 240 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉) → 𝐵 Btwn 〈𝐴, 𝐶〉))) |
| 71 | 70 | imp 406 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝐴 Colinear 〈𝐵, 𝐶〉) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉) → 𝐵 Btwn 〈𝐴, 𝐶〉)) |
| 72 | 19, 71 | impbid 212 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝐴 Colinear 〈𝐵, 𝐶〉) → (𝐵 Btwn 〈𝐴, 𝐶〉 ↔ (〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉))) |
| 73 | 72 | ex 412 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear 〈𝐵, 𝐶〉 → (𝐵 Btwn 〈𝐴, 𝐶〉 ↔ (〈𝐴, 𝐵〉 Seg≤ 〈𝐴, 𝐶〉 ∧ 〈𝐵, 𝐶〉 Seg≤ 〈𝐴, 𝐶〉)))) |