Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
2 | | simpr1 1067 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → 𝑃 ∈ (𝔼‘𝑁)) |
3 | | simpr2 1068 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
4 | | simpr3 1069 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
5 | | brsegle2 32216 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (〈𝑃, 𝐴〉 Seg≤ 〈𝑃, 𝐵〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) |
6 | 1, 2, 3, 2, 4, 5 | syl122anc 1335 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (〈𝑃, 𝐴〉 Seg≤ 〈𝑃, 𝐵〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) |
7 | 6 | adantr 481 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑃OutsideOf〈𝐴, 𝐵〉) → (〈𝑃, 𝐴〉 Seg≤ 〈𝑃, 𝐵〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) |
8 | | simprl 794 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → 𝑃OutsideOf〈𝐴, 𝐵〉) |
9 | | outsideofcom 32235 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ 𝑃OutsideOf〈𝐵, 𝐴〉)) |
10 | 9 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → (𝑃OutsideOf〈𝐴, 𝐵〉 ↔ 𝑃OutsideOf〈𝐵, 𝐴〉)) |
11 | 8, 10 | mpbid 222 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → 𝑃OutsideOf〈𝐵, 𝐴〉) |
12 | | simpll 790 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
13 | | simplr1 1103 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑃 ∈ (𝔼‘𝑁)) |
14 | | simplr3 1105 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁)) |
15 | 12, 13, 14 | cgrrflxd 32095 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 〈𝑃, 𝐵〉Cgr〈𝑃, 𝐵〉) |
16 | 15 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → 〈𝑃, 𝐵〉Cgr〈𝑃, 𝐵〉) |
17 | 11, 16 | jca 554 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → (𝑃OutsideOf〈𝐵, 𝐴〉 ∧ 〈𝑃, 𝐵〉Cgr〈𝑃, 𝐵〉)) |
18 | | simprrl 804 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → 𝐴 Btwn 〈𝑃, 𝑦〉) |
19 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑦 ∈ (𝔼‘𝑁)) |
20 | | simplr2 1104 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
21 | | btwncolinear1 32176 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝑃, 𝑦〉 → 𝑃 Colinear 〈𝑦, 𝐴〉)) |
22 | 12, 13, 19, 20, 21 | syl13anc 1328 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝐴 Btwn 〈𝑃, 𝑦〉 → 𝑃 Colinear 〈𝑦, 𝐴〉)) |
23 | 22 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → (𝐴 Btwn 〈𝑃, 𝑦〉 → 𝑃 Colinear 〈𝑦, 𝐴〉)) |
24 | 18, 23 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → 𝑃 Colinear 〈𝑦, 𝐴〉) |
25 | | outsidene1 32230 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 → 𝐴 ≠ 𝑃)) |
26 | 25 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → (𝑃OutsideOf〈𝐴, 𝐵〉 → 𝐴 ≠ 𝑃)) |
27 | 8, 26 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → 𝐴 ≠ 𝑃) |
28 | 27 | neneqd 2799 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → ¬ 𝐴 = 𝑃) |
29 | | df-3an 1039 |
. . . . . . . . . . . . 13
⊢ ((𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝑦, 𝐴〉) ↔ ((𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉)) ∧ 𝑃 Btwn 〈𝑦, 𝐴〉)) |
30 | | simpr2l 1120 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝑦, 𝐴〉)) → 𝐴 Btwn 〈𝑃, 𝑦〉) |
31 | 12, 20, 13, 19, 30 | btwncomand 32122 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝑦, 𝐴〉)) → 𝐴 Btwn 〈𝑦, 𝑃〉) |
32 | | simpr3 1069 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝑦, 𝐴〉)) → 𝑃 Btwn 〈𝑦, 𝐴〉) |
33 | | btwnswapid2 32125 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn 〈𝑦, 𝑃〉 ∧ 𝑃 Btwn 〈𝑦, 𝐴〉) → 𝐴 = 𝑃)) |
34 | 12, 20, 19, 13, 33 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn 〈𝑦, 𝑃〉 ∧ 𝑃 Btwn 〈𝑦, 𝐴〉) → 𝐴 = 𝑃)) |
35 | 34 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝑦, 𝐴〉)) → ((𝐴 Btwn 〈𝑦, 𝑃〉 ∧ 𝑃 Btwn 〈𝑦, 𝐴〉) → 𝐴 = 𝑃)) |
36 | 31, 32, 35 | mp2and 715 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉) ∧ 𝑃 Btwn 〈𝑦, 𝐴〉)) → 𝐴 = 𝑃) |
37 | 29, 36 | sylan2br 493 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ ((𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉)) ∧ 𝑃 Btwn 〈𝑦, 𝐴〉)) → 𝐴 = 𝑃) |
38 | 37 | expr 643 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → (𝑃 Btwn 〈𝑦, 𝐴〉 → 𝐴 = 𝑃)) |
39 | 28, 38 | mtod 189 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → ¬ 𝑃 Btwn 〈𝑦, 𝐴〉) |
40 | | broutsideof 32228 |
. . . . . . . . . 10
⊢ (𝑃OutsideOf〈𝑦, 𝐴〉 ↔ (𝑃 Colinear 〈𝑦, 𝐴〉 ∧ ¬ 𝑃 Btwn 〈𝑦, 𝐴〉)) |
41 | 24, 39, 40 | sylanbrc 698 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → 𝑃OutsideOf〈𝑦, 𝐴〉) |
42 | | simprrr 805 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉) |
43 | 41, 42 | jca 554 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → (𝑃OutsideOf〈𝑦, 𝐴〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉)) |
44 | | outsideofeq 32237 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (((𝑃OutsideOf〈𝐵, 𝐴〉 ∧ 〈𝑃, 𝐵〉Cgr〈𝑃, 𝐵〉) ∧ (𝑃OutsideOf〈𝑦, 𝐴〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉)) → 𝐵 = 𝑦)) |
45 | 12, 13, 20, 13, 14, 14, 19, 44 | syl133anc 1349 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (((𝑃OutsideOf〈𝐵, 𝐴〉 ∧ 〈𝑃, 𝐵〉Cgr〈𝑃, 𝐵〉) ∧ (𝑃OutsideOf〈𝑦, 𝐴〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉)) → 𝐵 = 𝑦)) |
46 | 45 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → (((𝑃OutsideOf〈𝐵, 𝐴〉 ∧ 〈𝑃, 𝐵〉Cgr〈𝑃, 𝐵〉) ∧ (𝑃OutsideOf〈𝑦, 𝐴〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉)) → 𝐵 = 𝑦)) |
47 | 17, 43, 46 | mp2and 715 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → 𝐵 = 𝑦) |
48 | | opeq2 4403 |
. . . . . . . . 9
⊢ (𝐵 = 𝑦 → 〈𝑃, 𝐵〉 = 〈𝑃, 𝑦〉) |
49 | 48 | breq2d 4665 |
. . . . . . . 8
⊢ (𝐵 = 𝑦 → (𝐴 Btwn 〈𝑃, 𝐵〉 ↔ 𝐴 Btwn 〈𝑃, 𝑦〉)) |
50 | 18, 49 | syl5ibrcom 237 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → (𝐵 = 𝑦 → 𝐴 Btwn 〈𝑃, 𝐵〉)) |
51 | 47, 50 | mpd 15 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑃OutsideOf〈𝐴, 𝐵〉 ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → 𝐴 Btwn 〈𝑃, 𝐵〉) |
52 | 51 | an4s 869 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑃OutsideOf〈𝐴, 𝐵〉) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ (𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉))) → 𝐴 Btwn 〈𝑃, 𝐵〉) |
53 | 52 | rexlimdvaa 3032 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑃OutsideOf〈𝐴, 𝐵〉) → (∃𝑦 ∈ (𝔼‘𝑁)(𝐴 Btwn 〈𝑃, 𝑦〉 ∧ 〈𝑃, 𝑦〉Cgr〈𝑃, 𝐵〉) → 𝐴 Btwn 〈𝑃, 𝐵〉)) |
54 | 7, 53 | sylbid 230 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑃OutsideOf〈𝐴, 𝐵〉) → (〈𝑃, 𝐴〉 Seg≤ 〈𝑃, 𝐵〉 → 𝐴 Btwn 〈𝑃, 𝐵〉)) |
55 | | btwnsegle 32224 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝑃, 𝐵〉 → 〈𝑃, 𝐴〉 Seg≤ 〈𝑃, 𝐵〉)) |
56 | 55 | adantr 481 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑃OutsideOf〈𝐴, 𝐵〉) → (𝐴 Btwn 〈𝑃, 𝐵〉 → 〈𝑃, 𝐴〉 Seg≤ 〈𝑃, 𝐵〉)) |
57 | 54, 56 | impbid 202 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) ∧ 𝑃OutsideOf〈𝐴, 𝐵〉) → (〈𝑃, 𝐴〉 Seg≤ 〈𝑃, 𝐵〉 ↔ 𝐴 Btwn 〈𝑃, 𝐵〉)) |
58 | 57 | ex 450 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf〈𝐴, 𝐵〉 → (〈𝑃, 𝐴〉 Seg≤ 〈𝑃, 𝐵〉 ↔ 𝐴 Btwn 〈𝑃, 𝐵〉))) |