Metamath Proof Explorer

Theorem rpnnen2lem5

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 rpnnen2lem5 ⊢ A ⊆ ℕ ∧ M ∈ ℕ → seq M + F ⁡ A ∈ dom ⁡ ⇝

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢ F = x ∈ 𝒫 ℕ ⟼ n ∈ ℕ ⟼ if n ∈ x 1 3 n 0
2 nnuz ⊢ ℕ = ℤ ≥ 1
3 1nn ⊢ 1 ∈ ℕ
4 3 a1i ⊢ A ⊆ ℕ → 1 ∈ ℕ
5 ssid ⊢ ℕ ⊆ ℕ
6 1 rpnnen2lem2 ⊢ ℕ ⊆ ℕ → F ⁡ ℕ : ℕ ⟶ ℝ
7 5 6 mp1i ⊢ A ⊆ ℕ → F ⁡ ℕ : ℕ ⟶ ℝ
8 7 ffvelrnda ⊢ A ⊆ ℕ ∧ k ∈ ℕ → F ⁡ ℕ ⁡ k ∈ ℝ
9 1 rpnnen2lem2 ⊢ A ⊆ ℕ → F ⁡ A : ℕ ⟶ ℝ
10 9 ffvelrnda ⊢ A ⊆ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k ∈ ℝ
11 1 rpnnen2lem3 ⊢ seq 1 + F ⁡ ℕ ⇝ 1 2
12 seqex ⊢ seq 1 + F ⁡ ℕ ∈ V
13 ovex ⊢ 1 2 ∈ V
14 12 13 breldm ⊢ seq 1 + F ⁡ ℕ ⇝ 1 2 → seq 1 + F ⁡ ℕ ∈ dom ⁡ ⇝
15 11 14 mp1i ⊢ A ⊆ ℕ → seq 1 + F ⁡ ℕ ∈ dom ⁡ ⇝
16 elnnuz ⊢ k ∈ ℕ ↔ k ∈ ℤ ≥ 1
17 1 rpnnen2lem4 ⊢ A ⊆ ℕ ∧ ℕ ⊆ ℕ ∧ k ∈ ℕ → 0 ≤ F ⁡ A ⁡ k ∧ F ⁡ A ⁡ k ≤ F ⁡ ℕ ⁡ k
18 5 17 mp3an2 ⊢ A ⊆ ℕ ∧ k ∈ ℕ → 0 ≤ F ⁡ A ⁡ k ∧ F ⁡ A ⁡ k ≤ F ⁡ ℕ ⁡ k
19 16 18 sylan2br ⊢ A ⊆ ℕ ∧ k ∈ ℤ ≥ 1 → 0 ≤ F ⁡ A ⁡ k ∧ F ⁡ A ⁡ k ≤ F ⁡ ℕ ⁡ k
20 19 simpld ⊢ A ⊆ ℕ ∧ k ∈ ℤ ≥ 1 → 0 ≤ F ⁡ A ⁡ k
21 19 simprd ⊢ A ⊆ ℕ ∧ k ∈ ℤ ≥ 1 → F ⁡ A ⁡ k ≤ F ⁡ ℕ ⁡ k
22 2 4 8 10 15 20 21 cvgcmp ⊢ A ⊆ ℕ → seq 1 + F ⁡ A ∈ dom ⁡ ⇝
23 22 adantr ⊢ A ⊆ ℕ ∧ M ∈ ℕ → seq 1 + F ⁡ A ∈ dom ⁡ ⇝
24 simpr ⊢ A ⊆ ℕ ∧ M ∈ ℕ → M ∈ ℕ
25 10 adantlr ⊢ A ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k ∈ ℝ
26 25 recnd ⊢ A ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k ∈ ℂ
27 2 24 26 iserex ⊢ A ⊆ ℕ ∧ M ∈ ℕ → seq 1 + F ⁡ A ∈ dom ⁡ ⇝ ↔ seq M + F ⁡ A ∈ dom ⁡ ⇝
28 23 27 mpbid ⊢ A ⊆ ℕ ∧ M ∈ ℕ → seq M + F ⁡ A ∈ dom ⁡ ⇝