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

Theorem efaddlem 11307
Description: Lemma for efadd 11308 (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 7753 . . 3 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
4 efadd.3 . . . 4 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛)))
54efcvg 11299 . . 3 ((𝐴 + 𝐵) ∈ ℂ → seq0( + , 𝐻) ⇝ (exp‘(𝐴 + 𝐵)))
63, 5syl 14 . 2 (𝜑 → seq0( + , 𝐻) ⇝ (exp‘(𝐴 + 𝐵)))
7 efadd.1 . . . . . 6 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) / (!‘𝑛)))
87eftvalcn 11290 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (𝐹𝑗) = ((𝐴𝑗) / (!‘𝑗)))
91, 8sylan 281 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐹𝑗) = ((𝐴𝑗) / (!‘𝑗)))
10 absexp 10819 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (abs‘(𝐴𝑗)) = ((abs‘𝐴)↑𝑗))
111, 10sylan 281 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (abs‘(𝐴𝑗)) = ((abs‘𝐴)↑𝑗))
12 faccl 10449 . . . . . . . 8 (𝑗 ∈ ℕ0 → (!‘𝑗) ∈ ℕ)
1312adantl 275 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑗) ∈ ℕ)
14 nnre 8695 . . . . . . . 8 ((!‘𝑗) ∈ ℕ → (!‘𝑗) ∈ ℝ)
15 nnnn0 8952 . . . . . . . . 9 ((!‘𝑗) ∈ ℕ → (!‘𝑗) ∈ ℕ0)
1615nn0ge0d 9001 . . . . . . . 8 ((!‘𝑗) ∈ ℕ → 0 ≤ (!‘𝑗))
1714, 16absidd 10907 . . . . . . 7 ((!‘𝑗) ∈ ℕ → (abs‘(!‘𝑗)) = (!‘𝑗))
1813, 17syl 14 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (abs‘(!‘𝑗)) = (!‘𝑗))
1911, 18oveq12d 5760 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((abs‘(𝐴𝑗)) / (abs‘(!‘𝑗))) = (((abs‘𝐴)↑𝑗) / (!‘𝑗)))
20 expcl 10279 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (𝐴𝑗) ∈ ℂ)
211, 20sylan 281 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝐴𝑗) ∈ ℂ)
2213nncnd 8702 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑗) ∈ ℂ)
2313nnap0d 8734 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑗) # 0)
2421, 22, 23absdivapd 10935 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (abs‘((𝐴𝑗) / (!‘𝑗))) = ((abs‘(𝐴𝑗)) / (abs‘(!‘𝑗))))
251abscld 10921 . . . . . . 7 (𝜑 → (abs‘𝐴) ∈ ℝ)
2625recnd 7762 . . . . . 6 (𝜑 → (abs‘𝐴) ∈ ℂ)
27 eqid 2117 . . . . . . 7 (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))
2827eftvalcn 11290 . . . . . 6 (((abs‘𝐴) ∈ ℂ ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))‘𝑗) = (((abs‘𝐴)↑𝑗) / (!‘𝑗)))
2926, 28sylan 281 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))‘𝑗) = (((abs‘𝐴)↑𝑗) / (!‘𝑗)))
3019, 24, 293eqtr4rd 2161 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))‘𝑗) = (abs‘((𝐴𝑗) / (!‘𝑗))))
31 eftcl 11287 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → ((𝐴𝑗) / (!‘𝑗)) ∈ ℂ)
321, 31sylan 281 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((𝐴𝑗) / (!‘𝑗)) ∈ ℂ)
33 efadd.2 . . . . . 6 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵𝑛) / (!‘𝑛)))
3433eftvalcn 11290 . . . . 5 ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = ((𝐵𝑘) / (!‘𝑘)))
352, 34sylan 281 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = ((𝐵𝑘) / (!‘𝑘)))
36 eftcl 11287 . . . . 5 ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐵𝑘) / (!‘𝑘)) ∈ ℂ)
372, 36sylan 281 . . . 4 ((𝜑𝑘 ∈ ℕ0) → ((𝐵𝑘) / (!‘𝑘)) ∈ ℂ)
384eftvalcn 11290 . . . . . 6 (((𝐴 + 𝐵) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐻𝑘) = (((𝐴 + 𝐵)↑𝑘) / (!‘𝑘)))
393, 38sylan 281 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = (((𝐴 + 𝐵)↑𝑘) / (!‘𝑘)))
401adantr 274 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → 𝐴 ∈ ℂ)
412adantr 274 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
42 simpr 109 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
43 binom 11221 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑘) = Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))))
4440, 41, 42, 43syl3anc 1201 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑘) = Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))))
4544oveq1d 5757 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (((𝐴 + 𝐵)↑𝑘) / (!‘𝑘)) = (Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)))
46 0zd 9034 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 0 ∈ ℤ)
4742nn0zd 9139 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
4846, 47fzfigd 10172 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (0...𝑘) ∈ Fin)
49 faccl 10449 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
5049adantl 275 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℕ)
5150nncnd 8702 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℂ)
52 bccl2 10482 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑘) → (𝑘C𝑗) ∈ ℕ)
5352adantl 275 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘C𝑗) ∈ ℕ)
5453nncnd 8702 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘C𝑗) ∈ ℂ)
551ad2antrr 479 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝐴 ∈ ℂ)
56 fznn0sub 9805 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑘) → (𝑘𝑗) ∈ ℕ0)
5756adantl 275 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘𝑗) ∈ ℕ0)
5855, 57expcld 10392 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴↑(𝑘𝑗)) ∈ ℂ)
592ad2antrr 479 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝐵 ∈ ℂ)
60 elfznn0 9862 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑘) → 𝑗 ∈ ℕ0)
6160adantl 275 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝑗 ∈ ℕ0)
6259, 61expcld 10392 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐵𝑗) ∈ ℂ)
6358, 62mulcld 7754 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝐴↑(𝑘𝑗)) · (𝐵𝑗)) ∈ ℂ)
6454, 63mulcld 7754 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) ∈ ℂ)
6550nnap0d 8734 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (!‘𝑘) # 0)
6648, 51, 64, 65fsumdivapc 11187 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)) = Σ𝑗 ∈ (0...𝑘)(((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)))
6755, 61expcld 10392 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴𝑗) ∈ ℂ)
6861, 12syl 14 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑗) ∈ ℕ)
6968nncnd 8702 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑗) ∈ ℂ)
7068nnap0d 8734 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑗) # 0)
7167, 69, 70divclapd 8518 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝐴𝑗) / (!‘𝑗)) ∈ ℂ)
7233eftvalcn 11290 . . . . . . . . . . . 12 ((𝐵 ∈ ℂ ∧ (𝑘𝑗) ∈ ℕ0) → (𝐺‘(𝑘𝑗)) = ((𝐵↑(𝑘𝑗)) / (!‘(𝑘𝑗))))
7359, 57, 72syl2anc 408 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘𝑗)) = ((𝐵↑(𝑘𝑗)) / (!‘(𝑘𝑗))))
7459, 57expcld 10392 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐵↑(𝑘𝑗)) ∈ ℂ)
75 faccl 10449 . . . . . . . . . . . . . 14 ((𝑘𝑗) ∈ ℕ0 → (!‘(𝑘𝑗)) ∈ ℕ)
7657, 75syl 14 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘(𝑘𝑗)) ∈ ℕ)
7776nncnd 8702 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘(𝑘𝑗)) ∈ ℂ)
7876nnap0d 8734 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘(𝑘𝑗)) # 0)
7974, 77, 78divclapd 8518 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝐵↑(𝑘𝑗)) / (!‘(𝑘𝑗))) ∈ ℂ)
8073, 79eqeltrd 2194 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘𝑗)) ∈ ℂ)
8171, 80mulcld 7754 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))) ∈ ℂ)
82 oveq2 5750 . . . . . . . . . . 11 (𝑗 = ((0 + 𝑘) − 𝑚) → (𝐴𝑗) = (𝐴↑((0 + 𝑘) − 𝑚)))
83 fveq2 5389 . . . . . . . . . . 11 (𝑗 = ((0 + 𝑘) − 𝑚) → (!‘𝑗) = (!‘((0 + 𝑘) − 𝑚)))
8482, 83oveq12d 5760 . . . . . . . . . 10 (𝑗 = ((0 + 𝑘) − 𝑚) → ((𝐴𝑗) / (!‘𝑗)) = ((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))))
85 oveq2 5750 . . . . . . . . . . 11 (𝑗 = ((0 + 𝑘) − 𝑚) → (𝑘𝑗) = (𝑘 − ((0 + 𝑘) − 𝑚)))
8685fveq2d 5393 . . . . . . . . . 10 (𝑗 = ((0 + 𝑘) − 𝑚) → (𝐺‘(𝑘𝑗)) = (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚))))
8784, 86oveq12d 5760 . . . . . . . . 9 (𝑗 = ((0 + 𝑘) − 𝑚) → (((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))) = (((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚)))))
8846, 47, 81, 87fisumrev2 11183 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑘)(((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))) = Σ𝑚 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚)))))
8933eftvalcn 11290 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (𝐺𝑗) = ((𝐵𝑗) / (!‘𝑗)))
9059, 61, 89syl2anc 408 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺𝑗) = ((𝐵𝑗) / (!‘𝑗)))
9190oveq2d 5758 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))) · (𝐺𝑗)) = (((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))) · ((𝐵𝑗) / (!‘𝑗))))
9276, 68nnmulcld 8737 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((!‘(𝑘𝑗)) · (!‘𝑗)) ∈ ℕ)
9392nncnd 8702 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((!‘(𝑘𝑗)) · (!‘𝑗)) ∈ ℂ)
9477, 69, 78, 70mulap0d 8387 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((!‘(𝑘𝑗)) · (!‘𝑗)) # 0)
9563, 93, 94divrecap2d 8522 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑(𝑘𝑗)) · (𝐵𝑗)) / ((!‘(𝑘𝑗)) · (!‘𝑗))) = ((1 / ((!‘(𝑘𝑗)) · (!‘𝑗))) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))))
9658, 77, 62, 69, 78, 70divmuldivapd 8560 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))) · ((𝐵𝑗) / (!‘𝑗))) = (((𝐴↑(𝑘𝑗)) · (𝐵𝑗)) / ((!‘(𝑘𝑗)) · (!‘𝑗))))
97 bcval2 10464 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑘) → (𝑘C𝑗) = ((!‘𝑘) / ((!‘(𝑘𝑗)) · (!‘𝑗))))
9897adantl 275 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘C𝑗) = ((!‘𝑘) / ((!‘(𝑘𝑗)) · (!‘𝑗))))
9998oveq1d 5757 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝑘C𝑗) / (!‘𝑘)) = (((!‘𝑘) / ((!‘(𝑘𝑗)) · (!‘𝑗))) / (!‘𝑘)))
10051adantr 274 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑘) ∈ ℂ)
10165adantr 274 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑘) # 0)
102100, 93, 100, 94, 101divdiv32apd 8544 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((!‘𝑘) / ((!‘(𝑘𝑗)) · (!‘𝑗))) / (!‘𝑘)) = (((!‘𝑘) / (!‘𝑘)) / ((!‘(𝑘𝑗)) · (!‘𝑗))))
103100, 101dividapd 8514 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((!‘𝑘) / (!‘𝑘)) = 1)
104103oveq1d 5757 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((!‘𝑘) / (!‘𝑘)) / ((!‘(𝑘𝑗)) · (!‘𝑗))) = (1 / ((!‘(𝑘𝑗)) · (!‘𝑗))))
105102, 104eqtrd 2150 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((!‘𝑘) / ((!‘(𝑘𝑗)) · (!‘𝑗))) / (!‘𝑘)) = (1 / ((!‘(𝑘𝑗)) · (!‘𝑗))))
10699, 105eqtrd 2150 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝑘C𝑗) / (!‘𝑘)) = (1 / ((!‘(𝑘𝑗)) · (!‘𝑗))))
107106oveq1d 5757 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝑘C𝑗) / (!‘𝑘)) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) = ((1 / ((!‘(𝑘𝑗)) · (!‘𝑗))) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))))
10895, 96, 1073eqtr4rd 2161 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝑘C𝑗) / (!‘𝑘)) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) = (((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))) · ((𝐵𝑗) / (!‘𝑗))))
10991, 108eqtr4d 2153 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))) · (𝐺𝑗)) = (((𝑘C𝑗) / (!‘𝑘)) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))))
110 nn0cn 8955 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
111110ad2antlr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝑘 ∈ ℂ)
112111addid2d 7880 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (0 + 𝑘) = 𝑘)
113112oveq1d 5757 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((0 + 𝑘) − 𝑗) = (𝑘𝑗))
114113oveq2d 5758 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴↑((0 + 𝑘) − 𝑗)) = (𝐴↑(𝑘𝑗)))
115113fveq2d 5393 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘((0 + 𝑘) − 𝑗)) = (!‘(𝑘𝑗)))
116114, 115oveq12d 5760 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) = ((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))))
117113oveq2d 5758 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − ((0 + 𝑘) − 𝑗)) = (𝑘 − (𝑘𝑗)))
118 nn0cn 8955 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0𝑗 ∈ ℂ)
11961, 118syl 14 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝑗 ∈ ℂ)
120111, 119nncand 8046 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − (𝑘𝑗)) = 𝑗)
121117, 120eqtrd 2150 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − ((0 + 𝑘) − 𝑗)) = 𝑗)
122121fveq2d 5393 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗))) = (𝐺𝑗))
123116, 122oveq12d 5760 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))) = (((𝐴↑(𝑘𝑗)) / (!‘(𝑘𝑗))) · (𝐺𝑗)))
12454, 63, 100, 101div23apd 8556 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)) = (((𝑘C𝑗) / (!‘𝑘)) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))))
125109, 123, 1243eqtr4rd 2161 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)) = (((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))))
126125sumeq2dv 11105 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑘)(((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)) = Σ𝑗 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))))
127 oveq2 5750 . . . . . . . . . . . . 13 (𝑗 = 𝑚 → ((0 + 𝑘) − 𝑗) = ((0 + 𝑘) − 𝑚))
128127oveq2d 5758 . . . . . . . . . . . 12 (𝑗 = 𝑚 → (𝐴↑((0 + 𝑘) − 𝑗)) = (𝐴↑((0 + 𝑘) − 𝑚)))
129127fveq2d 5393 . . . . . . . . . . . 12 (𝑗 = 𝑚 → (!‘((0 + 𝑘) − 𝑗)) = (!‘((0 + 𝑘) − 𝑚)))
130128, 129oveq12d 5760 . . . . . . . . . . 11 (𝑗 = 𝑚 → ((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) = ((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))))
131127oveq2d 5758 . . . . . . . . . . . 12 (𝑗 = 𝑚 → (𝑘 − ((0 + 𝑘) − 𝑗)) = (𝑘 − ((0 + 𝑘) − 𝑚)))
132131fveq2d 5393 . . . . . . . . . . 11 (𝑗 = 𝑚 → (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗))) = (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚))))
133130, 132oveq12d 5760 . . . . . . . . . 10 (𝑗 = 𝑚 → (((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))) = (((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚)))))
134133cbvsumv 11098 . . . . . . . . 9 Σ𝑗 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))) = Σ𝑚 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚))))
135126, 134syl6eq 2166 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑘)(((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)) = Σ𝑚 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚)))))
13688, 135eqtr4d 2153 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑘)(((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))) = Σ𝑗 ∈ (0...𝑘)(((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)))
13766, 136eqtr4d 2153 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘𝑗)) · (𝐵𝑗))) / (!‘𝑘)) = Σ𝑗 ∈ (0...𝑘)(((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))))
13845, 137eqtrd 2150 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (((𝐴 + 𝐵)↑𝑘) / (!‘𝑘)) = Σ𝑗 ∈ (0...𝑘)(((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))))
13939, 138eqtrd 2150 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = Σ𝑗 ∈ (0...𝑘)(((𝐴𝑗) / (!‘𝑗)) · (𝐺‘(𝑘𝑗))))
14027efcllem 11292 . . . . 5 ((abs‘𝐴) ∈ ℂ → seq0( + , (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))) ∈ dom ⇝ )
14126, 140syl 14 . . . 4 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))) ∈ dom ⇝ )
14233efcllem 11292 . . . . 5 (𝐵 ∈ ℂ → seq0( + , 𝐺) ∈ dom ⇝ )
1432, 142syl 14 . . . 4 (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
1447efcllem 11292 . . . . 5 (𝐴 ∈ ℂ → seq0( + , 𝐹) ∈ dom ⇝ )
1451, 144syl 14 . . . 4 (𝜑 → seq0( + , 𝐹) ∈ dom ⇝ )
1469, 30, 32, 35, 37, 139, 141, 143, 145mertensabs 11274 . . 3 (𝜑 → seq0( + , 𝐻) ⇝ (Σ𝑗 ∈ ℕ0 ((𝐴𝑗) / (!‘𝑗)) · Σ𝑘 ∈ ℕ0 ((𝐵𝑘) / (!‘𝑘))))
147 efval 11294 . . . . 5 (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑗 ∈ ℕ0 ((𝐴𝑗) / (!‘𝑗)))
1481, 147syl 14 . . . 4 (𝜑 → (exp‘𝐴) = Σ𝑗 ∈ ℕ0 ((𝐴𝑗) / (!‘𝑗)))
149 efval 11294 . . . . 5 (𝐵 ∈ ℂ → (exp‘𝐵) = Σ𝑘 ∈ ℕ0 ((𝐵𝑘) / (!‘𝑘)))
1502, 149syl 14 . . . 4 (𝜑 → (exp‘𝐵) = Σ𝑘 ∈ ℕ0 ((𝐵𝑘) / (!‘𝑘)))
151148, 150oveq12d 5760 . . 3 (𝜑 → ((exp‘𝐴) · (exp‘𝐵)) = (Σ𝑗 ∈ ℕ0 ((𝐴𝑗) / (!‘𝑗)) · Σ𝑘 ∈ ℕ0 ((𝐵𝑘) / (!‘𝑘))))
152146, 151breqtrrd 3926 . 2 (𝜑 → seq0( + , 𝐻) ⇝ ((exp‘𝐴) · (exp‘𝐵)))
153 climuni 11030 . 2 ((seq0( + , 𝐻) ⇝ (exp‘(𝐴 + 𝐵)) ∧ seq0( + , 𝐻) ⇝ ((exp‘𝐴) · (exp‘𝐵))) → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵)))
1546, 152, 153syl2anc 408 1 (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1316  wcel 1465   class class class wbr 3899  cmpt 3959  dom cdm 4509  cfv 5093  (class class class)co 5742  cc 7586  0cc0 7588  1c1 7589   + caddc 7591   · cmul 7593  cmin 7901   # cap 8311   / cdiv 8400  cn 8688  0cn0 8945  ...cfz 9758  seqcseq 10186  cexp 10260  !cfa 10439  Ccbc 10461  abscabs 10737  cli 11015  Σcsu 11090  expce 11275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-coll 4013  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-iinf 4472  ax-cnex 7679  ax-resscn 7680  ax-1cn 7681  ax-1re 7682  ax-icn 7683  ax-addcl 7684  ax-addrcl 7685  ax-mulcl 7686  ax-mulrcl 7687  ax-addcom 7688  ax-mulcom 7689  ax-addass 7690  ax-mulass 7691  ax-distr 7692  ax-i2m1 7693  ax-0lt1 7694  ax-1rid 7695  ax-0id 7696  ax-rnegex 7697  ax-precex 7698  ax-cnre 7699  ax-pre-ltirr 7700  ax-pre-ltwlin 7701  ax-pre-lttrn 7702  ax-pre-apti 7703  ax-pre-ltadd 7704  ax-pre-mulgt0 7705  ax-pre-mulext 7706  ax-arch 7707  ax-caucvg 7708
This theorem depends on definitions:  df-bi 116  df-dc 805  df-3or 948  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-nel 2381  df-ral 2398  df-rex 2399  df-reu 2400  df-rmo 2401  df-rab 2402  df-v 2662  df-sbc 2883  df-csb 2976  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-if 3445  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-int 3742  df-iun 3785  df-disj 3877  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-id 4185  df-po 4188  df-iso 4189  df-iord 4258  df-on 4260  df-ilim 4261  df-suc 4263  df-iom 4475  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-isom 5102  df-riota 5698  df-ov 5745  df-oprab 5746  df-mpo 5747  df-1st 6006  df-2nd 6007  df-recs 6170  df-irdg 6235  df-frec 6256  df-1o 6281  df-oadd 6285  df-er 6397  df-en 6603  df-dom 6604  df-fin 6605  df-sup 6839  df-pnf 7770  df-mnf 7771  df-xr 7772  df-ltxr 7773  df-le 7774  df-sub 7903  df-neg 7904  df-reap 8305  df-ap 8312  df-div 8401  df-inn 8689  df-2 8747  df-3 8748  df-4 8749  df-n0 8946  df-z 9023  df-uz 9295  df-q 9380  df-rp 9410  df-ico 9645  df-fz 9759  df-fzo 9888  df-seqfrec 10187  df-exp 10261  df-fac 10440  df-bc 10462  df-ihash 10490  df-cj 10582  df-re 10583  df-im 10584  df-rsqrt 10738  df-abs 10739  df-clim 11016  df-sumdc 11091  df-ef 11281
This theorem is referenced by:  efadd  11308
  Copyright terms: Public domain W3C validator