ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  efaddlem GIF version

Theorem efaddlem 11699
Description: Lemma for efadd 11700 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.)
Hypotheses
Ref Expression
efadd.1 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) / (!‘𝑛)))
efadd.2 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵𝑛) / (!‘𝑛)))
efadd.3 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛)))
efadd.4 (𝜑𝐴 ∈ ℂ)
efadd.5 (𝜑𝐵 ∈ ℂ)
Assertion
Ref Expression
efaddlem (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵)))
Distinct variable groups:   𝐴,𝑛   𝐵,𝑛
Allowed substitution hints:   𝜑(𝑛)   𝐹(𝑛)   𝐺(𝑛)   𝐻(𝑛)

Proof of Theorem efaddlem
Dummy variables 𝑗 𝑘 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efadd.4 . . . 4 (𝜑𝐴 ∈ ℂ)
2 efadd.5 . . . 4 (𝜑𝐵 ∈ ℂ)
31, 2addcld 7994 . . 3 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
4 efadd.3 . . . 4 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛)))
54efcvg 11691 . . 3 ((𝐴 + 𝐵) ∈ ℂ → seq0( + , 𝐻) ⇝ (exp‘(𝐴 + 𝐵)))
63, 5syl 14 . 2 (𝜑 → seq0( + , 𝐻) ⇝ (exp‘(𝐴 + 𝐵)))
7 efadd.1 . . . . . 6 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) / (!‘𝑛)))
87eftvalcn 11682 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (𝐹𝑗) = ((𝐴𝑗) / (!‘𝑗)))
91, 8sylan 283 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐹𝑗) = ((𝐴𝑗) / (!‘𝑗)))
10 absexp 11105 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (abs‘(𝐴𝑗)) = ((abs‘𝐴)↑𝑗))
111, 10sylan 283 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (abs‘(𝐴𝑗)) = ((abs‘𝐴)↑𝑗))
12 faccl 10732 . . . . . . . 8 (𝑗 ∈ ℕ0 → (!‘𝑗) ∈ ℕ)
1312adantl 277 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑗) ∈ ℕ)
14 nnre 8943 . . . . . . . 8 ((!‘𝑗) ∈ ℕ → (!‘𝑗) ∈ ℝ)
15 nnnn0 9200 . . . . . . . . 9 ((!‘𝑗) ∈ ℕ → (!‘𝑗) ∈ ℕ0)
1615nn0ge0d 9249 . . . . . . . 8 ((!‘𝑗) ∈ ℕ → 0 ≤ (!‘𝑗))
1714, 16absidd 11193 . . . . . . 7 ((!‘𝑗) ∈ ℕ → (abs‘(!‘𝑗)) = (!‘𝑗))
1813, 17syl 14 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (abs‘(!‘𝑗)) = (!‘𝑗))
1911, 18oveq12d 5908 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((abs‘(𝐴𝑗)) / (abs‘(!‘𝑗))) = (((abs‘𝐴)↑𝑗) / (!‘𝑗)))
20 expcl 10555 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (𝐴𝑗) ∈ ℂ)
211, 20sylan 283 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝐴𝑗) ∈ ℂ)
2213nncnd 8950 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑗) ∈ ℂ)
2313nnap0d 8982 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑗) # 0)
2421, 22, 23absdivapd 11221 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (abs‘((𝐴𝑗) / (!‘𝑗))) = ((abs‘(𝐴𝑗)) / (abs‘(!‘𝑗))))
251abscld 11207 . . . . . . 7 (𝜑 → (abs‘𝐴) ∈ ℝ)
2625recnd 8003 . . . . . 6 (𝜑 → (abs‘𝐴) ∈ ℂ)
27 eqid 2188 . . . . . . 7 (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))
2827eftvalcn 11682 . . . . . 6 (((abs‘𝐴) ∈ ℂ ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))‘𝑗) = (((abs‘𝐴)↑𝑗) / (!‘𝑗)))
2926, 28sylan 283 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))‘𝑗) = (((abs‘𝐴)↑𝑗) / (!‘𝑗)))
3019, 24, 293eqtr4rd 2232 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))‘𝑗) = (abs‘((𝐴𝑗) / (!‘𝑗))))
31 eftcl 11679 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → ((𝐴𝑗) / (!‘𝑗)) ∈ ℂ)
321, 31sylan 283 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((𝐴𝑗) / (!‘𝑗)) ∈ ℂ)
33 efadd.2 . . . . . 6 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵𝑛) / (!‘𝑛)))
3433eftvalcn 11682 . . . . 5 ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = ((𝐵𝑘) / (!‘𝑘)))
352, 34sylan 283 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = ((𝐵𝑘) / (!‘𝑘)))
36 eftcl 11679 . . . . 5 ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐵𝑘) / (!‘𝑘)) ∈ ℂ)
372, 36sylan 283 . . . 4 ((𝜑𝑘 ∈ ℕ0) → ((𝐵𝑘) / (!‘𝑘)) ∈ ℂ)
384eftvalcn 11682 . . . . . 6 (((𝐴 + 𝐵) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐻𝑘) = (((𝐴 + 𝐵)↑𝑘) / (!‘𝑘)))
393, 38sylan 283 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = (((𝐴 + 𝐵)↑𝑘) / (!‘𝑘)))
401adantr 276 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → 𝐴 ∈ ℂ)
412adantr 276 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
42 simpr 110 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
43 binom 11509 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑘) = Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))))
4440, 41, 42, 43syl3anc 1248 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑘) = Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))))
4544oveq1d 5905 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (((𝐴 + 𝐵)↑𝑘) / (!‘𝑘)) = (Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)))
46 0zd 9282 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 0 ∈ ℤ)
4742nn0zd 9390 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
4846, 47fzfigd 10448 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (0...𝑘) ∈ Fin)
49 faccl 10732 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
5049adantl 277 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℕ)
5150nncnd 8950 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℂ)
52 bccl2 10765 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑘) → (𝑘C𝑗) ∈ ℕ)
5352adantl 277 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘C𝑗) ∈ ℕ)
5453nncnd 8950 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘C𝑗) ∈ ℂ)
551ad2antrr 488 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝐴 ∈ ℂ)
56 fznn0sub 10074 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑘) → (𝑘𝑗) ∈ ℕ0)
5756adantl 277 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘𝑗) ∈ ℕ0)
5855, 57expcld 10671 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴↑(𝑘𝑗)) ∈ ℂ)
592ad2antrr 488 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝐵 ∈ ℂ)
60 elfznn0 10131 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑘) → 𝑗 ∈ ℕ0)
6160adantl 277 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝑗 ∈ ℕ0)
6259, 61expcld 10671 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐵𝑗) ∈ ℂ)
6358, 62mulcld 7995 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝐴↑(𝑘𝑗)) · (𝐵𝑗)) ∈ ℂ)
6454, 63mulcld 7995 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) ∈ ℂ)
6550nnap0d 8982 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (!‘𝑘) # 0)
6648, 51, 64, 65fsumdivapc 11475 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)) = Σ𝑗 ∈ (0...𝑘)(((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)))
6755, 61expcld 10671 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴𝑗) ∈ ℂ)
6861, 12syl 14 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑗) ∈ ℕ)
6968nncnd 8950 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑗) ∈ ℂ)
7068nnap0d 8982 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑗) # 0)
7167, 69, 70divclapd 8764 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝐴𝑗) / (!‘𝑗)) ∈ ℂ)
7233eftvalcn 11682 . . . . . . . . . . . 12 ((𝐵 ∈ ℂ ∧ (𝑘𝑗) ∈ ℕ0) → (𝐺‘(𝑘𝑗)) = ((𝐵↑(𝑘𝑗)) / (!‘(𝑘𝑗))))
7359, 57, 72syl2anc 411 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘𝑗)) = ((𝐵↑(𝑘𝑗)) / (!‘(𝑘𝑗))))
7459, 57expcld 10671 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐵↑(𝑘𝑗)) ∈ ℂ)
75 faccl 10732 . . . . . . . . . . . . . 14 ((𝑘𝑗) ∈ ℕ0 → (!‘(𝑘𝑗)) ∈ ℕ)
7657, 75syl 14 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘(𝑘𝑗)) ∈ ℕ)
7776nncnd 8950 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘(𝑘𝑗)) ∈ ℂ)
7876nnap0d 8982 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘(𝑘𝑗)) # 0)
7974, 77, 78divclapd 8764 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝐵↑(𝑘𝑗)) / (!‘(𝑘𝑗))) ∈ ℂ)
8073, 79eqeltrd 2265 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘𝑗)) ∈ ℂ)
8171, 80mulcld 7995 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))) ∈ ℂ)
82 oveq2 5898 . . . . . . . . . . 11 (𝑗 = ((0 + 𝑘) − 𝑚) → (𝐴𝑗) = (𝐴↑((0 + 𝑘) − 𝑚)))
83 fveq2 5529 . . . . . . . . . . 11 (𝑗 = ((0 + 𝑘) − 𝑚) → (!‘𝑗) = (!‘((0 + 𝑘) − 𝑚)))
8482, 83oveq12d 5908 . . . . . . . . . 10 (𝑗 = ((0 + 𝑘) − 𝑚) → ((𝐴𝑗) / (!‘𝑗)) = ((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))))
85 oveq2 5898 . . . . . . . . . . 11 (𝑗 = ((0 + 𝑘) − 𝑚) → (𝑘𝑗) = (𝑘 − ((0 + 𝑘) − 𝑚)))
8685fveq2d 5533 . . . . . . . . . 10 (𝑗 = ((0 + 𝑘) − 𝑚) → (𝐺‘(𝑘𝑗)) = (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚))))
8784, 86oveq12d 5908 . . . . . . . . 9 (𝑗 = ((0 + 𝑘) − 𝑚) → (((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))) = (((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚)))))
8846, 47, 81, 87fisumrev2 11471 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑘)(((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))) = Σ𝑚 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚)))))
8933eftvalcn 11682 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (𝐺𝑗) = ((𝐵𝑗) / (!‘𝑗)))
9059, 61, 89syl2anc 411 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺𝑗) = ((𝐵𝑗) / (!‘𝑗)))
9190oveq2d 5906 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))) · (𝐺𝑗)) = (((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))) · ((𝐵𝑗) / (!‘𝑗))))
9276, 68nnmulcld 8985 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((!‘(𝑘𝑗)) · (!‘𝑗)) ∈ ℕ)
9392nncnd 8950 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((!‘(𝑘𝑗)) · (!‘𝑗)) ∈ ℂ)
9477, 69, 78, 70mulap0d 8632 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((!‘(𝑘𝑗)) · (!‘𝑗)) # 0)
9563, 93, 94divrecap2d 8768 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑(𝑘𝑗)) · (𝐵𝑗)) / ((!‘(𝑘𝑗)) · (!‘𝑗))) = ((1 / ((!‘(𝑘𝑗)) · (!‘𝑗))) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))))
9658, 77, 62, 69, 78, 70divmuldivapd 8806 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))) · ((𝐵𝑗) / (!‘𝑗))) = (((𝐴↑(𝑘𝑗)) · (𝐵𝑗)) / ((!‘(𝑘𝑗)) · (!‘𝑗))))
97 bcval2 10747 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑘) → (𝑘C𝑗) = ((!‘𝑘) / ((!‘(𝑘𝑗)) · (!‘𝑗))))
9897adantl 277 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘C𝑗) = ((!‘𝑘) / ((!‘(𝑘𝑗)) · (!‘𝑗))))
9998oveq1d 5905 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝑘C𝑗) / (!‘𝑘)) = (((!‘𝑘) / ((!‘(𝑘𝑗)) · (!‘𝑗))) / (!‘𝑘)))
10051adantr 276 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑘) ∈ ℂ)
10165adantr 276 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑘) # 0)
102100, 93, 100, 94, 101divdiv32apd 8790 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((!‘𝑘) / ((!‘(𝑘𝑗)) · (!‘𝑗))) / (!‘𝑘)) = (((!‘𝑘) / (!‘𝑘)) / ((!‘(𝑘𝑗)) · (!‘𝑗))))
103100, 101dividapd 8760 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((!‘𝑘) / (!‘𝑘)) = 1)
104103oveq1d 5905 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((!‘𝑘) / (!‘𝑘)) / ((!‘(𝑘𝑗)) · (!‘𝑗))) = (1 / ((!‘(𝑘𝑗)) · (!‘𝑗))))
105102, 104eqtrd 2221 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((!‘𝑘) / ((!‘(𝑘𝑗)) · (!‘𝑗))) / (!‘𝑘)) = (1 / ((!‘(𝑘𝑗)) · (!‘𝑗))))
10699, 105eqtrd 2221 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝑘C𝑗) / (!‘𝑘)) = (1 / ((!‘(𝑘𝑗)) · (!‘𝑗))))
107106oveq1d 5905 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝑘C𝑗) / (!‘𝑘)) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) = ((1 / ((!‘(𝑘𝑗)) · (!‘𝑗))) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))))
10895, 96, 1073eqtr4rd 2232 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝑘C𝑗) / (!‘𝑘)) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) = (((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))) · ((𝐵𝑗) / (!‘𝑗))))
10991, 108eqtr4d 2224 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))) · (𝐺𝑗)) = (((𝑘C𝑗) / (!‘𝑘)) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))))
110 nn0cn 9203 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
111110ad2antlr 489 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝑘 ∈ ℂ)
112111addid2d 8124 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (0 + 𝑘) = 𝑘)
113112oveq1d 5905 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((0 + 𝑘) − 𝑗) = (𝑘𝑗))
114113oveq2d 5906 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴↑((0 + 𝑘) − 𝑗)) = (𝐴↑(𝑘𝑗)))
115113fveq2d 5533 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘((0 + 𝑘) − 𝑗)) = (!‘(𝑘𝑗)))
116114, 115oveq12d 5908 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) = ((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))))
117113oveq2d 5906 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − ((0 + 𝑘) − 𝑗)) = (𝑘 − (𝑘𝑗)))
118 nn0cn 9203 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0𝑗 ∈ ℂ)
11961, 118syl 14 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝑗 ∈ ℂ)
120111, 119nncand 8290 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − (𝑘𝑗)) = 𝑗)
121117, 120eqtrd 2221 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − ((0 + 𝑘) − 𝑗)) = 𝑗)
122121fveq2d 5533 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗))) = (𝐺𝑗))
123116, 122oveq12d 5908 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))) = (((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))) · (𝐺𝑗)))
12454, 63, 100, 101div23apd 8802 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)) = (((𝑘C𝑗) / (!‘𝑘)) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))))
125109, 123, 1243eqtr4rd 2232 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)) = (((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))))
126125sumeq2dv 11393 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑘)(((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)) = Σ𝑗 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))))
127 oveq2 5898 . . . . . . . . . . . . 13 (𝑗 = 𝑚 → ((0 + 𝑘) − 𝑗) = ((0 + 𝑘) − 𝑚))
128127oveq2d 5906 . . . . . . . . . . . 12 (𝑗 = 𝑚 → (𝐴↑((0 + 𝑘) − 𝑗)) = (𝐴↑((0 + 𝑘) − 𝑚)))
129127fveq2d 5533 . . . . . . . . . . . 12 (𝑗 = 𝑚 → (!‘((0 + 𝑘) − 𝑗)) = (!‘((0 + 𝑘) − 𝑚)))
130128, 129oveq12d 5908 . . . . . . . . . . 11 (𝑗 = 𝑚 → ((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) = ((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))))
131127oveq2d 5906 . . . . . . . . . . . 12 (𝑗 = 𝑚 → (𝑘 − ((0 + 𝑘) − 𝑗)) = (𝑘 − ((0 + 𝑘) − 𝑚)))
132131fveq2d 5533 . . . . . . . . . . 11 (𝑗 = 𝑚 → (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗))) = (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚))))
133130, 132oveq12d 5908 . . . . . . . . . 10 (𝑗 = 𝑚 → (((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))) = (((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚)))))
134133cbvsumv 11386 . . . . . . . . 9 Σ𝑗 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))) = Σ𝑚 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚))))
135126, 134eqtrdi 2237 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑘)(((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)) = Σ𝑚 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚)))))
13688, 135eqtr4d 2224 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑘)(((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))) = Σ𝑗 ∈ (0...𝑘)(((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)))
13766, 136eqtr4d 2224 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)) = Σ𝑗 ∈ (0...𝑘)(((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))))
13845, 137eqtrd 2221 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (((𝐴 + 𝐵)↑𝑘) / (!‘𝑘)) = Σ𝑗 ∈ (0...𝑘)(((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))))
13939, 138eqtrd 2221 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = Σ𝑗 ∈ (0...𝑘)(((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))))
14027efcllem 11684 . . . . 5 ((abs‘𝐴) ∈ ℂ → seq0( + , (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))) ∈ dom ⇝ )
14126, 140syl 14 . . . 4 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))) ∈ dom ⇝ )
14233efcllem 11684 . . . . 5 (𝐵 ∈ ℂ → seq0( + , 𝐺) ∈ dom ⇝ )
1432, 142syl 14 . . . 4 (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
1447efcllem 11684 . . . . 5 (𝐴 ∈ ℂ → seq0( + , 𝐹) ∈ dom ⇝ )
1451, 144syl 14 . . . 4 (𝜑 → seq0( + , 𝐹) ∈ dom ⇝ )
1469, 30, 32, 35, 37, 139, 141, 143, 145mertensabs 11562 . . 3 (𝜑 → seq0( + , 𝐻) ⇝ (Σ𝑗 ∈ ℕ0 ((𝐴𝑗) / (!‘𝑗)) · Σ𝑘 ∈ ℕ0 ((𝐵𝑘) / (!‘𝑘))))
147 efval 11686 . . . . 5 (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑗 ∈ ℕ0 ((𝐴𝑗) / (!‘𝑗)))
1481, 147syl 14 . . . 4 (𝜑 → (exp‘𝐴) = Σ𝑗 ∈ ℕ0 ((𝐴𝑗) / (!‘𝑗)))
149 efval 11686 . . . . 5 (𝐵 ∈ ℂ → (exp‘𝐵) = Σ𝑘 ∈ ℕ0 ((𝐵𝑘) / (!‘𝑘)))
1502, 149syl 14 . . . 4 (𝜑 → (exp‘𝐵) = Σ𝑘 ∈ ℕ0 ((𝐵𝑘) / (!‘𝑘)))
151148, 150oveq12d 5908 . . 3 (𝜑 → ((exp‘𝐴) · (exp‘𝐵)) = (Σ𝑗 ∈ ℕ0 ((𝐴𝑗) / (!‘𝑗)) · Σ𝑘 ∈ ℕ0 ((𝐵𝑘) / (!‘𝑘))))
152146, 151breqtrrd 4045 . 2 (𝜑 → seq0( + , 𝐻) ⇝ ((exp‘𝐴) · (exp‘𝐵)))
153 climuni 11318 . 2 ((seq0( + , 𝐻) ⇝ (exp‘(𝐴 + 𝐵)) ∧ seq0( + , 𝐻) ⇝ ((exp‘𝐴) · (exp‘𝐵))) → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵)))
1546, 152, 153syl2anc 411 1 (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1363  wcel 2159   class class class wbr 4017  cmpt 4078  dom cdm 4640  cfv 5230  (class class class)co 5890  cc 7826  0cc0 7828  1c1 7829   + caddc 7831   · cmul 7833  cmin 8145   # cap 8555   / cdiv 8646  cn 8936  0cn0 9193  ...cfz 10025  seqcseq 10462  cexp 10536  !cfa 10722  Ccbc 10744  abscabs 11023  cli 11303  Σcsu 11378  expce 11667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2161  ax-14 2162  ax-ext 2170  ax-coll 4132  ax-sep 4135  ax-nul 4143  ax-pow 4188  ax-pr 4223  ax-un 4447  ax-setind 4550  ax-iinf 4601  ax-cnex 7919  ax-resscn 7920  ax-1cn 7921  ax-1re 7922  ax-icn 7923  ax-addcl 7924  ax-addrcl 7925  ax-mulcl 7926  ax-mulrcl 7927  ax-addcom 7928  ax-mulcom 7929  ax-addass 7930  ax-mulass 7931  ax-distr 7932  ax-i2m1 7933  ax-0lt1 7934  ax-1rid 7935  ax-0id 7936  ax-rnegex 7937  ax-precex 7938  ax-cnre 7939  ax-pre-ltirr 7940  ax-pre-ltwlin 7941  ax-pre-lttrn 7942  ax-pre-apti 7943  ax-pre-ltadd 7944  ax-pre-mulgt0 7945  ax-pre-mulext 7946  ax-arch 7947  ax-caucvg 7948
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2040  df-mo 2041  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ne 2360  df-nel 2455  df-ral 2472  df-rex 2473  df-reu 2474  df-rmo 2475  df-rab 2476  df-v 2753  df-sbc 2977  df-csb 3072  df-dif 3145  df-un 3147  df-in 3149  df-ss 3156  df-nul 3437  df-if 3549  df-pw 3591  df-sn 3612  df-pr 3613  df-op 3615  df-uni 3824  df-int 3859  df-iun 3902  df-disj 3995  df-br 4018  df-opab 4079  df-mpt 4080  df-tr 4116  df-id 4307  df-po 4310  df-iso 4311  df-iord 4380  df-on 4382  df-ilim 4383  df-suc 4385  df-iom 4604  df-xp 4646  df-rel 4647  df-cnv 4648  df-co 4649  df-dm 4650  df-rn 4651  df-res 4652  df-ima 4653  df-iota 5192  df-fun 5232  df-fn 5233  df-f 5234  df-f1 5235  df-fo 5236  df-f1o 5237  df-fv 5238  df-isom 5239  df-riota 5846  df-ov 5893  df-oprab 5894  df-mpo 5895  df-1st 6158  df-2nd 6159  df-recs 6323  df-irdg 6388  df-frec 6409  df-1o 6434  df-oadd 6438  df-er 6552  df-en 6758  df-dom 6759  df-fin 6760  df-sup 7000  df-pnf 8011  df-mnf 8012  df-xr 8013  df-ltxr 8014  df-le 8015  df-sub 8147  df-neg 8148  df-reap 8549  df-ap 8556  df-div 8647  df-inn 8937  df-2 8995  df-3 8996  df-4 8997  df-n0 9194  df-z 9271  df-uz 9546  df-q 9637  df-rp 9671  df-ico 9911  df-fz 10026  df-fzo 10160  df-seqfrec 10463  df-exp 10537  df-fac 10723  df-bc 10745  df-ihash 10773  df-cj 10868  df-re 10869  df-im 10870  df-rsqrt 11024  df-abs 11025  df-clim 11304  df-sumdc 11379  df-ef 11673
This theorem is referenced by:  efadd  11700
  Copyright terms: Public domain W3C validator