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

Theorem xlemul1a 11509
Description: Extended real version of lemul1a 10421. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xlemul1a

Proof of Theorem xlemul1a
StepHypRef Expression
1 0xr 9661 . . . . . 6
2 simpr 461 . . . . . 6
3 xrleloe 11379 . . . . . 6
41, 2, 3sylancr 663 . . . . 5
5 simpllr 760 . . . . . . . . . . . 12
6 elxr 11354 . . . . . . . . . . . 12
75, 6sylib 196 . . . . . . . . . . 11
8 simplrr 762 . . . . . . . . . . . . . . 15
9 simprll 763 . . . . . . . . . . . . . . . 16
10 simprlr 764 . . . . . . . . . . . . . . . 16
11 simprr 757 . . . . . . . . . . . . . . . 16
12 simplrl 761 . . . . . . . . . . . . . . . 16
13 lemul1 10419 . . . . . . . . . . . . . . . 16
149, 10, 11, 12, 13syl112anc 1232 . . . . . . . . . . . . . . 15
158, 14mpbid 210 . . . . . . . . . . . . . 14
16 rexmul 11492 . . . . . . . . . . . . . . 15
179, 11, 16syl2anc 661 . . . . . . . . . . . . . 14
18 rexmul 11492 . . . . . . . . . . . . . . 15
1910, 11, 18syl2anc 661 . . . . . . . . . . . . . 14
2015, 17, 193brtr4d 4482 . . . . . . . . . . . . 13
2120expr 615 . . . . . . . . . . . 12
22 simprl 756 . . . . . . . . . . . . . . 15
23 0re 9617 . . . . . . . . . . . . . . 15
24 lttri4 9690 . . . . . . . . . . . . . . 15
2522, 23, 24sylancl 662 . . . . . . . . . . . . . 14
26 simplll 759 . . . . . . . . . . . . . . . . . . 19
2726adantr 465 . . . . . . . . . . . . . . . . . 18
28 xmulpnf1n 11499 . . . . . . . . . . . . . . . . . 18
2927, 28sylan 471 . . . . . . . . . . . . . . . . 17
30 simpllr 760 . . . . . . . . . . . . . . . . . . . . 21
3130adantr 465 . . . . . . . . . . . . . . . . . . . 20
3231adantr 465 . . . . . . . . . . . . . . . . . . 19
33 pnfxr 11350 . . . . . . . . . . . . . . . . . . 19
34 xmulcl 11494 . . . . . . . . . . . . . . . . . . 19
3532, 33, 34sylancl 662 . . . . . . . . . . . . . . . . . 18
36 mnfle 11371 . . . . . . . . . . . . . . . . . 18
3735, 36syl 16 . . . . . . . . . . . . . . . . 17
3829, 37eqbrtrd 4472 . . . . . . . . . . . . . . . 16
3938ex 434 . . . . . . . . . . . . . . 15
40 oveq1 6303 . . . . . . . . . . . . . . . . . . 19
41 xmul02 11489 . . . . . . . . . . . . . . . . . . . 20
4233, 41ax-mp 5 . . . . . . . . . . . . . . . . . . 19
4340, 42syl6eq 2514 . . . . . . . . . . . . . . . . . 18
4443adantl 466 . . . . . . . . . . . . . . . . 17
45 simplrr 762 . . . . . . . . . . . . . . . . . . . . 21
46 breq1 4455 . . . . . . . . . . . . . . . . . . . . 21
4745, 46syl5ibcom 220 . . . . . . . . . . . . . . . . . . . 20
48 simprr 757 . . . . . . . . . . . . . . . . . . . . 21
49 leloe 9692 . . . . . . . . . . . . . . . . . . . . 21
5023, 48, 49sylancr 663 . . . . . . . . . . . . . . . . . . . 20
5147, 50sylibd 214 . . . . . . . . . . . . . . . . . . 19
5251imp 429 . . . . . . . . . . . . . . . . . 18
53 pnfge 11368 . . . . . . . . . . . . . . . . . . . . 21
541, 53ax-mp 5 . . . . . . . . . . . . . . . . . . . 20
55 xmulpnf1 11495 . . . . . . . . . . . . . . . . . . . . 21
5631, 55sylan 471 . . . . . . . . . . . . . . . . . . . 20
5754, 56syl5breqr 4488 . . . . . . . . . . . . . . . . . . 19
58 xrleid 11385 . . . . . . . . . . . . . . . . . . . . . 22
591, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21
6059, 42breqtrri 4477 . . . . . . . . . . . . . . . . . . . 20
61 simpr 461 . . . . . . . . . . . . . . . . . . . . 21
6261oveq1d 6311 . . . . . . . . . . . . . . . . . . . 20
6360, 62syl5breq 4487 . . . . . . . . . . . . . . . . . . 19
6457, 63jaodan 785 . . . . . . . . . . . . . . . . . 18
6552, 64syldan 470 . . . . . . . . . . . . . . . . 17
6644, 65eqbrtrd 4472 . . . . . . . . . . . . . . . 16
6766ex 434 . . . . . . . . . . . . . . 15
68 pnfge 11368 . . . . . . . . . . . . . . . . . 18
6933, 68ax-mp 5 . . . . . . . . . . . . . . . . 17
7026adantr 465 . . . . . . . . . . . . . . . . . . 19
71 simprr 757 . . . . . . . . . . . . . . . . . . 19
72 xmulpnf1 11495 . . . . . . . . . . . . . . . . . . 19
7370, 71, 72syl2anc 661 . . . . . . . . . . . . . . . . . 18
7430adantr 465 . . . . . . . . . . . . . . . . . . 19
75 ltletr 9697 . . . . . . . . . . . . . . . . . . . . . . 23
7623, 75mp3an1 1311 . . . . . . . . . . . . . . . . . . . . . 22
7776adantl 466 . . . . . . . . . . . . . . . . . . . . 21
7845, 77mpan2d 674 . . . . . . . . . . . . . . . . . . . 20
7978impr 619 . . . . . . . . . . . . . . . . . . 19
8074, 79, 55syl2anc 661 . . . . . . . . . . . . . . . . . 18
8173, 80breq12d 4465 . . . . . . . . . . . . . . . . 17
8269, 81mpbiri 233 . . . . . . . . . . . . . . . 16
8382expr 615 . . . . . . . . . . . . . . 15
8439, 67, 833jaod 1292 . . . . . . . . . . . . . 14
8525, 84mpd 15 . . . . . . . . . . . . 13
86 oveq2 6304 . . . . . . . . . . . . . 14
87 oveq2 6304 . . . . . . . . . . . . . 14
8886, 87breq12d 4465 . . . . . . . . . . . . 13
8985, 88syl5ibrcom 222 . . . . . . . . . . . 12
90 nltmnf 11367 . . . . . . . . . . . . . . . . . 18
911, 90ax-mp 5 . . . . . . . . . . . . . . . . 17
92 breq2 4456 . . . . . . . . . . . . . . . . 17
9391, 92mtbiri 303 . . . . . . . . . . . . . . . 16
9493con2i 120 . . . . . . . . . . . . . . 15
9594ad2antrl 727 . . . . . . . . . . . . . 14
9695adantr 465 . . . . . . . . . . . . 13
9796pm2.21d 106 . . . . . . . . . . . 12
9821, 89, 973jaod 1292 . . . . . . . . . . 11
997, 98mpd 15 . . . . . . . . . 10
10099anassrs 648 . . . . . . . . 9
101 xmulcl 11494 . . . . . . . . . . . . . 14
102101adantlr 714 . . . . . . . . . . . . 13
103102ad2antrr 725 . . . . . . . . . . . 12
104 pnfge 11368 . . . . . . . . . . . 12
105103, 104syl 16 . . . . . . . . . . 11
106 oveq1 6303 . . . . . . . . . . . 12
107 xmulpnf2 11496 . . . . . . . . . . . . 13
108107ad2ant2lr 747 . . . . . . . . . . . 12
109106, 108sylan9eqr 2520 . . . . . . . . . . 11
110105, 109breqtrrd 4478 . . . . . . . . . 10
111110adantlr 714 . . . . . . . . 9
112 simplrr 762 . . . . . . . . . . . . 13
113 simpr 461 . . . . . . . . . . . . . 14
11426adantr 465 . . . . . . . . . . . . . . 15
115 mnfle 11371 . . . . . . . . . . . . . . 15
116114, 115syl 16 . . . . . . . . . . . . . 14
117113, 116eqbrtrd 4472 . . . . . . . . . . . . 13
118 xrletri3 11387 . . . . . . . . . . . . . 14
119118ad3antrrr 729 . . . . . . . . . . . . 13
120112, 117, 119mpbir2and 922 . . . . . . . . . . . 12
121120oveq1d 6311 . . . . . . . . . . 11
122 xmulcl 11494 . . . . . . . . . . . . . 14
123122adantll 713 . . . . . . . . . . . . 13
124123ad2antrr 725 . . . . . . . . . . . 12
125 xrleid 11385 . . . . . . . . . . . 12
126124, 125syl 16 . . . . . . . . . . 11
127121, 126eqbrtrd 4472 . . . . . . . . . 10
128127adantlr 714 . . . . . . . . 9
129 elxr 11354 . . . . . . . . . . 11
13030, 129sylib 196 . . . . . . . . . 10
131130adantr 465 . . . . . . . . 9
132100, 111, 128, 131mpjao3dan 1295 . . . . . . . 8
133 simplrr 762 . . . . . . . . . . 11
13430adantr 465 . . . . . . . . . . . . 13
135 pnfge 11368 . . . . . . . . . . . . 13
136134, 135syl 16 . . . . . . . . . . . 12
137 simpr 461 . . . . . . . . . . . 12
138136, 137breqtrrd 4478 . . . . . . . . . . 11
139118ad3antrrr 729 . . . . . . . . . . 11
140133, 138, 139mpbir2and 922 . . . . . . . . . 10
141140oveq1d 6311 . . . . . . . . 9
142123, 125syl 16 . . . . . . . . . 10
143142ad2antrr 725 . . . . . . . . 9
144141, 143eqbrtrd 4472 . . . . . . . 8
145 oveq1 6303 . . . . . . . . . 10
146 xmulmnf2 11498 . . . . . . . . . . 11
147146ad2ant2lr 747 . . . . . . . . . 10
148145, 147sylan9eqr 2520 . . . . . . . . 9
149123ad2antrr 725 . . . . . . . . . 10
150 mnfle 11371 . . . . . . . . . 10
151149, 150syl 16 . . . . . . . . 9
152148, 151eqbrtrd 4472 . . . . . . . 8
153 elxr 11354 . . . . . . . . 9
15426, 153sylib 196 . . . . . . . 8
155132, 144, 152, 154mpjao3dan 1295 . . . . . . 7
156155exp32 605 . . . . . 6
157 xmul01 11488 . . . . . . . . . . 11
158157ad2antrr 725 . . . . . . . . . 10
159 xmul01 11488 . . . . . . . . . . 11