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

Metamath Proof Explorer

Theorem climinf2mpt

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

Ref Expression
Hypotheses climinf2mpt.p ⊢ Ⅎ 𝑘 𝜑
climinf2mpt.j ⊢ Ⅎ 𝑗 𝜑
climinf2mpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climinf2mpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climinf2mpt.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
climinf2mpt.c ⊢ ( 𝑘 = 𝑗 → 𝐵 = 𝐶 )
climinf2mpt.l ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ 𝑗 = ( 𝑘 + 1 ) ) → 𝐶 ≤ 𝐵 )
climinf2mpt.e ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ )
Assertion climinf2mpt ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ⇝ inf ( ran ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 climinf2mpt.p ⊢ Ⅎ 𝑘 𝜑
2 climinf2mpt.j ⊢ Ⅎ 𝑗 𝜑
3 climinf2mpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 climinf2mpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 climinf2mpt.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
6 climinf2mpt.c ⊢ ( 𝑘 = 𝑗 → 𝐵 = 𝐶 )
7 climinf2mpt.l ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ 𝑗 = ( 𝑘 + 1 ) ) → 𝐶 ≤ 𝐵 )
8 climinf2mpt.e ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ )
9 nfv ⊢ Ⅎ 𝑖 𝜑
10 nfcv ⊢ Ⅎ 𝑖 ( 𝑘 ∈ 𝑍 ↦ 𝐵 )
11 1 5 fmptd2f ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ )
12 nfv ⊢ Ⅎ 𝑘 𝑖 ∈ 𝑍
13 1 12 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑖 ∈ 𝑍 )
14 nfv ⊢ Ⅎ 𝑘 ⦋ ( 𝑖 + 1 ) / 𝑗 ⦌ 𝐶 ≤ ⦋ 𝑖 / 𝑗 ⦌ 𝐶
15 13 14 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ⦋ ( 𝑖 + 1 ) / 𝑗 ⦌ 𝐶 ≤ ⦋ 𝑖 / 𝑗 ⦌ 𝐶 )
16 eleq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍 ) )
17 16 anbi2d ⊢ ( 𝑘 = 𝑖 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ) )
18 oveq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 + 1 ) = ( 𝑖 + 1 ) )
19 18 csbeq1d ⊢ ( 𝑘 = 𝑖 → ⦋ ( 𝑘 + 1 ) / 𝑗 ⦌ 𝐶 = ⦋ ( 𝑖 + 1 ) / 𝑗 ⦌ 𝐶 )
20 eqidd ⊢ ( 𝑘 = 𝑖 → 𝐵 = 𝐵 )
21 csbcow ⊢ ⦋ 𝑘 / 𝑗 ⦌ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑘 / 𝑘 ⦌ 𝐵
22 csbid ⊢ ⦋ 𝑘 / 𝑘 ⦌ 𝐵 = 𝐵
23 21 22 eqtr2i ⊢ 𝐵 = ⦋ 𝑘 / 𝑗 ⦌ ⦋ 𝑗 / 𝑘 ⦌ 𝐵
24 nfcv ⊢ Ⅎ 𝑗 𝐵
25 nfcv ⊢ Ⅎ 𝑘 𝐶
26 24 25 6 cbvcsbw ⊢ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑗 ⦌ 𝐶
27 csbid ⊢ ⦋ 𝑗 / 𝑗 ⦌ 𝐶 = 𝐶
28 26 27 eqtri ⊢ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 𝐶
29 28 csbeq2i ⊢ ⦋ 𝑘 / 𝑗 ⦌ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑘 / 𝑗 ⦌ 𝐶
30 23 29 eqtri ⊢ 𝐵 = ⦋ 𝑘 / 𝑗 ⦌ 𝐶
31 30 a1i ⊢ ( 𝑘 = 𝑖 → 𝐵 = ⦋ 𝑘 / 𝑗 ⦌ 𝐶 )
32 csbeq1 ⊢ ( 𝑘 = 𝑖 → ⦋ 𝑘 / 𝑗 ⦌ 𝐶 = ⦋ 𝑖 / 𝑗 ⦌ 𝐶 )
33 20 31 32 3eqtrd ⊢ ( 𝑘 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑗 ⦌ 𝐶 )
34 19 33 breq12d ⊢ ( 𝑘 = 𝑖 → ( ⦋ ( 𝑘 + 1 ) / 𝑗 ⦌ 𝐶 ≤ 𝐵 ↔ ⦋ ( 𝑖 + 1 ) / 𝑗 ⦌ 𝐶 ≤ ⦋ 𝑖 / 𝑗 ⦌ 𝐶 ) )
35 17 34 imbi12d ⊢ ( 𝑘 = 𝑖 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ⦋ ( 𝑘 + 1 ) / 𝑗 ⦌ 𝐶 ≤ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ⦋ ( 𝑖 + 1 ) / 𝑗 ⦌ 𝐶 ≤ ⦋ 𝑖 / 𝑗 ⦌ 𝐶 ) ) )
36 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝜑 )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
38 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 + 1 ) = ( 𝑘 + 1 ) )
39 nfv ⊢ Ⅎ 𝑗 𝑘 ∈ 𝑍
40 nfv ⊢ Ⅎ 𝑗 ( 𝑘 + 1 ) = ( 𝑘 + 1 )
41 2 39 40 nf3an ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑘 + 1 ) = ( 𝑘 + 1 ) )
42 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ ( 𝑘 + 1 ) / 𝑗 ⦌ 𝐶
43 nfcv ⊢ Ⅎ 𝑗 ≤
44 42 43 24 nfbr ⊢ Ⅎ 𝑗 ⦋ ( 𝑘 + 1 ) / 𝑗 ⦌ 𝐶 ≤ 𝐵
45 41 44 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑘 + 1 ) = ( 𝑘 + 1 ) ) → ⦋ ( 𝑘 + 1 ) / 𝑗 ⦌ 𝐶 ≤ 𝐵 )
46 ovex ⊢ ( 𝑘 + 1 ) ∈ V
47 eqeq1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 = ( 𝑘 + 1 ) ↔ ( 𝑘 + 1 ) = ( 𝑘 + 1 ) ) )
48 47 3anbi3d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ 𝑗 = ( 𝑘 + 1 ) ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑘 + 1 ) = ( 𝑘 + 1 ) ) ) )
49 csbeq1a ⊢ ( 𝑗 = ( 𝑘 + 1 ) → 𝐶 = ⦋ ( 𝑘 + 1 ) / 𝑗 ⦌ 𝐶 )
50 49 breq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐶 ≤ 𝐵 ↔ ⦋ ( 𝑘 + 1 ) / 𝑗 ⦌ 𝐶 ≤ 𝐵 ) )
51 48 50 imbi12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ 𝑗 = ( 𝑘 + 1 ) ) → 𝐶 ≤ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑘 + 1 ) = ( 𝑘 + 1 ) ) → ⦋ ( 𝑘 + 1 ) / 𝑗 ⦌ 𝐶 ≤ 𝐵 ) ) )
52 45 46 51 7 vtoclf ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑘 + 1 ) = ( 𝑘 + 1 ) ) → ⦋ ( 𝑘 + 1 ) / 𝑗 ⦌ 𝐶 ≤ 𝐵 )
53 36 37 38 52 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ⦋ ( 𝑘 + 1 ) / 𝑗 ⦌ 𝐶 ≤ 𝐵 )
54 15 35 53 chvarfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ⦋ ( 𝑖 + 1 ) / 𝑗 ⦌ 𝐶 ≤ ⦋ 𝑖 / 𝑗 ⦌ 𝐶 )
55 24 25 6 cbvcsbw ⊢ ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑖 + 1 ) / 𝑗 ⦌ 𝐶
56 55 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑖 + 1 ) / 𝑗 ⦌ 𝐶 )
57 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ⦋ 𝑖 / 𝑗 ⦌ 𝐶 = ⦋ 𝑖 / 𝑗 ⦌ 𝐶 )
58 56 57 breq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 ≤ ⦋ 𝑖 / 𝑗 ⦌ 𝐶 ↔ ⦋ ( 𝑖 + 1 ) / 𝑗 ⦌ 𝐶 ≤ ⦋ 𝑖 / 𝑗 ⦌ 𝐶 ) )
59 54 58 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 ≤ ⦋ 𝑖 / 𝑗 ⦌ 𝐶 )
60 4 peano2uzs ⊢ ( 𝑖 ∈ 𝑍 → ( 𝑖 + 1 ) ∈ 𝑍 )
61 60 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑖 + 1 ) ∈ 𝑍 )
62 nfv ⊢ Ⅎ 𝑘 ( 𝑖 + 1 ) ∈ 𝑍
63 1 62 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ 𝑍 )
64 nfcv ⊢ Ⅎ 𝑘 ( 𝑖 + 1 )
65 64 nfcsb1 ⊢ Ⅎ 𝑘 ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵
66 65 nfel1 ⊢ Ⅎ 𝑘 ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 ∈ ℝ
67 63 66 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ 𝑍 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 ∈ ℝ )
68 ovex ⊢ ( 𝑖 + 1 ) ∈ V
69 eleq1 ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( 𝑘 ∈ 𝑍 ↔ ( 𝑖 + 1 ) ∈ 𝑍 ) )
70 69 anbi2d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ 𝑍 ) ) )
71 csbeq1a ⊢ ( 𝑘 = ( 𝑖 + 1 ) → 𝐵 = ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 )
72 71 eleq1d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( 𝐵 ∈ ℝ ↔ ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 ∈ ℝ ) )
73 70 72 imbi12d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ 𝑍 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 ∈ ℝ ) ) )
74 67 68 73 5 vtoclf ⊢ ( ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ 𝑍 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 ∈ ℝ )
75 60 74 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 ∈ ℝ )
76 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑘 ∈ 𝑍 ↦ 𝐵 )
77 64 65 71 76 fvmptf ⊢ ( ( ( 𝑖 + 1 ) ∈ 𝑍 ∧ ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 ∈ ℝ ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ ( 𝑖 + 1 ) ) = ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 )
78 61 75 77 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ ( 𝑖 + 1 ) ) = ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 )
79 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ 𝑍 )
80 nfv ⊢ Ⅎ 𝑗 𝑖 ∈ 𝑍
81 2 80 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑖 ∈ 𝑍 )
82 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑖 / 𝑗 ⦌ 𝐶
83 nfcv ⊢ Ⅎ 𝑗 ℝ
84 82 83 nfel ⊢ Ⅎ 𝑗 ⦋ 𝑖 / 𝑗 ⦌ 𝐶 ∈ ℝ
85 81 84 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ⦋ 𝑖 / 𝑗 ⦌ 𝐶 ∈ ℝ )
86 eleq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍 ) )
87 86 anbi2d ⊢ ( 𝑗 = 𝑖 → ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ) )
88 csbeq1a ⊢ ( 𝑗 = 𝑖 → 𝐶 = ⦋ 𝑖 / 𝑗 ⦌ 𝐶 )
89 88 eleq1d ⊢ ( 𝑗 = 𝑖 → ( 𝐶 ∈ ℝ ↔ ⦋ 𝑖 / 𝑗 ⦌ 𝐶 ∈ ℝ ) )
90 87 89 imbi12d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐶 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ⦋ 𝑖 / 𝑗 ⦌ 𝐶 ∈ ℝ ) ) )
91 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
92 1 91 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
93 nfv ⊢ Ⅎ 𝑘 𝐶 ∈ ℝ
94 92 93 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐶 ∈ ℝ )
95 eleq1 ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
96 95 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
97 6 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ ) )
98 96 97 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐶 ∈ ℝ ) ) )
99 94 98 5 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐶 ∈ ℝ )
100 85 90 99 chvarfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ⦋ 𝑖 / 𝑗 ⦌ 𝐶 ∈ ℝ )
101 nfcv ⊢ Ⅎ 𝑘 𝑖
102 nfcv ⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑗 ⦌ 𝐶
103 101 102 33 76 fvmptf ⊢ ( ( 𝑖 ∈ 𝑍 ∧ ⦋ 𝑖 / 𝑗 ⦌ 𝐶 ∈ ℝ ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) = ⦋ 𝑖 / 𝑗 ⦌ 𝐶 )
104 79 100 103 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) = ⦋ 𝑖 / 𝑗 ⦌ 𝐶 )
105 78 104 breq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ ( 𝑖 + 1 ) ) ≤ ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) ↔ ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐵 ≤ ⦋ 𝑖 / 𝑗 ⦌ 𝐶 ) )
106 59 105 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ ( 𝑖 + 1 ) ) ≤ ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) )
107 104 100 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) ∈ ℝ )
108 107 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) ∈ ℂ )
109 108 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) ∈ ℂ )
110 10 4 climbddf ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ∧ ∀ 𝑖 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) ∈ ℂ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ( abs ‘ ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) ) ≤ 𝑥 )
111 3 8 109 110 syl3anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ( abs ‘ ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) ) ≤ 𝑥 )
112 9 107 rexabsle2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ( abs ‘ ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) ) ≤ 𝑥 ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑥 ≤ ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) ) ) )
113 111 112 mpbid ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑥 ≤ ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) ) )
114 113 simprd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑥 ≤ ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑖 ) )
115 9 10 4 3 11 106 114 climinf2 ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ⇝ inf ( ran ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) , ℝ* , < ) )