Metamath Proof Explorer

Theorem climinf

Description: A bounded monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 29-Jun-2017) (Revised by AV, 15-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 climinf.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climinf.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climinf.5 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4 climinf.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
5 climinf.7 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
6 3 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
7 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
8 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 2 8 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
10 9 1 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
11 fnfvelrn ⊢ ( ( 𝐹 Fn 𝑍 ∧ 𝑀 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑀 ) ∈ ran 𝐹 )
12 7 10 11 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ran 𝐹 )
13 12 ne0d ⊢ ( 𝜑 → ran 𝐹 ≠ ∅ )
14 breq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑘 ) → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
15 14 ralrn ⊢ ( 𝐹 Fn 𝑍 → ( ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ↔ ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
16 15 rexbidv ⊢ ( 𝐹 Fn 𝑍 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
17 7 16 syl ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
18 5 17 mpbird ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 )
19 6 13 18 3jca ⊢ ( 𝜑 → ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ) )
21 infrecl ⊢ ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ) → inf ( ran 𝐹 , ℝ , < ) ∈ ℝ )
22 20 21 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → inf ( ran 𝐹 , ℝ , < ) ∈ ℝ )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
24 22 23 ltaddrpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → inf ( ran 𝐹 , ℝ , < ) < ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) )
25 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ )
27 22 26 readdcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) ∈ ℝ )
28 infrglb ⊢ ( ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ) ∧ ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) ∈ ℝ ) → ( inf ( ran 𝐹 , ℝ , < ) < ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) ↔ ∃ 𝑘 ∈ ran 𝐹 𝑘 < ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) ) )
29 20 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( inf ( ran 𝐹 , ℝ , < ) < ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) ↔ ∃ 𝑘 ∈ ran 𝐹 𝑘 < ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) ) )
30 24 29 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑘 ∈ ran 𝐹 𝑘 < ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) )
31 6 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ran 𝐹 ) → 𝑘 ∈ ℝ )
32 31 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ran 𝐹 ) → 𝑘 ∈ ℝ )
33 22 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ran 𝐹 ) → inf ( ran 𝐹 , ℝ , < ) ∈ ℝ )
34 25 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ )
35 33 34 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ran 𝐹 ) → ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) ∈ ℝ )
36 32 35 34 ltsub1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ran 𝐹 ) → ( 𝑘 < ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) ↔ ( 𝑘 − 𝑦 ) < ( ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) − 𝑦 ) ) )
37 6 13 18 21 syl3anc ⊢ ( 𝜑 → inf ( ran 𝐹 , ℝ , < ) ∈ ℝ )
38 37 recnd ⊢ ( 𝜑 → inf ( ran 𝐹 , ℝ , < ) ∈ ℂ )
39 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ran 𝐹 ) → inf ( ran 𝐹 , ℝ , < ) ∈ ℂ )
40 34 recnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ran 𝐹 ) → 𝑦 ∈ ℂ )
41 39 40 pncand ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ran 𝐹 ) → ( ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) − 𝑦 ) = inf ( ran 𝐹 , ℝ , < ) )
42 41 breq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ran 𝐹 ) → ( ( 𝑘 − 𝑦 ) < ( ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) − 𝑦 ) ↔ ( 𝑘 − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ) )
43 36 42 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ran 𝐹 ) → ( 𝑘 < ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) ↔ ( 𝑘 − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ) )
44 43 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ran 𝐹 ) → ( 𝑘 < ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) → ( 𝑘 − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ) )
45 44 reximdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑘 ∈ ran 𝐹 𝑘 < ( inf ( ran 𝐹 , ℝ , < ) + 𝑦 ) → ∃ 𝑘 ∈ ran 𝐹 ( 𝑘 − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ) )
46 30 45 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑘 ∈ ran 𝐹 ( 𝑘 − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) )
47 oveq1 ⊢ ( 𝑘 = ( 𝐹 ‘ 𝑗 ) → ( 𝑘 − 𝑦 ) = ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) )
48 47 breq1d ⊢ ( 𝑘 = ( 𝐹 ‘ 𝑗 ) → ( ( 𝑘 − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ↔ ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ) )
49 48 rexrn ⊢ ( 𝐹 Fn 𝑍 → ( ∃ 𝑘 ∈ ran 𝐹 ( 𝑘 − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ↔ ∃ 𝑗 ∈ 𝑍 ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ) )
50 7 49 syl ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ran 𝐹 ( 𝑘 − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ↔ ∃ 𝑗 ∈ 𝑍 ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ) )
51 50 biimpa ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ ran 𝐹 ( 𝑘 − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ) → ∃ 𝑗 ∈ 𝑍 ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) )
52 46 51 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) )
53 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐹 : 𝑍 ⟶ ℝ )
54 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
55 ffvelcdm ⊢ ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
56 53 54 55 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
57 simpl ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑗 ∈ 𝑍 )
58 ffvelcdm ⊢ ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
59 53 57 58 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
60 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → inf ( ran 𝐹 , ℝ , < ) ∈ ℝ )
61 simprr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) )
62 fzssuz ⊢ ( 𝑗 ... 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑗 )
63 uzss ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑗 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
64 63 1 sseqtrrdi ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑗 ) ⊆ 𝑍 )
65 64 1 eleq2s ⊢ ( 𝑗 ∈ 𝑍 → ( ℤ≥ ‘ 𝑗 ) ⊆ 𝑍 )
66 65 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ℤ≥ ‘ 𝑗 ) ⊆ 𝑍 )
67 62 66 sstrid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑗 ... 𝑘 ) ⊆ 𝑍 )
68 ffvelcdm ⊢ ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
69 68 ralrimiva ⊢ ( 𝐹 : 𝑍 ⟶ ℝ → ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
70 3 69 syl ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
71 70 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
72 ssralv ⊢ ( ( 𝑗 ... 𝑘 ) ⊆ 𝑍 → ( ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℝ → ∀ 𝑛 ∈ ( 𝑗 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) )
73 67 71 72 sylc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ∀ 𝑛 ∈ ( 𝑗 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
74 73 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( 𝑗 ... 𝑘 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
75 fzssuz ⊢ ( 𝑗 ... ( 𝑘 − 1 ) ) ⊆ ( ℤ≥ ‘ 𝑗 )
76 75 66 sstrid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑗 ... ( 𝑘 − 1 ) ) ⊆ 𝑍 )
77 76 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( 𝑗 ... ( 𝑘 − 1 ) ) ) → 𝑛 ∈ 𝑍 )
78 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
79 78 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
80 fvoveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
81 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
82 80 81 breq12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝐹 ‘ 𝑛 ) ) )
83 82 rspccva ⊢ ( ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝐹 ‘ 𝑛 ) )
84 79 83 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝐹 ‘ 𝑛 ) )
85 77 84 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( 𝑗 ... ( 𝑘 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝐹 ‘ 𝑛 ) )
86 61 74 85 monoord2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 𝑗 ) )
87 56 59 60 86 lesub1dd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) − inf ( ran 𝐹 , ℝ , < ) ) )
88 56 60 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ∈ ℝ )
89 59 60 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐹 ‘ 𝑗 ) − inf ( ran 𝐹 , ℝ , < ) ) ∈ ℝ )
90 25 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑦 ∈ ℝ )
91 lelttr ⊢ ( ( ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑗 ) − inf ( ran 𝐹 , ℝ , < ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) − inf ( ran 𝐹 , ℝ , < ) ) ∧ ( ( 𝐹 ‘ 𝑗 ) − inf ( ran 𝐹 , ℝ , < ) ) < 𝑦 ) → ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) < 𝑦 ) )
92 88 89 90 91 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) − inf ( ran 𝐹 , ℝ , < ) ) ∧ ( ( 𝐹 ‘ 𝑗 ) − inf ( ran 𝐹 , ℝ , < ) ) < 𝑦 ) → ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) < 𝑦 ) )
93 87 92 mpand ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝐹 ‘ 𝑗 ) − inf ( ran 𝐹 , ℝ , < ) ) < 𝑦 → ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) < 𝑦 ) )
94 ltsub23 ⊢ ( ( ( 𝐹 ‘ 𝑗 ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ inf ( ran 𝐹 , ℝ , < ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ↔ ( ( 𝐹 ‘ 𝑗 ) − inf ( ran 𝐹 , ℝ , < ) ) < 𝑦 ) )
95 59 90 60 94 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) ↔ ( ( 𝐹 ‘ 𝑗 ) − inf ( ran 𝐹 , ℝ , < ) ) < 𝑦 ) )
96 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ran 𝐹 ⊆ ℝ )
97 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐹 Fn 𝑍 )
98 fnfvelrn ⊢ ( ( 𝐹 Fn 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 )
99 97 54 98 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 )
100 96 99 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
101 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 )
102 infrelb ⊢ ( ( ran 𝐹 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 ) → inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹 ‘ 𝑘 ) )
103 96 101 99 102 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹 ‘ 𝑘 ) )
104 60 100 103 abssubge0d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ) = ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) )
105 104 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 ↔ ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) < 𝑦 ) )
106 93 95 105 3imtr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 ) )
107 106 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 ) )
108 107 ralrimdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 ) )
109 108 reximdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ( ( 𝐹 ‘ 𝑗 ) − 𝑦 ) < inf ( ran 𝐹 , ℝ , < ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 ) )
110 52 109 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 )
111 110 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 )
112 1 fvexi ⊢ 𝑍 ∈ V
113 fex ⊢ ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝑍 ∈ V ) → 𝐹 ∈ V )
114 3 112 113 sylancl ⊢ ( 𝜑 → 𝐹 ∈ V )
115 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
116 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
117 116 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
118 1 2 114 115 38 117 clim2c ⊢ ( 𝜑 → ( 𝐹 ⇝ inf ( ran 𝐹 , ℝ , < ) ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − inf ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 ) )
119 111 118 mpbird ⊢ ( 𝜑 → 𝐹 ⇝ inf ( ran 𝐹 , ℝ , < ) )