Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
2 | | simp3r 1203 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
3 | | simp2l 1200 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
4 | | btwndiff 34658 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → ∃𝑝 ∈ (𝔼‘𝑁)(𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝)) |
5 | 1, 2, 3, 4 | syl3anc 1372 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∃𝑝 ∈ (𝔼‘𝑁)(𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝)) |
6 | | simprlr 779 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩))) → 𝐴 ≠ 𝑝) |
7 | 6 | necomd 2996 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩))) → 𝑝 ≠ 𝐴) |
8 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
9 | | simpl2l 1227 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
10 | | simpl2r 1228 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁)) |
11 | | simpr 486 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) → 𝑝 ∈ (𝔼‘𝑁)) |
12 | | simpl3r 1230 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁)) |
13 | | simprrl 780 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩))) → 𝐵 Btwn ⟨𝐴, 𝐷⟩) |
14 | 8, 10, 9, 12, 13 | btwncomand 34646 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩))) → 𝐵 Btwn ⟨𝐷, 𝐴⟩) |
15 | | simprll 778 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩))) → 𝐴 Btwn ⟨𝐷, 𝑝⟩) |
16 | 8, 12, 10, 9, 11, 14, 15 | btwnexch3and 34652 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩))) → 𝐴 Btwn ⟨𝐵, 𝑝⟩) |
17 | 8, 9, 10, 11, 16 | btwncomand 34646 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩))) → 𝐴 Btwn ⟨𝑝, 𝐵⟩) |
18 | | simpl3l 1229 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁)) |
19 | | simprrr 781 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩))) → 𝐶 Btwn ⟨𝐴, 𝐷⟩) |
20 | 8, 18, 9, 12, 19 | btwncomand 34646 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩))) → 𝐶 Btwn ⟨𝐷, 𝐴⟩) |
21 | 8, 12, 18, 9, 11, 20, 15 | btwnexch3and 34652 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩))) → 𝐴 Btwn ⟨𝐶, 𝑝⟩) |
22 | 8, 9, 18, 11, 21 | btwncomand 34646 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩))) → 𝐴 Btwn ⟨𝑝, 𝐶⟩) |
23 | 7, 17, 22 | 3jca 1129 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩))) → (𝑝 ≠ 𝐴 ∧ 𝐴 Btwn ⟨𝑝, 𝐵⟩ ∧ 𝐴 Btwn ⟨𝑝, 𝐶⟩)) |
24 | 23 | ex 414 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) → (((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩)) → (𝑝 ≠ 𝐴 ∧ 𝐴 Btwn ⟨𝑝, 𝐵⟩ ∧ 𝐴 Btwn ⟨𝑝, 𝐶⟩))) |
25 | | btwnconn2 34733 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑝 ≠ 𝐴 ∧ 𝐴 Btwn ⟨𝑝, 𝐵⟩ ∧ 𝐴 Btwn ⟨𝑝, 𝐶⟩) → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩))) |
26 | 8, 11, 9, 10, 18, 25 | syl122anc 1380 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) → ((𝑝 ≠ 𝐴 ∧ 𝐴 Btwn ⟨𝑝, 𝐵⟩ ∧ 𝐴 Btwn ⟨𝑝, 𝐶⟩) → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩))) |
27 | 24, 26 | syld 47 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) → (((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) ∧ (𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩)) → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩))) |
28 | 27 | expd 417 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑝 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) → ((𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩) → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩)))) |
29 | 28 | rexlimdva 3149 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑝 ∈ (𝔼‘𝑁)(𝐴 Btwn ⟨𝐷, 𝑝⟩ ∧ 𝐴 ≠ 𝑝) → ((𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩) → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩)))) |
30 | 5, 29 | mpd 15 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩) → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩))) |