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

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

Proof of Theorem xadddilem
StepHypRef Expression
1 simpl1 1189 . . . 4 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ๐ด โˆˆ โ„)
2 recn 11229 . . . . . . . 8 (๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„‚)
3 recn 11229 . . . . . . . 8 (๐ต โˆˆ โ„ โ†’ ๐ต โˆˆ โ„‚)
4 recn 11229 . . . . . . . 8 (๐ถ โˆˆ โ„ โ†’ ๐ถ โˆˆ โ„‚)
5 adddi 11228 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
62, 3, 4, 5syl3an 1158 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
763expa 1116 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
8 readdcl 11222 . . . . . . . 8 ((๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต + ๐ถ) โˆˆ โ„)
9 rexmul 13283 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง (๐ต + ๐ถ) โˆˆ โ„) โ†’ (๐ด ยทe (๐ต + ๐ถ)) = (๐ด ยท (๐ต + ๐ถ)))
108, 9sylan2 592 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„)) โ†’ (๐ด ยทe (๐ต + ๐ถ)) = (๐ด ยท (๐ต + ๐ถ)))
1110anassrs 467 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต + ๐ถ)) = (๐ด ยท (๐ต + ๐ถ)))
12 remulcl 11224 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยท ๐ต) โˆˆ โ„)
1312adantr 480 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท ๐ต) โˆˆ โ„)
14 remulcl 11224 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท ๐ถ) โˆˆ โ„)
1514adantlr 714 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท ๐ถ) โˆˆ โ„)
1613, 15rexaddd 13246 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยท ๐ต) +๐‘’ (๐ด ยท ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
177, 11, 163eqtr4d 2778 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) +๐‘’ (๐ด ยท ๐ถ)))
18 rexadd 13244 . . . . . . 7 ((๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต +๐‘’ ๐ถ) = (๐ต + ๐ถ))
1918adantll 713 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต +๐‘’ ๐ถ) = (๐ต + ๐ถ))
2019oveq2d 7436 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe (๐ต + ๐ถ)))
21 rexmul 13283 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต))
2221adantr 480 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต))
23 rexmul 13283 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) = (๐ด ยท ๐ถ))
2423adantlr 714 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) = (๐ด ยท ๐ถ))
2522, 24oveq12d 7438 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยท ๐ต) +๐‘’ (๐ด ยท ๐ถ)))
2617, 20, 253eqtr4d 2778 . . . 4 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
271, 26sylanl1 679 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
28 rexr 11291 . . . . . . . . 9 (๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„*)
29283ad2ant1 1131 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โ†’ ๐ด โˆˆ โ„*)
30 xmulpnf1 13286 . . . . . . . 8 ((๐ด โˆˆ โ„* โˆง 0 < ๐ด) โ†’ (๐ด ยทe +โˆž) = +โˆž)
3129, 30sylan 579 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe +โˆž) = +โˆž)
3231adantr 480 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe +โˆž) = +โˆž)
3321, 12eqeltrd 2829 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) โˆˆ โ„)
341, 33sylan 579 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) โˆˆ โ„)
35 rexr 11291 . . . . . . . 8 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ (๐ด ยทe ๐ต) โˆˆ โ„*)
36 renemnf 11294 . . . . . . . 8 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ (๐ด ยทe ๐ต) โ‰  -โˆž)
37 xaddpnf1 13238 . . . . . . . 8 (((๐ด ยทe ๐ต) โˆˆ โ„* โˆง (๐ด ยทe ๐ต) โ‰  -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ +โˆž) = +โˆž)
3835, 36, 37syl2anc 583 . . . . . . 7 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ ((๐ด ยทe ๐ต) +๐‘’ +โˆž) = +โˆž)
3934, 38syl 17 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ ((๐ด ยทe ๐ต) +๐‘’ +โˆž) = +โˆž)
4032, 39eqtr4d 2771 . . . . 5 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe +โˆž) = ((๐ด ยทe ๐ต) +๐‘’ +โˆž))
4140adantr 480 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe +โˆž) = ((๐ด ยทe ๐ต) +๐‘’ +โˆž))
42 oveq2 7428 . . . . . 6 (๐ถ = +โˆž โ†’ (๐ต +๐‘’ ๐ถ) = (๐ต +๐‘’ +โˆž))
43 rexr 11291 . . . . . . . 8 (๐ต โˆˆ โ„ โ†’ ๐ต โˆˆ โ„*)
44 renemnf 11294 . . . . . . . 8 (๐ต โˆˆ โ„ โ†’ ๐ต โ‰  -โˆž)
45 xaddpnf1 13238 . . . . . . . 8 ((๐ต โˆˆ โ„* โˆง ๐ต โ‰  -โˆž) โ†’ (๐ต +๐‘’ +โˆž) = +โˆž)
4643, 44, 45syl2anc 583 . . . . . . 7 (๐ต โˆˆ โ„ โ†’ (๐ต +๐‘’ +โˆž) = +โˆž)
4746adantl 481 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ต +๐‘’ +โˆž) = +โˆž)
4842, 47sylan9eqr 2790 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = +โˆž)
4948oveq2d 7436 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe +โˆž))
50 oveq2 7428 . . . . . 6 (๐ถ = +โˆž โ†’ (๐ด ยทe ๐ถ) = (๐ด ยทe +โˆž))
5150, 32sylan9eqr 2790 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe ๐ถ) = +โˆž)
5251oveq2d 7436 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ +โˆž))
5341, 49, 523eqtr4d 2778 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
54 xmulmnf1 13288 . . . . . . . 8 ((๐ด โˆˆ โ„* โˆง 0 < ๐ด) โ†’ (๐ด ยทe -โˆž) = -โˆž)
5529, 54sylan 579 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe -โˆž) = -โˆž)
5655adantr 480 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe -โˆž) = -โˆž)
5756adantr 480 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe -โˆž) = -โˆž)
5834adantr 480 . . . . . 6 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe ๐ต) โˆˆ โ„)
59 renepnf 11293 . . . . . . 7 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ (๐ด ยทe ๐ต) โ‰  +โˆž)
60 xaddmnf1 13240 . . . . . . 7 (((๐ด ยทe ๐ต) โˆˆ โ„* โˆง (๐ด ยทe ๐ต) โ‰  +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ -โˆž) = -โˆž)
6135, 59, 60syl2anc 583 . . . . . 6 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ ((๐ด ยทe ๐ต) +๐‘’ -โˆž) = -โˆž)
6258, 61syl 17 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ -โˆž) = -โˆž)
6357, 62eqtr4d 2771 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe -โˆž) = ((๐ด ยทe ๐ต) +๐‘’ -โˆž))
64 oveq2 7428 . . . . . 6 (๐ถ = -โˆž โ†’ (๐ต +๐‘’ ๐ถ) = (๐ต +๐‘’ -โˆž))
65 renepnf 11293 . . . . . . . 8 (๐ต โˆˆ โ„ โ†’ ๐ต โ‰  +โˆž)
66 xaddmnf1 13240 . . . . . . . 8 ((๐ต โˆˆ โ„* โˆง ๐ต โ‰  +โˆž) โ†’ (๐ต +๐‘’ -โˆž) = -โˆž)
6743, 65, 66syl2anc 583 . . . . . . 7 (๐ต โˆˆ โ„ โ†’ (๐ต +๐‘’ -โˆž) = -โˆž)
6867adantl 481 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ต +๐‘’ -โˆž) = -โˆž)
6964, 68sylan9eqr 2790 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = -โˆž)
7069oveq2d 7436 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe -โˆž))
71 oveq2 7428 . . . . . 6 (๐ถ = -โˆž โ†’ (๐ด ยทe ๐ถ) = (๐ด ยทe -โˆž))
7271, 56sylan9eqr 2790 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe ๐ถ) = -โˆž)
7372oveq2d 7436 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ -โˆž))
7463, 70, 733eqtr4d 2778 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
75 simpl3 1191 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ๐ถ โˆˆ โ„*)
76 elxr 13129 . . . . 5 (๐ถ โˆˆ โ„* โ†” (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
7775, 76sylib 217 . . . 4 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
7877adantr 480 . . 3 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
7927, 53, 74, 78mpjao3dan 1429 . 2 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
8031ad2antrr 725 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe +โˆž) = +โˆž)
811adantr 480 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ ๐ด โˆˆ โ„)
8223, 14eqeltrd 2829 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) โˆˆ โ„)
8381, 82sylan 579 . . . . . 6 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) โˆˆ โ„)
84 rexr 11291 . . . . . . 7 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (๐ด ยทe ๐ถ) โˆˆ โ„*)
85 renemnf 11294 . . . . . . 7 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (๐ด ยทe ๐ถ) โ‰  -โˆž)
86 xaddpnf2 13239 . . . . . . 7 (((๐ด ยทe ๐ถ) โˆˆ โ„* โˆง (๐ด ยทe ๐ถ) โ‰  -โˆž) โ†’ (+โˆž +๐‘’ (๐ด ยทe ๐ถ)) = +โˆž)
8784, 85, 86syl2anc 583 . . . . . 6 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (+โˆž +๐‘’ (๐ด ยทe ๐ถ)) = +โˆž)
8883, 87syl 17 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (+โˆž +๐‘’ (๐ด ยทe ๐ถ)) = +โˆž)
8980, 88eqtr4d 2771 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe +โˆž) = (+โˆž +๐‘’ (๐ด ยทe ๐ถ)))
90 simpr 484 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ ๐ต = +โˆž)
9190oveq1d 7435 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (+โˆž +๐‘’ ๐ถ))
92 rexr 11291 . . . . . . 7 (๐ถ โˆˆ โ„ โ†’ ๐ถ โˆˆ โ„*)
93 renemnf 11294 . . . . . . 7 (๐ถ โˆˆ โ„ โ†’ ๐ถ โ‰  -โˆž)
94 xaddpnf2 13239 . . . . . . 7 ((๐ถ โˆˆ โ„* โˆง ๐ถ โ‰  -โˆž) โ†’ (+โˆž +๐‘’ ๐ถ) = +โˆž)
9592, 93, 94syl2anc 583 . . . . . 6 (๐ถ โˆˆ โ„ โ†’ (+โˆž +๐‘’ ๐ถ) = +โˆž)
9691, 95sylan9eq 2788 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต +๐‘’ ๐ถ) = +โˆž)
9796oveq2d 7436 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe +โˆž))
98 oveq2 7428 . . . . . . 7 (๐ต = +โˆž โ†’ (๐ด ยทe ๐ต) = (๐ด ยทe +โˆž))
9998, 31sylan9eqr 2790 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ (๐ด ยทe ๐ต) = +โˆž)
10099adantr 480 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) = +โˆž)
101100oveq1d 7435 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = (+โˆž +๐‘’ (๐ด ยทe ๐ถ)))
10289, 97, 1013eqtr4d 2778 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
103 pnfxr 11299 . . . . . . 7 +โˆž โˆˆ โ„*
104 pnfnemnf 11300 . . . . . . 7 +โˆž โ‰  -โˆž
105 xaddpnf1 13238 . . . . . . 7 ((+โˆž โˆˆ โ„* โˆง +โˆž โ‰  -โˆž) โ†’ (+โˆž +๐‘’ +โˆž) = +โˆž)
106103, 104, 105mp2an 691 . . . . . 6 (+โˆž +๐‘’ +โˆž) = +โˆž
10731, 31oveq12d 7438 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)) = (+โˆž +๐‘’ +โˆž))
108106, 107, 313eqtr4a 2794 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)) = (๐ด ยทe +โˆž))
109108ad2antrr 725 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)) = (๐ด ยทe +โˆž))
11098, 50oveqan12d 7439 . . . . 5 ((๐ต = +โˆž โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)))
111110adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)))
112 oveq12 7429 . . . . . . 7 ((๐ต = +โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (+โˆž +๐‘’ +โˆž))
113112, 106eqtrdi 2784 . . . . . 6 ((๐ต = +โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = +โˆž)
114113oveq2d 7436 . . . . 5 ((๐ต = +โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe +โˆž))
115114adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe +โˆž))
116109, 111, 1153eqtr4rd 2779 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
117 pnfaddmnf 13242 . . . . . 6 (+โˆž +๐‘’ -โˆž) = 0
11831, 55oveq12d 7438 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (+โˆž +๐‘’ -โˆž))
119 xmul01 13279 . . . . . . 7 (๐ด โˆˆ โ„* โ†’ (๐ด ยทe 0) = 0)
1201, 28, 1193syl 18 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe 0) = 0)
121117, 118, 1203eqtr4a 2794 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (๐ด ยทe 0))
122121ad2antrr 725 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (๐ด ยทe 0))
12398, 71oveqan12d 7439 . . . . 5 ((๐ต = +โˆž โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)))
124123adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)))
125 oveq12 7429 . . . . . . 7 ((๐ต = +โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (+โˆž +๐‘’ -โˆž))
126125, 117eqtrdi 2784 . . . . . 6 ((๐ต = +โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = 0)
127126oveq2d 7436 . . . . 5 ((๐ต = +โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe 0))
128127adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe 0))
129122, 124, 1283eqtr4rd 2779 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
13077adantr 480 . . 3 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
131102, 116, 129, 130mpjao3dan 1429 . 2 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
13255ad2antrr 725 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe -โˆž) = -โˆž)
1331adantr 480 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ ๐ด โˆˆ โ„)
134133, 82sylan 579 . . . . . 6 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) โˆˆ โ„)
135 renepnf 11293 . . . . . . 7 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (๐ด ยทe ๐ถ) โ‰  +โˆž)
136 xaddmnf2 13241 . . . . . . 7 (((๐ด ยทe ๐ถ) โˆˆ โ„* โˆง (๐ด ยทe ๐ถ) โ‰  +โˆž) โ†’ (-โˆž +๐‘’ (๐ด ยทe ๐ถ)) = -โˆž)
13784, 135, 136syl2anc 583 . . . . . 6 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (-โˆž +๐‘’ (๐ด ยทe ๐ถ)) = -โˆž)
138134, 137syl 17 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (-โˆž +๐‘’ (๐ด ยทe ๐ถ)) = -โˆž)
139132, 138eqtr4d 2771 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe -โˆž) = (-โˆž +๐‘’ (๐ด ยทe ๐ถ)))
140 simpr 484 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ ๐ต = -โˆž)
141140oveq1d 7435 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (-โˆž +๐‘’ ๐ถ))
142 renepnf 11293 . . . . . . 7 (๐ถ โˆˆ โ„ โ†’ ๐ถ โ‰  +โˆž)
143 xaddmnf2 13241 . . . . . . 7 ((๐ถ โˆˆ โ„* โˆง ๐ถ โ‰  +โˆž) โ†’ (-โˆž +๐‘’ ๐ถ) = -โˆž)
14492, 142, 143syl2anc 583 . . . . . 6 (๐ถ โˆˆ โ„ โ†’ (-โˆž +๐‘’ ๐ถ) = -โˆž)
145141, 144sylan9eq 2788 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต +๐‘’ ๐ถ) = -โˆž)
146145oveq2d 7436 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe -โˆž))
147 oveq2 7428 . . . . . . 7 (๐ต = -โˆž โ†’ (๐ด ยทe ๐ต) = (๐ด ยทe -โˆž))
148147, 55sylan9eqr 2790 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ (๐ด ยทe ๐ต) = -โˆž)
149148adantr 480 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) = -โˆž)
150149oveq1d 7435 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = (-โˆž +๐‘’ (๐ด ยทe ๐ถ)))
151139, 146, 1503eqtr4d 2778 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
15255, 31oveq12d 7438 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)) = (-โˆž +๐‘’ +โˆž))
153 mnfaddpnf 13243 . . . . . . 7 (-โˆž +๐‘’ +โˆž) = 0
154152, 153eqtrdi 2784 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)) = 0)
155120, 154eqtr4d 2771 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe 0) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)))
156155ad2antrr 725 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe 0) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)))
157 oveq12 7429 . . . . . . 7 ((๐ต = -โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (-โˆž +๐‘’ +โˆž))
158157, 153eqtrdi 2784 . . . . . 6 ((๐ต = -โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = 0)
159158oveq2d 7436 . . . . 5 ((๐ต = -โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe 0))
160159adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe 0))
161147, 50oveqan12d 7439 . . . . 5 ((๐ต = -โˆž โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)))
162161adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)))
163156, 160, 1623eqtr4d 2778 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
164 mnfxr 11302 . . . . . . 7 -โˆž โˆˆ โ„*
165 mnfnepnf 11301 . . . . . . 7 -โˆž โ‰  +โˆž
166 xaddmnf1 13240 . . . . . . 7 ((-โˆž โˆˆ โ„* โˆง -โˆž โ‰  +โˆž) โ†’ (-โˆž +๐‘’ -โˆž) = -โˆž)
167164, 165, 166mp2an 691 . . . . . 6 (-โˆž +๐‘’ -โˆž) = -โˆž
16855, 55oveq12d 7438 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (-โˆž +๐‘’ -โˆž))
169167, 168, 553eqtr4a 2794 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (๐ด ยทe -โˆž))
170169ad2antrr 725 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (๐ด ยทe -โˆž))
171147, 71oveqan12d 7439 . . . . 5 ((๐ต = -โˆž โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)))
172171adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)))
173 oveq12 7429 . . . . . . 7 ((๐ต = -โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (-โˆž +๐‘’ -โˆž))
174173, 167eqtrdi 2784 . . . . . 6 ((๐ต = -โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = -โˆž)
175174oveq2d 7436 . . . . 5 ((๐ต = -โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe -โˆž))
176175adantll 713 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe -โˆž))
177170, 172, 1763eqtr4rd 2779 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
17877adantr 480 . . 3 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
179151, 163, 177, 178mpjao3dan 1429 . 2 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
180 simpl2 1190 . . 3 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ๐ต โˆˆ โ„*)
181 elxr 13129 . . 3 (๐ต โˆˆ โ„* โ†” (๐ต โˆˆ โ„ โˆจ ๐ต = +โˆž โˆจ ๐ต = -โˆž))
182180, 181sylib 217 . 2 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ต โˆˆ โ„ โˆจ ๐ต = +โˆž โˆจ ๐ต = -โˆž))
18379, 131, 179, 182mpjao3dan 1429 1 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   โˆจ w3o 1084   โˆง w3a 1085   = wceq 1534   โˆˆ wcel 2099   โ‰  wne 2937   class class class wbr 5148  (class class class)co 7420  โ„‚cc 11137  โ„cr 11138  0cc0 11139   + caddc 11142   ยท cmul 11144  +โˆžcpnf 11276  -โˆžcmnf 11277  โ„*cxr 11278   < clt 11279   +๐‘’ cxad 13123   ยทe cxmu 13124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-cnex 11195  ax-resscn 11196  ax-1cn 11197  ax-icn 11198  ax-addcl 11199  ax-addrcl 11200  ax-mulcl 11201  ax-mulrcl 11202  ax-mulcom 11203  ax-addass 11204  ax-mulass 11205  ax-distr 11206  ax-i2m1 11207  ax-1ne0 11208  ax-1rid 11209  ax-rnegex 11210  ax-rrecex 11211  ax-cnre 11212  ax-pre-lttri 11213  ax-pre-lttrn 11214  ax-pre-ltadd 11215
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11281  df-mnf 11282  df-xr 11283  df-ltxr 11284  df-le 11285  df-sub 11477  df-neg 11478  df-xneg 13125  df-xadd 13126  df-xmul 13127
This theorem is referenced by:  xadddi  13307
  Copyright terms: Public domain W3C validator