This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climlec2

Description: Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008) (Revised by Mario Carneiro, 1-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climlec2.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climlec2.3 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
climlec2.4 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐵 )
climlec2.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
climlec2.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ≤ ( 𝐹 ‘ 𝑘 ) )
Assertion climlec2 ( 𝜑 → 𝐴 ≤ 𝐵 )

Proof

Step Hyp Ref Expression
1 clim2ser.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climlec2.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climlec2.3 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4 climlec2.4 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐵 )
5 climlec2.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
6 climlec2.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ≤ ( 𝐹 ‘ 𝑘 ) )
7 3 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
8 0z ⊢ 0 ∈ ℤ
9 uzssz ⊢ ( ℤ≥ ‘ 0 ) ⊆ ℤ
10 zex ⊢ ℤ ∈ V
11 9 10 climconst2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℤ ) → ( ℤ × { 𝐴 } ) ⇝ 𝐴 )
12 7 8 11 sylancl ⊢ ( 𝜑 → ( ℤ × { 𝐴 } ) ⇝ 𝐴 )
13 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
14 13 1 eleq2s ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
15 fvconst2g ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℤ ) → ( ( ℤ × { 𝐴 } ) ‘ 𝑘 ) = 𝐴 )
16 3 14 15 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ℤ × { 𝐴 } ) ‘ 𝑘 ) = 𝐴 )
17 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
18 16 17 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ℤ × { 𝐴 } ) ‘ 𝑘 ) ∈ ℝ )
19 16 6 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ℤ × { 𝐴 } ) ‘ 𝑘 ) ≤ ( 𝐹 ‘ 𝑘 ) )
20 1 2 12 4 18 5 19 climle ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )