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	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
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 𝐹 , ℝ* , < ) )