Metamath Proof Explorer

Theorem climinf2

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

Ref Expression
Hypotheses climinf2.k ⊢ Ⅎ 𝑘 𝜑
climinf2.n ⊢ Ⅎ 𝑘 𝐹
climinf2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climinf2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climinf2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
climinf2.l ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
climinf2.e ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
Assertion climinf2 ( 𝜑 → 𝐹 ⇝ inf ( ran 𝐹 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 climinf2.k ⊢ Ⅎ 𝑘 𝜑
2 climinf2.n ⊢ Ⅎ 𝑘 𝐹
3 climinf2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 climinf2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5 climinf2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
6 climinf2.l ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
7 climinf2.e ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
8 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
9 1 8 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
10 nfcv ⊢ Ⅎ 𝑘 ( 𝑗 + 1 )
11 2 10 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ ( 𝑗 + 1 ) )
12 nfcv ⊢ Ⅎ 𝑘 ≤
13 nfcv ⊢ Ⅎ 𝑘 𝑗
14 2 13 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
15 11 12 14 nfbr ⊢ Ⅎ 𝑘 ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 )
16 9 15 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 ) )
17 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
18 17 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
19 fvoveq1 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
20 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
21 19 20 breq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 ) ) )
22 18 21 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
23 16 22 6 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 ) )
24 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ↔ 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ) )
25 24 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ) )
26 nfv ⊢ Ⅎ 𝑗 𝑦 ≤ ( 𝐹 ‘ 𝑘 )
27 nfcv ⊢ Ⅎ 𝑘 𝑦
28 27 12 14 nfbr ⊢ Ⅎ 𝑘 𝑦 ≤ ( 𝐹 ‘ 𝑗 )
29 20 breq2d ⊢ ( 𝑘 = 𝑗 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ↔ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
30 26 28 29 cbvralw ⊢ ( ∀ 𝑘 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑗 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) )
31 30 a1i ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑘 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑗 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
32 25 31 bitrd ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑗 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
33 32 cbvrexvw ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) )
34 7 33 sylib ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) )
35 3 4 5 23 34 climinf2lem ⊢ ( 𝜑 → 𝐹 ⇝ inf ( ran 𝐹 , ℝ* , < ) )