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 ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) , ℝ* , < ) )