Metamath Proof Explorer

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 ⊢Z=ℤ≥M
climlec3.2 ⊢φ→M∈ℤ
climlec3.3 ⊢φ→B∈ℝ
climlec3.4 ⊢φ→F⇝A
climlec3.5 ⊢φ∧k∈Z→F⁡k∈ℝ
climlec3.6 ⊢φ∧k∈Z→F⁡k≤B
Assertion climlec3 ⊢φ→A≤B

Proof

Step Hyp Ref Expression
1 climlec3.1 ⊢Z=ℤ≥M
2 climlec3.2 ⊢φ→M∈ℤ
3 climlec3.3 ⊢φ→B∈ℝ
4 climlec3.4 ⊢φ→F⇝A
5 climlec3.5 ⊢φ∧k∈Z→F⁡k∈ℝ
6 climlec3.6 ⊢φ∧k∈Z→F⁡k≤B
7 3 renegcld ⊢φ→−B∈ℝ
8 0cnd ⊢φ→0∈ℂ
9 1 fvexi ⊢Z∈V
10 9 mptex ⊢m∈Z⟼−F⁡m∈V
11 10 a1i ⊢φ→m∈Z⟼−F⁡m∈V
12 5 recnd ⊢φ∧k∈Z→F⁡k∈ℂ
13 eqid ⊢m∈Z⟼−F⁡m=m∈Z⟼−F⁡m
14 fveq2 ⊢m=k→F⁡m=F⁡k
15 14 negeqd ⊢m=k→−F⁡m=−F⁡k
16 simpr ⊢φ∧k∈Z→k∈Z
17 5 renegcld ⊢φ∧k∈Z→−F⁡k∈ℝ
18 13 15 16 17 fvmptd3 ⊢φ∧k∈Z→m∈Z⟼−F⁡m⁡k=−F⁡k
19 df-neg ⊢−F⁡k=0−F⁡k
20 18 19 eqtrdi ⊢φ∧k∈Z→m∈Z⟼−F⁡m⁡k=0−F⁡k
21 1 2 4 8 11 12 20 climsubc2 ⊢φ→m∈Z⟼−F⁡m⇝0−A
22 df-neg ⊢−A=0−A
23 21 22 breqtrrdi ⊢φ→m∈Z⟼−F⁡m⇝−A
24 18 17 eqeltrd ⊢φ∧k∈Z→m∈Z⟼−F⁡m⁡k∈ℝ
25 3 adantr ⊢φ∧k∈Z→B∈ℝ
26 5 25 lenegd ⊢φ∧k∈Z→F⁡k≤B↔−B≤−F⁡k
27 6 26 mpbid ⊢φ∧k∈Z→−B≤−F⁡k
28 27 18 breqtrrd ⊢φ∧k∈Z→−B≤m∈Z⟼−F⁡m⁡k
29 1 2 7 23 24 28 climlec2 ⊢φ→−B≤−A
30 1 2 4 5 climrecl ⊢φ→A∈ℝ
31 30 3 lenegd ⊢φ→A≤B↔−B≤−A
32 29 31 mpbird ⊢φ→A≤B