| Step | Hyp | Ref
| Expression |
| 1 | | simpl1 1192 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉)) → 𝑁 ∈ ℕ) |
| 2 | | simpl3r 1230 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉)) → 𝐹 ∈ (𝔼‘𝑁)) |
| 3 | | simpl3l 1229 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉)) → 𝐷 ∈ (𝔼‘𝑁)) |
| 4 | | btwndiff 36028 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐹 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → ∃𝑔 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) |
| 5 | 1, 2, 3, 4 | syl3anc 1373 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉)) → ∃𝑔 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) |
| 6 | | simpl1 1192 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
| 7 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) → 𝑔 ∈ (𝔼‘𝑁)) |
| 8 | | simpl3l 1229 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁)) |
| 9 | | simpl21 1252 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
| 10 | | simpl22 1253 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁)) |
| 11 | | axsegcon 28942 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) |
| 12 | 6, 7, 8, 9, 10, 11 | syl122anc 1381 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) |
| 13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔))) → ∃𝑒 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) |
| 14 | | anass 468 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) ∧ 𝑒 ∈ (𝔼‘𝑁)) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)))) |
| 15 | | simpl1 1192 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 16 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → 𝑔 ∈ (𝔼‘𝑁)) |
| 17 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → 𝑒 ∈ (𝔼‘𝑁)) |
| 18 | | simpl22 1253 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
| 19 | | simpl23 1254 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 20 | | axsegcon 28942 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ∃𝑓 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉)) |
| 21 | 15, 16, 17, 18, 19, 20 | syl122anc 1381 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) → ∃𝑓 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉)) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉))) → ∃𝑓 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉)) |
| 23 | | anass 468 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ 𝑓 ∈ (𝔼‘𝑁)) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ ((𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ 𝑓 ∈ (𝔼‘𝑁)))) |
| 24 | | df-3an 1089 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)) ↔ ((𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ 𝑓 ∈ (𝔼‘𝑁))) |
| 25 | 24 | anbi2i 623 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ ((𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁)) ∧ 𝑓 ∈ (𝔼‘𝑁)))) |
| 26 | 23, 25 | bitr4i 278 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ 𝑓 ∈ (𝔼‘𝑁)) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁)))) |
| 27 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) → 𝐷 ≠ 𝑔) |
| 28 | 27 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 𝐷 ≠ 𝑔) |
| 29 | 28 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 𝑔 ≠ 𝐷) |
| 30 | | simpl1 1192 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 31 | | simpr1 1195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑔 ∈ (𝔼‘𝑁)) |
| 32 | | simpl3l 1229 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
| 33 | | simpr2 1196 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑒 ∈ (𝔼‘𝑁)) |
| 34 | | simpr3 1197 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝑓 ∈ (𝔼‘𝑁)) |
| 35 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) → 𝐷 Btwn 〈𝑔, 𝑒〉) |
| 36 | 35 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 𝐷 Btwn 〈𝑔, 𝑒〉) |
| 37 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 𝑒 Btwn 〈𝑔, 𝑓〉) |
| 38 | 30, 31, 32, 33, 34, 36, 37 | btwnexchand 36027 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 𝐷 Btwn 〈𝑔, 𝑓〉) |
| 39 | | simpl21 1252 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 40 | | simpl22 1253 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
| 41 | | simpl23 1254 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 42 | 30, 31, 32, 33, 34, 36, 37 | btwnexch3and 36022 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 𝑒 Btwn 〈𝐷, 𝑓〉) |
| 43 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) → 𝐵 Btwn 〈𝐴, 𝐶〉) |
| 44 | 43 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 𝐵 Btwn 〈𝐴, 𝐶〉) |
| 45 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) → 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉) |
| 46 | 45 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉) |
| 47 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉) |
| 48 | 30, 32, 33, 34, 39, 40, 41, 42, 44, 46, 47 | cgrextendand 36010 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 〈𝐷, 𝑓〉Cgr〈𝐴, 𝐶〉) |
| 49 | 38, 48 | jca 511 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → (𝐷 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝐷, 𝑓〉Cgr〈𝐴, 𝐶〉)) |
| 50 | | simpl3r 1230 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁)) |
| 51 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) → 𝐷 Btwn 〈𝐹, 𝑔〉) |
| 52 | 51 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 𝐷 Btwn 〈𝐹, 𝑔〉) |
| 53 | 30, 32, 50, 31, 52 | btwncomand 36016 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 𝐷 Btwn 〈𝑔, 𝐹〉) |
| 54 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) → 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) |
| 55 | 54 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) |
| 56 | 30, 39, 41, 32, 50, 55 | cgrcomand 35992 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 〈𝐷, 𝐹〉Cgr〈𝐴, 𝐶〉) |
| 57 | 53, 56 | jca 511 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → (𝐷 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝐷, 𝐹〉Cgr〈𝐴, 𝐶〉)) |
| 58 | 29, 49, 57 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → (𝑔 ≠ 𝐷 ∧ (𝐷 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝐷, 𝑓〉Cgr〈𝐴, 𝐶〉) ∧ (𝐷 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝐷, 𝐹〉Cgr〈𝐴, 𝐶〉))) |
| 59 | 58 | ex 412 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉)) → (𝑔 ≠ 𝐷 ∧ (𝐷 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝐷, 𝑓〉Cgr〈𝐴, 𝐶〉) ∧ (𝐷 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝐷, 𝐹〉Cgr〈𝐴, 𝐶〉)))) |
| 60 | | segconeq 36011 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝑔 ≠ 𝐷 ∧ (𝐷 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝐷, 𝑓〉Cgr〈𝐴, 𝐶〉) ∧ (𝐷 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝐷, 𝐹〉Cgr〈𝐴, 𝐶〉)) → 𝑓 = 𝐹)) |
| 61 | 30, 32, 39, 41, 31, 34, 50, 60 | syl133anc 1395 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝑔 ≠ 𝐷 ∧ (𝐷 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝐷, 𝑓〉Cgr〈𝐴, 𝐶〉) ∧ (𝐷 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝐷, 𝐹〉Cgr〈𝐴, 𝐶〉)) → 𝑓 = 𝐹)) |
| 62 | 59, 61 | syld 47 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉)) → 𝑓 = 𝐹)) |
| 63 | 62 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → 𝑓 = 𝐹) |
| 64 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝐹 → 〈𝑔, 𝑓〉 = 〈𝑔, 𝐹〉) |
| 65 | 64 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝐹 → (𝑒 Btwn 〈𝑔, 𝑓〉 ↔ 𝑒 Btwn 〈𝑔, 𝐹〉)) |
| 66 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝐹 → 〈𝑒, 𝑓〉 = 〈𝑒, 𝐹〉) |
| 67 | 66 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝐹 → (〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉 ↔ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉)) |
| 68 | 65, 67 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝐹 → ((𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉) ↔ (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉))) |
| 69 | 68 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 = 𝐹 ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉)) → (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉)) |
| 70 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉) → 𝑒 Btwn 〈𝑔, 𝐹〉) |
| 71 | | btwnexch3 36021 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝑒 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 𝑒 Btwn 〈𝑔, 𝐹〉) → 𝑒 Btwn 〈𝐷, 𝐹〉)) |
| 72 | 30, 31, 32, 33, 50, 71 | syl122anc 1381 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 𝑒 Btwn 〈𝑔, 𝐹〉) → 𝑒 Btwn 〈𝐷, 𝐹〉)) |
| 73 | 35, 70, 72 | syl2ani 607 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉)) → 𝑒 Btwn 〈𝐷, 𝐹〉)) |
| 74 | 73 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉))) → 𝑒 Btwn 〈𝐷, 𝐹〉) |
| 75 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐵 Btwn
〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉)) → 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉) |
| 76 | 75 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉))) → 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉) |
| 77 | 30, 32, 33, 39, 40, 76 | cgrcomand 35992 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉))) → 〈𝐴, 𝐵〉Cgr〈𝐷, 𝑒〉) |
| 78 | 54 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉))) → 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) |
| 79 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉))) → 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉) |
| 80 | 30, 33, 50, 40, 41, 79 | cgrcomand 35992 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉))) → 〈𝐵, 𝐶〉Cgr〈𝑒, 𝐹〉) |
| 81 | | brcgr3 36047 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐷, 𝑒〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑒, 𝐹〉))) |
| 82 | 30, 39, 40, 41, 32, 33, 50, 81 | syl133anc 1395 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐷, 𝑒〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑒, 𝐹〉))) |
| 83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉))) → (〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐷, 𝑒〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑒, 𝐹〉))) |
| 84 | 77, 78, 80, 83 | mpbir3and 1343 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉))) → 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉) |
| 85 | 74, 84 | jca 511 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉))) → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉)) |
| 86 | 85 | expr 456 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉))) → ((𝑒 Btwn 〈𝑔, 𝐹〉 ∧ 〈𝑒, 𝐹〉Cgr〈𝐵, 𝐶〉) → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 87 | 69, 86 | syl5 34 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉))) → ((𝑓 = 𝐹 ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉)) → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 88 | 87 | expcomd 416 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉))) → ((𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉) → (𝑓 = 𝐹 → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉)))) |
| 89 | 88 | impr 454 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → (𝑓 = 𝐹 → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 90 | 63, 89 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ ((((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉)) ∧ (𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉))) → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉)) |
| 91 | 90 | expr 456 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁) ∧ 𝑓 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉))) → ((𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉) → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 92 | 26, 91 | sylanb 581 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐹 ∈
(𝔼‘𝑁))) ∧
(𝑔 ∈
(𝔼‘𝑁) ∧
𝑒 ∈
(𝔼‘𝑁))) ∧
𝑓 ∈
(𝔼‘𝑁)) ∧
(((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉))) → ((𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉) → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 93 | 92 | an32s 652 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐹 ∈
(𝔼‘𝑁))) ∧
(𝑔 ∈
(𝔼‘𝑁) ∧
𝑒 ∈
(𝔼‘𝑁))) ∧
(((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉))) ∧ 𝑓 ∈ (𝔼‘𝑁)) → ((𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉) → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 94 | 93 | rexlimdva 3155 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉))) → (∃𝑓 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝑔, 𝑓〉 ∧ 〈𝑒, 𝑓〉Cgr〈𝐵, 𝐶〉) → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 95 | 22, 94 | mpd 15 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔)) ∧ (𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉))) → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉)) |
| 96 | 95 | expr 456 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑔 ∈ (𝔼‘𝑁) ∧ 𝑒 ∈ (𝔼‘𝑁))) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔))) → ((𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉) → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 97 | 14, 96 | sylanb 581 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐹 ∈
(𝔼‘𝑁))) ∧
𝑔 ∈
(𝔼‘𝑁)) ∧
𝑒 ∈
(𝔼‘𝑁)) ∧
((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔))) → ((𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉) → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 98 | 97 | an32s 652 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐹 ∈
(𝔼‘𝑁))) ∧
𝑔 ∈
(𝔼‘𝑁)) ∧
((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔))) ∧ 𝑒 ∈ (𝔼‘𝑁)) → ((𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉) → (𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 99 | 98 | reximdva 3168 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔))) → (∃𝑒 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝑔, 𝑒〉 ∧ 〈𝐷, 𝑒〉Cgr〈𝐴, 𝐵〉) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 100 | 13, 99 | mpd 15 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) ∧ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) ∧ (𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔))) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉)) |
| 101 | 100 | expr 456 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ 𝑔 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉)) → ((𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 102 | 101 | an32s 652 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉)) ∧ 𝑔 ∈ (𝔼‘𝑁)) → ((𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 103 | 102 | rexlimdva 3155 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉)) → (∃𝑔 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝐹, 𝑔〉 ∧ 𝐷 ≠ 𝑔) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |
| 104 | 5, 103 | mpd 15 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉)) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉)) |
| 105 | 104 | ex 412 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) → ∃𝑒 ∈ (𝔼‘𝑁)(𝑒 Btwn 〈𝐷, 𝐹〉 ∧ 〈𝐴, 〈𝐵, 𝐶〉〉Cgr3〈𝐷, 〈𝑒, 𝐹〉〉))) |