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	sselid	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤 ) ) → 𝑧 ∈ ℤ )
28		simprl	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑧 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤 ) ) → 𝑤 ∈ 𝑍 )
29	19 28	sselid	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑧 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑧 ) ( 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	⊢ ( 𝜑 → ( 𝐹 ⇝_𝑟 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )

Metamath Proof Explorer

Theorem rlimclim

Proof