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

Theorem xadddilem 11515
Description: Lemma for xadddi 11516. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xadddilem

Proof of Theorem xadddilem
StepHypRef Expression
1 simpl1 999 . . . 4
2 recn 9603 . . . . . . . 8
3 recn 9603 . . . . . . . 8
4 recn 9603 . . . . . . . 8
5 adddi 9602 . . . . . . . 8
62, 3, 4, 5syl3an 1270 . . . . . . 7
763expa 1196 . . . . . 6
8 readdcl 9596 . . . . . . . 8
9 rexmul 11492 . . . . . . . 8
108, 9sylan2 474 . . . . . . 7
1110anassrs 648 . . . . . 6
12 remulcl 9598 . . . . . . . 8
1312adantr 465 . . . . . . 7
14 remulcl 9598 . . . . . . . 8
1514adantlr 714 . . . . . . 7
16 rexadd 11460 . . . . . . 7
1713, 15, 16syl2anc 661 . . . . . 6
187, 11, 173eqtr4d 2508 . . . . 5
19 rexadd 11460 . . . . . . 7
2019adantll 713 . . . . . 6
2120oveq2d 6312 . . . . 5
22 rexmul 11492 . . . . . . 7
2322adantr 465 . . . . . 6
24 rexmul 11492 . . . . . . 7
2524adantlr 714 . . . . . 6
2623, 25oveq12d 6314 . . . . 5
2718, 21, 263eqtr4d 2508 . . . 4
281, 27sylanl1 650 . . 3
29 rexr 9660 . . . . . . . . 9
30293ad2ant1 1017 . . . . . . . 8
31 xmulpnf1 11495 . . . . . . . 8
3230, 31sylan 471 . . . . . . 7
3332adantr 465 . . . . . 6
3422, 12eqeltrd 2545 . . . . . . . 8
351, 34sylan 471 . . . . . . 7
36 rexr 9660 . . . . . . . 8
37 renemnf 9663 . . . . . . . 8
38 xaddpnf1 11454 . . . . . . . 8
3936, 37, 38syl2anc 661 . . . . . . 7
4035, 39syl 16 . . . . . 6
4133, 40eqtr4d 2501 . . . . 5
4241adantr 465 . . . 4
43 oveq2 6304 . . . . . 6
44 rexr 9660 . . . . . . . 8
45 renemnf 9663 . . . . . . . 8
46 xaddpnf1 11454 . . . . . . . 8
4744, 45, 46syl2anc 661 . . . . . . 7
4847adantl 466 . . . . . 6
4943, 48sylan9eqr 2520 . . . . 5
5049oveq2d 6312 . . . 4
51 oveq2 6304 . . . . . 6
5251, 33sylan9eqr 2520 . . . . 5
5352oveq2d 6312 . . . 4
5442, 50, 533eqtr4d 2508 . . 3
55 xmulmnf1 11497 . . . . . . . 8
5630, 55sylan 471 . . . . . . 7
5756adantr 465 . . . . . 6
5857adantr 465 . . . . 5
5935adantr 465 . . . . . 6
60 renepnf 9662 . . . . . . 7
61 xaddmnf1 11456 . . . . . . 7
6236, 60, 61syl2anc 661 . . . . . 6
6359, 62syl 16 . . . . 5
6458, 63eqtr4d 2501 . . . 4
65 oveq2 6304 . . . . . 6
66 renepnf 9662 . . . . . . . 8
67 xaddmnf1 11456 . . . . . . . 8
6844, 66, 67syl2anc 661 . . . . . . 7
6968adantl 466 . . . . . 6
7065, 69sylan9eqr 2520 . . . . 5
7170oveq2d 6312 . . . 4
72 oveq2 6304 . . . . . 6
7372, 57sylan9eqr 2520 . . . . 5
7473oveq2d 6312 . . . 4
7564, 71, 743eqtr4d 2508 . . 3
76 simpl3 1001 . . . . 5
77 elxr 11354 . . . . 5
7876, 77sylib 196 . . . 4
7978adantr 465 . . 3
8028, 54, 75, 79mpjao3dan 1295 . 2
8132ad2antrr 725 . . . . 5
821adantr 465 . . . . . . 7
8324, 14eqeltrd 2545 . . . . . . 7
8482, 83sylan 471 . . . . . 6
85 rexr 9660 . . . . . . 7
86 renemnf 9663 . . . . . . 7
87 xaddpnf2 11455 . . . . . . 7
8885, 86, 87syl2anc 661 . . . . . 6
8984, 88syl 16 . . . . 5
9081, 89eqtr4d 2501 . . . 4
91 simpr 461 . . . . . . 7
9291oveq1d 6311 . . . . . 6
93 rexr 9660 . . . . . . 7
94 renemnf 9663 . . . . . . 7
95 xaddpnf2 11455 . . . . . . 7
9693, 94, 95syl2anc 661 . . . . . 6
9792, 96sylan9eq 2518 . . . . 5
9897oveq2d 6312 . . . 4
99 oveq2 6304 . . . . . . 7
10099, 32sylan9eqr 2520 . . . . . 6
101100adantr 465 . . . . 5
102101oveq1d 6311 . . . 4
10390, 98, 1023eqtr4d 2508 . . 3
104 pnfxr 11350 . . . . . . 7
105 pnfnemnf 11355 . . . . . . 7
106 xaddpnf1 11454 . . . . . . 7
107104, 105, 106mp2an 672 . . . . . 6
10832, 32oveq12d 6314 . . . . . 6
109107, 108, 323eqtr4a 2524 . . . . 5
110109ad2antrr 725 . . . 4
11199, 51oveqan12d 6315 . . . . 5
112111adantll 713 . . . 4
113 oveq12 6305 . . . . . . 7
114113, 107syl6eq 2514 . . . . . 6
115114oveq2d 6312 . . . . 5
116115adantll 713 . . . 4
117110, 112, 1163eqtr4rd 2509 . . 3
118 pnfaddmnf 11458 . . . . . 6
11932, 56oveq12d 6314 . . . . . 6
120 xmul01 11488 . . . . . . 7
1211, 29, 1203syl 20 . . . . . 6
122118, 119, 1213eqtr4a 2524 . . . . 5
123122ad2antrr 725 . . . 4
12499, 72oveqan12d 6315 . . . . 5
125124adantll 713 . . . 4
126 oveq12 6305 . . . . . . 7
127126, 118syl6eq 2514 . . . . . 6
128127oveq2d 6312 . . . . 5
129128adantll 713 . . . 4
130123, 125, 1293eqtr4rd 2509 . . 3
13178adantr 465 . . 3
132103, 117, 130, 131mpjao3dan 1295 . 2
13356ad2antrr 725 . . . . 5
1341adantr 465 . . . . . . 7
135134, 83sylan 471 . . . . . 6
136 renepnf 9662 . . . . . . 7
137 xaddmnf2 11457 . . . . . . 7
13885, 136, 137syl2anc 661 . . . . . 6
139135, 138syl 16 . . . . 5
140133, 139eqtr4d 2501 . . . 4
141 simpr 461 . . . . . . 7
142141oveq1d 6311 . . . . . 6
143 renepnf 9662 . . . . . . 7
144 xaddmnf2 11457 . . . . . . 7
14593, 143, 144syl2anc 661 . . . . . 6
146142, 145sylan9eq 2518 . . . . 5
147146oveq2d 6312 . . . 4
148 oveq2 6304 . . . . . . 7
149148, 56sylan9eqr 2520 . . . . . 6
150149adantr 465 . . . . 5
151150oveq1d 6311 . . . 4
152140, 147, 1513eqtr4d 2508 . . 3
15356, 32oveq12d 6314 . . . . . . 7
154 mnfaddpnf 11459 . . . . . . 7
155153, 154syl6eq 2514 . . . . . 6
156121, 155eqtr4d 2501 . . . . 5
157156ad2antrr 725 . . . 4
158 oveq12 6305 . . . . . . 7
159158, 154syl6eq 2514 . . . . . 6
160159oveq2d 6312 . . . . 5
161160adantll 713 . . . 4
162148, 51oveqan12d 6315 . . . . 5
163162adantll 713 . . . 4
164157, 161, 1633eqtr4d 2508 . . 3
165 mnfxr 11352 . . . . . . 7
166 mnfnepnf 11356 . . . . . . 7
167 xaddmnf1 11456 . . . . . . 7
168165, 166, 167mp2an 672 . . . . . 6
16956, 56oveq12d 6314 . . . . . 6
170168, 169, 563eqtr4a 2524 . . . . 5
171170ad2antrr 725 . . . 4
172148, 72oveqan12d 6315 . . . . 5
173172adantll 713 . . . 4
174 oveq12 6305 . . . . . . 7
175174, 168syl6eq 2514 . . . . . 6
176175oveq2d 6312 . . . . 5
177176adantll 713 . . . 4
178171, 173, 1773eqtr4rd 2509 . . 3
17978adantr 465 . . 3
180152, 164, 178, 179mpjao3dan 1295 . 2
181 simpl2 1000 . . 3