This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )