Theorem geoisum1c

Description: The infinite sum of A x. ( R ^ 1 ) + A x. ( R ^ 2 ) ... is ( A x. R ) / ( 1 - R ) . (Contributed by NM, 2-Nov-2007) (Revised by Mario Carneiro, 26-Apr-2014)

	Ref	Expression
Assertion	geoisum1c	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → Σ 𝑘 ∈ ℕ ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) = ( ( 𝐴 · 𝑅 ) / ( 1 − 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → 𝐴 ∈ ℂ )
2		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → 𝑅 ∈ ℂ )
3		ax-1cn	⊢ 1 ∈ ℂ
4		subcl	⊢ ( ( 1 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( 1 − 𝑅 ) ∈ ℂ )
5	3 2 4	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( 1 − 𝑅 ) ∈ ℂ )
6		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( abs ‘ 𝑅 ) < 1 )
7		1re	⊢ 1 ∈ ℝ
8	7	ltnri	⊢ ¬ 1 < 1
9		abs1	⊢ ( abs ‘ 1 ) = 1
10		fveq2	⊢ ( 1 = 𝑅 → ( abs ‘ 1 ) = ( abs ‘ 𝑅 ) )
11	9 10	eqtr3id	⊢ ( 1 = 𝑅 → 1 = ( abs ‘ 𝑅 ) )
12	11	breq1d	⊢ ( 1 = 𝑅 → ( 1 < 1 ↔ ( abs ‘ 𝑅 ) < 1 ) )
13	8 12	mtbii	⊢ ( 1 = 𝑅 → ¬ ( abs ‘ 𝑅 ) < 1 )
14	13	necon2ai	⊢ ( ( abs ‘ 𝑅 ) < 1 → 1 ≠ 𝑅 )
15	6 14	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → 1 ≠ 𝑅 )
16		subeq0	⊢ ( ( 1 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( ( 1 − 𝑅 ) = 0 ↔ 1 = 𝑅 ) )
17	16	necon3bid	⊢ ( ( 1 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( ( 1 − 𝑅 ) ≠ 0 ↔ 1 ≠ 𝑅 ) )
18	3 2 17	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( ( 1 − 𝑅 ) ≠ 0 ↔ 1 ≠ 𝑅 ) )
19	15 18	mpbird	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( 1 − 𝑅 ) ≠ 0 )
20	1 2 5 19	divassd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( ( 𝐴 · 𝑅 ) / ( 1 − 𝑅 ) ) = ( 𝐴 · ( 𝑅 / ( 1 − 𝑅 ) ) ) )
21		geoisum1	⊢ ( ( 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → Σ 𝑘 ∈ ℕ ( 𝑅 ↑ 𝑘 ) = ( 𝑅 / ( 1 − 𝑅 ) ) )
22	21	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → Σ 𝑘 ∈ ℕ ( 𝑅 ↑ 𝑘 ) = ( 𝑅 / ( 1 − 𝑅 ) ) )
23	22	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( 𝐴 · Σ 𝑘 ∈ ℕ ( 𝑅 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑅 / ( 1 − 𝑅 ) ) ) )
24		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
25		1zzd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → 1 ∈ ℤ )
26		oveq2	⊢ ( 𝑛 = 𝑘 → ( 𝑅 ↑ 𝑛 ) = ( 𝑅 ↑ 𝑘 ) )
27		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) )
28		ovex	⊢ ( 𝑅 ↑ 𝑘 ) ∈ V
29	26 27 28	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝑅 ↑ 𝑘 ) )
30	29	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝑅 ↑ 𝑘 ) )
31		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
32		expcl	⊢ ( ( 𝑅 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 ↑ 𝑘 ) ∈ ℂ )
33	2 31 32	syl2an	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑅 ↑ 𝑘 ) ∈ ℂ )
34		1nn0	⊢ 1 ∈ ℕ0
35	34	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → 1 ∈ ℕ0 )
36		elnnuz	⊢ ( 𝑘 ∈ ℕ ↔ 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
37	36 30	sylan2br	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝑅 ↑ 𝑘 ) )
38	2 6 35 37	geolim2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ) ⇝ ( ( 𝑅 ↑ 1 ) / ( 1 − 𝑅 ) ) )
39		seqex	⊢ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ) ∈ V
40		ovex	⊢ ( ( 𝑅 ↑ 1 ) / ( 1 − 𝑅 ) ) ∈ V
41	39 40	breldm	⊢ ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ) ⇝ ( ( 𝑅 ↑ 1 ) / ( 1 − 𝑅 ) ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ) ∈ dom ⇝ )
42	38 41	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑅 ↑ 𝑛 ) ) ) ∈ dom ⇝ )
43	24 25 30 33 42 1	isummulc2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → ( 𝐴 · Σ 𝑘 ∈ ℕ ( 𝑅 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ℕ ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) )
44	20 23 43	3eqtr2rd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( abs ‘ 𝑅 ) < 1 ) → Σ 𝑘 ∈ ℕ ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) = ( ( 𝐴 · 𝑅 ) / ( 1 − 𝑅 ) ) )