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	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )