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