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	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	climinf2lem.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climinf2lem.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
	climinf2lem.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
	climinf2lem.5	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
Assertion	climinf2lem	⊢ ( 𝜑 → 𝐹 ⇝ inf ( ran 𝐹 , ℝ^* , < ) )

Proof

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

Metamath Proof Explorer

Theorem climinf2lem

Proof