| Step | Hyp | Ref
| Expression |
| 1 | | simprrl 781 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) → 𝑦 Btwn 〈𝐶, 𝐷〉) |
| 2 | | simprlr 780 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) → 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) |
| 3 | | simpl11 1249 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
| 4 | | simpl21 1252 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁)) |
| 5 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑦 ∈ (𝔼‘𝑁)) |
| 6 | | simpl22 1253 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁)) |
| 7 | | simpl32 1256 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐺 ∈ (𝔼‘𝑁)) |
| 8 | | simpl33 1257 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐻 ∈ (𝔼‘𝑁)) |
| 9 | | cgrxfr 36056 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐺, 〈𝑧, 𝐻〉〉))) |
| 10 | 3, 4, 5, 6, 7, 8, 9 | syl132anc 1390 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐺, 〈𝑧, 𝐻〉〉))) |
| 11 | 10 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐺, 〈𝑧, 𝐻〉〉))) |
| 12 | 1, 2, 11 | mp2and 699 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐺, 〈𝑧, 𝐻〉〉)) |
| 13 | | anass 468 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
𝑧 ∈
(𝔼‘𝑁)) ↔
(((𝑁 ∈ ℕ ∧
𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁)))) |
| 14 | | simpl11 1249 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 15 | | simpl21 1252 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 16 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝑦 ∈ (𝔼‘𝑁)) |
| 17 | | simpl22 1253 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
| 18 | | simpl32 1256 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐺 ∈ (𝔼‘𝑁)) |
| 19 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝑧 ∈ (𝔼‘𝑁)) |
| 20 | | simpl33 1257 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐻 ∈ (𝔼‘𝑁)) |
| 21 | | brcgr3 36047 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐺, 〈𝑧, 𝐻〉〉 ↔ (〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑧, 𝐻〉))) |
| 22 | 14, 15, 16, 17, 18, 19, 20, 21 | syl133anc 1395 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐺, 〈𝑧, 𝐻〉〉 ↔ (〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑧, 𝐻〉))) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐺, 〈𝑧, 𝐻〉〉 ↔ (〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑧, 𝐻〉))) |
| 24 | | df-3an 1089 |
. . . . . . . . . . . . . . 15
⊢
(((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑧, 𝐻〉)) ↔ (((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) ∧ (〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑧, 𝐻〉))) |
| 25 | | simpl23 1254 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁)) |
| 26 | | simpl31 1255 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁)) |
| 27 | | simpl12 1250 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 28 | | simpl13 1251 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
| 29 | | simpr1l 1231 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑧, 𝐻〉))) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) |
| 30 | | simpr2r 1234 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑧, 𝐻〉))) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) |
| 31 | 14, 27, 28, 25, 26, 15, 16, 29, 30 | cgrtr4and 35987 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑧, 𝐻〉))) → 〈𝐸, 𝐹〉Cgr〈𝐶, 𝑦〉) |
| 32 | | simpr31 1264 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑧, 𝐻〉))) → 〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉) |
| 33 | 14, 25, 26, 15, 16, 18, 19, 31, 32 | cgrtrand 35994 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑧, 𝐻〉))) → 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉) |
| 34 | 24, 33 | sylan2br 595 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
(((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) ∧ (〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑧, 𝐻〉))) → 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉) |
| 35 | 34 | expr 456 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) → ((〈𝐶, 𝑦〉Cgr〈𝐺, 𝑧〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑧, 𝐻〉) → 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉)) |
| 36 | 23, 35 | sylbid 240 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐺, 〈𝑧, 𝐻〉〉 → 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉)) |
| 37 | 36 | anim2d 612 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) → ((𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐺, 〈𝑧, 𝐻〉〉) → (𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉))) |
| 38 | 13, 37 | sylanb 581 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
𝑧 ∈
(𝔼‘𝑁)) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) → ((𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐺, 〈𝑧, 𝐻〉〉) → (𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉))) |
| 39 | 38 | an32s 652 |
. . . . . . . . 9
⊢
((((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → ((𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐺, 〈𝑧, 𝐻〉〉) → (𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉))) |
| 40 | 39 | reximdva 3168 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) → (∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐺, 〈𝑧, 𝐻〉〉) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉))) |
| 41 | 12, 40 | mpd 15 |
. . . . . . 7
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉)) |
| 42 | 41 | expr 456 |
. . . . . 6
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉))) |
| 43 | 42 | an32s 652 |
. . . . 5
⊢
(((((𝑁 ∈
ℕ ∧ 𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁)) ∧
(𝐹 ∈
(𝔼‘𝑁) ∧
𝐺 ∈
(𝔼‘𝑁) ∧
𝐻 ∈
(𝔼‘𝑁))) ∧
(〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉))) |
| 44 | 43 | rexlimdva 3155 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉))) |
| 45 | | simp11 1204 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 46 | | simp12 1205 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 47 | | simp13 1206 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
| 48 | | simp21 1207 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 49 | | simp22 1208 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
| 50 | | brsegle 36109 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 51 | 45, 46, 47, 48, 49, 50 | syl122anc 1381 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 52 | 51 | adantr 480 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 53 | | simp23 1209 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁)) |
| 54 | | simp31 1210 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁)) |
| 55 | | simp32 1211 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐺 ∈ (𝔼‘𝑁)) |
| 56 | | simp33 1212 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → 𝐻 ∈ (𝔼‘𝑁)) |
| 57 | | brsegle 36109 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁)) ∧ (𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈𝐸, 𝐹〉 Seg≤ 〈𝐺, 𝐻〉 ↔ ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉))) |
| 58 | 45, 53, 54, 55, 56, 57 | syl122anc 1381 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈𝐸, 𝐹〉 Seg≤ 〈𝐺, 𝐻〉 ↔ ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉))) |
| 59 | 58 | adantr 480 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → (〈𝐸, 𝐹〉 Seg≤ 〈𝐺, 𝐻〉 ↔ ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐺, 𝐻〉 ∧ 〈𝐸, 𝐹〉Cgr〈𝐺, 𝑧〉))) |
| 60 | 44, 52, 59 | 3imtr4d 294 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 → 〈𝐸, 𝐹〉 Seg≤ 〈𝐺, 𝐻〉)) |
| 61 | 60 | exp32 420 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 → (〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 → 〈𝐸, 𝐹〉 Seg≤ 〈𝐺, 𝐻〉)))) |
| 62 | 61 | 3impd 1349 |
1
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉 ∧ 〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉) → 〈𝐸, 𝐹〉 Seg≤ 〈𝐺, 𝐻〉)) |