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

Theorem brbtwn2 22830
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 22824 . 2
2 fveere 22826 . . . . . . . . . 10
323ad2antl2 1136 . . . . . . . . 9
4 fveere 22826 . . . . . . . . . 10
543ad2antl3 1137 . . . . . . . . 9
63, 5jca 522 . . . . . . . 8
7 resubcl 9619 . . . . . . . . . . . . . . 15
873adant3 993 . . . . . . . . . . . . . 14
98recnd 9358 . . . . . . . . . . . . 13
109sqvald 11946 . . . . . . . . . . . 12
1110oveq2d 6077 . . . . . . . . . . 11
12 0re 9332 . . . . . . . . . . . . . . . 16
13 1re 9331 . . . . . . . . . . . . . . . 16
1412, 13elicc2i 11306 . . . . . . . . . . . . . . 15
1514simp1bi 988 . . . . . . . . . . . . . 14
1615recnd 9358 . . . . . . . . . . . . 13
17163ad2ant3 996 . . . . . . . . . . . 12
18 resubcl 9619 . . . . . . . . . . . . . . . 16
1913, 15, 18sylancr 648 . . . . . . . . . . . . . . 15
20193ad2ant3 996 . . . . . . . . . . . . . 14
2120recnd 9358 . . . . . . . . . . . . 13
2221negcld 9652 . . . . . . . . . . . 12
2317, 9, 22, 9mul4d 9527 . . . . . . . . . . 11
24 recn 9318 . . . . . . . . . . . . . . 15
25243ad2ant1 994 . . . . . . . . . . . . . 14
26 recn 9318 . . . . . . . . . . . . . . 15
27263ad2ant2 995 . . . . . . . . . . . . . 14
2817, 25, 27subdid 9746 . . . . . . . . . . . . 13
29 ax-1cn 9286 . . . . . . . . . . . . . . . . 17
30 subdir 9725 . . . . . . . . . . . . . . . . 17
3129, 30mp3an1 1286 . . . . . . . . . . . . . . . 16
3221, 25, 31syl2anc 646 . . . . . . . . . . . . . . 15
33 nncan 9584 . . . . . . . . . . . . . . . . 17
3429, 17, 33sylancr 648 . . . . . . . . . . . . . . . 16
3534oveq1d 6076 . . . . . . . . . . . . . . 15
3625mulid2d 9350 . . . . . . . . . . . . . . . 16
3736oveq1d 6076 . . . . . . . . . . . . . . 15
3832, 35, 373eqtr3d 2462 . . . . . . . . . . . . . 14
3938oveq1d 6076 . . . . . . . . . . . . 13
40 simp1 973 . . . . . . . . . . . . . . . 16
4120, 40remulcld 9360 . . . . . . . . . . . . . . 15
4241recnd 9358 . . . . . . . . . . . . . 14
43153ad2ant3 996 . . . . . . . . . . . . . . . 16
44 simp2 974 . . . . . . . . . . . . . . . 16
4543, 44remulcld 9360 . . . . . . . . . . . . . . 15
4645recnd 9358 . . . . . . . . . . . . . 14
4725, 42, 46subsub4d 9696 . . . . . . . . . . . . 13
4828, 39, 473eqtrd 2458 . . . . . . . . . . . 12
4921, 9mulneg1d 9743 . . . . . . . . . . . . 13
5021, 25, 27subdid 9746 . . . . . . . . . . . . . . 15
51 subdir 9725 . . . . . . . . . . . . . . . . . . 19
5229, 51mp3an1 1286 . . . . . . . . . . . . . . . . . 18
5317, 27, 52syl2anc 646 . . . . . . . . . . . . . . . . 17
5427mulid2d 9350 . . . . . . . . . . . . . . . . . 18
5554oveq1d 6076 . . . . . . . . . . . . . . . . 17
5653, 55eqtrd 2454 . . . . . . . . . . . . . . . 16
5756oveq2d 6077 . . . . . . . . . . . . . . 15
5842, 27, 46subsub3d 9695 . . . . . . . . . . . . . . 15
5950, 57, 583eqtrd 2458 . . . . . . . . . . . . . 14
6059negeqd 9550 . . . . . . . . . . . . 13
6141, 45readdcld 9359 . . . . . . . . . . . . . . 15
6261recnd 9358 . . . . . . . . . . . . . 14
6362, 27negsubdi2d 9681 . . . . . . . . . . . . 13
6449, 60, 633eqtrd 2458 . . . . . . . . . . . 12
6548, 64oveq12d 6079 . . . . . . . . . . 11
6611, 23, 653eqtr2rd 2461 . . . . . . . . . 10
6717, 21mulneg2d 9744 . . . . . . . . . . . . 13
6867oveq1d 6076 . . . . . . . . . . . 12
6943, 20remulcld 9360 . . . . . . . . . . . . . 14
7069recnd 9358 . . . . . . . . . . . . 13
718resqcld 11975 . . . . . . . . . . . . . 14
7271recnd 9358 . . . . . . . . . . . . 13
7370, 72mulneg1d 9743 . . . . . . . . . . . 12
7468, 73eqtrd 2454 . . . . . . . . . . 11
7514simp2bi 989 . . . . . . . . . . . . . . 15
7614simp3bi 990 . . . . . . . . . . . . . . . 16
77 subge0 9798 . . . . . . . . . . . . . . . . 17
7813, 15, 77sylancr 648 . . . . . . . . . . . . . . . 16
7976, 78mpbird 226 . . . . . . . . . . . . . . 15
8015, 19, 75, 79mulge0d 9862 . . . . . . . . . . . . . 14
81803ad2ant3 996 . . . . . . . . . . . . 13
828sqge0d 11976 . . . . . . . . . . . . 13
8369, 71, 81, 82mulge0d 9862 . . . . . . . . . . . 12
8469, 71remulcld 9360 . . . . . . . . . . . . 13
8584le0neg2d 9858 . . . . . . . . . . . 12
8683, 85mpbid 204 . . . . . . . . . . 11
8774, 86eqbrtrd 4287 . . . . . . . . . 10
8866, 87eqbrtrd 4287 . . . . . . . . 9
89883expa 1172 . . . . . . . 8
906, 89sylan 461 . . . . . . 7
9190an32s 787 . . . . . 6
9291ralrimiva 2778 . . . . 5
93 fveecn 22827 . . . . . . . . . . . 12
94 fveecn 22827 . . . . . . . . . . . 12
9593, 94anim12i 553 . . . . . . . . . . 11
9695anandirs 812 . . . . . . . . . 10
97 fveecn 22827 . . . . . . . . . . . 12
98 fveecn 22827 . . . . . . . . . . . 12
9997, 98anim12i 553 . . . . . . . . . . 11
10099anandirs 812 . . . . . . . . . 10
10196, 100anim12dan 818 . . . . . . . . 9
1021013adantl1 1129 . . . . . . . 8
103 subcl 9555 . . . . . . . . . . . . . 14
1041033ad2ant1 994 . . . . . . . . . . . . 13
105 subcl 9555 . . . . . . . . . . . . . . 15
106105ancoms 443 . . . . . . . . . . . . . 14
1071063ad2ant2 995 . . . . . . . . . . . . 13
108104, 107mulcomd 9353 . . . . . . . . . . . 12
109 simp2r 1000 . . . . . . . . . . . . 13
110 simp2l 999 . . . . . . . . . . . . 13
111 simp1l 997 . . . . . . . . . . . . 13
112 simp1r 998 . . . . . . . . . . . . 13
113 mulsub2 9734 . . . . . . . . . . . . 13
114109, 110, 111, 112, 113syl22anc 1204 . . . . . . . . . . . 12
115108, 114eqtrd 2454 . . . . . . . . . . 11
116115oveq2d 6077 . . . . . . . . . 10
117 simp3 975 . . . . . . . . . . . 12
118 subcl 9555 . . . . . . . . . . . . . 14
11929, 118mpan 655 . . . . . . . . . . . . 13
1201193ad2ant3 996 . . . . . . . . . . . 12
121117, 120, 104, 107mul4d 9527 . . . . . . . . . . 11
122117, 111, 112subdid 9746 . . . . . . . . . . . . 13
123120, 111, 31syl2anc 646 . . . . . . . . . . . . . . 15
12429, 33mpan 655 . . . . . . . . . . . . . . . . 17
1251243ad2ant3 996 . . . . . . . . . . . . . . . 16
126125oveq1d 6076 . . . . . . . . . . . . . . 15
127111mulid2d 9350 . . . . . . . . . . . . . . . 16
128127oveq1d 6076 . . . . . . . . . . . . . . 15
129123, 126, 1283eqtr3d 2462 . . . . . . . . . . . . . 14
130129oveq1d 6076 . . . . . . . . . . . . 13
131120, 111mulcld 9352 . . . . . . . . . . . . . 14
132117, 112mulcld 9352 . . . . . . . . . . . . . 14
133111, 131, 132subsub4d 9696 . . . . . . . . . . . . 13
134122, 130, 1333eqtrd 2458 . . . . . . . . . . . 12
135120, 109, 110subdid 9746 . . . . . . . . . . . . . 14
136 subdir 9725 . . . . . . . . . . . . . . . . . 18
13729, 136mp3an1 1286 . . . . . . . . . . . . . . . . 17
138117, 109, 137syl2anc 646 . . . . . . . . . . . . . . . 16
139109mulid2d 9350 . . . . . . . . . . . . . . . . 17
140139oveq1d 6076 . . . . . . . . . . . . . . . 16
141138, 140eqtrd 2454 . . . . . . . . . . . . . . 15
142141oveq1d 6076 . . . . . . . . . . . . . 14
143135, 142eqtrd 2454 . . . . . . . . . . . . 13
144117, 109mulcld 9352 . . . . . . . . . . . . . 14
145120, 110mulcld 9352 . . . . . . . . . . . . . 14
146109, 144, 145sub32d 9697 . . . . . . . . . . . . 13
147109, 145, 144subsub4d 9696 . . . . . . . . . . . . 13
148143, 146, 1473eqtrd 2458 . . . . . . . . . . . 12
149134, 148oveq12d 6079 . . . . . . . . . . 11
150121, 149eqtrd 2454 . . . . . . . . . 10
151 subcl 9555 . . . . . . . . . . . . 13
1521513ad2ant2 995 . . . . . . . . . . . 12