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 ⊢ F = x ∈ 𝒫 ℕ ⟼ n ∈ ℕ ⟼ if n ∈ x 1 3 n 0
Assertion rpnnen2lem9 ⊢ M ∈ ℕ → ∑ k ∈ ℤ ≥ M F ⁡ ℕ ∖ M ⁡ k = 0 + 1 3 M + 1 1 − 1 3

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢ F = x ∈ 𝒫 ℕ ⟼ n ∈ ℕ ⟼ if n ∈ x 1 3 n 0
2 eqid ⊢ ℤ ≥ M = ℤ ≥ M
3 nnz ⊢ M ∈ ℕ → M ∈ ℤ
4 eqidd ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M → F ⁡ ℕ ∖ M ⁡ k = F ⁡ ℕ ∖ M ⁡ k
5 eluznn ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M → k ∈ ℕ
6 difss ⊢ ℕ ∖ M ⊆ ℕ
7 1 rpnnen2lem2 ⊢ ℕ ∖ M ⊆ ℕ → F ⁡ ℕ ∖ M : ℕ ⟶ ℝ
8 6 7 ax-mp ⊢ F ⁡ ℕ ∖ M : ℕ ⟶ ℝ
9 8 ffvelcdmi ⊢ k ∈ ℕ → F ⁡ ℕ ∖ M ⁡ k ∈ ℝ
10 9 recnd ⊢ k ∈ ℕ → F ⁡ ℕ ∖ M ⁡ k ∈ ℂ
11 5 10 syl ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M → F ⁡ ℕ ∖ M ⁡ k ∈ ℂ
12 1 rpnnen2lem5 ⊢ ℕ ∖ M ⊆ ℕ ∧ M ∈ ℕ → seq M + F ⁡ ℕ ∖ M ∈ dom ⁡ ⇝
13 6 12 mpan ⊢ M ∈ ℕ → seq M + F ⁡ ℕ ∖ M ∈ dom ⁡ ⇝
14 2 3 4 11 13 isum1p ⊢ M ∈ ℕ → ∑ k ∈ ℤ ≥ M F ⁡ ℕ ∖ M ⁡ k = F ⁡ ℕ ∖ M ⁡ M + ∑ k ∈ ℤ ≥ M + 1 F ⁡ ℕ ∖ M ⁡ k
15 1 rpnnen2lem1 ⊢ ℕ ∖ M ⊆ ℕ ∧ M ∈ ℕ → F ⁡ ℕ ∖ M ⁡ M = if M ∈ ℕ ∖ M 1 3 M 0
16 6 15 mpan ⊢ M ∈ ℕ → F ⁡ ℕ ∖ M ⁡ M = if M ∈ ℕ ∖ M 1 3 M 0
17 neldifsnd ⊢ M ∈ ℕ → ¬ M ∈ ℕ ∖ M
18 17 iffalsed ⊢ M ∈ ℕ → if M ∈ ℕ ∖ M 1 3 M 0 = 0
19 16 18 eqtrd ⊢ M ∈ ℕ → F ⁡ ℕ ∖ M ⁡ M = 0
20 eqid ⊢ ℤ ≥ M + 1 = ℤ ≥ M + 1
21 peano2nn ⊢ M ∈ ℕ → M + 1 ∈ ℕ
22 21 nnzd ⊢ M ∈ ℕ → M + 1 ∈ ℤ
23 eqidd ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → F ⁡ ℕ ∖ M ⁡ k = F ⁡ ℕ ∖ M ⁡ k
24 eluznn ⊢ M + 1 ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → k ∈ ℕ
25 21 24 sylan ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → k ∈ ℕ
26 25 10 syl ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → F ⁡ ℕ ∖ M ⁡ k ∈ ℂ
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 ⊢ M ∈ ℕ → 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 → 1 3 = 1 3
39 30 37 38 mp2an ⊢ 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 ⊢ 1 3 < 1
45 44 a1i ⊢ M ∈ ℕ → 1 3 < 1
46 21 nnnn0d ⊢ M ∈ ℕ → M + 1 ∈ ℕ 0
47 1 rpnnen2lem1 ⊢ ℕ ∖ M ⊆ ℕ ∧ k ∈ ℕ → F ⁡ ℕ ∖ M ⁡ k = if k ∈ ℕ ∖ M 1 3 k 0
48 6 47 mpan ⊢ k ∈ ℕ → F ⁡ ℕ ∖ M ⁡ k = if k ∈ ℕ ∖ M 1 3 k 0
49 25 48 syl ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → F ⁡ ℕ ∖ M ⁡ k = if k ∈ ℕ ∖ M 1 3 k 0
50 nnre ⊢ M ∈ ℕ → M ∈ ℝ
51 50 adantr ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → M ∈ ℝ
52 eluzle ⊢ k ∈ ℤ ≥ M + 1 → M + 1 ≤ k
53 52 adantl ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → M + 1 ≤ k
54 nnltp1le ⊢ M ∈ ℕ ∧ k ∈ ℕ → M < k ↔ M + 1 ≤ k
55 25 54 syldan ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → M < k ↔ M + 1 ≤ k
56 53 55 mpbird ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → M < k
57 51 56 gtned ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → k ≠ M
58 eldifsn ⊢ k ∈ ℕ ∖ M ↔ k ∈ ℕ ∧ k ≠ M
59 25 57 58 sylanbrc ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → k ∈ ℕ ∖ M
60 59 iftrued ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → if k ∈ ℕ ∖ M 1 3 k 0 = 1 3 k
61 49 60 eqtrd ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M + 1 → F ⁡ ℕ ∖ M ⁡ k = 1 3 k
62 32 45 46 61 geolim2 ⊢ M ∈ ℕ → seq M + 1 + F ⁡ ℕ ∖ M ⇝ 1 3 M + 1 1 − 1 3
63 20 22 23 26 62 isumclim ⊢ M ∈ ℕ → ∑ k ∈ ℤ ≥ M + 1 F ⁡ ℕ ∖ M ⁡ k = 1 3 M + 1 1 − 1 3
64 19 63 oveq12d ⊢ M ∈ ℕ → F ⁡ ℕ ∖ M ⁡ M + ∑ k ∈ ℤ ≥ M + 1 F ⁡ ℕ ∖ M ⁡ k = 0 + 1 3 M + 1 1 − 1 3
65 14 64 eqtrd ⊢ M ∈ ℕ → ∑ k ∈ ℤ ≥ M F ⁡ ℕ ∖ M ⁡ k = 0 + 1 3 M + 1 1 − 1 3