Metamath Proof Explorer

Theorem rpnnen2lem9

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

Ref Expression
Hypothesis rpnnen2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
Assertion rpnnen2lem9 ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) = ( 0 + ( ( ( 1 / 3 ) ↑ ( 𝑀 + 1 ) ) / ( 1 − ( 1 / 3 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
2 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
3 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
4 eqidd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) )
5 eluznn ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ )
6 difss ⊢ ( ℕ ∖ { 𝑀 } ) ⊆ ℕ
7 1 rpnnen2lem2 ⊢ ( ( ℕ ∖ { 𝑀 } ) ⊆ ℕ → ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) : ℕ ⟶ ℝ )
8 6 7 ax-mp ⊢ ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) : ℕ ⟶ ℝ
9 8 ffvelcdmi ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) ∈ ℝ )
10 9 recnd ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) ∈ ℂ )
11 5 10 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) ∈ ℂ )
12 1 rpnnen2lem5 ⊢ ( ( ( ℕ ∖ { 𝑀 } ) ⊆ ℕ ∧ 𝑀 ∈ ℕ ) → seq 𝑀 ( + , ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ) ∈ dom ⇝ )
13 6 12 mpan ⊢ ( 𝑀 ∈ ℕ → seq 𝑀 ( + , ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ) ∈ dom ⇝ )
14 2 3 4 11 13 isum1p ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) = ( ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑀 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) ) )
15 1 rpnnen2lem1 ⊢ ( ( ( ℕ ∖ { 𝑀 } ) ⊆ ℕ ∧ 𝑀 ∈ ℕ ) → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑀 ) = if ( 𝑀 ∈ ( ℕ ∖ { 𝑀 } ) , ( ( 1 / 3 ) ↑ 𝑀 ) , 0 ) )
16 6 15 mpan ⊢ ( 𝑀 ∈ ℕ → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑀 ) = if ( 𝑀 ∈ ( ℕ ∖ { 𝑀 } ) , ( ( 1 / 3 ) ↑ 𝑀 ) , 0 ) )
17 neldifsnd ⊢ ( 𝑀 ∈ ℕ → ¬ 𝑀 ∈ ( ℕ ∖ { 𝑀 } ) )
18 17 iffalsed ⊢ ( 𝑀 ∈ ℕ → if ( 𝑀 ∈ ( ℕ ∖ { 𝑀 } ) , ( ( 1 / 3 ) ↑ 𝑀 ) , 0 ) = 0 )
19 16 18 eqtrd ⊢ ( 𝑀 ∈ ℕ → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑀 ) = 0 )
20 eqid ⊢ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) = ( ℤ≥ ‘ ( 𝑀 + 1 ) )
21 peano2nn ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 + 1 ) ∈ ℕ )
22 21 nnzd ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 + 1 ) ∈ ℤ )
23 eqidd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) )
24 eluznn ⊢ ( ( ( 𝑀 + 1 ) ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑘 ∈ ℕ )
25 21 24 sylan ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑘 ∈ ℕ )
26 25 10 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) ∈ ℂ )
27 1re ⊢ 1 ∈ ℝ
28 3nn ⊢ 3 ∈ ℕ
29 nndivre ⊢ ( ( 1 ∈ ℝ ∧ 3 ∈ ℕ ) → ( 1 / 3 ) ∈ ℝ )
30 27 28 29 mp2an ⊢ ( 1 / 3 ) ∈ ℝ
31 30 recni ⊢ ( 1 / 3 ) ∈ ℂ
32 31 a1i ⊢ ( 𝑀 ∈ ℕ → ( 1 / 3 ) ∈ ℂ )
33 0re ⊢ 0 ∈ ℝ
34 3re ⊢ 3 ∈ ℝ
35 3pos ⊢ 0 < 3
36 34 35 recgt0ii ⊢ 0 < ( 1 / 3 )
37 33 30 36 ltleii ⊢ 0 ≤ ( 1 / 3 )
38 absid ⊢ ( ( ( 1 / 3 ) ∈ ℝ ∧ 0 ≤ ( 1 / 3 ) ) → ( abs ‘ ( 1 / 3 ) ) = ( 1 / 3 ) )
39 30 37 38 mp2an ⊢ ( abs ‘ ( 1 / 3 ) ) = ( 1 / 3 )
40 1lt3 ⊢ 1 < 3
41 recgt1 ⊢ ( ( 3 ∈ ℝ ∧ 0 < 3 ) → ( 1 < 3 ↔ ( 1 / 3 ) < 1 ) )
42 34 35 41 mp2an ⊢ ( 1 < 3 ↔ ( 1 / 3 ) < 1 )
43 40 42 mpbi ⊢ ( 1 / 3 ) < 1
44 39 43 eqbrtri ⊢ ( abs ‘ ( 1 / 3 ) ) < 1
45 44 a1i ⊢ ( 𝑀 ∈ ℕ → ( abs ‘ ( 1 / 3 ) ) < 1 )
46 21 nnnn0d ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 + 1 ) ∈ ℕ0 )
47 1 rpnnen2lem1 ⊢ ( ( ( ℕ ∖ { 𝑀 } ) ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( ℕ ∖ { 𝑀 } ) , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
48 6 47 mpan ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( ℕ ∖ { 𝑀 } ) , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
49 25 48 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( ℕ ∖ { 𝑀 } ) , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
50 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
51 50 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑀 ∈ ℝ )
52 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝑀 + 1 ) ≤ 𝑘 )
53 52 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑀 + 1 ) ≤ 𝑘 )
54 nnltp1le ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑀 < 𝑘 ↔ ( 𝑀 + 1 ) ≤ 𝑘 ) )
55 25 54 syldan ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑀 < 𝑘 ↔ ( 𝑀 + 1 ) ≤ 𝑘 ) )
56 53 55 mpbird ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑀 < 𝑘 )
57 51 56 gtned ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑘 ≠ 𝑀 )
58 eldifsn ⊢ ( 𝑘 ∈ ( ℕ ∖ { 𝑀 } ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ≠ 𝑀 ) )
59 25 57 58 sylanbrc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑘 ∈ ( ℕ ∖ { 𝑀 } ) )
60 59 iftrued ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → if ( 𝑘 ∈ ( ℕ ∖ { 𝑀 } ) , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) = ( ( 1 / 3 ) ↑ 𝑘 ) )
61 49 60 eqtrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) = ( ( 1 / 3 ) ↑ 𝑘 ) )
62 32 45 46 61 geolim2 ⊢ ( 𝑀 ∈ ℕ → seq ( 𝑀 + 1 ) ( + , ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ) ⇝ ( ( ( 1 / 3 ) ↑ ( 𝑀 + 1 ) ) / ( 1 − ( 1 / 3 ) ) ) )
63 20 22 23 26 62 isumclim ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) = ( ( ( 1 / 3 ) ↑ ( 𝑀 + 1 ) ) / ( 1 − ( 1 / 3 ) ) ) )
64 19 63 oveq12d ⊢ ( 𝑀 ∈ ℕ → ( ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑀 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) ) = ( 0 + ( ( ( 1 / 3 ) ↑ ( 𝑀 + 1 ) ) / ( 1 − ( 1 / 3 ) ) ) ) )
65 14 64 eqtrd ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( ( 𝐹 ‘ ( ℕ ∖ { 𝑀 } ) ) ‘ 𝑘 ) = ( 0 + ( ( ( 1 / 3 ) ↑ ( 𝑀 + 1 ) ) / ( 1 − ( 1 / 3 ) ) ) ) )