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