Metamath Proof Explorer

Theorem colinbtwnle

Description: Given three colinear points A , B , and C , B falls in the middle iff the two segments to B are no longer than A C . Theorem 5.12 of Schwabhauser p. 42. (Contributed by Scott Fenton, 15-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion colinbtwnle ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearBC→BBtwnAC↔ABSeg≤AC∧BCSeg≤AC

Proof

Step Hyp Ref Expression
1 btwnsegle ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC→ABSeg≤AC
2 3anrev ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N↔C∈𝔼⁡N∧B∈𝔼⁡N∧A∈𝔼⁡N
3 btwnsegle ⊢N∈ℕ∧C∈𝔼⁡N∧B∈𝔼⁡N∧A∈𝔼⁡N→BBtwnCA→CBSeg≤CA
4 2 3 sylan2b ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnCA→CBSeg≤CA
5 3ancoma ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N↔B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N
6 btwncom ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC↔BBtwnCA
7 5 6 sylan2b ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC↔BBtwnCA
8 simpl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→N∈ℕ
9 simpr2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B∈𝔼⁡N
10 simpr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→C∈𝔼⁡N
11 8 9 10 cgrrflx2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BCCgrCB
12 simpr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→A∈𝔼⁡N
13 8 12 10 cgrrflx2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ACCgrCA
14 seglecgr12 ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→BCCgrCB∧ACCgrCA→BCSeg≤AC↔CBSeg≤CA
15 8 9 10 12 10 10 9 10 12 14 syl333anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BCCgrCB∧ACCgrCA→BCSeg≤AC↔CBSeg≤CA
16 11 13 15 mp2and ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BCSeg≤AC↔CBSeg≤CA
17 4 7 16 3imtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC→BCSeg≤AC
18 1 17 jcad ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC→ABSeg≤AC∧BCSeg≤AC
19 18 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧AColinearBC→BBtwnAC→ABSeg≤AC∧BCSeg≤AC
20 brcolinear ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearBC↔ABtwnBC∨BBtwnCA∨CBtwnAB
21 simprl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧ABtwnBC∧BCSeg≤AC→ABtwnBC
22 8 12 9 10 21 btwncomand ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧ABtwnBC∧BCSeg≤AC→ABtwnCB
23 16 biimpa ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧BCSeg≤AC→CBSeg≤CA
24 23 adantrl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧ABtwnBC∧BCSeg≤AC→CBSeg≤CA
25 btwncom ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC↔ABtwnCB
26 3anrot ⊢C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N↔A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N
27 btwnsegle ⊢N∈ℕ∧C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N→ABtwnCB→CASeg≤CB
28 26 27 sylan2br ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnCB→CASeg≤CB
29 25 28 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC→CASeg≤CB
30 29 imp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧ABtwnBC→CASeg≤CB
31 30 adantrr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧ABtwnBC∧BCSeg≤AC→CASeg≤CB
32 segleantisym ⊢N∈ℕ∧C∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→CBSeg≤CA∧CASeg≤CB→CBCgrCA
33 8 10 9 10 12 32 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→CBSeg≤CA∧CASeg≤CB→CBCgrCA
34 33 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧ABtwnBC∧BCSeg≤AC→CBSeg≤CA∧CASeg≤CB→CBCgrCA
35 24 31 34 mp2and ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧ABtwnBC∧BCSeg≤AC→CBCgrCA
36 8 10 9 12 22 35 endofsegidand ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧ABtwnBC∧BCSeg≤AC→B=A
37 btwntriv1 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N→ABtwnAC
38 37 3adant3r2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnAC
39 breq1 ⊢B=A→BBtwnAC↔ABtwnAC
40 38 39 syl5ibrcom ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B=A→BBtwnAC
41 40 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧ABtwnBC∧BCSeg≤AC→B=A→BBtwnAC
42 36 41 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧ABtwnBC∧BCSeg≤AC→BBtwnAC
43 42 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧ABtwnBC→BCSeg≤AC→BBtwnAC
44 43 adantld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧ABtwnBC→ABSeg≤AC∧BCSeg≤AC→BBtwnAC
45 44 ex ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC→ABSeg≤AC∧BCSeg≤AC→BBtwnAC
46 7 biimprd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnCA→BBtwnAC
47 46 a1dd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnCA→ABSeg≤AC∧BCSeg≤AC→BBtwnAC
48 simprl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧CBtwnAB∧ABSeg≤AC→CBtwnAB
49 simprr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧CBtwnAB∧ABSeg≤AC→ABSeg≤AC
50 3ancomb ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N↔A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N
51 btwnsegle ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N→CBtwnAB→ACSeg≤AB
52 50 51 sylan2b ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→CBtwnAB→ACSeg≤AB
53 52 imp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧CBtwnAB→ACSeg≤AB
54 53 adantrr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧CBtwnAB∧ABSeg≤AC→ACSeg≤AB
55 segleantisym ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N→ABSeg≤AC∧ACSeg≤AB→ABCgrAC
56 8 12 9 12 10 55 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABSeg≤AC∧ACSeg≤AB→ABCgrAC
57 56 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧CBtwnAB∧ABSeg≤AC→ABSeg≤AC∧ACSeg≤AB→ABCgrAC
58 49 54 57 mp2and ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧CBtwnAB∧ABSeg≤AC→ABCgrAC
59 8 12 9 10 48 58 endofsegidand ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧CBtwnAB∧ABSeg≤AC→B=C
60 btwntriv2 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N→CBtwnAC
61 60 3adant3r2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→CBtwnAC
62 breq1 ⊢B=C→BBtwnAC↔CBtwnAC
63 61 62 syl5ibrcom ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B=C→BBtwnAC
64 63 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧CBtwnAB∧ABSeg≤AC→B=C→BBtwnAC
65 59 64 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧CBtwnAB∧ABSeg≤AC→BBtwnAC
66 65 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧CBtwnAB→ABSeg≤AC→BBtwnAC
67 66 adantrd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧CBtwnAB→ABSeg≤AC∧BCSeg≤AC→BBtwnAC
68 67 ex ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→CBtwnAB→ABSeg≤AC∧BCSeg≤AC→BBtwnAC
69 45 47 68 3jaod ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC∨BBtwnCA∨CBtwnAB→ABSeg≤AC∧BCSeg≤AC→BBtwnAC
70 20 69 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearBC→ABSeg≤AC∧BCSeg≤AC→BBtwnAC
71 70 imp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧AColinearBC→ABSeg≤AC∧BCSeg≤AC→BBtwnAC
72 19 71 impbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧AColinearBC→BBtwnAC↔ABSeg≤AC∧BCSeg≤AC
73 72 ex ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearBC→BBtwnAC↔ABSeg≤AC∧BCSeg≤AC