Step | Hyp | Ref
| Expression |
1 | | brsegle 31385 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
2 | | simprl 790 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → 𝑦 Btwn 〈𝐶, 𝐷〉) |
3 | | simpl1 1057 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
4 | | simpl3l 1109 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁)) |
5 | | simpl3r 1110 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁)) |
6 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑦 ∈ (𝔼‘𝑁)) |
7 | | btwncolinear2 31347 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑦 Btwn 〈𝐶, 𝐷〉 → 𝐶 Colinear 〈𝑦, 𝐷〉)) |
8 | 3, 4, 5, 6, 7 | syl13anc 1320 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑦 Btwn 〈𝐶, 𝐷〉 → 𝐶 Colinear 〈𝑦, 𝐷〉)) |
9 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → (𝑦 Btwn 〈𝐶, 𝐷〉 → 𝐶 Colinear 〈𝑦, 𝐷〉)) |
10 | 2, 9 | mpd 15 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → 𝐶 Colinear 〈𝑦, 𝐷〉) |
11 | | simpl2l 1107 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
12 | | simpl2r 1108 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁)) |
13 | | simprr 792 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) |
14 | 3, 11, 12, 4, 6, 13 | cgrcomand 31268 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉) |
15 | | simpl2 1058 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) |
16 | | lineext 31353 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ((𝐶 Colinear 〈𝑦, 𝐷〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉) → ∃𝑥 ∈ (𝔼‘𝑁)〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉)) |
17 | 3, 4, 6, 5, 15, 16 | syl131anc 1331 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → ((𝐶 Colinear 〈𝑦, 𝐷〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉) → ∃𝑥 ∈ (𝔼‘𝑁)〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉)) |
18 | 17 | adantr 480 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → ((𝐶 Colinear 〈𝑦, 𝐷〉 ∧ 〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉) → ∃𝑥 ∈ (𝔼‘𝑁)〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉)) |
19 | 10, 14, 18 | mp2and 711 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → ∃𝑥 ∈ (𝔼‘𝑁)〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉) |
20 | | an32 835 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ↔ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁))) |
21 | | simpll1 1093 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
22 | | simpl3l 1109 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁)) |
23 | 22 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁)) |
24 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑦 ∈ (𝔼‘𝑁)) |
25 | | simpl3r 1110 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁)) |
26 | 25 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁)) |
27 | | simpl2l 1107 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
28 | 27 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
29 | | simpl2r 1108 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁)) |
30 | 29 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁)) |
31 | | simplr 788 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁)) |
32 | | brcgr3 31323 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉 ↔ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉))) |
33 | 21, 23, 24, 26, 28, 30, 31, 32 | syl133anc 1341 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉 ↔ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉))) |
34 | 33 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉 ↔ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉))) |
35 | | simp2l 1080 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉)) → 𝑦 Btwn 〈𝐶, 𝐷〉) |
36 | | simp3 1056 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉)) → (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉)) |
37 | 33 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉)) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉 ↔ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉))) |
38 | 36, 37 | mpbird 246 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉)) → 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉) |
39 | | btwnxfr 31333 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉) → 𝐵 Btwn 〈𝐴, 𝑥〉)) |
40 | 21, 23, 24, 26, 28, 30, 31, 39 | syl133anc 1341 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉) → 𝐵 Btwn 〈𝐴, 𝑥〉)) |
41 | 40 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉)) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉) → 𝐵 Btwn 〈𝐴, 𝑥〉)) |
42 | 35, 38, 41 | mp2and 711 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉)) → 𝐵 Btwn 〈𝐴, 𝑥〉) |
43 | | simp32 1091 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉)) → 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉) |
44 | | cgrcom 31267 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ↔ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) |
45 | 21, 23, 26, 28, 31, 44 | syl122anc 1327 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ↔ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) |
46 | 45 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉)) → (〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ↔ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) |
47 | 43, 46 | mpbid 221 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉)) → 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) |
48 | 42, 47 | jca 553 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉)) → (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) |
49 | 48 | 3expia 1259 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → ((〈𝐶, 𝑦〉Cgr〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝐵, 𝑥〉) → (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉))) |
50 | 34, 49 | sylbid 229 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉 → (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉))) |
51 | 20, 50 | sylanb 488 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉 → (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉))) |
52 | 51 | an32s 842 |
. . . . . . 7
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉 → (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉))) |
53 | 52 | reximdva 3000 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → (∃𝑥 ∈ (𝔼‘𝑁)〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐴, 〈𝐵, 𝑥〉〉 → ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉))) |
54 | 19, 53 | mpd 15 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) |
55 | 54 | ex 449 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) → ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉))) |
56 | 55 | rexlimdva 3013 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) → ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉))) |
57 | | simprl 790 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → 𝐵 Btwn 〈𝐴, 𝑥〉) |
58 | | simpll1 1093 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → 𝑁 ∈ ℕ) |
59 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → 𝐴 ∈ (𝔼‘𝑁)) |
60 | | simplr 788 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → 𝑥 ∈ (𝔼‘𝑁)) |
61 | 29 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → 𝐵 ∈ (𝔼‘𝑁)) |
62 | | btwncolinear1 31346 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝐵 Btwn 〈𝐴, 𝑥〉 → 𝐴 Colinear 〈𝑥, 𝐵〉)) |
63 | 58, 59, 60, 61, 62 | syl13anc 1320 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → (𝐵 Btwn 〈𝐴, 𝑥〉 → 𝐴 Colinear 〈𝑥, 𝐵〉)) |
64 | 57, 63 | mpd 15 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → 𝐴 Colinear 〈𝑥, 𝐵〉) |
65 | | simprr 792 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) |
66 | | simpl1 1057 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
67 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁)) |
68 | | simpl3 1059 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) |
69 | | lineext 31353 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐴 Colinear 〈𝑥, 𝐵〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) → ∃𝑦 ∈ (𝔼‘𝑁)〈𝐴, 〈𝑥, 𝐵〉〉Cgr3〈𝐶, 〈𝐷, 𝑦〉〉)) |
70 | 66, 27, 67, 29, 68, 69 | syl131anc 1331 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝐴 Colinear 〈𝑥, 𝐵〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) → ∃𝑦 ∈ (𝔼‘𝑁)〈𝐴, 〈𝑥, 𝐵〉〉Cgr3〈𝐶, 〈𝐷, 𝑦〉〉)) |
71 | 70 | adantr 480 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → ((𝐴 Colinear 〈𝑥, 𝐵〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) → ∃𝑦 ∈ (𝔼‘𝑁)〈𝐴, 〈𝑥, 𝐵〉〉Cgr3〈𝐶, 〈𝐷, 𝑦〉〉)) |
72 | 64, 65, 71 | mp2and 711 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → ∃𝑦 ∈ (𝔼‘𝑁)〈𝐴, 〈𝑥, 𝐵〉〉Cgr3〈𝐶, 〈𝐷, 𝑦〉〉) |
73 | 27, 67, 29 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) |
74 | 73 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) |
75 | | brcgr3 31323 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝑥, 𝐵〉〉Cgr3〈𝐶, 〈𝐷, 𝑦〉〉 ↔ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉))) |
76 | 21, 74, 23, 26, 24, 75 | syl113anc 1330 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (〈𝐴, 〈𝑥, 𝐵〉〉Cgr3〈𝐶, 〈𝐷, 𝑦〉〉 ↔ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉))) |
77 | 76 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → (〈𝐴, 〈𝑥, 𝐵〉〉Cgr3〈𝐶, 〈𝐷, 𝑦〉〉 ↔ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉))) |
78 | | simp2l 1080 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∧ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉)) → 𝐵 Btwn 〈𝐴, 𝑥〉) |
79 | | simp32 1091 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∧ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉)) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) |
80 | | simp2r 1081 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∧ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉)) → 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) |
81 | | simp33 1092 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∧ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉)) → 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉) |
82 | | cgrcomlr 31275 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉 ↔ 〈𝐵, 𝑥〉Cgr〈𝑦, 𝐷〉)) |
83 | 21, 31, 30, 26, 24, 82 | syl122anc 1327 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉 ↔ 〈𝐵, 𝑥〉Cgr〈𝑦, 𝐷〉)) |
84 | 83 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∧ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉)) → (〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉 ↔ 〈𝐵, 𝑥〉Cgr〈𝑦, 𝐷〉)) |
85 | 81, 84 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∧ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉)) → 〈𝐵, 𝑥〉Cgr〈𝑦, 𝐷〉) |
86 | 79, 80, 85 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∧ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉)) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐵, 𝑥〉Cgr〈𝑦, 𝐷〉)) |
87 | | brcgr3 31323 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 〈𝐵, 𝑥〉〉Cgr3〈𝐶, 〈𝑦, 𝐷〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐵, 𝑥〉Cgr〈𝑦, 𝐷〉))) |
88 | 21, 28, 30, 31, 23, 24, 26, 87 | syl133anc 1341 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (〈𝐴, 〈𝐵, 𝑥〉〉Cgr3〈𝐶, 〈𝑦, 𝐷〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐵, 𝑥〉Cgr〈𝑦, 𝐷〉))) |
89 | 88 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∧ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉)) → (〈𝐴, 〈𝐵, 𝑥〉〉Cgr3〈𝐶, 〈𝑦, 𝐷〉〉 ↔ (〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐵, 𝑥〉Cgr〈𝑦, 𝐷〉))) |
90 | 86, 89 | mpbird 246 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∧ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉)) → 〈𝐴, 〈𝐵, 𝑥〉〉Cgr3〈𝐶, 〈𝑦, 𝐷〉〉) |
91 | | btwnxfr 31333 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 〈𝐵, 𝑥〉〉Cgr3〈𝐶, 〈𝑦, 𝐷〉〉) → 𝑦 Btwn 〈𝐶, 𝐷〉)) |
92 | 21, 28, 30, 31, 23, 24, 26, 91 | syl133anc 1341 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → ((𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 〈𝐵, 𝑥〉〉Cgr3〈𝐶, 〈𝑦, 𝐷〉〉) → 𝑦 Btwn 〈𝐶, 𝐷〉)) |
93 | 92 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∧ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉)) → ((𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 〈𝐵, 𝑥〉〉Cgr3〈𝐶, 〈𝑦, 𝐷〉〉) → 𝑦 Btwn 〈𝐶, 𝐷〉)) |
94 | 78, 90, 93 | mp2and 711 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∧ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉)) → 𝑦 Btwn 〈𝐶, 𝐷〉) |
95 | 94, 79 | jca 553 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∧ (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉)) → (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) |
96 | 95 | 3expia 1259 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → ((〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉 ∧ 〈𝑥, 𝐵〉Cgr〈𝐷, 𝑦〉) → (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
97 | 77, 96 | sylbid 229 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
𝑦 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → (〈𝐴, 〈𝑥, 𝐵〉〉Cgr3〈𝐶, 〈𝐷, 𝑦〉〉 → (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
98 | 97 | an32s 842 |
. . . . . . 7
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁)) ∧
(𝐶 ∈
(𝔼‘𝑁) ∧
𝐷 ∈
(𝔼‘𝑁))) ∧
𝑥 ∈
(𝔼‘𝑁)) ∧
(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (〈𝐴, 〈𝑥, 𝐵〉〉Cgr3〈𝐶, 〈𝐷, 𝑦〉〉 → (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
99 | 98 | reximdva 3000 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → (∃𝑦 ∈ (𝔼‘𝑁)〈𝐴, 〈𝑥, 𝐵〉〉Cgr3〈𝐶, 〈𝐷, 𝑦〉〉 → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
100 | 72, 99 | mpd 15 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) |
101 | 100 | ex 449 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
102 | 101 | rexlimdva 3013 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
103 | 56, 102 | impbid 201 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ↔ ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉))) |
104 | 1, 103 | bitrd 267 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉))) |