Theorem rpnnen2lem3

Description: Lemma for rpnnen2 . (Contributed by Mario Carneiro, 13-May-2013)

	Ref	Expression
Hypothesis	rpnnen2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
Assertion	rpnnen2lem3	⊢ seq 1 ( + , ( 𝐹 ‘ ℕ ) ) ⇝ ( 1 / 2 )

Proof

Step	Hyp	Ref	Expression
1		rpnnen2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
2		1re	⊢ 1 ∈ ℝ
3		3nn	⊢ 3 ∈ ℕ
4		nndivre	⊢ ( ( 1 ∈ ℝ ∧ 3 ∈ ℕ ) → ( 1 / 3 ) ∈ ℝ )
5	2 3 4	mp2an	⊢ ( 1 / 3 ) ∈ ℝ
6	5	recni	⊢ ( 1 / 3 ) ∈ ℂ
7	6	a1i	⊢ ( ⊤ → ( 1 / 3 ) ∈ ℂ )
8		0re	⊢ 0 ∈ ℝ
9		3re	⊢ 3 ∈ ℝ
10		3pos	⊢ 0 < 3
11	9 10	recgt0ii	⊢ 0 < ( 1 / 3 )
12	8 5 11	ltleii	⊢ 0 ≤ ( 1 / 3 )
13		absid	⊢ ( ( ( 1 / 3 ) ∈ ℝ ∧ 0 ≤ ( 1 / 3 ) ) → ( abs ‘ ( 1 / 3 ) ) = ( 1 / 3 ) )
14	5 12 13	mp2an	⊢ ( abs ‘ ( 1 / 3 ) ) = ( 1 / 3 )
15		1lt3	⊢ 1 < 3
16		recgt1	⊢ ( ( 3 ∈ ℝ ∧ 0 < 3 ) → ( 1 < 3 ↔ ( 1 / 3 ) < 1 ) )
17	9 10 16	mp2an	⊢ ( 1 < 3 ↔ ( 1 / 3 ) < 1 )
18	15 17	mpbi	⊢ ( 1 / 3 ) < 1
19	14 18	eqbrtri	⊢ ( abs ‘ ( 1 / 3 ) ) < 1
20	19	a1i	⊢ ( ⊤ → ( abs ‘ ( 1 / 3 ) ) < 1 )
21		1nn0	⊢ 1 ∈ ℕ0
22	21	a1i	⊢ ( ⊤ → 1 ∈ ℕ0 )
23		ssid	⊢ ℕ ⊆ ℕ
24		simpr	⊢ ( ( ⊤ ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
25		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
26	24 25	eleqtrrdi	⊢ ( ( ⊤ ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → 𝑘 ∈ ℕ )
27	1	rpnnen2lem1	⊢ ( ( ℕ ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℕ , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
28	23 26 27	sylancr	⊢ ( ( ⊤ ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℕ , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
29	26	iftrued	⊢ ( ( ⊤ ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → if ( 𝑘 ∈ ℕ , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) = ( ( 1 / 3 ) ↑ 𝑘 ) )
30	28 29	eqtrd	⊢ ( ( ⊤ ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) = ( ( 1 / 3 ) ↑ 𝑘 ) )
31	7 20 22 30	geolim2	⊢ ( ⊤ → seq 1 ( + , ( 𝐹 ‘ ℕ ) ) ⇝ ( ( ( 1 / 3 ) ↑ 1 ) / ( 1 − ( 1 / 3 ) ) ) )
32	31	mptru	⊢ seq 1 ( + , ( 𝐹 ‘ ℕ ) ) ⇝ ( ( ( 1 / 3 ) ↑ 1 ) / ( 1 − ( 1 / 3 ) ) )
33		exp1	⊢ ( ( 1 / 3 ) ∈ ℂ → ( ( 1 / 3 ) ↑ 1 ) = ( 1 / 3 ) )
34	6 33	ax-mp	⊢ ( ( 1 / 3 ) ↑ 1 ) = ( 1 / 3 )
35		3cn	⊢ 3 ∈ ℂ
36		ax-1cn	⊢ 1 ∈ ℂ
37		3ne0	⊢ 3 ≠ 0
38	35 37	pm3.2i	⊢ ( 3 ∈ ℂ ∧ 3 ≠ 0 )
39		divsubdir	⊢ ( ( 3 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( 3 − 1 ) / 3 ) = ( ( 3 / 3 ) − ( 1 / 3 ) ) )
40	35 36 38 39	mp3an	⊢ ( ( 3 − 1 ) / 3 ) = ( ( 3 / 3 ) − ( 1 / 3 ) )
41		3m1e2	⊢ ( 3 − 1 ) = 2
42	41	oveq1i	⊢ ( ( 3 − 1 ) / 3 ) = ( 2 / 3 )
43	35 37	dividi	⊢ ( 3 / 3 ) = 1
44	43	oveq1i	⊢ ( ( 3 / 3 ) − ( 1 / 3 ) ) = ( 1 − ( 1 / 3 ) )
45	40 42 44	3eqtr3ri	⊢ ( 1 − ( 1 / 3 ) ) = ( 2 / 3 )
46	34 45	oveq12i	⊢ ( ( ( 1 / 3 ) ↑ 1 ) / ( 1 − ( 1 / 3 ) ) ) = ( ( 1 / 3 ) / ( 2 / 3 ) )
47		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
48		divcan7	⊢ ( ( 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( 1 / 3 ) / ( 2 / 3 ) ) = ( 1 / 2 ) )
49	36 47 38 48	mp3an	⊢ ( ( 1 / 3 ) / ( 2 / 3 ) ) = ( 1 / 2 )
50	46 49	eqtri	⊢ ( ( ( 1 / 3 ) ↑ 1 ) / ( 1 − ( 1 / 3 ) ) ) = ( 1 / 2 )
51	32 50	breqtri	⊢ seq 1 ( + , ( 𝐹 ‘ ℕ ) ) ⇝ ( 1 / 2 )