Step |
Hyp |
Ref |
Expression |
1 |
|
axbtwnid |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑃 Btwn 〈 𝐴 , 𝐴 〉 → 𝑃 = 𝐴 ) ) |
2 |
|
eqcom |
⊢ ( 𝑃 = 𝐴 ↔ 𝐴 = 𝑃 ) |
3 |
1 2
|
syl6ib |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑃 Btwn 〈 𝐴 , 𝐴 〉 → 𝐴 = 𝑃 ) ) |
4 |
3
|
necon3ad |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 ≠ 𝑃 → ¬ 𝑃 Btwn 〈 𝐴 , 𝐴 〉 ) ) |
5 |
|
colineartriv2 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑃 Colinear 〈 𝐴 , 𝐴 〉 ) |
6 |
4 5
|
jctild |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 ≠ 𝑃 → ( 𝑃 Colinear 〈 𝐴 , 𝐴 〉 ∧ ¬ 𝑃 Btwn 〈 𝐴 , 𝐴 〉 ) ) ) |
7 |
|
broutsideof |
⊢ ( 𝑃 OutsideOf 〈 𝐴 , 𝐴 〉 ↔ ( 𝑃 Colinear 〈 𝐴 , 𝐴 〉 ∧ ¬ 𝑃 Btwn 〈 𝐴 , 𝐴 〉 ) ) |
8 |
6 7
|
syl6ibr |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 ≠ 𝑃 → 𝑃 OutsideOf 〈 𝐴 , 𝐴 〉 ) ) |