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

Theorem xmulneg1 11490
Description: Extended real version of mulneg1 10018. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xmulneg1

Proof of Theorem xmulneg1
StepHypRef Expression
1 xneg0 11440 . . . . . . . . 9
21eqeq2i 2475 . . . . . . . 8
3 0xr 9661 . . . . . . . . 9
4 xneg11 11443 . . . . . . . . 9
53, 4mpan2 671 . . . . . . . 8
62, 5syl5bbr 259 . . . . . . 7
76adantr 465 . . . . . 6
87orbi1d 702 . . . . 5
98ifbid 3963 . . . 4
10 xnegpnf 11437 . . . . . . . . . . . . . 14
1110eqeq2i 2475 . . . . . . . . . . . . 13
12 simpll 753 . . . . . . . . . . . . . 14
13 pnfxr 11350 . . . . . . . . . . . . . 14
14 xneg11 11443 . . . . . . . . . . . . . 14
1512, 13, 14sylancl 662 . . . . . . . . . . . . 13
1611, 15syl5bbr 259 . . . . . . . . . . . 12
1716anbi2d 703 . . . . . . . . . . 11
18 xnegmnf 11438 . . . . . . . . . . . . . 14
1918eqeq2i 2475 . . . . . . . . . . . . 13
20 mnfxr 11352 . . . . . . . . . . . . . 14
21 xneg11 11443 . . . . . . . . . . . . . 14
2212, 20, 21sylancl 662 . . . . . . . . . . . . 13
2319, 22syl5bbr 259 . . . . . . . . . . . 12
2423anbi2d 703 . . . . . . . . . . 11
2517, 24orbi12d 709 . . . . . . . . . 10
26 xlt0neg1 11447 . . . . . . . . . . . . . . 15
2726ad2antrr 725 . . . . . . . . . . . . . 14
2827bicomd 201 . . . . . . . . . . . . 13
2928anbi1d 704 . . . . . . . . . . . 12
30 xlt0neg2 11448 . . . . . . . . . . . . . . 15
3130ad2antrr 725 . . . . . . . . . . . . . 14
3231bicomd 201 . . . . . . . . . . . . 13
3332anbi1d 704 . . . . . . . . . . . 12
3429, 33orbi12d 709 . . . . . . . . . . 11
35 orcom 387 . . . . . . . . . . 11
3634, 35syl6bb 261 . . . . . . . . . 10
3725, 36orbi12d 709 . . . . . . . . 9
3837biimpar 485 . . . . . . . 8
3938iftrued 3949 . . . . . . 7
40 xmullem2 11486 . . . . . . . . . . 11
4140adantr 465 . . . . . . . . . 10
4223anbi2d 703 . . . . . . . . . . . . 13
4316anbi2d 703 . . . . . . . . . . . . 13
4442, 43orbi12d 709 . . . . . . . . . . . 12
4528anbi1d 704 . . . . . . . . . . . . . 14
4632anbi1d 704 . . . . . . . . . . . . . 14
4745, 46orbi12d 709 . . . . . . . . . . . . 13
48 orcom 387 . . . . . . . . . . . . 13
4947, 48syl6bb 261 . . . . . . . . . . . 12
5044, 49orbi12d 709 . . . . . . . . . . 11
5150notbid 294 . . . . . . . . . 10
5241, 51sylibrd 234 . . . . . . . . 9
5352imp 429 . . . . . . . 8
5453iffalsed 3952 . . . . . . 7
55 iftrue 3947 . . . . . . . . . 10
5655adantl 466 . . . . . . . . 9
57 xnegeq 11435 . . . . . . . . 9
5856, 57syl 16 . . . . . . . 8
5958, 10syl6eq 2514 . . . . . . 7
6039, 54, 593eqtr4d 2508 . . . . . 6
6150biimpar 485 . . . . . . . . . 10
6261iftrued 3949 . . . . . . . . 9
6341con2d 115 . . . . . . . . . . . . . 14
6463imp 429 . . . . . . . . . . . . 13
6564iffalsed 3952 . . . . . . . . . . . 12
66 iftrue 3947 . . . . . . . . . . . . 13
6766adantl 466 . . . . . . . . . . . 12
6865, 67eqtrd 2498 . . . . . . . . . . 11
69 xnegeq 11435 . . . . . . . . . . 11
7068, 69syl 16 . . . . . . . . . 10
7170, 18syl6eq 2514 . . . . . . . . 9
7262, 71eqtr4d 2501 . . . . . . . 8
7372adantlr 714 . . . . . . 7