Step | Hyp | Ref
| Expression |
1 | | brsegle 34040 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
2 | | brsegle2 34041 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉 ↔ ∃𝑡 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) |
3 | 2 | 3com23 1127 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉 ↔ ∃𝑡 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) |
4 | 1, 3 | anbi12d 634 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉) ↔ (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ ∃𝑡 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉)))) |
5 | | reeanv 3269 |
. . 3
⊢
(∃𝑦 ∈
(𝔼‘𝑁)∃𝑡 ∈ (𝔼‘𝑁)((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉)) ↔ (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ ∃𝑡 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) |
6 | 4, 5 | bitr4di 292 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑡 ∈ (𝔼‘𝑁)((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉)))) |
7 | | simpl1 1192 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
8 | | simpl3l 1229 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
9 | | simprr 773 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) → 𝑡 ∈ (𝔼‘𝑁)) |
10 | | simprl 771 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) → 𝑦 ∈ (𝔼‘𝑁)) |
11 | | simpl3r 1230 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
12 | | simprll 779 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) → 𝑦 Btwn 〈𝐶, 𝐷〉) |
13 | | simprrl 781 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) → 𝐷 Btwn 〈𝐶, 𝑡〉) |
14 | 7, 8, 10, 11, 9, 12, 13 | btwnexchand 33958 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) → 𝑦 Btwn 〈𝐶, 𝑡〉) |
15 | | simpl2l 1227 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
16 | | simpl2r 1228 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
17 | | simprrr 782 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) → 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉) |
18 | | simprlr 780 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) |
19 | 7, 8, 9, 15, 16, 8, 10, 17, 18 | cgrtrand 33925 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) → 〈𝐶, 𝑡〉Cgr〈𝐶, 𝑦〉) |
20 | 7, 8, 9, 10, 14, 19 | endofsegidand 34018 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) → 𝑡 = 𝑦) |
21 | | opeq2 4758 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑦 → 〈𝐶, 𝑡〉 = 〈𝐶, 𝑦〉) |
22 | 21 | breq2d 5039 |
. . . . . . . . 9
⊢ (𝑡 = 𝑦 → (𝐷 Btwn 〈𝐶, 𝑡〉 ↔ 𝐷 Btwn 〈𝐶, 𝑦〉)) |
23 | 21 | breq1d 5037 |
. . . . . . . . 9
⊢ (𝑡 = 𝑦 → (〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉 ↔ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉)) |
24 | 22, 23 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑡 = 𝑦 → ((𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉) ↔ (𝐷 Btwn 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉))) |
25 | 24 | anbi2d 632 |
. . . . . . 7
⊢ (𝑡 = 𝑦 → (((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉)) ↔ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉)))) |
26 | 25 | anbi2d 632 |
. . . . . 6
⊢ (𝑡 = 𝑦 → ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) ↔ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉))))) |
27 | | simprrl 781 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉))) → 𝐷 Btwn 〈𝐶, 𝑦〉) |
28 | 7, 11, 8, 10, 27 | btwncomand 33947 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉))) → 𝐷 Btwn 〈𝑦, 𝐶〉) |
29 | | simprll 779 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉))) → 𝑦 Btwn 〈𝐶, 𝐷〉) |
30 | 7, 10, 8, 11, 29 | btwncomand 33947 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉))) → 𝑦 Btwn 〈𝐷, 𝐶〉) |
31 | | btwnswapid 33949 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn 〈𝑦, 𝐶〉 ∧ 𝑦 Btwn 〈𝐷, 𝐶〉) → 𝐷 = 𝑦)) |
32 | 7, 11, 10, 8, 31 | syl13anc 1373 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn 〈𝑦, 𝐶〉 ∧ 𝑦 Btwn 〈𝐷, 𝐶〉) → 𝐷 = 𝑦)) |
33 | 32 | adantr 484 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉))) → ((𝐷 Btwn 〈𝑦, 𝐶〉 ∧ 𝑦 Btwn 〈𝐷, 𝐶〉) → 𝐷 = 𝑦)) |
34 | 28, 30, 33 | mp2and 699 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉))) → 𝐷 = 𝑦) |
35 | | simprlr 780 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉))) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) |
36 | | opeq2 4758 |
. . . . . . . . 9
⊢ (𝐷 = 𝑦 → 〈𝐶, 𝐷〉 = 〈𝐶, 𝑦〉) |
37 | 36 | breq2d 5039 |
. . . . . . . 8
⊢ (𝐷 = 𝑦 → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) |
38 | 35, 37 | syl5ibrcom 250 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉))) → (𝐷 = 𝑦 → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉)) |
39 | 34, 38 | mpd 15 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉))) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) |
40 | 26, 39 | syl6bi 256 |
. . . . 5
⊢ (𝑡 = 𝑦 → ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉)) |
41 | 20, 40 | mpcom 38 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉))) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) |
42 | 41 | exp31 423 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝑦 ∈ (𝔼‘𝑁) ∧ 𝑡 ∈ (𝔼‘𝑁)) → (((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉)) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉))) |
43 | 42 | rexlimdvv 3202 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑦 ∈ (𝔼‘𝑁)∃𝑡 ∈ (𝔼‘𝑁)((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝐷 Btwn 〈𝐶, 𝑡〉 ∧ 〈𝐶, 𝑡〉Cgr〈𝐴, 𝐵〉)) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉)) |
44 | 6, 43 | sylbid 243 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉)) |