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→POutsideOfAB↔A≠P∧B≠P∧ABtwnPB∨BBtwnPA

Proof

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