Metamath Proof Explorer


Theorem lmconst

Description: A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007) (Revised by Mario Carneiro, 14-Nov-2013)

Ref Expression
Hypothesis lmconst.2 𝑍 = ( ℤ𝑀 )
Assertion lmconst ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) → ( 𝑍 × { 𝑃 } ) ( ⇝𝑡𝐽 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 lmconst.2 𝑍 = ( ℤ𝑀 )
2 simp2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) → 𝑃𝑋 )
3 simp3 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
4 uzid ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ𝑀 ) )
5 3 4 syl ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) → 𝑀 ∈ ( ℤ𝑀 ) )
6 5 1 eleqtrrdi ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) → 𝑀𝑍 )
7 idd ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) ∧ 𝑘 ∈ ( ℤ𝑀 ) ) → ( 𝑃𝑢𝑃𝑢 ) )
8 7 ralrimdva ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) → ( 𝑃𝑢 → ∀ 𝑘 ∈ ( ℤ𝑀 ) 𝑃𝑢 ) )
9 fveq2 ( 𝑗 = 𝑀 → ( ℤ𝑗 ) = ( ℤ𝑀 ) )
10 9 raleqdv ( 𝑗 = 𝑀 → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) 𝑃𝑢 ↔ ∀ 𝑘 ∈ ( ℤ𝑀 ) 𝑃𝑢 ) )
11 10 rspcev ( ( 𝑀𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑀 ) 𝑃𝑢 ) → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) 𝑃𝑢 )
12 6 8 11 syl6an ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) → ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) 𝑃𝑢 ) )
13 12 ralrimivw ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) → ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) 𝑃𝑢 ) )
14 simp1 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15 fconst6g ( 𝑃𝑋 → ( 𝑍 × { 𝑃 } ) : 𝑍𝑋 )
16 2 15 syl ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) → ( 𝑍 × { 𝑃 } ) : 𝑍𝑋 )
17 fvconst2g ( ( 𝑃𝑋𝑘𝑍 ) → ( ( 𝑍 × { 𝑃 } ) ‘ 𝑘 ) = 𝑃 )
18 2 17 sylan ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) ∧ 𝑘𝑍 ) → ( ( 𝑍 × { 𝑃 } ) ‘ 𝑘 ) = 𝑃 )
19 14 1 3 16 18 lmbrf ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) → ( ( 𝑍 × { 𝑃 } ) ( ⇝𝑡𝐽 ) 𝑃 ↔ ( 𝑃𝑋 ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) 𝑃𝑢 ) ) ) )
20 2 13 19 mpbir2and ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃𝑋𝑀 ∈ ℤ ) → ( 𝑍 × { 𝑃 } ) ( ⇝𝑡𝐽 ) 𝑃 )