Metamath Proof Explorer

Theorem rlimclim

Description: A sequence on an upper integer set converges in the real sense iff it converges in the integer sense. (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Hypotheses rlimclim.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
rlimclim.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
rlimclim.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
Assertion rlimclim ( 𝜑 → ( 𝐹 ⇝𝑟 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 rlimclim.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 rlimclim.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 rlimclim.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
4 2 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝐴 ) → 𝑀 ∈ ℤ )
5 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝐴 ) → 𝐹 ⇝𝑟 𝐴 )
6 fdm ⊢ ( 𝐹 : 𝑍 ⟶ ℂ → dom 𝐹 = 𝑍 )
7 eqimss2 ⊢ ( dom 𝐹 = 𝑍 → 𝑍 ⊆ dom 𝐹 )
8 3 6 7 3syl ⊢ ( 𝜑 → 𝑍 ⊆ dom 𝐹 )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝐴 ) → 𝑍 ⊆ dom 𝐹 )
10 1 4 5 9 rlimclim1 ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝐴 ) → 𝐹 ⇝ 𝐴 )
11 climcl ⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝐴 ∈ ℂ )
13 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
14 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
15 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
16 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → 𝐹 ⇝ 𝐴 )
17 1 13 14 15 16 climi2 ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 )
18 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
19 1 18 eqsstri ⊢ 𝑍 ⊆ ℤ
20 zssre ⊢ ℤ ⊆ ℝ
21 19 20 sstri ⊢ 𝑍 ⊆ ℝ
22 fveq2 ⊢ ( 𝑘 = 𝑤 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑤 ) )
23 22 fvoveq1d ⊢ ( 𝑘 = 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) )
24 23 breq1d ⊢ ( 𝑘 = 𝑤 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) )
25 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 )
26 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤 ) ) → 𝑧 ∈ 𝑍 )
27 19 26 sseldi ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤 ) ) → 𝑧 ∈ ℤ )
28 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤 ) ) → 𝑤 ∈ 𝑍 )
29 19 28 sseldi ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤 ) ) → 𝑤 ∈ ℤ )
30 simprr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤 ) ) → 𝑧 ≤ 𝑤 )
31 eluz2 ⊢ ( 𝑤 ∈ ( ℤ≥ ‘ 𝑧 ) ↔ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ 𝑧 ≤ 𝑤 ) )
32 27 29 30 31 syl3anbrc ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤 ) ) → 𝑤 ∈ ( ℤ≥ ‘ 𝑧 ) )
33 24 25 32 rspcdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 )
34 33 expr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ 𝑍 ) → ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) )
35 34 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) → ∀ 𝑤 ∈ 𝑍 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) )
36 35 expr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 → ∀ 𝑤 ∈ 𝑍 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) )
37 36 reximdva ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 → ∃ 𝑧 ∈ 𝑍 ∀ 𝑤 ∈ 𝑍 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) )
38 ssrexv ⊢ ( 𝑍 ⊆ ℝ → ( ∃ 𝑧 ∈ 𝑍 ∀ 𝑤 ∈ 𝑍 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑍 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) )
39 21 37 38 mpsylsyld ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑍 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) )
40 17 39 mpd ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑍 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) )
41 40 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑍 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) )
42 3 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 : 𝑍 ⟶ ℂ )
43 21 a1i ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝑍 ⊆ ℝ )
44 eqidd ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑤 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
45 42 43 44 rlim ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → ( 𝐹 ⇝𝑟 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑍 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) )
46 12 41 45 mpbir2and ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 ⇝𝑟 𝐴 )
47 10 46 impbida ⊢ ( 𝜑 → ( 𝐹 ⇝𝑟 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )