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∈ℕ⟼ifn∈x13n0
Assertion rpnnen2lem5 ⊢A⊆ℕ∧M∈ℕ→seqM+F⁡A∈dom⁡⇝

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢F=x∈𝒫ℕ⟼n∈ℕ⟼ifn∈x13n0
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 ffvelcdmda ⊢A⊆ℕ∧k∈ℕ→F⁡ℕ⁡k∈ℝ
9 1 rpnnen2lem2 ⊢A⊆ℕ→F⁡A:ℕ⟶ℝ
10 9 ffvelcdmda ⊢A⊆ℕ∧k∈ℕ→F⁡A⁡k∈ℝ
11 1 rpnnen2lem3 ⊢seq1+F⁡ℕ⇝12
12 seqex ⊢seq1+F⁡ℕ∈V
13 ovex ⊢12∈V
14 12 13 breldm ⊢seq1+F⁡ℕ⇝12→seq1+F⁡ℕ∈dom⁡⇝
15 11 14 mp1i ⊢A⊆ℕ→seq1+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⊆ℕ→seq1+F⁡A∈dom⁡⇝
23 22 adantr ⊢A⊆ℕ∧M∈ℕ→seq1+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∈ℕ→seq1+F⁡A∈dom⁡⇝↔seqM+F⁡A∈dom⁡⇝
28 23 27 mpbid ⊢A⊆ℕ∧M∈ℕ→seqM+F⁡A∈dom⁡⇝