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

Metamath Proof Explorer

Theorem climsup

Description: A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of Gleason p. 180. (Contributed by NM, 13-Mar-2005) (Revised by Mario Carneiro, 10-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 climsup.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climsup.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climsup.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4 climsup.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
5 climsup.5 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
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 breq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑘 ) → ( 𝑦 ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
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 suprcl ⊢ ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
21 19 20 syl ⊢ ( 𝜑 → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
22 ltsubrp ⊢ ( ( sup ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < sup ( ran 𝐹 , ℝ , < ) )
23 21 22 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < sup ( ran 𝐹 , ℝ , < ) )
24 19 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) )
25 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
26 resubcl ⊢ ( ( sup ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) ∈ ℝ )
27 21 25 26 syl2an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) ∈ ℝ )
28 suprlub ⊢ ( ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) ∈ ℝ ) → ( ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < sup ( ran 𝐹 , ℝ , < ) ↔ ∃ 𝑘 ∈ ran 𝐹 ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < 𝑘 ) )
29 24 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < sup ( ran 𝐹 , ℝ , < ) ↔ ∃ 𝑘 ∈ ran 𝐹 ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < 𝑘 ) )
30 23 29 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑘 ∈ ran 𝐹 ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < 𝑘 )
31 breq2 ⊢ ( 𝑘 = ( 𝐹 ‘ 𝑗 ) → ( ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < 𝑘 ↔ ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < ( 𝐹 ‘ 𝑗 ) ) )
32 31 rexrn ⊢ ( 𝐹 Fn 𝑍 → ( ∃ 𝑘 ∈ ran 𝐹 ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < 𝑘 ↔ ∃ 𝑗 ∈ 𝑍 ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < ( 𝐹 ‘ 𝑗 ) ) )
33 7 32 syl ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ran 𝐹 ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < 𝑘 ↔ ∃ 𝑗 ∈ 𝑍 ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < ( 𝐹 ‘ 𝑗 ) ) )
34 33 biimpa ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ ran 𝐹 ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < 𝑘 ) → ∃ 𝑗 ∈ 𝑍 ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < ( 𝐹 ‘ 𝑗 ) )
35 30 34 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < ( 𝐹 ‘ 𝑗 ) )
36 ffvelcdm ⊢ ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
37 3 36 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
38 37 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
39 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐹 : 𝑍 ⟶ ℝ )
40 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
41 ffvelcdm ⊢ ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
42 39 40 41 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
43 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
44 simprr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) )
45 fzssuz ⊢ ( 𝑗 ... 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑗 )
46 uzss ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑗 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
47 46 1 sseqtrrdi ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑗 ) ⊆ 𝑍 )
48 47 1 eleq2s ⊢ ( 𝑗 ∈ 𝑍 → ( ℤ≥ ‘ 𝑗 ) ⊆ 𝑍 )
49 48 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ℤ≥ ‘ 𝑗 ) ⊆ 𝑍 )
50 45 49 sstrid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑗 ... 𝑘 ) ⊆ 𝑍 )
51 ffvelcdm ⊢ ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
52 51 ralrimiva ⊢ ( 𝐹 : 𝑍 ⟶ ℝ → ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
53 3 52 syl ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
54 53 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
55 ssralv ⊢ ( ( 𝑗 ... 𝑘 ) ⊆ 𝑍 → ( ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℝ → ∀ 𝑛 ∈ ( 𝑗 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) )
56 50 54 55 sylc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ∀ 𝑛 ∈ ( 𝑗 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
57 56 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( 𝑗 ... 𝑘 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
58 fzssuz ⊢ ( 𝑗 ... ( 𝑘 − 1 ) ) ⊆ ( ℤ≥ ‘ 𝑗 )
59 58 49 sstrid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑗 ... ( 𝑘 − 1 ) ) ⊆ 𝑍 )
60 59 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( 𝑗 ... ( 𝑘 − 1 ) ) ) → 𝑛 ∈ 𝑍 )
61 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
62 61 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
63 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
64 fvoveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
65 63 64 breq12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
66 65 rspccva ⊢ ( ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
67 62 66 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
68 60 67 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( 𝑗 ... ( 𝑘 − 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
69 44 57 68 monoord ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑗 ) ≤ ( 𝐹 ‘ 𝑘 ) )
70 38 42 43 69 lesub2dd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑘 ) ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑗 ) ) )
71 43 42 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
72 43 38 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
73 25 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑦 ∈ ℝ )
74 lelttr ⊢ ( ( ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑘 ) ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑗 ) ) ∧ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑗 ) ) < 𝑦 ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑘 ) ) < 𝑦 ) )
75 71 72 73 74 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑘 ) ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑗 ) ) ∧ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑗 ) ) < 𝑦 ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑘 ) ) < 𝑦 ) )
76 70 75 mpand ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑗 ) ) < 𝑦 → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑘 ) ) < 𝑦 ) )
77 ltsub23 ⊢ ( ( sup ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) → ( ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < ( 𝐹 ‘ 𝑗 ) ↔ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑗 ) ) < 𝑦 ) )
78 43 73 38 77 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < ( 𝐹 ‘ 𝑗 ) ↔ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑗 ) ) < 𝑦 ) )
79 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) )
80 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐹 Fn 𝑍 )
81 fnfvelrn ⊢ ( ( 𝐹 Fn 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 )
82 80 40 81 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 )
83 suprub ⊢ ( ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ran 𝐹 ) → ( 𝐹 ‘ 𝑘 ) ≤ sup ( ran 𝐹 , ℝ , < ) )
84 79 82 83 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ≤ sup ( ran 𝐹 , ℝ , < ) )
85 42 43 84 abssuble0d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − sup ( ran 𝐹 , ℝ , < ) ) ) = ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑘 ) ) )
86 85 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − sup ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 ↔ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑘 ) ) < 𝑦 ) )
87 76 78 86 3imtr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < ( 𝐹 ‘ 𝑗 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − sup ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 ) )
88 87 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < ( 𝐹 ‘ 𝑗 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − sup ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 ) )
89 88 ralrimdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < ( 𝐹 ‘ 𝑗 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − sup ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 ) )
90 89 reximdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ( sup ( ran 𝐹 , ℝ , < ) − 𝑦 ) < ( 𝐹 ‘ 𝑗 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − sup ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 ) )
91 35 90 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − sup ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 )
92 91 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − sup ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 )
93 1 fvexi ⊢ 𝑍 ∈ V
94 fex ⊢ ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝑍 ∈ V ) → 𝐹 ∈ V )
95 3 93 94 sylancl ⊢ ( 𝜑 → 𝐹 ∈ V )
96 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
97 21 recnd ⊢ ( 𝜑 → sup ( ran 𝐹 , ℝ , < ) ∈ ℂ )
98 3 41 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
99 98 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
100 1 2 95 96 97 99 clim2c ⊢ ( 𝜑 → ( 𝐹 ⇝ sup ( ran 𝐹 , ℝ , < ) ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − sup ( ran 𝐹 , ℝ , < ) ) ) < 𝑦 ) )
101 92 100 mpbird ⊢ ( 𝜑 → 𝐹 ⇝ sup ( ran 𝐹 , ℝ , < ) )