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

Theorem xadddilem 13222
Description: Lemma for xadddi 13223. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xadddilem (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))

Proof of Theorem xadddilem
StepHypRef Expression
1 simpl1 1192 . . . 4 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ๐ด โˆˆ โ„)
2 recn 11149 . . . . . . . 8 (๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„‚)
3 recn 11149 . . . . . . . 8 (๐ต โˆˆ โ„ โ†’ ๐ต โˆˆ โ„‚)
4 recn 11149 . . . . . . . 8 (๐ถ โˆˆ โ„ โ†’ ๐ถ โˆˆ โ„‚)
5 adddi 11148 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
62, 3, 4, 5syl3an 1161 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
763expa 1119 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
8 readdcl 11142 . . . . . . . 8 ((๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต + ๐ถ) โˆˆ โ„)
9 rexmul 13199 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง (๐ต + ๐ถ) โˆˆ โ„) โ†’ (๐ด ยทe (๐ต + ๐ถ)) = (๐ด ยท (๐ต + ๐ถ)))
108, 9sylan2 594 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„)) โ†’ (๐ด ยทe (๐ต + ๐ถ)) = (๐ด ยท (๐ต + ๐ถ)))
1110anassrs 469 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต + ๐ถ)) = (๐ด ยท (๐ต + ๐ถ)))
12 remulcl 11144 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยท ๐ต) โˆˆ โ„)
1312adantr 482 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท ๐ต) โˆˆ โ„)
14 remulcl 11144 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท ๐ถ) โˆˆ โ„)
1514adantlr 714 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท ๐ถ) โˆˆ โ„)
1613, 15rexaddd 13162 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยท ๐ต) +๐‘’ (๐ด ยท ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
177, 11, 163eqtr4d 2783 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) +๐‘’ (๐ด ยท ๐ถ)))
18 rexadd 13160 . . . . . . 7 ((๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต +๐‘’ ๐ถ) = (๐ต + ๐ถ))
1918adantll 713 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต +๐‘’ ๐ถ) = (๐ต + ๐ถ))
2019oveq2d 7377 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe (๐ต + ๐ถ)))
21 rexmul 13199 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต))
2221adantr 482 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต))
23 rexmul 13199 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) = (๐ด ยท ๐ถ))
2423adantlr 714 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) = (๐ด ยท ๐ถ))
2522, 24oveq12d 7379 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยท ๐ต) +๐‘’ (๐ด ยท ๐ถ)))
2617, 20, 253eqtr4d 2783 . . . 4 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
271, 26sylanl1 679 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
28 rexr 11209 . . . . . . . . 9 (๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„*)
29283ad2ant1 1134 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โ†’ ๐ด โˆˆ โ„*)
30 xmulpnf1 13202 . . . . . . . 8 ((๐ด โˆˆ โ„* โˆง 0 < ๐ด) โ†’ (๐ด ยทe +โˆž) = +โˆž)
3129, 30sylan 581 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe +โˆž) = +โˆž)
3231adantr 482 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe +โˆž) = +โˆž)
3321, 12eqeltrd 2834 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) โˆˆ โ„)
341, 33sylan 581 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) โˆˆ โ„)
35 rexr 11209 . . . . . . . 8 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ (๐ด ยทe ๐ต) โˆˆ โ„*)
36 renemnf 11212 . . . . . . . 8 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ (๐ด ยทe ๐ต) โ‰  -โˆž)
37 xaddpnf1 13154 . . . . . . . 8 (((๐ด ยทe ๐ต) โˆˆ โ„* โˆง (๐ด ยทe ๐ต) โ‰  -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ +โˆž) = +โˆž)
3835, 36, 37syl2anc 585 . . . . . . 7 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ ((๐ด ยทe ๐ต) +๐‘’ +โˆž) = +โˆž)
3934, 38syl 17 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ ((๐ด ยทe ๐ต) +๐‘’ +โˆž) = +โˆž)
4032, 39eqtr4d 2776 . . . . 5 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe +โˆž) = ((๐ด ยทe ๐ต) +๐‘’ +โˆž))
4140adantr 482 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe +โˆž) = ((๐ด ยทe ๐ต) +๐‘’ +โˆž))
42 oveq2 7369 . . . . . 6 (๐ถ = +โˆž โ†’ (๐ต +๐‘’ ๐ถ) = (๐ต +๐‘’ +โˆž))
43 rexr 11209 . . . . . . . 8 (๐ต โˆˆ โ„ โ†’ ๐ต โˆˆ โ„*)
44 renemnf 11212 . . . . . . . 8 (๐ต โˆˆ โ„ โ†’ ๐ต โ‰  -โˆž)
45 xaddpnf1 13154 . . . . . . . 8 ((๐ต โˆˆ โ„* โˆง ๐ต โ‰  -โˆž) โ†’ (๐ต +๐‘’ +โˆž) = +โˆž)
4643, 44, 45syl2anc 585 . . . . . . 7 (๐ต โˆˆ โ„ โ†’ (๐ต +๐‘’ +โˆž) = +โˆž)
4746adantl 483 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ต +๐‘’ +โˆž) = +โˆž)
4842, 47sylan9eqr 2795 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = +โˆž)
4948oveq2d 7377 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe +โˆž))
50 oveq2 7369 . . . . . 6 (๐ถ = +โˆž โ†’ (๐ด ยทe ๐ถ) = (๐ด ยทe +โˆž))
5150, 32sylan9eqr 2795 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe ๐ถ) = +โˆž)
5251oveq2d 7377 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ +โˆž))
5341, 49, 523eqtr4d 2783 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
54 xmulmnf1 13204 . . . . . . . 8 ((๐ด โˆˆ โ„* โˆง 0 < ๐ด) โ†’ (๐ด ยทe -โˆž) = -โˆž)
5529, 54sylan 581 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe -โˆž) = -โˆž)
5655adantr 482 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe -โˆž) = -โˆž)
5756adantr 482 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe -โˆž) = -โˆž)
5834adantr 482 . . . . . 6 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe ๐ต) โˆˆ โ„)
59 renepnf 11211 . . . . . . 7 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ (๐ด ยทe ๐ต) โ‰  +โˆž)
60 xaddmnf1 13156 . . . . . . 7 (((๐ด ยทe ๐ต) โˆˆ โ„* โˆง (๐ด ยทe ๐ต) โ‰  +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ -โˆž) = -โˆž)
6135, 59, 60syl2anc 585 . . . . . 6 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ ((๐ด ยทe ๐ต) +๐‘’ -โˆž) = -โˆž)
6258, 61syl 17 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ -โˆž) = -โˆž)
6357, 62eqtr4d 2776 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe -โˆž) = ((๐ด ยทe ๐ต) +๐‘’ -โˆž))
64 oveq2 7369 . . . . . 6 (๐ถ = -โˆž โ†’ (๐ต +๐‘’ ๐ถ) = (๐ต +๐‘’ -โˆž))
65 renepnf 11211 . . . . . . . 8 (๐ต โˆˆ โ„ โ†’ ๐ต โ‰  +โˆž)
66 xaddmnf1 13156 . . . . . . . 8 ((๐ต โˆˆ โ„* โˆง ๐ต โ‰  +โˆž) โ†’ (๐ต +๐‘’ -โˆž) = -โˆž)
6743, 65, 66syl2anc 585 . . . . . . 7 (๐ต โˆˆ โ„ โ†’ (๐ต +๐‘’ -โˆž) = -โˆž)
6867adantl 483 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ต +๐‘’ -โˆž) = -โˆž)
6964, 68sylan9eqr 2795 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = -โˆž)
7069oveq2d 7377 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe -โˆž))
71 oveq2 7369 . . . . . 6 (๐ถ = -โˆž โ†’ (๐ด ยทe ๐ถ) = (๐ด ยทe -โˆž))
7271, 56sylan9eqr 2795 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe ๐ถ) = -โˆž)
7372oveq2d 7377 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ -โˆž))
7463, 70, 733eqtr4d 2783 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
75 simpl3 1194 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ๐ถ โˆˆ โ„*)
76 elxr 13045 . . . . 5 (๐ถ โˆˆ โ„* โ†” (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
7775, 76sylib 217 . . . 4 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
7877adantr 482 . . 3 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
7927, 53, 74, 78mpjao3dan 1432 . 2 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
8031ad2antrr 725 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe +โˆž) = +โˆž)
811adantr 482 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ ๐ด โˆˆ โ„)
8223, 14eqeltrd 2834 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) โˆˆ โ„)
8381, 82sylan 581 . . . . . 6 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) โˆˆ โ„)
84 rexr 11209 . . . . . . 7 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (๐ด ยทe ๐ถ) โˆˆ โ„*)
85 renemnf 11212 . . . . . . 7 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (๐ด ยทe ๐ถ) โ‰  -โˆž)
86 xaddpnf2 13155 . . . . . . 7 (((๐ด ยทe ๐ถ) โˆˆ โ„* โˆง (๐ด ยทe ๐ถ) โ‰  -โˆž) โ†’ (+โˆž +๐‘’ (๐ด ยทe ๐ถ)) = +โˆž)
8784, 85, 86syl2anc 585 . . . . . 6 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (+โˆž +๐‘’ (๐ด ยทe ๐ถ)) = +โˆž)
8883, 87syl 17 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (+โˆž +๐‘’ (๐ด ยทe ๐ถ)) = +โˆž)
8980, 88eqtr4d 2776 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe +โˆž) = (+โˆž +๐‘’ (๐ด ยทe ๐ถ)))
90 simpr 486 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ ๐ต = +โˆž)
9190oveq1d 7376 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (+โˆž +๐‘’ ๐ถ))
92 rexr 11209 . . . . . . 7 (๐ถ โˆˆ โ„ โ†’ ๐ถ โˆˆ โ„*)
93 renemnf 11212 . . . . . . 7 (๐ถ โˆˆ โ„ โ†’ ๐ถ โ‰  -โˆž)
94 xaddpnf2 13155 . . . . . . 7 ((๐ถ โˆˆ โ„* โˆง ๐ถ โ‰  -โˆž) โ†’ (+โˆž +๐‘’ ๐ถ) = +โˆž)
9592, 93, 94syl2anc 585 . . . . . 6 (๐ถ โˆˆ โ„ โ†’ (+โˆž +๐‘’ ๐ถ) = +โˆž)
9691, 95sylan9eq 2793 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต +๐‘’ ๐ถ) = +โˆž)
9796oveq2d 7377 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe +โˆž))
98 oveq2 7369 . . . . . . 7 (๐ต = +โˆž โ†’ (๐ด ยทe ๐ต) = (๐ด ยทe +โˆž))
9998, 31sylan9eqr 2795 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ (๐ด ยทe ๐ต) = +โˆž)
10099adantr 482 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) = +โˆž)
101100oveq1d 7376 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = (+โˆž +๐‘’ (๐ด ยทe ๐ถ)))
10289, 97, 1013eqtr4d 2783 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
103 pnfxr 11217 . . . . . . 7 +โˆž โˆˆ โ„*
104 pnfnemnf 11218 . . . . . . 7 +โˆž โ‰  -โˆž
105 xaddpnf1 13154 . . . . . . 7 ((+โˆž โˆˆ โ„* โˆง +โˆž โ‰  -โˆž) โ†’ (+โˆž +๐‘’ +โˆž) = +โˆž)
106103, 104, 105mp2an 691 . . . . . 6 (+โˆž +๐‘’ +โˆž) = +โˆž
10731, 31oveq12d 7379 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)) = (+โˆž +๐‘’ +โˆž))
108106, 107, 313eqtr4a 2799 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)) = (๐ด ยทe +โˆž))
109108ad2antrr 725 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)) = (๐ด ยทe +โˆž))
11098, 50oveqan12d 7380 . . . . 5 ((๐ต = +โˆž โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)))
111110adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)))
112 oveq12 7370 . . . . . . 7 ((๐ต = +โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (+โˆž +๐‘’ +โˆž))
113112, 106eqtrdi 2789 . . . . . 6 ((๐ต = +โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = +โˆž)
114113oveq2d 7377 . . . . 5 ((๐ต = +โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe +โˆž))
115114adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe +โˆž))
116109, 111, 1153eqtr4rd 2784 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
117 pnfaddmnf 13158 . . . . . 6 (+โˆž +๐‘’ -โˆž) = 0
11831, 55oveq12d 7379 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (+โˆž +๐‘’ -โˆž))
119 xmul01 13195 . . . . . . 7 (๐ด โˆˆ โ„* โ†’ (๐ด ยทe 0) = 0)
1201, 28, 1193syl 18 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe 0) = 0)
121117, 118, 1203eqtr4a 2799 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (๐ด ยทe 0))
122121ad2antrr 725 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (๐ด ยทe 0))
12398, 71oveqan12d 7380 . . . . 5 ((๐ต = +โˆž โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)))
124123adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)))
125 oveq12 7370 . . . . . . 7 ((๐ต = +โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (+โˆž +๐‘’ -โˆž))
126125, 117eqtrdi 2789 . . . . . 6 ((๐ต = +โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = 0)
127126oveq2d 7377 . . . . 5 ((๐ต = +โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe 0))
128127adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe 0))
129122, 124, 1283eqtr4rd 2784 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
13077adantr 482 . . 3 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
131102, 116, 129, 130mpjao3dan 1432 . 2 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
13255ad2antrr 725 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe -โˆž) = -โˆž)
1331adantr 482 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ ๐ด โˆˆ โ„)
134133, 82sylan 581 . . . . . 6 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) โˆˆ โ„)
135 renepnf 11211 . . . . . . 7 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (๐ด ยทe ๐ถ) โ‰  +โˆž)
136 xaddmnf2 13157 . . . . . . 7 (((๐ด ยทe ๐ถ) โˆˆ โ„* โˆง (๐ด ยทe ๐ถ) โ‰  +โˆž) โ†’ (-โˆž +๐‘’ (๐ด ยทe ๐ถ)) = -โˆž)
13784, 135, 136syl2anc 585 . . . . . 6 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (-โˆž +๐‘’ (๐ด ยทe ๐ถ)) = -โˆž)
138134, 137syl 17 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (-โˆž +๐‘’ (๐ด ยทe ๐ถ)) = -โˆž)
139132, 138eqtr4d 2776 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe -โˆž) = (-โˆž +๐‘’ (๐ด ยทe ๐ถ)))
140 simpr 486 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ ๐ต = -โˆž)
141140oveq1d 7376 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (-โˆž +๐‘’ ๐ถ))
142 renepnf 11211 . . . . . . 7 (๐ถ โˆˆ โ„ โ†’ ๐ถ โ‰  +โˆž)
143 xaddmnf2 13157 . . . . . . 7 ((๐ถ โˆˆ โ„* โˆง ๐ถ โ‰  +โˆž) โ†’ (-โˆž +๐‘’ ๐ถ) = -โˆž)
14492, 142, 143syl2anc 585 . . . . . 6 (๐ถ โˆˆ โ„ โ†’ (-โˆž +๐‘’ ๐ถ) = -โˆž)
145141, 144sylan9eq 2793 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต +๐‘’ ๐ถ) = -โˆž)
146145oveq2d 7377 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe -โˆž))
147 oveq2 7369 . . . . . . 7 (๐ต = -โˆž โ†’ (๐ด ยทe ๐ต) = (๐ด ยทe -โˆž))
148147, 55sylan9eqr 2795 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ (๐ด ยทe ๐ต) = -โˆž)
149148adantr 482 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) = -โˆž)
150149oveq1d 7376 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = (-โˆž +๐‘’ (๐ด ยทe ๐ถ)))
151139, 146, 1503eqtr4d 2783 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
15255, 31oveq12d 7379 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)) = (-โˆž +๐‘’ +โˆž))
153 mnfaddpnf 13159 . . . . . . 7 (-โˆž +๐‘’ +โˆž) = 0
154152, 153eqtrdi 2789 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)) = 0)
155120, 154eqtr4d 2776 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe 0) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)))
156155ad2antrr 725 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe 0) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)))
157 oveq12 7370 . . . . . . 7 ((๐ต = -โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (-โˆž +๐‘’ +โˆž))
158157, 153eqtrdi 2789 . . . . . 6 ((๐ต = -โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = 0)
159158oveq2d 7377 . . . . 5 ((๐ต = -โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe 0))
160159adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe 0))
161147, 50oveqan12d 7380 . . . . 5 ((๐ต = -โˆž โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)))
162161adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)))
163156, 160, 1623eqtr4d 2783 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
164 mnfxr 11220 . . . . . . 7 -โˆž โˆˆ โ„*
165 mnfnepnf 11219 . . . . . . 7 -โˆž โ‰  +โˆž
166 xaddmnf1 13156 . . . . . . 7 ((-โˆž โˆˆ โ„* โˆง -โˆž โ‰  +โˆž) โ†’ (-โˆž +๐‘’ -โˆž) = -โˆž)
167164, 165, 166mp2an 691 . . . . . 6 (-โˆž +๐‘’ -โˆž) = -โˆž
16855, 55oveq12d 7379 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (-โˆž +๐‘’ -โˆž))
169167, 168, 553eqtr4a 2799 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (๐ด ยทe -โˆž))
170169ad2antrr 725 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (๐ด ยทe -โˆž))
171147, 71oveqan12d 7380 . . . . 5 ((๐ต = -โˆž โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)))
172171adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)))
173 oveq12 7370 . . . . . . 7 ((๐ต = -โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (-โˆž +๐‘’ -โˆž))
174173, 167eqtrdi 2789 . . . . . 6 ((๐ต = -โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = -โˆž)
175174oveq2d 7377 . . . . 5 ((๐ต = -โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe -โˆž))
176175adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe -โˆž))
177170, 172, 1763eqtr4rd 2784 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
17877adantr 482 . . 3 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
179151, 163, 177, 178mpjao3dan 1432 . 2 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
180 simpl2 1193 . . 3 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ๐ต โˆˆ โ„*)
181 elxr 13045 . . 3 (๐ต โˆˆ โ„* โ†” (๐ต โˆˆ โ„ โˆจ ๐ต = +โˆž โˆจ ๐ต = -โˆž))
182180, 181sylib 217 . 2 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ต โˆˆ โ„ โˆจ ๐ต = +โˆž โˆจ ๐ต = -โˆž))
18379, 131, 179, 182mpjao3dan 1432 1 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   โˆจ w3o 1087   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940   class class class wbr 5109  (class class class)co 7361  โ„‚cc 11057  โ„cr 11058  0cc0 11059   + caddc 11062   ยท cmul 11064  +โˆžcpnf 11194  -โˆžcmnf 11195  โ„*cxr 11196   < clt 11197   +๐‘’ cxad 13039   ยทe cxmu 13040
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-po 5549  df-so 5550  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8654  df-en 8890  df-dom 8891  df-sdom 8892  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-xneg 13041  df-xadd 13042  df-xmul 13043
This theorem is referenced by:  xadddi  13223
  Copyright terms: Public domain W3C validator