Metamath Proof Explorer

Theorem climinf2lem

Description: A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses climinf2lem.1 ⊢ Z = ℤ ≥ M
climinf2lem.2 ⊢ φ → M ∈ ℤ
climinf2lem.3 ⊢ φ → F : Z ⟶ ℝ
climinf2lem.4 ⊢ φ ∧ k ∈ Z → F ⁡ k + 1 ≤ F ⁡ k
climinf2lem.5 ⊢ φ → ∃ x ∈ ℝ ∀ k ∈ Z x ≤ F ⁡ k
Assertion climinf2lem ⊢ φ → F ⇝ inf ran ⁡ F ℝ * <

Proof

Step Hyp Ref Expression
1 climinf2lem.1 ⊢ Z = ℤ ≥ M
2 climinf2lem.2 ⊢ φ → M ∈ ℤ
3 climinf2lem.3 ⊢ φ → F : Z ⟶ ℝ
4 climinf2lem.4 ⊢ φ ∧ k ∈ Z → F ⁡ k + 1 ≤ F ⁡ k
5 climinf2lem.5 ⊢ φ → ∃ x ∈ ℝ ∀ k ∈ Z x ≤ F ⁡ k
6 1 2 3 4 5 climinf ⊢ φ → F ⇝ inf ran ⁡ F ℝ <
7 3 frnd ⊢ φ → ran ⁡ F ⊆ ℝ
8 3 ffnd ⊢ φ → F Fn Z
9 2 1 uzidd2 ⊢ φ → M ∈ Z
10 fnfvelrn ⊢ F Fn Z ∧ M ∈ Z → F ⁡ M ∈ ran ⁡ F
11 8 9 10 syl2anc ⊢ φ → F ⁡ M ∈ ran ⁡ F
12 11 ne0d ⊢ φ → ran ⁡ F ≠ ∅
13 simpr ⊢ φ ∧ y ∈ ran ⁡ F → y ∈ ran ⁡ F
14 fvelrnb ⊢ F Fn Z → y ∈ ran ⁡ F ↔ ∃ k ∈ Z F ⁡ k = y
15 8 14 syl ⊢ φ → y ∈ ran ⁡ F ↔ ∃ k ∈ Z F ⁡ k = y
16 15 adantr ⊢ φ ∧ y ∈ ran ⁡ F → y ∈ ran ⁡ F ↔ ∃ k ∈ Z F ⁡ k = y
17 13 16 mpbid ⊢ φ ∧ y ∈ ran ⁡ F → ∃ k ∈ Z F ⁡ k = y
18 17 adantlr ⊢ φ ∧ ∀ k ∈ Z x ≤ F ⁡ k ∧ y ∈ ran ⁡ F → ∃ k ∈ Z F ⁡ k = y
19 nfv ⊢ Ⅎ k φ
20 nfra1 ⊢ Ⅎ k ∀ k ∈ Z x ≤ F ⁡ k
21 19 20 nfan ⊢ Ⅎ k φ ∧ ∀ k ∈ Z x ≤ F ⁡ k
22 nfv ⊢ Ⅎ k x ≤ y
23 rspa ⊢ ∀ k ∈ Z x ≤ F ⁡ k ∧ k ∈ Z → x ≤ F ⁡ k
24 simpl ⊢ x ≤ F ⁡ k ∧ F ⁡ k = y → x ≤ F ⁡ k
25 simpr ⊢ x ≤ F ⁡ k ∧ F ⁡ k = y → F ⁡ k = y
26 24 25 breqtrd ⊢ x ≤ F ⁡ k ∧ F ⁡ k = y → x ≤ y
27 26 ex ⊢ x ≤ F ⁡ k → F ⁡ k = y → x ≤ y
28 23 27 syl ⊢ ∀ k ∈ Z x ≤ F ⁡ k ∧ k ∈ Z → F ⁡ k = y → x ≤ y
29 28 ex ⊢ ∀ k ∈ Z x ≤ F ⁡ k → k ∈ Z → F ⁡ k = y → x ≤ y
30 29 adantl ⊢ φ ∧ ∀ k ∈ Z x ≤ F ⁡ k → k ∈ Z → F ⁡ k = y → x ≤ y
31 21 22 30 rexlimd ⊢ φ ∧ ∀ k ∈ Z x ≤ F ⁡ k → ∃ k ∈ Z F ⁡ k = y → x ≤ y
32 31 adantr ⊢ φ ∧ ∀ k ∈ Z x ≤ F ⁡ k ∧ y ∈ ran ⁡ F → ∃ k ∈ Z F ⁡ k = y → x ≤ y
33 18 32 mpd ⊢ φ ∧ ∀ k ∈ Z x ≤ F ⁡ k ∧ y ∈ ran ⁡ F → x ≤ y
34 33 ralrimiva ⊢ φ ∧ ∀ k ∈ Z x ≤ F ⁡ k → ∀ y ∈ ran ⁡ F x ≤ y
35 34 adantlr ⊢ φ ∧ x ∈ ℝ ∧ ∀ k ∈ Z x ≤ F ⁡ k → ∀ y ∈ ran ⁡ F x ≤ y
36 35 ex ⊢ φ ∧ x ∈ ℝ → ∀ k ∈ Z x ≤ F ⁡ k → ∀ y ∈ ran ⁡ F x ≤ y
37 36 reximdva ⊢ φ → ∃ x ∈ ℝ ∀ k ∈ Z x ≤ F ⁡ k → ∃ x ∈ ℝ ∀ y ∈ ran ⁡ F x ≤ y
38 5 37 mpd ⊢ φ → ∃ x ∈ ℝ ∀ y ∈ ran ⁡ F x ≤ y
39 infxrre ⊢ ran ⁡ F ⊆ ℝ ∧ ran ⁡ F ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ ran ⁡ F x ≤ y → inf ran ⁡ F ℝ * < = inf ran ⁡ F ℝ <
40 7 12 38 39 syl3anc ⊢ φ → inf ran ⁡ F ℝ * < = inf ran ⁡ F ℝ <
41 6 40 breqtrrd ⊢ φ → F ⇝ inf ran ⁡ F ℝ * <