Metamath Proof Explorer

Theorem rpnnen2lem10

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

Ref Expression
Hypotheses rpnnen2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
rpnnen2.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
rpnnen2.3 ⊢ ( 𝜑 → 𝐵 ⊆ ℕ )
rpnnen2.4 ⊢ ( 𝜑 → 𝑚 ∈ ( 𝐴 ∖ 𝐵 ) )
rpnnen2.5 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵 ) ) )
rpnnen2.6 ⊢ ( 𝜓 ↔ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) )
Assertion rpnnen2lem10 ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) )

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
2 rpnnen2.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
3 rpnnen2.3 ⊢ ( 𝜑 → 𝐵 ⊆ ℕ )
4 rpnnen2.4 ⊢ ( 𝜑 → 𝑚 ∈ ( 𝐴 ∖ 𝐵 ) )
5 rpnnen2.5 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵 ) ) )
6 rpnnen2.6 ⊢ ( 𝜓 ↔ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) )
7 6 bilani ⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) )
8 eldifi ⊢ ( 𝑚 ∈ ( 𝐴 ∖ 𝐵 ) → 𝑚 ∈ 𝐴 )
9 ssel2 ⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑚 ∈ 𝐴 ) → 𝑚 ∈ ℕ )
10 8 9 sylan2 ⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑚 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝑚 ∈ ℕ )
11 2 4 10 syl2anc ⊢ ( 𝜑 → 𝑚 ∈ ℕ )
12 1 rpnnen2lem8 ⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ) )
13 2 11 12 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ) )
14 1z ⊢ 1 ∈ ℤ
15 nnz ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
16 elfzm11 ⊢ ( ( 1 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ↔ ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑚 ) ) )
17 14 15 16 sylancr ⊢ ( 𝑚 ∈ ℕ → ( 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ↔ ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑚 ) ) )
18 17 biimpa ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑚 ) )
19 11 18 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ∧ 𝑘 < 𝑚 ) )
20 19 simp3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ) → 𝑘 < 𝑚 )
21 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) → 𝑘 ∈ ℕ )
22 breq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 < 𝑚 ↔ 𝑘 < 𝑚 ) )
23 eleq1w ⊢ ( 𝑛 = 𝑘 → ( 𝑛 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴 ) )
24 eleq1w ⊢ ( 𝑛 = 𝑘 → ( 𝑛 ∈ 𝐵 ↔ 𝑘 ∈ 𝐵 ) )
25 23 24 bibi12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵 ) ↔ ( 𝑘 ∈ 𝐴 ↔ 𝑘 ∈ 𝐵 ) ) )
26 22 25 imbi12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵 ) ) ↔ ( 𝑘 < 𝑚 → ( 𝑘 ∈ 𝐴 ↔ 𝑘 ∈ 𝐵 ) ) ) )
27 26 rspccva ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 < 𝑚 → ( 𝑘 ∈ 𝐴 ↔ 𝑘 ∈ 𝐵 ) ) )
28 5 21 27 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ) → ( 𝑘 < 𝑚 → ( 𝑘 ∈ 𝐴 ↔ 𝑘 ∈ 𝐵 ) ) )
29 20 28 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ) → ( 𝑘 ∈ 𝐴 ↔ 𝑘 ∈ 𝐵 ) )
30 29 ifbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ) → if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) = if ( 𝑘 ∈ 𝐵 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
31 1 rpnnen2lem1 ⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
32 2 21 31 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
33 1 rpnnen2lem1 ⊢ ( ( 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐵 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
34 3 21 33 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐵 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
35 30 32 34 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) )
36 35 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) )
37 36 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ) )
38 13 37 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ) )
40 1 rpnnen2lem8 ⊢ ( ( 𝐵 ⊆ ℕ ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) )
41 3 11 40 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) )
43 7 39 42 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) )
44 1 rpnnen2lem6 ⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℝ )
45 2 11 44 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℝ )
46 1 rpnnen2lem6 ⊢ ( ( 𝐵 ⊆ ℕ ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
47 3 11 46 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
48 fzfid ⊢ ( 𝜑 → ( 1 ... ( 𝑚 − 1 ) ) ∈ Fin )
49 1 rpnnen2lem2 ⊢ ( 𝐵 ⊆ ℕ → ( 𝐹 ‘ 𝐵 ) : ℕ ⟶ ℝ )
50 3 49 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) : ℕ ⟶ ℝ )
51 ffvelcdm ⊢ ( ( ( 𝐹 ‘ 𝐵 ) : ℕ ⟶ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
52 50 21 51 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
53 48 52 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
54 readdcan ⊢ ( ( Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℝ ∧ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ ∧ Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ ) → ( ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) ↔ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) )
55 45 47 53 54 syl3anc ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) ↔ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝑚 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) ↔ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) )
57 43 56 mpbid ⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) )