| Step | Hyp | Ref
| Expression |
| 1 | | brifs 36044 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 InnerFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) |
| 2 | | simp1l 1198 |
. . . . . 6
⊢ (((𝐵 Btwn 〈𝐶, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → 𝐵 Btwn 〈𝐶, 𝐶〉) |
| 3 | | simp11 1204 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 4 | | simp13 1206 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
| 5 | | simp21 1207 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 6 | | axbtwnid 28954 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐵 Btwn 〈𝐶, 𝐶〉 → 𝐵 = 𝐶)) |
| 7 | 3, 4, 5, 6 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐶, 𝐶〉 → 𝐵 = 𝐶)) |
| 8 | 2, 7 | syl5 34 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn 〈𝐶, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → 𝐵 = 𝐶)) |
| 9 | | simp2r 1201 |
. . . . . . . . 9
⊢ (((𝐵 Btwn 〈𝐶, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) |
| 10 | | simp3r 1203 |
. . . . . . . . 9
⊢ (((𝐵 Btwn 〈𝐶, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) |
| 11 | 9, 10 | jca 511 |
. . . . . . . 8
⊢ (((𝐵 Btwn 〈𝐶, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → (〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) |
| 12 | | opeq2 4874 |
. . . . . . . . . . 11
⊢ (𝐵 = 𝐶 → 〈𝐵, 𝐵〉 = 〈𝐵, 𝐶〉) |
| 13 | 12 | breq1d 5153 |
. . . . . . . . . 10
⊢ (𝐵 = 𝐶 → (〈𝐵, 𝐵〉Cgr〈𝐹, 𝐺〉 ↔ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉)) |
| 14 | | opeq1 4873 |
. . . . . . . . . . 11
⊢ (𝐵 = 𝐶 → 〈𝐵, 𝐷〉 = 〈𝐶, 𝐷〉) |
| 15 | 14 | breq1d 5153 |
. . . . . . . . . 10
⊢ (𝐵 = 𝐶 → (〈𝐵, 𝐷〉Cgr〈𝐺, 𝐻〉 ↔ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) |
| 16 | 13, 15 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝐵 = 𝐶 → ((〈𝐵, 𝐵〉Cgr〈𝐹, 𝐺〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐺, 𝐻〉) ↔ (〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) |
| 17 | 16 | biimprd 248 |
. . . . . . . 8
⊢ (𝐵 = 𝐶 → ((〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) → (〈𝐵, 𝐵〉Cgr〈𝐹, 𝐺〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐺, 𝐻〉))) |
| 18 | 11, 17 | mpan9 506 |
. . . . . . 7
⊢ ((((𝐵 Btwn 〈𝐶, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐵 = 𝐶) → (〈𝐵, 𝐵〉Cgr〈𝐹, 𝐺〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐺, 𝐻〉)) |
| 19 | | simp31 1210 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁)) |
| 20 | | simp32 1211 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐺 ∈ (𝔼‘𝑁)) |
| 21 | | cgrid2 36004 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁))) → (〈𝐵, 𝐵〉Cgr〈𝐹, 𝐺〉 → 𝐹 = 𝐺)) |
| 22 | 3, 4, 19, 20, 21 | syl13anc 1374 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈𝐵, 𝐵〉Cgr〈𝐹, 𝐺〉 → 𝐹 = 𝐺)) |
| 23 | | opeq1 4873 |
. . . . . . . . . . 11
⊢ (𝐹 = 𝐺 → 〈𝐹, 𝐻〉 = 〈𝐺, 𝐻〉) |
| 24 | 23 | breq2d 5155 |
. . . . . . . . . 10
⊢ (𝐹 = 𝐺 → (〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉 ↔ 〈𝐵, 𝐷〉Cgr〈𝐺, 𝐻〉)) |
| 25 | 24 | biimprd 248 |
. . . . . . . . 9
⊢ (𝐹 = 𝐺 → (〈𝐵, 𝐷〉Cgr〈𝐺, 𝐻〉 → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 26 | 22, 25 | syl6 35 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈𝐵, 𝐵〉Cgr〈𝐹, 𝐺〉 → (〈𝐵, 𝐷〉Cgr〈𝐺, 𝐻〉 → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 27 | 26 | impd 410 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((〈𝐵, 𝐵〉Cgr〈𝐹, 𝐺〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐺, 𝐻〉) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 28 | 18, 27 | syl5 34 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((((𝐵 Btwn 〈𝐶, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐵 = 𝐶) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 29 | 28 | expd 415 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn 〈𝐶, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → (𝐵 = 𝐶 → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 30 | 8, 29 | mpdd 43 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn 〈𝐶, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 31 | | opeq1 4873 |
. . . . . . . 8
⊢ (𝐴 = 𝐶 → 〈𝐴, 𝐶〉 = 〈𝐶, 𝐶〉) |
| 32 | 31 | breq2d 5155 |
. . . . . . 7
⊢ (𝐴 = 𝐶 → (𝐵 Btwn 〈𝐴, 𝐶〉 ↔ 𝐵 Btwn 〈𝐶, 𝐶〉)) |
| 33 | 32 | anbi1d 631 |
. . . . . 6
⊢ (𝐴 = 𝐶 → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ↔ (𝐵 Btwn 〈𝐶, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉))) |
| 34 | 31 | breq1d 5153 |
. . . . . . 7
⊢ (𝐴 = 𝐶 → (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ↔ 〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉)) |
| 35 | 34 | anbi1d 631 |
. . . . . 6
⊢ (𝐴 = 𝐶 → ((〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ↔ (〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉))) |
| 36 | 33, 35 | 3anbi12d 1439 |
. . . . 5
⊢ (𝐴 = 𝐶 → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ↔ ((𝐵 Btwn 〈𝐶, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) |
| 37 | 36 | imbi1d 341 |
. . . 4
⊢ (𝐴 = 𝐶 → ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉) ↔ (((𝐵 Btwn 〈𝐶, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐶, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 38 | 30, 37 | imbitrrid 246 |
. . 3
⊢ (𝐴 = 𝐶 → (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 39 | | simp12 1205 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 40 | | btwndiff 36028 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) |
| 41 | 3, 39, 5, 40 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) |
| 42 | | simpl11 1249 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
| 43 | | simpl23 1254 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐸 ∈ (𝔼‘𝑁)) |
| 44 | | simpl32 1256 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐺 ∈ (𝔼‘𝑁)) |
| 45 | | simpl21 1252 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁)) |
| 46 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → 𝑒 ∈ (𝔼‘𝑁)) |
| 47 | | axsegcon 28942 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → ∃𝑓 ∈ (𝔼‘𝑁)(𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉)) |
| 48 | 42, 43, 44, 45, 46, 47 | syl122anc 1381 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ∃𝑓 ∈ (𝔼‘𝑁)(𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉)) |
| 49 | | anass 468 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐴 ≠ 𝐶)) ↔ ((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ ((𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐴 ≠ 𝐶)))) |
| 50 | | anass 468 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 Btwn
〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 𝐴 ≠ 𝐶) ↔ (((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐴 ≠ 𝐶))) |
| 51 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) → 𝐶 Btwn 〈𝐴, 𝑒〉) |
| 52 | 51 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → 𝐶 Btwn 〈𝐴, 𝑒〉) |
| 53 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) → 𝐺 Btwn 〈𝐸, 𝑓〉) |
| 54 | 53 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → 𝐺 Btwn 〈𝐸, 𝑓〉) |
| 55 | 52, 54 | jca 511 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐺 Btwn 〈𝐸, 𝑓〉)) |
| 56 | | simpr2l 1233 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) → 〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉) |
| 57 | 56 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → 〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉) |
| 58 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) → 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) |
| 59 | 58 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) |
| 60 | 3 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → 𝑁 ∈ ℕ) |
| 61 | 20 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → 𝐺 ∈ (𝔼‘𝑁)) |
| 62 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → 𝑓 ∈ (𝔼‘𝑁)) |
| 63 | 5 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 64 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → 𝑒 ∈ (𝔼‘𝑁)) |
| 65 | | cgrcom 35991 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → (〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉 ↔ 〈𝐶, 𝑒〉Cgr〈𝐺, 𝑓〉)) |
| 66 | 60, 61, 62, 63, 64, 65 | syl122anc 1381 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → (〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉 ↔ 〈𝐶, 𝑒〉Cgr〈𝐺, 𝑓〉)) |
| 67 | 59, 66 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → 〈𝐶, 𝑒〉Cgr〈𝐺, 𝑓〉) |
| 68 | 57, 67 | jca 511 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐶, 𝑒〉Cgr〈𝐺, 𝑓〉)) |
| 69 | | simprr3 1224 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) |
| 70 | 55, 68, 69 | 3jca 1129 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
(((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) → ((𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐺 Btwn 〈𝐸, 𝑓〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐶, 𝑒〉Cgr〈𝐺, 𝑓〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) |
| 71 | 70 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) → ((𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐺 Btwn 〈𝐸, 𝑓〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐶, 𝑒〉Cgr〈𝐺, 𝑓〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) |
| 72 | | simpl11 1249 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 73 | | simpl12 1250 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 74 | | simpl21 1252 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 75 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑒 ∈ (𝔼‘𝑁)) |
| 76 | | simpl22 1253 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
| 77 | | simpl23 1254 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁)) |
| 78 | | simpl32 1256 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐺 ∈ (𝔼‘𝑁)) |
| 79 | | simprr 773 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑓 ∈ (𝔼‘𝑁)) |
| 80 | | simpl33 1257 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐻 ∈ (𝔼‘𝑁)) |
| 81 | | brofs 36006 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐶〉, 〈𝑒, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐺〉, 〈𝑓, 𝐻〉〉 ↔ ((𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐺 Btwn 〈𝐸, 𝑓〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐶, 𝑒〉Cgr〈𝐺, 𝑓〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) |
| 82 | 72, 73, 74, 75, 76, 77, 78, 79, 80, 81 | syl333anc 1404 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐶〉, 〈𝑒, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐺〉, 〈𝑓, 𝐻〉〉 ↔ ((𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐺 Btwn 〈𝐸, 𝑓〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐶, 𝑒〉Cgr〈𝐺, 𝑓〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) |
| 83 | 71, 82 | sylibrd 259 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) → 〈〈𝐴, 𝐶〉, 〈𝑒, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐺〉, 〈𝑓, 𝐻〉〉)) |
| 84 | | 5segofs 36007 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((〈〈𝐴, 𝐶〉, 〈𝑒, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐺〉, 〈𝑓, 𝐻〉〉 ∧ 𝐴 ≠ 𝐶) → 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) |
| 85 | 72, 73, 74, 75, 76, 77, 78, 79, 80, 84 | syl333anc 1404 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((〈〈𝐴, 𝐶〉, 〈𝑒, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐺〉, 〈𝑓, 𝐻〉〉 ∧ 𝐴 ≠ 𝐶) → 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) |
| 86 | 83, 85 | syland 603 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 𝐴 ≠ 𝐶) → 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) |
| 87 | | simpr1l 1231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) → 𝐵 Btwn 〈𝐴, 𝐶〉) |
| 88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐺 Btwn
〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → 𝐵 Btwn 〈𝐴, 𝐶〉) |
| 89 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐺 Btwn
〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → 𝐶 Btwn 〈𝐴, 𝑒〉) |
| 90 | 88, 89 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐺 Btwn
〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐴, 𝑒〉)) |
| 91 | | simpr1r 1232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) → 𝐹 Btwn 〈𝐸, 𝐺〉) |
| 92 | 91 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐺 Btwn
〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → 𝐹 Btwn 〈𝐸, 𝐺〉) |
| 93 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐺 Btwn
〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → 𝐺 Btwn 〈𝐸, 𝑓〉) |
| 94 | 90, 92, 93 | jca32 515 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐺 Btwn
〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐴, 𝑒〉) ∧ (𝐹 Btwn 〈𝐸, 𝐺〉 ∧ 𝐺 Btwn 〈𝐸, 𝑓〉))) |
| 95 | | simpl13 1251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
| 96 | | btwnexch3 36021 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐴, 𝑒〉) → 𝐶 Btwn 〈𝐵, 𝑒〉)) |
| 97 | 72, 73, 95, 74, 75, 96 | syl122anc 1381 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐴, 𝑒〉) → 𝐶 Btwn 〈𝐵, 𝑒〉)) |
| 98 | | simpl31 1255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁)) |
| 99 | | btwnexch3 36021 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℕ ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐹 Btwn 〈𝐸, 𝐺〉 ∧ 𝐺 Btwn 〈𝐸, 𝑓〉) → 𝐺 Btwn 〈𝐹, 𝑓〉)) |
| 100 | 72, 77, 98, 78, 79, 99 | syl122anc 1381 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐹 Btwn 〈𝐸, 𝐺〉 ∧ 𝐺 Btwn 〈𝐸, 𝑓〉) → 𝐺 Btwn 〈𝐹, 𝑓〉)) |
| 101 | 97, 100 | anim12d 609 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐴, 𝑒〉) ∧ (𝐹 Btwn 〈𝐸, 𝐺〉 ∧ 𝐺 Btwn 〈𝐸, 𝑓〉)) → (𝐶 Btwn 〈𝐵, 𝑒〉 ∧ 𝐺 Btwn 〈𝐹, 𝑓〉))) |
| 102 | 94, 101 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → (𝐶 Btwn 〈𝐵, 𝑒〉 ∧ 𝐺 Btwn 〈𝐹, 𝑓〉))) |
| 103 | 102 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → (𝐶 Btwn 〈𝐵, 𝑒〉 ∧ 𝐺 Btwn 〈𝐹, 𝑓〉)) |
| 104 | | btwncom 36015 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐵, 𝑒〉 ↔ 𝐶 Btwn 〈𝑒, 𝐵〉)) |
| 105 | 72, 74, 95, 75, 104 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (𝐶 Btwn 〈𝐵, 𝑒〉 ↔ 𝐶 Btwn 〈𝑒, 𝐵〉)) |
| 106 | | btwncom 36015 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℕ ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (𝐺 Btwn 〈𝐹, 𝑓〉 ↔ 𝐺 Btwn 〈𝑓, 𝐹〉)) |
| 107 | 72, 78, 98, 79, 106 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (𝐺 Btwn 〈𝐹, 𝑓〉 ↔ 𝐺 Btwn 〈𝑓, 𝐹〉)) |
| 108 | 105, 107 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐶 Btwn 〈𝐵, 𝑒〉 ∧ 𝐺 Btwn 〈𝐹, 𝑓〉) ↔ (𝐶 Btwn 〈𝑒, 𝐵〉 ∧ 𝐺 Btwn 〈𝑓, 𝐹〉))) |
| 109 | 108 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → ((𝐶 Btwn 〈𝐵, 𝑒〉 ∧ 𝐺 Btwn 〈𝐹, 𝑓〉) ↔ (𝐶 Btwn 〈𝑒, 𝐵〉 ∧ 𝐺 Btwn 〈𝑓, 𝐹〉))) |
| 110 | 103, 109 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → (𝐶 Btwn 〈𝑒, 𝐵〉 ∧ 𝐺 Btwn 〈𝑓, 𝐹〉)) |
| 111 | 58 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) |
| 112 | 72, 78, 79, 74, 75, 65 | syl122anc 1381 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉 ↔ 〈𝐶, 𝑒〉Cgr〈𝐺, 𝑓〉)) |
| 113 | | cgrcomlr 35999 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝑒〉Cgr〈𝐺, 𝑓〉 ↔ 〈𝑒, 𝐶〉Cgr〈𝑓, 𝐺〉)) |
| 114 | 72, 74, 75, 78, 79, 113 | syl122anc 1381 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝑒〉Cgr〈𝐺, 𝑓〉 ↔ 〈𝑒, 𝐶〉Cgr〈𝑓, 𝐺〉)) |
| 115 | 112, 114 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉 ↔ 〈𝑒, 𝐶〉Cgr〈𝑓, 𝐺〉)) |
| 116 | 115 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → (〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉 ↔ 〈𝑒, 𝐶〉Cgr〈𝑓, 𝐺〉)) |
| 117 | 111, 116 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → 〈𝑒, 𝐶〉Cgr〈𝑓, 𝐺〉) |
| 118 | | simpr2r 1234 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) → 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) |
| 119 | 118 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) |
| 120 | 72, 95, 74, 98, 78, 119 | cgrcomlrand 36002 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → 〈𝐶, 𝐵〉Cgr〈𝐺, 𝐹〉) |
| 121 | 117, 120 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → (〈𝑒, 𝐶〉Cgr〈𝑓, 𝐺〉 ∧ 〈𝐶, 𝐵〉Cgr〈𝐺, 𝐹〉)) |
| 122 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) |
| 123 | | simpr3r 1236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) → 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) |
| 124 | 123 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) |
| 125 | 122, 124 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → (〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) |
| 126 | 110, 121,
125 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑒 ∈
(𝔼‘𝑁) ∧
𝑓 ∈
(𝔼‘𝑁))) ∧
((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉)) → ((𝐶 Btwn 〈𝑒, 𝐵〉 ∧ 𝐺 Btwn 〈𝑓, 𝐹〉) ∧ (〈𝑒, 𝐶〉Cgr〈𝑓, 𝐺〉 ∧ 〈𝐶, 𝐵〉Cgr〈𝐺, 𝐹〉) ∧ (〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) |
| 127 | 126 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → ((𝐶 Btwn 〈𝑒, 𝐵〉 ∧ 𝐺 Btwn 〈𝑓, 𝐹〉) ∧ (〈𝑒, 𝐶〉Cgr〈𝑓, 𝐺〉 ∧ 〈𝐶, 𝐵〉Cgr〈𝐺, 𝐹〉) ∧ (〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) |
| 128 | | brofs 36006 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝑒, 𝐶〉, 〈𝐵, 𝐷〉〉 OuterFiveSeg 〈〈𝑓, 𝐺〉, 〈𝐹, 𝐻〉〉 ↔ ((𝐶 Btwn 〈𝑒, 𝐵〉 ∧ 𝐺 Btwn 〈𝑓, 𝐹〉) ∧ (〈𝑒, 𝐶〉Cgr〈𝑓, 𝐺〉 ∧ 〈𝐶, 𝐵〉Cgr〈𝐺, 𝐹〉) ∧ (〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) |
| 129 | 72, 75, 74, 95, 76, 79, 78, 98, 80, 128 | syl333anc 1404 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (〈〈𝑒, 𝐶〉, 〈𝐵, 𝐷〉〉 OuterFiveSeg 〈〈𝑓, 𝐺〉, 〈𝐹, 𝐻〉〉 ↔ ((𝐶 Btwn 〈𝑒, 𝐵〉 ∧ 𝐺 Btwn 〈𝑓, 𝐹〉) ∧ (〈𝑒, 𝐶〉Cgr〈𝑓, 𝐺〉 ∧ 〈𝐶, 𝐵〉Cgr〈𝐺, 𝐹〉) ∧ (〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)))) |
| 130 | 127, 129 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → 〈〈𝑒, 𝐶〉, 〈𝐵, 𝐷〉〉 OuterFiveSeg 〈〈𝑓, 𝐺〉, 〈𝐹, 𝐻〉〉)) |
| 131 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) → 𝐶 ≠ 𝑒) |
| 132 | 131 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 Btwn
〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → 𝐶 ≠ 𝑒) |
| 133 | 132 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 Btwn
〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → 𝑒 ≠ 𝐶) |
| 134 | 133 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → 𝑒 ≠ 𝐶)) |
| 135 | 130, 134 | jcad 512 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → (〈〈𝑒, 𝐶〉, 〈𝐵, 𝐷〉〉 OuterFiveSeg 〈〈𝑓, 𝐺〉, 〈𝐹, 𝐻〉〉 ∧ 𝑒 ≠ 𝐶))) |
| 136 | | 5segofs 36007 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((〈〈𝑒, 𝐶〉, 〈𝐵, 𝐷〉〉 OuterFiveSeg 〈〈𝑓, 𝐺〉, 〈𝐹, 𝐻〉〉 ∧ 𝑒 ≠ 𝐶) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 137 | 72, 75, 74, 95, 76, 79, 78, 98, 80, 136 | syl333anc 1404 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((〈〈𝑒, 𝐶〉, 〈𝐵, 𝐷〉〉 OuterFiveSeg 〈〈𝑓, 𝐺〉, 〈𝐹, 𝐻〉〉 ∧ 𝑒 ≠ 𝐶) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 138 | 135, 137 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 139 | 138 | expd 415 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) → (〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉 → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 140 | 139 | adantrd 491 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 𝐴 ≠ 𝐶) → (〈𝑒, 𝐷〉Cgr〈𝑓, 𝐻〉 → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 141 | 86, 140 | mpdd 43 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉))) ∧ 𝐴 ≠ 𝐶) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 142 | 50, 141 | biimtrrid 243 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ (𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒)) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐴 ≠ 𝐶)) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 143 | 49, 142 | biimtrrid 243 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) ∧ ((𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐴 ≠ 𝐶))) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 144 | 143 | expd 415 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) → (((𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐴 ≠ 𝐶)) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 145 | 144 | anassrs 467 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
𝑓 ∈
(𝔼‘𝑁)) →
((𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) → (((𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐴 ≠ 𝐶)) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 146 | 145 | rexlimdva 3155 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → (∃𝑓 ∈ (𝔼‘𝑁)(𝐺 Btwn 〈𝐸, 𝑓〉 ∧ 〈𝐺, 𝑓〉Cgr〈𝐶, 𝑒〉) → (((𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐴 ≠ 𝐶)) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 147 | 48, 146 | mpd 15 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → (((𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐴 ≠ 𝐶)) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 148 | 147 | expd 415 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ((𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒) → ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐴 ≠ 𝐶) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 149 | 148 | rexlimdva 3155 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (∃𝑒 ∈ (𝔼‘𝑁)(𝐶 Btwn 〈𝐴, 𝑒〉 ∧ 𝐶 ≠ 𝑒) → ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐴 ≠ 𝐶) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 150 | 41, 149 | mpd 15 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝐴 ≠ 𝐶) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 151 | 150 | expd 415 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → (𝐴 ≠ 𝐶 → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 152 | 151 | com3r 87 |
. . 3
⊢ (𝐴 ≠ 𝐶 → (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 153 | 38, 152 | pm2.61ine 3025 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐶〉Cgr〈𝐸, 𝐺〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 154 | 1, 153 | sylbid 240 |
1
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 InnerFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 → 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |