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

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

Proof of Theorem xadddilem
StepHypRef Expression
1 simpl1 1188 . . . 4 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ๐ด โˆˆ โ„)
2 recn 11197 . . . . . . . 8 (๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„‚)
3 recn 11197 . . . . . . . 8 (๐ต โˆˆ โ„ โ†’ ๐ต โˆˆ โ„‚)
4 recn 11197 . . . . . . . 8 (๐ถ โˆˆ โ„ โ†’ ๐ถ โˆˆ โ„‚)
5 adddi 11196 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
62, 3, 4, 5syl3an 1157 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
763expa 1115 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
8 readdcl 11190 . . . . . . . 8 ((๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต + ๐ถ) โˆˆ โ„)
9 rexmul 13251 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง (๐ต + ๐ถ) โˆˆ โ„) โ†’ (๐ด ยทe (๐ต + ๐ถ)) = (๐ด ยท (๐ต + ๐ถ)))
108, 9sylan2 592 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„)) โ†’ (๐ด ยทe (๐ต + ๐ถ)) = (๐ด ยท (๐ต + ๐ถ)))
1110anassrs 467 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต + ๐ถ)) = (๐ด ยท (๐ต + ๐ถ)))
12 remulcl 11192 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยท ๐ต) โˆˆ โ„)
1312adantr 480 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท ๐ต) โˆˆ โ„)
14 remulcl 11192 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท ๐ถ) โˆˆ โ„)
1514adantlr 712 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยท ๐ถ) โˆˆ โ„)
1613, 15rexaddd 13214 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยท ๐ต) +๐‘’ (๐ด ยท ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
177, 11, 163eqtr4d 2774 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) +๐‘’ (๐ด ยท ๐ถ)))
18 rexadd 13212 . . . . . . 7 ((๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต +๐‘’ ๐ถ) = (๐ต + ๐ถ))
1918adantll 711 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต +๐‘’ ๐ถ) = (๐ต + ๐ถ))
2019oveq2d 7418 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe (๐ต + ๐ถ)))
21 rexmul 13251 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต))
2221adantr 480 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต))
23 rexmul 13251 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) = (๐ด ยท ๐ถ))
2423adantlr 712 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) = (๐ด ยท ๐ถ))
2522, 24oveq12d 7420 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยท ๐ต) +๐‘’ (๐ด ยท ๐ถ)))
2617, 20, 253eqtr4d 2774 . . . 4 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
271, 26sylanl1 677 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
28 rexr 11259 . . . . . . . . 9 (๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„*)
29283ad2ant1 1130 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โ†’ ๐ด โˆˆ โ„*)
30 xmulpnf1 13254 . . . . . . . 8 ((๐ด โˆˆ โ„* โˆง 0 < ๐ด) โ†’ (๐ด ยทe +โˆž) = +โˆž)
3129, 30sylan 579 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe +โˆž) = +โˆž)
3231adantr 480 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe +โˆž) = +โˆž)
3321, 12eqeltrd 2825 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) โˆˆ โ„)
341, 33sylan 579 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) โˆˆ โ„)
35 rexr 11259 . . . . . . . 8 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ (๐ด ยทe ๐ต) โˆˆ โ„*)
36 renemnf 11262 . . . . . . . 8 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ (๐ด ยทe ๐ต) โ‰  -โˆž)
37 xaddpnf1 13206 . . . . . . . 8 (((๐ด ยทe ๐ต) โˆˆ โ„* โˆง (๐ด ยทe ๐ต) โ‰  -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ +โˆž) = +โˆž)
3835, 36, 37syl2anc 583 . . . . . . 7 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ ((๐ด ยทe ๐ต) +๐‘’ +โˆž) = +โˆž)
3934, 38syl 17 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ ((๐ด ยทe ๐ต) +๐‘’ +โˆž) = +โˆž)
4032, 39eqtr4d 2767 . . . . 5 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe +โˆž) = ((๐ด ยทe ๐ต) +๐‘’ +โˆž))
4140adantr 480 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe +โˆž) = ((๐ด ยทe ๐ต) +๐‘’ +โˆž))
42 oveq2 7410 . . . . . 6 (๐ถ = +โˆž โ†’ (๐ต +๐‘’ ๐ถ) = (๐ต +๐‘’ +โˆž))
43 rexr 11259 . . . . . . . 8 (๐ต โˆˆ โ„ โ†’ ๐ต โˆˆ โ„*)
44 renemnf 11262 . . . . . . . 8 (๐ต โˆˆ โ„ โ†’ ๐ต โ‰  -โˆž)
45 xaddpnf1 13206 . . . . . . . 8 ((๐ต โˆˆ โ„* โˆง ๐ต โ‰  -โˆž) โ†’ (๐ต +๐‘’ +โˆž) = +โˆž)
4643, 44, 45syl2anc 583 . . . . . . 7 (๐ต โˆˆ โ„ โ†’ (๐ต +๐‘’ +โˆž) = +โˆž)
4746adantl 481 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ต +๐‘’ +โˆž) = +โˆž)
4842, 47sylan9eqr 2786 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = +โˆž)
4948oveq2d 7418 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe +โˆž))
50 oveq2 7410 . . . . . 6 (๐ถ = +โˆž โ†’ (๐ด ยทe ๐ถ) = (๐ด ยทe +โˆž))
5150, 32sylan9eqr 2786 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe ๐ถ) = +โˆž)
5251oveq2d 7418 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ +โˆž))
5341, 49, 523eqtr4d 2774 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
54 xmulmnf1 13256 . . . . . . . 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 11261 . . . . . . 7 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ (๐ด ยทe ๐ต) โ‰  +โˆž)
60 xaddmnf1 13208 . . . . . . 7 (((๐ด ยทe ๐ต) โˆˆ โ„* โˆง (๐ด ยทe ๐ต) โ‰  +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ -โˆž) = -โˆž)
6135, 59, 60syl2anc 583 . . . . . 6 ((๐ด ยทe ๐ต) โˆˆ โ„ โ†’ ((๐ด ยทe ๐ต) +๐‘’ -โˆž) = -โˆž)
6258, 61syl 17 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ -โˆž) = -โˆž)
6357, 62eqtr4d 2767 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe -โˆž) = ((๐ด ยทe ๐ต) +๐‘’ -โˆž))
64 oveq2 7410 . . . . . 6 (๐ถ = -โˆž โ†’ (๐ต +๐‘’ ๐ถ) = (๐ต +๐‘’ -โˆž))
65 renepnf 11261 . . . . . . . 8 (๐ต โˆˆ โ„ โ†’ ๐ต โ‰  +โˆž)
66 xaddmnf1 13208 . . . . . . . 8 ((๐ต โˆˆ โ„* โˆง ๐ต โ‰  +โˆž) โ†’ (๐ต +๐‘’ -โˆž) = -โˆž)
6743, 65, 66syl2anc 583 . . . . . . 7 (๐ต โˆˆ โ„ โ†’ (๐ต +๐‘’ -โˆž) = -โˆž)
6867adantl 481 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ต +๐‘’ -โˆž) = -โˆž)
6964, 68sylan9eqr 2786 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = -โˆž)
7069oveq2d 7418 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe -โˆž))
71 oveq2 7410 . . . . . 6 (๐ถ = -โˆž โ†’ (๐ด ยทe ๐ถ) = (๐ด ยทe -โˆž))
7271, 56sylan9eqr 2786 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe ๐ถ) = -โˆž)
7372oveq2d 7418 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ -โˆž))
7463, 70, 733eqtr4d 2774 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
75 simpl3 1190 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ๐ถ โˆˆ โ„*)
76 elxr 13097 . . . . 5 (๐ถ โˆˆ โ„* โ†” (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
7775, 76sylib 217 . . . 4 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
7877adantr 480 . . 3 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
7927, 53, 74, 78mpjao3dan 1428 . 2 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
8031ad2antrr 723 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe +โˆž) = +โˆž)
811adantr 480 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ ๐ด โˆˆ โ„)
8223, 14eqeltrd 2825 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) โˆˆ โ„)
8381, 82sylan 579 . . . . . 6 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) โˆˆ โ„)
84 rexr 11259 . . . . . . 7 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (๐ด ยทe ๐ถ) โˆˆ โ„*)
85 renemnf 11262 . . . . . . 7 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (๐ด ยทe ๐ถ) โ‰  -โˆž)
86 xaddpnf2 13207 . . . . . . 7 (((๐ด ยทe ๐ถ) โˆˆ โ„* โˆง (๐ด ยทe ๐ถ) โ‰  -โˆž) โ†’ (+โˆž +๐‘’ (๐ด ยทe ๐ถ)) = +โˆž)
8784, 85, 86syl2anc 583 . . . . . 6 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (+โˆž +๐‘’ (๐ด ยทe ๐ถ)) = +โˆž)
8883, 87syl 17 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (+โˆž +๐‘’ (๐ด ยทe ๐ถ)) = +โˆž)
8980, 88eqtr4d 2767 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe +โˆž) = (+โˆž +๐‘’ (๐ด ยทe ๐ถ)))
90 simpr 484 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ ๐ต = +โˆž)
9190oveq1d 7417 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (+โˆž +๐‘’ ๐ถ))
92 rexr 11259 . . . . . . 7 (๐ถ โˆˆ โ„ โ†’ ๐ถ โˆˆ โ„*)
93 renemnf 11262 . . . . . . 7 (๐ถ โˆˆ โ„ โ†’ ๐ถ โ‰  -โˆž)
94 xaddpnf2 13207 . . . . . . 7 ((๐ถ โˆˆ โ„* โˆง ๐ถ โ‰  -โˆž) โ†’ (+โˆž +๐‘’ ๐ถ) = +โˆž)
9592, 93, 94syl2anc 583 . . . . . 6 (๐ถ โˆˆ โ„ โ†’ (+โˆž +๐‘’ ๐ถ) = +โˆž)
9691, 95sylan9eq 2784 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต +๐‘’ ๐ถ) = +โˆž)
9796oveq2d 7418 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe +โˆž))
98 oveq2 7410 . . . . . . 7 (๐ต = +โˆž โ†’ (๐ด ยทe ๐ต) = (๐ด ยทe +โˆž))
9998, 31sylan9eqr 2786 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ (๐ด ยทe ๐ต) = +โˆž)
10099adantr 480 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) = +โˆž)
101100oveq1d 7417 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = (+โˆž +๐‘’ (๐ด ยทe ๐ถ)))
10289, 97, 1013eqtr4d 2774 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
103 pnfxr 11267 . . . . . . 7 +โˆž โˆˆ โ„*
104 pnfnemnf 11268 . . . . . . 7 +โˆž โ‰  -โˆž
105 xaddpnf1 13206 . . . . . . 7 ((+โˆž โˆˆ โ„* โˆง +โˆž โ‰  -โˆž) โ†’ (+โˆž +๐‘’ +โˆž) = +โˆž)
106103, 104, 105mp2an 689 . . . . . 6 (+โˆž +๐‘’ +โˆž) = +โˆž
10731, 31oveq12d 7420 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)) = (+โˆž +๐‘’ +โˆž))
108106, 107, 313eqtr4a 2790 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)) = (๐ด ยทe +โˆž))
109108ad2antrr 723 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)) = (๐ด ยทe +โˆž))
11098, 50oveqan12d 7421 . . . . 5 ((๐ต = +โˆž โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)))
111110adantll 711 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe +โˆž)))
112 oveq12 7411 . . . . . . 7 ((๐ต = +โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (+โˆž +๐‘’ +โˆž))
113112, 106eqtrdi 2780 . . . . . 6 ((๐ต = +โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = +โˆž)
114113oveq2d 7418 . . . . 5 ((๐ต = +โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe +โˆž))
115114adantll 711 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe +โˆž))
116109, 111, 1153eqtr4rd 2775 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
117 pnfaddmnf 13210 . . . . . 6 (+โˆž +๐‘’ -โˆž) = 0
11831, 55oveq12d 7420 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (+โˆž +๐‘’ -โˆž))
119 xmul01 13247 . . . . . . 7 (๐ด โˆˆ โ„* โ†’ (๐ด ยทe 0) = 0)
1201, 28, 1193syl 18 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe 0) = 0)
121117, 118, 1203eqtr4a 2790 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (๐ด ยทe 0))
122121ad2antrr 723 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (๐ด ยทe 0))
12398, 71oveqan12d 7421 . . . . 5 ((๐ต = +โˆž โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)))
124123adantll 711 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โˆž) +๐‘’ (๐ด ยทe -โˆž)))
125 oveq12 7411 . . . . . . 7 ((๐ต = +โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (+โˆž +๐‘’ -โˆž))
126125, 117eqtrdi 2780 . . . . . 6 ((๐ต = +โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = 0)
127126oveq2d 7418 . . . . 5 ((๐ต = +โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe 0))
128127adantll 711 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe 0))
129122, 124, 1283eqtr4rd 2775 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
13077adantr 480 . . 3 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
131102, 116, 129, 130mpjao3dan 1428 . 2 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
13255ad2antrr 723 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe -โˆž) = -โˆž)
1331adantr 480 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ ๐ด โˆˆ โ„)
134133, 82sylan 579 . . . . . 6 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ถ) โˆˆ โ„)
135 renepnf 11261 . . . . . . 7 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (๐ด ยทe ๐ถ) โ‰  +โˆž)
136 xaddmnf2 13209 . . . . . . 7 (((๐ด ยทe ๐ถ) โˆˆ โ„* โˆง (๐ด ยทe ๐ถ) โ‰  +โˆž) โ†’ (-โˆž +๐‘’ (๐ด ยทe ๐ถ)) = -โˆž)
13784, 135, 136syl2anc 583 . . . . . 6 ((๐ด ยทe ๐ถ) โˆˆ โ„ โ†’ (-โˆž +๐‘’ (๐ด ยทe ๐ถ)) = -โˆž)
138134, 137syl 17 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (-โˆž +๐‘’ (๐ด ยทe ๐ถ)) = -โˆž)
139132, 138eqtr4d 2767 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe -โˆž) = (-โˆž +๐‘’ (๐ด ยทe ๐ถ)))
140 simpr 484 . . . . . . 7 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ ๐ต = -โˆž)
141140oveq1d 7417 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (-โˆž +๐‘’ ๐ถ))
142 renepnf 11261 . . . . . . 7 (๐ถ โˆˆ โ„ โ†’ ๐ถ โ‰  +โˆž)
143 xaddmnf2 13209 . . . . . . 7 ((๐ถ โˆˆ โ„* โˆง ๐ถ โ‰  +โˆž) โ†’ (-โˆž +๐‘’ ๐ถ) = -โˆž)
14492, 142, 143syl2anc 583 . . . . . 6 (๐ถ โˆˆ โ„ โ†’ (-โˆž +๐‘’ ๐ถ) = -โˆž)
145141, 144sylan9eq 2784 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ต +๐‘’ ๐ถ) = -โˆž)
146145oveq2d 7418 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe -โˆž))
147 oveq2 7410 . . . . . . 7 (๐ต = -โˆž โ†’ (๐ด ยทe ๐ต) = (๐ด ยทe -โˆž))
148147, 55sylan9eqr 2786 . . . . . 6 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ (๐ด ยทe ๐ต) = -โˆž)
149148adantr 480 . . . . 5 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe ๐ต) = -โˆž)
150149oveq1d 7417 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = (-โˆž +๐‘’ (๐ด ยทe ๐ถ)))
151139, 146, 1503eqtr4d 2774 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ โˆˆ โ„) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
15255, 31oveq12d 7420 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)) = (-โˆž +๐‘’ +โˆž))
153 mnfaddpnf 13211 . . . . . . 7 (-โˆž +๐‘’ +โˆž) = 0
154152, 153eqtrdi 2780 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)) = 0)
155120, 154eqtr4d 2767 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe 0) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)))
156155ad2antrr 723 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe 0) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)))
157 oveq12 7411 . . . . . . 7 ((๐ต = -โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (-โˆž +๐‘’ +โˆž))
158157, 153eqtrdi 2780 . . . . . 6 ((๐ต = -โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = 0)
159158oveq2d 7418 . . . . 5 ((๐ต = -โˆž โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe 0))
160159adantll 711 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe 0))
161147, 50oveqan12d 7421 . . . . 5 ((๐ต = -โˆž โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)))
162161adantll 711 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = +โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe +โˆž)))
163156, 160, 1623eqtr4d 2774 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = +โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
164 mnfxr 11270 . . . . . . 7 -โˆž โˆˆ โ„*
165 mnfnepnf 11269 . . . . . . 7 -โˆž โ‰  +โˆž
166 xaddmnf1 13208 . . . . . . 7 ((-โˆž โˆˆ โ„* โˆง -โˆž โ‰  +โˆž) โ†’ (-โˆž +๐‘’ -โˆž) = -โˆž)
167164, 165, 166mp2an 689 . . . . . 6 (-โˆž +๐‘’ -โˆž) = -โˆž
16855, 55oveq12d 7420 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (-โˆž +๐‘’ -โˆž))
169167, 168, 553eqtr4a 2790 . . . . 5 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (๐ด ยทe -โˆž))
170169ad2antrr 723 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)) = (๐ด ยทe -โˆž))
171147, 71oveqan12d 7421 . . . . 5 ((๐ต = -โˆž โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)))
172171adantll 711 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = -โˆž) โ†’ ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โˆž) +๐‘’ (๐ด ยทe -โˆž)))
173 oveq12 7411 . . . . . . 7 ((๐ต = -โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = (-โˆž +๐‘’ -โˆž))
174173, 167eqtrdi 2780 . . . . . 6 ((๐ต = -โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ต +๐‘’ ๐ถ) = -โˆž)
175174oveq2d 7418 . . . . 5 ((๐ต = -โˆž โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe -โˆž))
176175adantll 711 . . . 4 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = (๐ด ยทe -โˆž))
177170, 172, 1763eqtr4rd 2775 . . 3 (((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โˆง ๐ถ = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
17877adantr 480 . . 3 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ (๐ถ โˆˆ โ„ โˆจ ๐ถ = +โˆž โˆจ ๐ถ = -โˆž))
179151, 163, 177, 178mpjao3dan 1428 . 2 ((((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โˆง ๐ต = -โˆž) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
180 simpl2 1189 . . 3 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ ๐ต โˆˆ โ„*)
181 elxr 13097 . . 3 (๐ต โˆˆ โ„* โ†” (๐ต โˆˆ โ„ โˆจ ๐ต = +โˆž โˆจ ๐ต = -โˆž))
182180, 181sylib 217 . 2 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ต โˆˆ โ„ โˆจ ๐ต = +โˆž โˆจ ๐ต = -โˆž))
18379, 131, 179, 182mpjao3dan 1428 1 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„* โˆง ๐ถ โˆˆ โ„*) โˆง 0 < ๐ด) โ†’ (๐ด ยทe (๐ต +๐‘’ ๐ถ)) = ((๐ด ยทe ๐ต) +๐‘’ (๐ด ยทe ๐ถ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   โˆจ w3o 1083   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2932   class class class wbr 5139  (class class class)co 7402  โ„‚cc 11105  โ„cr 11106  0cc0 11107   + caddc 11110   ยท cmul 11112  +โˆžcpnf 11244  -โˆžcmnf 11245  โ„*cxr 11246   < clt 11247   +๐‘’ cxad 13091   ยทe cxmu 13092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-po 5579  df-so 5580  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-xneg 13093  df-xadd 13094  df-xmul 13095
This theorem is referenced by:  xadddi  13275
  Copyright terms: Public domain W3C validator