Proof of Theorem endofsegid
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) | 
| 2 |  | simpr1 1195 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) | 
| 3 |  | simpr3 1197 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) | 
| 4 |  | simpr2 1196 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) | 
| 5 |  | cgrcom 35991 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉 ↔ 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉)) | 
| 6 | 1, 2, 3, 2, 4, 5 | syl122anc 1381 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉 ↔ 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉)) | 
| 7 | 6 | biimpd 229 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉 → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉)) | 
| 8 |  | idd 24 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉 → 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉)) | 
| 9 |  | axcgrrflx 28929 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → 〈𝐵, 𝐶〉Cgr〈𝐶, 𝐵〉) | 
| 10 | 9 | 3adant3r1 1183 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 〈𝐵, 𝐶〉Cgr〈𝐶, 𝐵〉) | 
| 11 | 10 | a1d 25 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉 → 〈𝐵, 𝐶〉Cgr〈𝐶, 𝐵〉)) | 
| 12 | 7, 8, 11 | 3jcad 1130 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉 → (〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐶, 𝐵〉))) | 
| 13 |  | 3ancomb 1099 | . . . . . . 7
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ↔ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) | 
| 14 |  | brcgr3 36047 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐴, 〈𝐶, 𝐵〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐶, 𝐵〉))) | 
| 15 | 13, 14 | syl3an3br 1410 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐴, 〈𝐶, 𝐵〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐶, 𝐵〉))) | 
| 16 | 15 | 3anidm23 1423 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐴, 〈𝐶, 𝐵〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐶, 𝐵〉))) | 
| 17 | 12, 16 | sylibrd 259 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉 → 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐴, 〈𝐶, 𝐵〉〉)) | 
| 18 |  | btwnxfr 36057 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐴, 〈𝐶, 𝐵〉〉) → 𝐶 Btwn 〈𝐴, 𝐵〉)) | 
| 19 | 13, 18 | syl3an3br 1410 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐴, 〈𝐶, 𝐵〉〉) → 𝐶 Btwn 〈𝐴, 𝐵〉)) | 
| 20 | 19 | 3anidm23 1423 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐴, 〈𝐶, 𝐵〉〉) → 𝐶 Btwn 〈𝐴, 𝐵〉)) | 
| 21 | 17, 20 | sylan2d 605 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉) → 𝐶 Btwn 〈𝐴, 𝐵〉)) | 
| 22 |  | simpl 482 | . . . 4
⊢ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉) → 𝐵 Btwn 〈𝐴, 𝐶〉) | 
| 23 | 22 | a1i 11 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉) → 𝐵 Btwn 〈𝐴, 𝐶〉)) | 
| 24 | 21, 23 | jcad 512 | . 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉) → (𝐶 Btwn 〈𝐴, 𝐵〉 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉))) | 
| 25 |  | 3anrot 1100 | . . 3
⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ↔ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) | 
| 26 |  | btwnswapid2 36019 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ((𝐶 Btwn 〈𝐴, 𝐵〉 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉) → 𝐶 = 𝐵)) | 
| 27 | 25, 26 | sylan2br 595 | . 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐶 Btwn 〈𝐴, 𝐵〉 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉) → 𝐶 = 𝐵)) | 
| 28 | 24, 27 | syld 47 | 1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐴, 𝐵〉) → 𝐶 = 𝐵)) |