Mathbox for Steve Rodriguez |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > binomcxplemcvg | Structured version Visualization version GIF version |
Description: Lemma for binomcxp 42214. The sum in binomcxplemnn0 42206 and its derivative (see the next theorem, binomcxplemdvsum 42212) converge, as long as their base 𝐽 is within the disk of convergence. Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
Ref | Expression |
---|---|
binomcxp.a | ⊢ (𝜑 → 𝐴 ∈ ℝ+) |
binomcxp.b | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
binomcxp.lt | ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) |
binomcxp.c | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
binomcxplem.f | ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) |
binomcxplem.s | ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) |
binomcxplem.r | ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) |
binomcxplem.e | ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) |
binomcxplem.d | ⊢ 𝐷 = (◡abs “ (0[,)𝑅)) |
Ref | Expression |
---|---|
binomcxplemcvg | ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → (seq0( + , (𝑆‘𝐽)) ∈ dom ⇝ ∧ seq1( + , (𝐸‘𝐽)) ∈ dom ⇝ )) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | binomcxplem.s | . . 3 ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) | |
2 | binomcxp.c | . . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
3 | 2 | adantr 481 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐶 ∈ ℂ) |
4 | simpr 485 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0) | |
5 | 3, 4 | bcccl 42196 | . . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐶C𝑐𝑗) ∈ ℂ) |
6 | binomcxplem.f | . . . . 5 ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) | |
7 | 5, 6 | fmptd 7027 | . . . 4 ⊢ (𝜑 → 𝐹:ℕ0⟶ℂ) |
8 | 7 | adantr 481 | . . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → 𝐹:ℕ0⟶ℂ) |
9 | binomcxplem.r | . . 3 ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) | |
10 | binomcxplem.d | . . . . . . 7 ⊢ 𝐷 = (◡abs “ (0[,)𝑅)) | |
11 | 10 | eleq2i 2828 | . . . . . 6 ⊢ (𝐽 ∈ 𝐷 ↔ 𝐽 ∈ (◡abs “ (0[,)𝑅))) |
12 | absf 15125 | . . . . . . 7 ⊢ abs:ℂ⟶ℝ | |
13 | ffn 6637 | . . . . . . 7 ⊢ (abs:ℂ⟶ℝ → abs Fn ℂ) | |
14 | elpreima 6974 | . . . . . . 7 ⊢ (abs Fn ℂ → (𝐽 ∈ (◡abs “ (0[,)𝑅)) ↔ (𝐽 ∈ ℂ ∧ (abs‘𝐽) ∈ (0[,)𝑅)))) | |
15 | 12, 13, 14 | mp2b 10 | . . . . . 6 ⊢ (𝐽 ∈ (◡abs “ (0[,)𝑅)) ↔ (𝐽 ∈ ℂ ∧ (abs‘𝐽) ∈ (0[,)𝑅))) |
16 | 11, 15 | bitri 274 | . . . . 5 ⊢ (𝐽 ∈ 𝐷 ↔ (𝐽 ∈ ℂ ∧ (abs‘𝐽) ∈ (0[,)𝑅))) |
17 | 16 | simplbi 498 | . . . 4 ⊢ (𝐽 ∈ 𝐷 → 𝐽 ∈ ℂ) |
18 | 17 | adantl 482 | . . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → 𝐽 ∈ ℂ) |
19 | 16 | simprbi 497 | . . . . 5 ⊢ (𝐽 ∈ 𝐷 → (abs‘𝐽) ∈ (0[,)𝑅)) |
20 | 0re 11056 | . . . . . . 7 ⊢ 0 ∈ ℝ | |
21 | ssrab2 4023 | . . . . . . . . . 10 ⊢ {𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ } ⊆ ℝ | |
22 | ressxr 11098 | . . . . . . . . . 10 ⊢ ℝ ⊆ ℝ* | |
23 | 21, 22 | sstri 3939 | . . . . . . . . 9 ⊢ {𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ } ⊆ ℝ* |
24 | supxrcl 13128 | . . . . . . . . 9 ⊢ ({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ } ⊆ ℝ* → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*) | |
25 | 23, 24 | ax-mp 5 | . . . . . . . 8 ⊢ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ* |
26 | 9, 25 | eqeltri 2833 | . . . . . . 7 ⊢ 𝑅 ∈ ℝ* |
27 | elico2 13222 | . . . . . . 7 ⊢ ((0 ∈ ℝ ∧ 𝑅 ∈ ℝ*) → ((abs‘𝐽) ∈ (0[,)𝑅) ↔ ((abs‘𝐽) ∈ ℝ ∧ 0 ≤ (abs‘𝐽) ∧ (abs‘𝐽) < 𝑅))) | |
28 | 20, 26, 27 | mp2an 689 | . . . . . 6 ⊢ ((abs‘𝐽) ∈ (0[,)𝑅) ↔ ((abs‘𝐽) ∈ ℝ ∧ 0 ≤ (abs‘𝐽) ∧ (abs‘𝐽) < 𝑅)) |
29 | 28 | simp3bi 1146 | . . . . 5 ⊢ ((abs‘𝐽) ∈ (0[,)𝑅) → (abs‘𝐽) < 𝑅) |
30 | 19, 29 | syl 17 | . . . 4 ⊢ (𝐽 ∈ 𝐷 → (abs‘𝐽) < 𝑅) |
31 | 30 | adantl 482 | . . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → (abs‘𝐽) < 𝑅) |
32 | 1, 8, 9, 18, 31 | radcnvlt2 25658 | . 2 ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → seq0( + , (𝑆‘𝐽)) ∈ dom ⇝ ) |
33 | binomcxplem.e | . . . . . . 7 ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) | |
34 | 33 | a1i 11 | . . . . . 6 ⊢ ((𝜑 ∧ 𝐽 ∈ ℂ) → 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))))) |
35 | simplr 766 | . . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐽 ∈ ℂ) ∧ 𝑏 = 𝐽) ∧ 𝑘 ∈ ℕ) → 𝑏 = 𝐽) | |
36 | 35 | oveq1d 7331 | . . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐽 ∈ ℂ) ∧ 𝑏 = 𝐽) ∧ 𝑘 ∈ ℕ) → (𝑏↑(𝑘 − 1)) = (𝐽↑(𝑘 − 1))) |
37 | 36 | oveq2d 7332 | . . . . . . 7 ⊢ ((((𝜑 ∧ 𝐽 ∈ ℂ) ∧ 𝑏 = 𝐽) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))) = ((𝑘 · (𝐹‘𝑘)) · (𝐽↑(𝑘 − 1)))) |
38 | 37 | mpteq2dva 5186 | . . . . . 6 ⊢ (((𝜑 ∧ 𝐽 ∈ ℂ) ∧ 𝑏 = 𝐽) → (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1)))) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝐽↑(𝑘 − 1))))) |
39 | simpr 485 | . . . . . 6 ⊢ ((𝜑 ∧ 𝐽 ∈ ℂ) → 𝐽 ∈ ℂ) | |
40 | nnex 12058 | . . . . . . . 8 ⊢ ℕ ∈ V | |
41 | 40 | mptex 7138 | . . . . . . 7 ⊢ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝐽↑(𝑘 − 1)))) ∈ V |
42 | 41 | a1i 11 | . . . . . 6 ⊢ ((𝜑 ∧ 𝐽 ∈ ℂ) → (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝐽↑(𝑘 − 1)))) ∈ V) |
43 | 34, 38, 39, 42 | fvmptd 6921 | . . . . 5 ⊢ ((𝜑 ∧ 𝐽 ∈ ℂ) → (𝐸‘𝐽) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝐽↑(𝑘 − 1))))) |
44 | 17, 43 | sylan2 593 | . . . 4 ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → (𝐸‘𝐽) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝐽↑(𝑘 − 1))))) |
45 | 44 | seqeq3d 13808 | . . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → seq1( + , (𝐸‘𝐽)) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝐽↑(𝑘 − 1)))))) |
46 | eqid 2736 | . . . 4 ⊢ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝐽↑(𝑘 − 1)))) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝐽↑(𝑘 − 1)))) | |
47 | 1, 9, 46, 8, 18, 31 | dvradcnv2 42204 | . . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝐽↑(𝑘 − 1))))) ∈ dom ⇝ ) |
48 | 45, 47 | eqeltrd 2837 | . 2 ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → seq1( + , (𝐸‘𝐽)) ∈ dom ⇝ ) |
49 | 32, 48 | jca 512 | 1 ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → (seq0( + , (𝑆‘𝐽)) ∈ dom ⇝ ∧ seq1( + , (𝐸‘𝐽)) ∈ dom ⇝ )) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 {crab 3403 Vcvv 3440 ⊆ wss 3896 class class class wbr 5086 ↦ cmpt 5169 ◡ccnv 5606 dom cdm 5607 “ cima 5610 Fn wfn 6460 ⟶wf 6461 ‘cfv 6465 (class class class)co 7316 supcsup 9275 ℂcc 10948 ℝcr 10949 0cc0 10950 1c1 10951 + caddc 10953 · cmul 10955 ℝ*cxr 11087 < clt 11088 ≤ cle 11089 − cmin 11284 ℕcn 12052 ℕ0cn0 12312 ℝ+crp 12809 [,)cico 13160 seqcseq 13800 ↑cexp 13861 abscabs 15021 ⇝ cli 15269 C𝑐cbcc 42193 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5223 ax-sep 5237 ax-nul 5244 ax-pow 5302 ax-pr 5366 ax-un 7629 ax-inf2 9476 ax-cnex 11006 ax-resscn 11007 ax-1cn 11008 ax-icn 11009 ax-addcl 11010 ax-addrcl 11011 ax-mulcl 11012 ax-mulrcl 11013 ax-mulcom 11014 ax-addass 11015 ax-mulass 11016 ax-distr 11017 ax-i2m1 11018 ax-1ne0 11019 ax-1rid 11020 ax-rnegex 11021 ax-rrecex 11022 ax-cnre 11023 ax-pre-lttri 11024 ax-pre-lttrn 11025 ax-pre-ltadd 11026 ax-pre-mulgt0 11027 ax-pre-sup 11028 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3349 df-reu 3350 df-rab 3404 df-v 3442 df-sbc 3726 df-csb 3842 df-dif 3899 df-un 3901 df-in 3903 df-ss 3913 df-pss 3915 df-nul 4267 df-if 4471 df-pw 4546 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4850 df-int 4892 df-iun 4938 df-br 5087 df-opab 5149 df-mpt 5170 df-tr 5204 df-id 5506 df-eprel 5512 df-po 5520 df-so 5521 df-fr 5562 df-se 5563 df-we 5564 df-xp 5613 df-rel 5614 df-cnv 5615 df-co 5616 df-dm 5617 df-rn 5618 df-res 5619 df-ima 5620 df-pred 6224 df-ord 6291 df-on 6292 df-lim 6293 df-suc 6294 df-iota 6417 df-fun 6467 df-fn 6468 df-f 6469 df-f1 6470 df-fo 6471 df-f1o 6472 df-fv 6473 df-isom 6474 df-riota 7273 df-ov 7319 df-oprab 7320 df-mpo 7321 df-om 7759 df-1st 7877 df-2nd 7878 df-frecs 8145 df-wrecs 8176 df-recs 8250 df-rdg 8289 df-1o 8345 df-er 8547 df-pm 8667 df-en 8783 df-dom 8784 df-sdom 8785 df-fin 8786 df-sup 9277 df-inf 9278 df-oi 9345 df-card 9774 df-pnf 11090 df-mnf 11091 df-xr 11092 df-ltxr 11093 df-le 11094 df-sub 11286 df-neg 11287 df-div 11712 df-nn 12053 df-2 12115 df-3 12116 df-n0 12313 df-z 12399 df-uz 12662 df-rp 12810 df-ico 13164 df-icc 13165 df-fz 13319 df-fzo 13462 df-fl 13591 df-seq 13801 df-exp 13862 df-fac 14067 df-hash 14124 df-shft 14854 df-cj 14886 df-re 14887 df-im 14888 df-sqrt 15022 df-abs 15023 df-limsup 15256 df-clim 15273 df-rlim 15274 df-sum 15474 df-prod 15692 df-fallfac 15793 df-bcc 42194 |
This theorem is referenced by: binomcxplemnotnn0 42213 |
Copyright terms: Public domain | W3C validator |