Theorem climlec3

Description: Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018)

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

Proof

Step	Hyp	Ref	Expression
1		climlec3.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climlec3.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climlec3.3	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4		climlec3.4	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
5		climlec3.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
6		climlec3.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ≤ 𝐵 )
7	3	renegcld	⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
8		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
9	1	fvexi	⊢ 𝑍 ∈ V
10	9	mptex	⊢ ( 𝑚 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑚 ) ) ∈ V
11	10	a1i	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑚 ) ) ∈ V )
12	5	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
13		eqid	⊢ ( 𝑚 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑚 ) ) = ( 𝑚 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑚 ) )
14		fveq2	⊢ ( 𝑚 = 𝑘 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑘 ) )
15	14	negeqd	⊢ ( 𝑚 = 𝑘 → - ( 𝐹 ‘ 𝑚 ) = - ( 𝐹 ‘ 𝑘 ) )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
17	5	renegcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → - ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
18	13 15 16 17	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑘 ) = - ( 𝐹 ‘ 𝑘 ) )
19		df-neg	⊢ - ( 𝐹 ‘ 𝑘 ) = ( 0 − ( 𝐹 ‘ 𝑘 ) )
20	18 19	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑘 ) = ( 0 − ( 𝐹 ‘ 𝑘 ) ) )
21	1 2 4 8 11 12 20	climsubc2	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑚 ) ) ⇝ ( 0 − 𝐴 ) )
22		df-neg	⊢ - 𝐴 = ( 0 − 𝐴 )
23	21 22	breqtrrdi	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑚 ) ) ⇝ - 𝐴 )
24	18 17	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑘 ) ∈ ℝ )
25	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
26	5 25	lenegd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) ≤ 𝐵 ↔ - 𝐵 ≤ - ( 𝐹 ‘ 𝑘 ) ) )
27	6 26	mpbid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → - 𝐵 ≤ - ( 𝐹 ‘ 𝑘 ) )
28	27 18	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → - 𝐵 ≤ ( ( 𝑚 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑘 ) )
29	1 2 7 23 24 28	climlec2	⊢ ( 𝜑 → - 𝐵 ≤ - 𝐴 )
30	1 2 4 5	climrecl	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
31	30 3	lenegd	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ - 𝐵 ≤ - 𝐴 ) )
32	29 31	mpbird	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )