Theorem geo2lim 14813

Description: The value of the infinite geometric series 2↑-1 + 2↑-2 +... , multiplied by a constant. (Contributed by Mario Carneiro, 15-Jun-2014.)

Hypothesis

Ref	Expression
geo2lim.1	⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘)))

Assertion

Ref	Expression
geo2lim	⊢ (𝐴 ∈ ℂ → seq1( + , 𝐹) ⇝ 𝐴)

Distinct variable group:   𝐴,𝑘

Allowed substitution hint:   𝐹(𝑘)

Proof of Theorem geo2lim

Dummy variables 𝑗 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 11925	. . 3 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 11610	. . 3 ⊢ (𝐴 ∈ ℂ → 1 ∈ ℤ)
3		halfcn 11449	. . . . . . 7 ⊢ (1 / 2) ∈ ℂ
4	3	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (1 / 2) ∈ ℂ)
5		halfre 11448	. . . . . . . . 9 ⊢ (1 / 2) ∈ ℝ
6		0re 10242	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
7		halfgt0 11450	. . . . . . . . . 10 ⊢ 0 < (1 / 2)
8	6, 5, 7	ltleii 10362	. . . . . . . . 9 ⊢ 0 ≤ (1 / 2)
9		absid 14244	. . . . . . . . 9 ⊢ (((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 / 2))
10	5, 8, 9	mp2an 672	. . . . . . . 8 ⊢ (abs‘(1 / 2)) = (1 / 2)
11		halflt1 11452	. . . . . . . 8 ⊢ (1 / 2) < 1
12	10, 11	eqbrtri 4807	. . . . . . 7 ⊢ (abs‘(1 / 2)) < 1
13	12	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (abs‘(1 / 2)) < 1)
14	4, 13	expcnv 14803	. . . . 5 ⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℕ0 ↦ ((1 / 2)↑𝑘)) ⇝ 0)
15		id 22	. . . . 5 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
16		geo2lim.1	. . . . . . 7 ⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘)))
17		nnex 11228	. . . . . . . 8 ⊢ ℕ ∈ V
18	17	mptex 6630	. . . . . . 7 ⊢ (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘))) ∈ V
19	16, 18	eqeltri 2846	. . . . . 6 ⊢ 𝐹 ∈ V
20	19	a1i 11	. . . . 5 ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ V)
21		nnnn0 11501	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ0)
22	21	adantl 467	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0)
23		oveq2 6801	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → ((1 / 2)↑𝑘) = ((1 / 2)↑𝑗))
24		eqid 2771	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 ↦ ((1 / 2)↑𝑘)) = (𝑘 ∈ ℕ0 ↦ ((1 / 2)↑𝑘))
25		ovex 6823	. . . . . . . . 9 ⊢ ((1 / 2)↑𝑗) ∈ V
26	23, 24, 25	fvmpt 6424	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((1 / 2)↑𝑘))‘𝑗) = ((1 / 2)↑𝑗))
27	22, 26	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ ((1 / 2)↑𝑘))‘𝑗) = ((1 / 2)↑𝑗))
28		nnz 11601	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
29	28	adantl 467	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
30		2cn 11293	. . . . . . . . 9 ⊢ 2 ∈ ℂ
31		2ne0 11315	. . . . . . . . 9 ⊢ 2 ≠ 0
32		exprec 13108	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 𝑗 ∈ ℤ) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗)))
33	30, 31, 32	mp3an12 1562	. . . . . . . 8 ⊢ (𝑗 ∈ ℤ → ((1 / 2)↑𝑗) = (1 / (2↑𝑗)))
34	29, 33	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗)))
35	27, 34	eqtrd 2805	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ ((1 / 2)↑𝑘))‘𝑗) = (1 / (2↑𝑗)))
36		2nn 11387	. . . . . . . . 9 ⊢ 2 ∈ ℕ
37		nnexpcl 13080	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2↑𝑗) ∈ ℕ)
38	36, 22, 37	sylancr 575	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈ ℕ)
39	38	nnrecred 11268	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (1 / (2↑𝑗)) ∈ ℝ)
40	39	recnd 10270	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (1 / (2↑𝑗)) ∈ ℂ)
41	35, 40	eqeltrd 2850	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ ((1 / 2)↑𝑘))‘𝑗) ∈ ℂ)
42		simpl 468	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ ℂ)
43	38	nncnd 11238	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈ ℂ)
44	38	nnne0d 11267	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ≠ 0)
45	42, 43, 44	divrecd 11006	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 / (2↑𝑗)) = (𝐴 · (1 / (2↑𝑗))))
46		oveq2 6801	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (2↑𝑘) = (2↑𝑗))
47	46	oveq2d 6809	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (𝐴 / (2↑𝑘)) = (𝐴 / (2↑𝑗)))
48		ovex 6823	. . . . . . . 8 ⊢ (𝐴 / (2↑𝑗)) ∈ V
49	47, 16, 48	fvmpt 6424	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = (𝐴 / (2↑𝑗)))
50	49	adantl 467	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (𝐴 / (2↑𝑗)))
51	35	oveq2d 6809	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 · ((𝑘 ∈ ℕ0 ↦ ((1 / 2)↑𝑘))‘𝑗)) = (𝐴 · (1 / (2↑𝑗))))
52	45, 50, 51	3eqtr4d 2815	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (𝐴 · ((𝑘 ∈ ℕ0 ↦ ((1 / 2)↑𝑘))‘𝑗)))
53	1, 2, 14, 15, 20, 41, 52	climmulc2 14575	. . . 4 ⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ (𝐴 · 0))
54		mul01 10417	. . . 4 ⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
55	53, 54	breqtrd 4812	. . 3 ⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ 0)
56		seqex 13010	. . . 4 ⊢ seq1( + , 𝐹) ∈ V
57	56	a1i 11	. . 3 ⊢ (𝐴 ∈ ℂ → seq1( + , 𝐹) ∈ V)
58	42, 43, 44	divcld 11003	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 / (2↑𝑗)) ∈ ℂ)
59	50, 58	eqeltrd 2850	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℂ)
60	50	oveq2d 6809	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 − (𝐹‘𝑗)) = (𝐴 − (𝐴 / (2↑𝑗))))
61		geo2sum 14811	. . . . 5 ⊢ ((𝑗 ∈ ℕ ∧ 𝐴 ∈ ℂ) → Σ𝑛 ∈ (1...𝑗)(𝐴 / (2↑𝑛)) = (𝐴 − (𝐴 / (2↑𝑗))))
62	61	ancoms 455	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → Σ𝑛 ∈ (1...𝑗)(𝐴 / (2↑𝑛)) = (𝐴 − (𝐴 / (2↑𝑗))))
63		elfznn 12577	. . . . . . 7 ⊢ (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
64	63	adantl 467	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ)
65		oveq2 6801	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛))
66	65	oveq2d 6809	. . . . . . 7 ⊢ (𝑘 = 𝑛 → (𝐴 / (2↑𝑘)) = (𝐴 / (2↑𝑛)))
67		ovex 6823	. . . . . . 7 ⊢ (𝐴 / (2↑𝑛)) ∈ V
68	66, 16, 67	fvmpt 6424	. . . . . 6 ⊢ (𝑛 ∈ ℕ → (𝐹‘𝑛) = (𝐴 / (2↑𝑛)))
69	64, 68	syl 17	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐹‘𝑛) = (𝐴 / (2↑𝑛)))
70		simpr 471	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
71	70, 1	syl6eleq 2860	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ≥‘1))
72		simpll 750	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝐴 ∈ ℂ)
73		nnnn0 11501	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
74		nnexpcl 13080	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
75	36, 73, 74	sylancr 575	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
76	64, 75	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2↑𝑛) ∈ ℕ)
77	76	nncnd 11238	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2↑𝑛) ∈ ℂ)
78	76	nnne0d 11267	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2↑𝑛) ≠ 0)
79	72, 77, 78	divcld 11003	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐴 / (2↑𝑛)) ∈ ℂ)
80	69, 71, 79	fsumser 14669	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → Σ𝑛 ∈ (1...𝑗)(𝐴 / (2↑𝑛)) = (seq1( + , 𝐹)‘𝑗))
81	60, 62, 80	3eqtr2rd 2812	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘𝑗) = (𝐴 − (𝐹‘𝑗)))
82	1, 2, 55, 15, 57, 59, 81	climsubc2 14577	. 2 ⊢ (𝐴 ∈ ℂ → seq1( + , 𝐹) ⇝ (𝐴 − 0))
83		subid1 10503	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
84	82, 83	breqtrd 4812	1 ⊢ (𝐴 ∈ ℂ → seq1( + , 𝐹) ⇝ 𝐴)

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  Vcvv 3351   class class class wbr 4786   ↦ cmpt 4863  ‘cfv 6031  (class class class)co 6793  ℂcc 10136  ℝcr 10137  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143   < clt 10276   ≤ cle 10277   − cmin 10468   / cdiv 10886  ℕcn 11222  2c2 11272  ℕ₀cn0 11494  ℤcz 11579  ℤ_≥cuz 11888  ...cfz 12533  seqcseq 13008  ↑cexp 13067  abscabs 14182   ⇝ cli 14423  Σcsu 14624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-rp 12036  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-rlim 14428  df-sum 14625

This theorem is referenced by:  omssubadd  30702  sge0ad2en  41165