This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climinf3

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

Ref Expression
Hypotheses climinf3.1 ⊢ Ⅎ 𝑘 𝜑
climinf3.2 ⊢ Ⅎ 𝑘 𝐹
climinf3.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climinf3.4 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climinf3.5 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
climinf3.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
climinf3.7 ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
Assertion climinf3 ( 𝜑 → 𝐹 ⇝ inf ( ran 𝐹 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 climinf3.1 ⊢ Ⅎ 𝑘 𝜑
2 climinf3.2 ⊢ Ⅎ 𝑘 𝐹
3 climinf3.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 climinf3.4 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 climinf3.5 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
6 climinf3.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
7 climinf3.7 ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
8 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
9 8 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
10 1 9 ralrimia ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
11 2 4 climbddf ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )
12 3 7 10 11 syl3anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )
13 renegcl ⊢ ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ )
14 13 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) → - 𝑥 ∈ ℝ )
15 nfv ⊢ Ⅎ 𝑘 𝑥 ∈ ℝ
16 1 15 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑥 ∈ ℝ )
17 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥
18 16 17 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )
19 simpll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝜑 ∧ 𝑥 ∈ ℝ ) )
20 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
21 rspa ⊢ ( ( ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )
22 21 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )
23 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )
24 8 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
25 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) → 𝑥 ∈ ℝ )
26 24 25 absled ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ↔ ( - 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ) )
27 23 26 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) → ( - 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
28 27 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) → - 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
29 19 20 22 28 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) ∧ 𝑘 ∈ 𝑍 ) → - 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
30 29 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) → ( 𝑘 ∈ 𝑍 → - 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
31 18 30 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) → ∀ 𝑘 ∈ 𝑍 - 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
32 breq1 ⊢ ( 𝑦 = - 𝑥 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ↔ - 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
33 32 ralbidv ⊢ ( 𝑦 = - 𝑥 → ( ∀ 𝑘 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝑍 - 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
34 33 rspcev ⊢ ( ( - 𝑥 ∈ ℝ ∧ ∀ 𝑘 ∈ 𝑍 - 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) )
35 14 31 34 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) )
36 35 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) ) )
37 12 36 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑦 ≤ ( 𝐹 ‘ 𝑘 ) )
38 1 2 4 3 5 6 37 climinf2 ⊢ ( 𝜑 → 𝐹 ⇝ inf ( ran 𝐹 , ℝ* , < ) )