Metamath Proof Explorer

Theorem broutsideof2

Description: Alternate form of OutsideOf . Definition 6.1 of Schwabhauser p. 43. (Contributed by Scott Fenton, 17-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion broutsideof2 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → P OutsideOf A B ↔ A ≠ P ∧ B ≠ P ∧ A Btwn P B ∨ B Btwn P A

Proof

Step Hyp Ref Expression
1 broutsideof ⊢ P OutsideOf A B ↔ P Colinear A B ∧ ¬ P Btwn A B
2 btwntriv1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn A B
3 2 3adant3r1 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn A B
4 breq1 ⊢ A = P → A Btwn A B ↔ P Btwn A B
5 3 4 syl5ibcom ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = P → P Btwn A B
6 5 necon3bd ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ¬ P Btwn A B → A ≠ P
7 6 imp ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ ¬ P Btwn A B → A ≠ P
8 7 adantrl ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ P Colinear A B ∧ ¬ P Btwn A B → A ≠ P
9 btwntriv2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B Btwn A B
10 9 3adant3r1 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B Btwn A B
11 breq1 ⊢ B = P → B Btwn A B ↔ P Btwn A B
12 10 11 syl5ibcom ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B = P → P Btwn A B
13 12 necon3bd ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ¬ P Btwn A B → B ≠ P
14 13 imp ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ ¬ P Btwn A B → B ≠ P
15 14 adantrl ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ P Colinear A B ∧ ¬ P Btwn A B → B ≠ P
16 brcolinear ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → P Colinear A B ↔ P Btwn A B ∨ A Btwn B P ∨ B Btwn P A
17 pm2.24 ⊢ P Btwn A B → ¬ P Btwn A B → A Btwn P B ∨ B Btwn P A
18 17 a1i ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → P Btwn A B → ¬ P Btwn A B → A Btwn P B ∨ B Btwn P A
19 3anrot ⊢ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ↔ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N
20 btwncom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N → A Btwn B P ↔ A Btwn P B
21 19 20 sylan2b ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn B P ↔ A Btwn P B
22 orc ⊢ A Btwn P B → A Btwn P B ∨ B Btwn P A
23 21 22 syl6bi ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn B P → A Btwn P B ∨ B Btwn P A
24 23 a1dd ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn B P → ¬ P Btwn A B → A Btwn P B ∨ B Btwn P A
25 olc ⊢ B Btwn P A → A Btwn P B ∨ B Btwn P A
26 25 a1d ⊢ B Btwn P A → ¬ P Btwn A B → A Btwn P B ∨ B Btwn P A
27 26 a1i ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B Btwn P A → ¬ P Btwn A B → A Btwn P B ∨ B Btwn P A
28 18 24 27 3jaod ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → P Btwn A B ∨ A Btwn B P ∨ B Btwn P A → ¬ P Btwn A B → A Btwn P B ∨ B Btwn P A
29 16 28 sylbid ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → P Colinear A B → ¬ P Btwn A B → A Btwn P B ∨ B Btwn P A
30 29 imp32 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ P Colinear A B ∧ ¬ P Btwn A B → A Btwn P B ∨ B Btwn P A
31 8 15 30 3jca ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ P Colinear A B ∧ ¬ P Btwn A B → A ≠ P ∧ B ≠ P ∧ A Btwn P B ∨ B Btwn P A
32 simp3 ⊢ A ≠ P ∧ B ≠ P ∧ A Btwn P B ∨ B Btwn P A → A Btwn P B ∨ B Btwn P A
33 3ancomb ⊢ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ↔ P ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N
34 btwncolinear2 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → A Btwn P B → P Colinear A B
35 33 34 sylan2b ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn P B → P Colinear A B
36 btwncolinear1 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B Btwn P A → P Colinear A B
37 35 36 jaod ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn P B ∨ B Btwn P A → P Colinear A B
38 32 37 syl5 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A ≠ P ∧ B ≠ P ∧ A Btwn P B ∨ B Btwn P A → P Colinear A B
39 38 imp ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ P ∧ B ≠ P ∧ A Btwn P B ∨ B Btwn P A → P Colinear A B
40 simpr2 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A Btwn P B ∧ A ≠ P ∧ B ≠ P → A ≠ P
41 40 neneqd ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A Btwn P B ∧ A ≠ P ∧ B ≠ P → ¬ A = P
42 simprl1 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A Btwn P B ∧ A ≠ P ∧ B ≠ P ∧ P Btwn A B → A Btwn P B
43 simprr ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A Btwn P B ∧ A ≠ P ∧ B ≠ P ∧ P Btwn A B → P Btwn A B
44 simpl ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → N ∈ ℕ
45 simpr2 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
46 simpr1 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → P ∈ 𝔼 ⁡ N
47 simpr3 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
48 btwnswapid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn P B ∧ P Btwn A B → A = P
49 44 45 46 47 48 syl13anc ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn P B ∧ P Btwn A B → A = P
50 49 adantr ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A Btwn P B ∧ A ≠ P ∧ B ≠ P ∧ P Btwn A B → A Btwn P B ∧ P Btwn A B → A = P
51 42 43 50 mp2and ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A Btwn P B ∧ A ≠ P ∧ B ≠ P ∧ P Btwn A B → A = P
52 51 expr ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A Btwn P B ∧ A ≠ P ∧ B ≠ P → P Btwn A B → A = P
53 41 52 mtod ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A Btwn P B ∧ A ≠ P ∧ B ≠ P → ¬ P Btwn A B
54 53 3exp2 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn P B → A ≠ P → B ≠ P → ¬ P Btwn A B
55 simpr3 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B Btwn P A ∧ A ≠ P ∧ B ≠ P → B ≠ P
56 55 neneqd ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B Btwn P A ∧ A ≠ P ∧ B ≠ P → ¬ B = P
57 simprl1 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B Btwn P A ∧ A ≠ P ∧ B ≠ P ∧ P Btwn A B → B Btwn P A
58 simprr ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B Btwn P A ∧ A ≠ P ∧ B ≠ P ∧ P Btwn A B → P Btwn A B
59 44 46 45 47 58 btwncomand ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B Btwn P A ∧ A ≠ P ∧ B ≠ P ∧ P Btwn A B → P Btwn B A
60 3anrot ⊢ B ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ↔ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N
61 btwnswapid ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → B Btwn P A ∧ P Btwn B A → B = P
62 60 61 sylan2br ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B Btwn P A ∧ P Btwn B A → B = P
63 62 adantr ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B Btwn P A ∧ A ≠ P ∧ B ≠ P ∧ P Btwn A B → B Btwn P A ∧ P Btwn B A → B = P
64 57 59 63 mp2and ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B Btwn P A ∧ A ≠ P ∧ B ≠ P ∧ P Btwn A B → B = P
65 64 expr ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B Btwn P A ∧ A ≠ P ∧ B ≠ P → P Btwn A B → B = P
66 56 65 mtod ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B Btwn P A ∧ A ≠ P ∧ B ≠ P → ¬ P Btwn A B
67 66 3exp2 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B Btwn P A → A ≠ P → B ≠ P → ¬ P Btwn A B
68 54 67 jaod ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn P B ∨ B Btwn P A → A ≠ P → B ≠ P → ¬ P Btwn A B
69 68 com12 ⊢ A Btwn P B ∨ B Btwn P A → N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A ≠ P → B ≠ P → ¬ P Btwn A B
70 69 com4l ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A ≠ P → B ≠ P → A Btwn P B ∨ B Btwn P A → ¬ P Btwn A B
71 70 3imp2 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ P ∧ B ≠ P ∧ A Btwn P B ∨ B Btwn P A → ¬ P Btwn A B
72 39 71 jca ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ P ∧ B ≠ P ∧ A Btwn P B ∨ B Btwn P A → P Colinear A B ∧ ¬ P Btwn A B
73 31 72 impbida ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → P Colinear A B ∧ ¬ P Btwn A B ↔ A ≠ P ∧ B ≠ P ∧ A Btwn P B ∨ B Btwn P A
74 1 73 syl5bb ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → P OutsideOf A B ↔ A ≠ P ∧ B ≠ P ∧ A Btwn P B ∨ B Btwn P A