MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brbtwn2 Unicode version

Theorem brbtwn2 23620
Description: Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013.)
Assertion
Ref Expression
brbtwn2
Distinct variable groups:   ,N,   , ,   , ,   , ,

Proof of Theorem brbtwn2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brbtwn 23614 . 2
2 fveere 23616 . . . . . . . . . 10
323ad2antl2 1151 . . . . . . . . 9
4 fveere 23616 . . . . . . . . . 10
543ad2antl3 1152 . . . . . . . . 9
63, 5jca 532 . . . . . . . 8
7 resubcl 9810 . . . . . . . . . . . . . . 15
873adant3 1008 . . . . . . . . . . . . . 14
98recnd 9549 . . . . . . . . . . . . 13
109sqvald 12162 . . . . . . . . . . . 12
1110oveq2d 6238 . . . . . . . . . . 11
12 0re 9523 . . . . . . . . . . . . . . . 16
13 1re 9522 . . . . . . . . . . . . . . . 16
1412, 13elicc2i 11500 . . . . . . . . . . . . . . 15
1514simp1bi 1003 . . . . . . . . . . . . . 14
1615recnd 9549 . . . . . . . . . . . . 13
17163ad2ant3 1011 . . . . . . . . . . . 12
18 resubcl 9810 . . . . . . . . . . . . . . . 16
1913, 15, 18sylancr 663 . . . . . . . . . . . . . . 15
20193ad2ant3 1011 . . . . . . . . . . . . . 14
2120recnd 9549 . . . . . . . . . . . . 13
2221negcld 9843 . . . . . . . . . . . 12
2317, 9, 22, 9mul4d 9718 . . . . . . . . . . 11
24 recn 9509 . . . . . . . . . . . . . . 15
25243ad2ant1 1009 . . . . . . . . . . . . . 14
26 recn 9509 . . . . . . . . . . . . . . 15
27263ad2ant2 1010 . . . . . . . . . . . . . 14
2817, 25, 27subdid 9937 . . . . . . . . . . . . 13
29 ax-1cn 9477 . . . . . . . . . . . . . . . . 17
30 subdir 9916 . . . . . . . . . . . . . . . . 17
3129, 30mp3an1 1302 . . . . . . . . . . . . . . . 16
3221, 25, 31syl2anc 661 . . . . . . . . . . . . . . 15
33 nncan 9775 . . . . . . . . . . . . . . . . 17
3429, 17, 33sylancr 663 . . . . . . . . . . . . . . . 16
3534oveq1d 6237 . . . . . . . . . . . . . . 15
3625mulid2d 9541 . . . . . . . . . . . . . . . 16
3736oveq1d 6237 . . . . . . . . . . . . . . 15
3832, 35, 373eqtr3d 2503 . . . . . . . . . . . . . 14
3938oveq1d 6237 . . . . . . . . . . . . 13
40 simp1 988 . . . . . . . . . . . . . . . 16
4120, 40remulcld 9551 . . . . . . . . . . . . . . 15
4241recnd 9549 . . . . . . . . . . . . . 14
43153ad2ant3 1011 . . . . . . . . . . . . . . . 16
44 simp2 989 . . . . . . . . . . . . . . . 16
4543, 44remulcld 9551 . . . . . . . . . . . . . . 15
4645recnd 9549 . . . . . . . . . . . . . 14
4725, 42, 46subsub4d 9887 . . . . . . . . . . . . 13
4828, 39, 473eqtrd 2499 . . . . . . . . . . . 12
4921, 9mulneg1d 9934 . . . . . . . . . . . . 13
5021, 25, 27subdid 9937 . . . . . . . . . . . . . . 15
51 subdir 9916 . . . . . . . . . . . . . . . . . . 19
5229, 51mp3an1 1302 . . . . . . . . . . . . . . . . . 18
5317, 27, 52syl2anc 661 . . . . . . . . . . . . . . . . 17
5427mulid2d 9541 . . . . . . . . . . . . . . . . . 18
5554oveq1d 6237 . . . . . . . . . . . . . . . . 17
5653, 55eqtrd 2495 . . . . . . . . . . . . . . . 16
5756oveq2d 6238 . . . . . . . . . . . . . . 15
5842, 27, 46subsub3d 9886 . . . . . . . . . . . . . . 15
5950, 57, 583eqtrd 2499 . . . . . . . . . . . . . 14
6059negeqd 9741 . . . . . . . . . . . . 13
6141, 45readdcld 9550 . . . . . . . . . . . . . . 15
6261recnd 9549 . . . . . . . . . . . . . 14
6362, 27negsubdi2d 9872 . . . . . . . . . . . . 13
6449, 60, 633eqtrd 2499 . . . . . . . . . . . 12
6548, 64oveq12d 6240 . . . . . . . . . . 11
6611, 23, 653eqtr2rd 2502 . . . . . . . . . 10
6717, 21mulneg2d 9935 . . . . . . . . . . . . 13
6867oveq1d 6237 . . . . . . . . . . . 12
6943, 20remulcld 9551 . . . . . . . . . . . . . 14
7069recnd 9549 . . . . . . . . . . . . 13
718resqcld 12191 . . . . . . . . . . . . . 14
7271recnd 9549 . . . . . . . . . . . . 13
7370, 72mulneg1d 9934 . . . . . . . . . . . 12
7468, 73eqtrd 2495 . . . . . . . . . . 11
7514simp2bi 1004 . . . . . . . . . . . . . . 15
7614simp3bi 1005 . . . . . . . . . . . . . . . 16
77 subge0 9989 . . . . . . . . . . . . . . . . 17
7813, 15, 77sylancr 663 . . . . . . . . . . . . . . . 16
7976, 78mpbird 232 . . . . . . . . . . . . . . 15
8015, 19, 75, 79mulge0d 10053 . . . . . . . . . . . . . 14
81803ad2ant3 1011 . . . . . . . . . . . . 13
828sqge0d 12192 . . . . . . . . . . . . 13
8369, 71, 81, 82mulge0d 10053 . . . . . . . . . . . 12
8469, 71remulcld 9551 . . . . . . . . . . . . 13
8584le0neg2d 10049 . . . . . . . . . . . 12
8683, 85mpbid 210 . . . . . . . . . . 11
8774, 86eqbrtrd 4429 . . . . . . . . . 10
8866, 87eqbrtrd 4429 . . . . . . . . 9
89883expa 1188 . . . . . . . 8
906, 89sylan 471 . . . . . . 7
9190an32s 802 . . . . . 6
9291ralrimiva 2831 . . . . 5
93 fveecn 23617 . . . . . . . . . . . 12
94 fveecn 23617 . . . . . . . . . . . 12
9593, 94anim12i 566 . . . . . . . . . . 11
9695anandirs 827 . . . . . . . . . 10
97 fveecn 23617 . . . . . . . . . . . 12
98 fveecn 23617 . . . . . . . . . . . 12
9997, 98anim12i 566 . . . . . . . . . . 11
10099anandirs 827 . . . . . . . . . 10
10196, 100anim12dan 833 . . . . . . . . 9
1021013adantl1 1144 . . . . . . . 8
103 subcl 9746 . . . . . . . . . . . . . 14
1041033ad2ant1 1009 . . . . . . . . . . . . 13
105 subcl 9746 . . . . . . . . . . . . . . 15
106105ancoms 453 . . . . . . . . . . . . . 14
1071063ad2ant2 1010 . . . . . . . . . . . . 13
108104, 107mulcomd 9544 . . . . . . . . . . . 12
109 simp2r 1015 . . . . . . . . . . . . 13
110 simp2l 1014 . . . . . . . . . . . . 13
111 simp1l 1012 . . . . . . . . . . . . 13
112 simp1r 1013 . . . . . . . . . . . . 13
113 mulsub2 9925 . . . . . . . . . . . . 13
114109, 110, 111, 112, 113syl22anc 1220 . . . . . . . . . . . 12
115108, 114eqtrd 2495 . . . . . . . . . . 11
116115oveq2d 6238 . . . . . . . . . 10
117 simp3 990 . . . . . . . . . . . 12
118 subcl 9746 . . . . . . . . . . . . . 14
11929, 118mpan 670 . . . . . . . . . . . . 13
1201193ad2ant3 1011 . . . . . . . . . . . 12
121117, 120, 104, 107mul4d 9718 . . . . . . . . . . 11
122117, 111, 112subdid 9937 . . . . . . . . . . . . 13
123120, 111, 31syl2anc 661 . . . . . . . . . . . . . . 15
12429, 33mpan 670 . . . . . . . . . . . . . . . . 17
1251243ad2ant3 1011 . . . . . . . . . . . . . . . 16
126125oveq1d 6237 . . . . . . . . . . . . . . 15
127111mulid2d 9541 . . . . . . . . . . . . . . . 16
128127oveq1d 6237 . . . . . . . . . . . . . . 15
129123, 126, 1283eqtr3d 2503 . . . . . . . . . . . . . 14
130129oveq1d 6237 . . . . . . . . . . . . 13
131120, 111mulcld 9543 . . . . . . . . . . . . . 14
132117, 112mulcld 9543 . . . . . . . . . . . . . 14
133111, 131, 132subsub4d 9887 . . . . . . . . . . . . 13
134122, 130, 1333eqtrd 2499 . . . . . . . . . . . 12
135120, 109, 110subdid 9937 . . . . . . . . . . . . . 14
136 subdir 9916 . . . . . . . . . . . . . . . . . 18
13729, 136mp3an1 1302 . . . . . . . . . . . . . . . . 17
138117, 109, 137syl2anc 661 . . . . . . . . . . . . . . . 16
139109mulid2d 9541 . . . . . . . . . . . . . . . . 17
140139oveq1d 6237 . . . . . . . . . . . . . . . 16
141138, 140eqtrd 2495 . . . . . . . . . . . . . . 15
142141oveq1d 6237 . . . . . . . . . . . . . 14
143135, 142eqtrd 2495 . . . . . . . . . . . . 13
144117, 109mulcld 9543 . . . . . . . . . . . . . 14
145120, 110mulcld 9543 . . . . . . . . . . . . . 14
146109, 144, 145sub32d 9888 . . . . . . . . . . . . 13
147109, 145, 144subsub4d 9887 . . . . . . . . . . . . 13
148143, 146, 1473eqtrd 2499 . . . . . . . . . . . 12
149134, 148oveq12d 6240 . . . . . . . . . . 11
150121, 149eqtrd 2495 . . . . . . . . . 10
151 subcl 9746 . . . . . . . . . . . . 13
1521513ad2ant2 1010 . . . . . . . . . . . 12