Step |
Hyp |
Ref |
Expression |
1 |
|
df-3an |
⊢ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ↔ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) |
2 |
|
simpr11 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) → 𝐴 ≠ 𝑃 ) |
3 |
|
simpr12 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) → 𝐵 ≠ 𝑃 ) |
4 |
|
simpr13 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) → 𝐶 ≠ 𝑃 ) |
5 |
|
simp1 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ ) |
6 |
|
simp3r |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) |
7 |
|
simp2l |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) |
8 |
|
simp3l |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) |
9 |
|
simpr2 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) → 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) |
10 |
5 6 7 8 9
|
btwncomand |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) → 𝑃 Btwn 〈 𝐶 , 𝐴 〉 ) |
11 |
|
simp2r |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) |
12 |
|
simpr3 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) → 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) |
13 |
5 6 11 8 12
|
btwncomand |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) → 𝑃 Btwn 〈 𝐶 , 𝐵 〉 ) |
14 |
|
btwnconn2 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 ≠ 𝑃 ∧ 𝑃 Btwn 〈 𝐶 , 𝐴 〉 ∧ 𝑃 Btwn 〈 𝐶 , 𝐵 〉 ) → ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) ) |
15 |
14
|
3com23 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 ≠ 𝑃 ∧ 𝑃 Btwn 〈 𝐶 , 𝐴 〉 ∧ 𝑃 Btwn 〈 𝐶 , 𝐵 〉 ) → ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) ) |
16 |
15
|
adantr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) → ( ( 𝐶 ≠ 𝑃 ∧ 𝑃 Btwn 〈 𝐶 , 𝐴 〉 ∧ 𝑃 Btwn 〈 𝐶 , 𝐵 〉 ) → ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) ) |
17 |
4 10 13 16
|
mp3and |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) → ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) |
18 |
2 3 17
|
3jca |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) → ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) ) |
19 |
1 18
|
sylan2br |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ∧ 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) → ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) ) |
20 |
19
|
expr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ) → ( 𝑃 Btwn 〈 𝐵 , 𝐶 〉 → ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) ) ) |
21 |
|
simp3 |
⊢ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) → ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) |
22 |
|
df-3an |
⊢ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ) ↔ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ∧ 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ) ) |
23 |
|
simpr11 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ) ) → 𝐴 ≠ 𝑃 ) |
24 |
|
simpr3 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ) ) → 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ) |
25 |
5 7 6 11 24
|
btwncomand |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ) ) → 𝐴 Btwn 〈 𝐵 , 𝑃 〉 ) |
26 |
|
simpr2 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ) ) → 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) |
27 |
|
btwnouttr2 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 ≠ 𝑃 ∧ 𝐴 Btwn 〈 𝐵 , 𝑃 〉 ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) → 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) |
28 |
5 11 7 6 8 27
|
syl122anc |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 ≠ 𝑃 ∧ 𝐴 Btwn 〈 𝐵 , 𝑃 〉 ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) → 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) |
29 |
28
|
adantr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ) ) → ( ( 𝐴 ≠ 𝑃 ∧ 𝐴 Btwn 〈 𝐵 , 𝑃 〉 ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) → 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) |
30 |
23 25 26 29
|
mp3and |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ) ) → 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) |
31 |
22 30
|
sylan2br |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ∧ 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ) ) → 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) |
32 |
31
|
expr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ) → ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 → 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) |
33 |
|
df-3an |
⊢ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ↔ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ∧ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) |
34 |
|
simpr3 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) → 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) |
35 |
5 11 6 7 34
|
btwncomand |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) → 𝐵 Btwn 〈 𝐴 , 𝑃 〉 ) |
36 |
|
simpr2 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) → 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) |
37 |
5 7 11 6 8 35 36
|
btwnexch3and |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) → 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) |
38 |
33 37
|
sylan2br |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ∧ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) → 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) |
39 |
38
|
expr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ) → ( 𝐵 Btwn 〈 𝑃 , 𝐴 〉 → 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) |
40 |
32 39
|
jaod |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ) → ( ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) → 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) |
41 |
21 40
|
syl5 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ) → ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) → 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ) ) |
42 |
20 41
|
impbid |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ) → ( 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) ) ) |
43 |
|
broutsideof2 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf 〈 𝐴 , 𝐵 〉 ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) ) ) |
44 |
5 6 7 11 43
|
syl13anc |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf 〈 𝐴 , 𝐵 〉 ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) ) ) |
45 |
44
|
adantr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ) → ( 𝑃 OutsideOf 〈 𝐴 , 𝐵 〉 ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn 〈 𝑃 , 𝐵 〉 ∨ 𝐵 Btwn 〈 𝑃 , 𝐴 〉 ) ) ) ) |
46 |
42 45
|
bitr4d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) ) → ( 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ↔ 𝑃 OutsideOf 〈 𝐴 , 𝐵 〉 ) ) |
47 |
46
|
ex |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝑃 Btwn 〈 𝐴 , 𝐶 〉 ) → ( 𝑃 Btwn 〈 𝐵 , 𝐶 〉 ↔ 𝑃 OutsideOf 〈 𝐴 , 𝐵 〉 ) ) ) |