climinfmpt

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

	Ref	Expression
Hypotheses	climinfmpt.p	$⊢ Ⅎ k φ$
	climinfmpt.j	$⊢ Ⅎ j φ$
	climinfmpt.m	$⊢ φ \to M \in ℤ$
	climinfmpt.z	$⊢ Z = ℤ_{\geq M}$
	climinfmpt.b	$⊢ (φ \land k \in Z) \to B \in ℝ$
	climinfmpt.c	$⊢ k = j \to B = C$
	climinfmpt.l	$⊢ (φ \land k \in Z \land j = k + 1) \to C \leq B$
	climinfmpt.e	$⊢ φ \to \exists x \in ℝ \forall k \in Z x \leq B$
Assertion	climinfmpt	$⊢ φ \to (k \in Z ⟼ B) ⇝ sup (ran (k \in Z ⟼ B) ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		climinfmpt.p	$⊢ Ⅎ k φ$
2		climinfmpt.j	$⊢ Ⅎ j φ$
3		climinfmpt.m	$⊢ φ \to M \in ℤ$
4		climinfmpt.z	$⊢ Z = ℤ_{\geq M}$
5		climinfmpt.b	$⊢ (φ \land k \in Z) \to B \in ℝ$
6		climinfmpt.c	$⊢ k = j \to B = C$
7		climinfmpt.l	$⊢ (φ \land k \in Z \land j = k + 1) \to C \leq B$
8		climinfmpt.e	$⊢ φ \to \exists x \in ℝ \forall k \in Z x \leq B$
9		nfv	$⊢ Ⅎ i φ$
10		nfcv	$⊢ \underline{Ⅎ} i (k \in Z ⟼ B)$
11	1 5	fmptd2f	$⊢ φ \to (k \in Z ⟼ B) : Z ⟶ ℝ$
12		nfv	$⊢ Ⅎ k i \in Z$
13	1 12	nfan	$⊢ Ⅎ k (φ \land i \in Z)$
14		nfv	$⊢ Ⅎ k ⦋ (i + 1) / j ⦌ C \leq ⦋ i / j ⦌ C$
15	13 14	nfim	$⊢ Ⅎ k ((φ \land i \in Z) \to ⦋ (i + 1) / j ⦌ C \leq ⦋ i / j ⦌ C)$
16		eleq1	$⊢ k = i \to (k \in Z \leftrightarrow i \in Z)$
17	16	anbi2d	$⊢ k = i \to ((φ \land k \in Z) \leftrightarrow (φ \land i \in Z))$
18		oveq1	$⊢ k = i \to k + 1 = i + 1$
19	18	csbeq1d	$⊢ k = i \to ⦋ (k + 1) / j ⦌ C = ⦋ (i + 1) / j ⦌ C$
20		eqidd	$⊢ k = i \to B = B$
21		csbcow	$⊢ ⦋ k / j ⦌ ⦋ j / k ⦌ B = ⦋ k / k ⦌ B$
22		csbid	$⊢ ⦋ k / k ⦌ B = B$
23	21 22	eqtr2i	$⊢ B = ⦋ k / j ⦌ ⦋ j / k ⦌ B$
24		nfcv	$⊢ \underline{Ⅎ} j B$
25		nfcv	$⊢ \underline{Ⅎ} k C$
26	24 25 6	cbvcsbw	$⊢ ⦋ j / k ⦌ B = ⦋ j / j ⦌ C$
27		csbid	$⊢ ⦋ j / j ⦌ C = C$
28	26 27	eqtri	$⊢ ⦋ j / k ⦌ B = C$
29	28	csbeq2i	$⊢ ⦋ k / j ⦌ ⦋ j / k ⦌ B = ⦋ k / j ⦌ C$
30	23 29	eqtri	$⊢ B = ⦋ k / j ⦌ C$
31	30	a1i	$⊢ k = i \to B = ⦋ k / j ⦌ C$
32		csbeq1	$⊢ k = i \to ⦋ k / j ⦌ C = ⦋ i / j ⦌ C$
33	20 31 32	3eqtrd	$⊢ k = i \to B = ⦋ i / j ⦌ C$
34	19 33	breq12d	$⊢ k = i \to (⦋ (k + 1) / j ⦌ C \leq B \leftrightarrow ⦋ (i + 1) / j ⦌ C \leq ⦋ i / j ⦌ C)$
35	17 34	imbi12d	$⊢ k = i \to (((φ \land k \in Z) \to ⦋ (k + 1) / j ⦌ C \leq B) \leftrightarrow ((φ \land i \in Z) \to ⦋ (i + 1) / j ⦌ C \leq ⦋ i / j ⦌ C))$
36		simpl	$⊢ (φ \land k \in Z) \to φ$
37		simpr	$⊢ (φ \land k \in Z) \to k \in Z$
38		eqidd	$⊢ (φ \land k \in Z) \to k + 1 = k + 1$
39		nfv	$⊢ Ⅎ j k \in Z$
40		nfv	$⊢ Ⅎ j k + 1 = k + 1$
41	2 39 40	nf3an	$⊢ Ⅎ j (φ \land k \in Z \land k + 1 = k + 1)$
42		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ (k + 1) / j ⦌ C$
43		nfcv	$⊢ \underline{Ⅎ} j \leq$
44	42 43 24	nfbr	$⊢ Ⅎ j ⦋ (k + 1) / j ⦌ C \leq B$
45	41 44	nfim	$⊢ Ⅎ j ((φ \land k \in Z \land k + 1 = k + 1) \to ⦋ (k + 1) / j ⦌ C \leq B)$
46		ovex	$⊢ k + 1 \in V$
47		eqeq1	$⊢ j = k + 1 \to (j = k + 1 \leftrightarrow k + 1 = k + 1)$
48	47	3anbi3d	$⊢ j = k + 1 \to ((φ \land k \in Z \land j = k + 1) \leftrightarrow (φ \land k \in Z \land k + 1 = k + 1))$
49		csbeq1a	$⊢ j = k + 1 \to C = ⦋ (k + 1) / j ⦌ C$
50	49	breq1d	$⊢ j = k + 1 \to (C \leq B \leftrightarrow ⦋ (k + 1) / j ⦌ C \leq B)$
51	48 50	imbi12d	$⊢ j = k + 1 \to (((φ \land k \in Z \land j = k + 1) \to C \leq B) \leftrightarrow ((φ \land k \in Z \land k + 1 = k + 1) \to ⦋ (k + 1) / j ⦌ C \leq B))$
52	45 46 51 7	vtoclf	$⊢ (φ \land k \in Z \land k + 1 = k + 1) \to ⦋ (k + 1) / j ⦌ C \leq B$
53	36 37 38 52	syl3anc	$⊢ (φ \land k \in Z) \to ⦋ (k + 1) / j ⦌ C \leq B$
54	15 35 53	chvarfv	$⊢ (φ \land i \in Z) \to ⦋ (i + 1) / j ⦌ C \leq ⦋ i / j ⦌ C$
55	24 25 6	cbvcsbw	$⊢ ⦋ (i + 1) / k ⦌ B = ⦋ (i + 1) / j ⦌ C$
56	55	a1i	$⊢ (φ \land i \in Z) \to ⦋ (i + 1) / k ⦌ B = ⦋ (i + 1) / j ⦌ C$
57		eqidd	$⊢ (φ \land i \in Z) \to ⦋ i / j ⦌ C = ⦋ i / j ⦌ C$
58	56 57	breq12d	$⊢ (φ \land i \in Z) \to (⦋ (i + 1) / k ⦌ B \leq ⦋ i / j ⦌ C \leftrightarrow ⦋ (i + 1) / j ⦌ C \leq ⦋ i / j ⦌ C)$
59	54 58	mpbird	$⊢ (φ \land i \in Z) \to ⦋ (i + 1) / k ⦌ B \leq ⦋ i / j ⦌ C$
60	4	peano2uzs	$⊢ i \in Z \to i + 1 \in Z$
61	60	adantl	$⊢ (φ \land i \in Z) \to i + 1 \in Z$
62		nfv	$⊢ Ⅎ k i + 1 \in Z$
63	1 62	nfan	$⊢ Ⅎ k (φ \land i + 1 \in Z)$
64		nfcv	$⊢ \underline{Ⅎ} k (i + 1)$
65	64	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ (i + 1) / k ⦌ B$
66	65	nfel1	$⊢ Ⅎ k ⦋ (i + 1) / k ⦌ B \in ℝ$
67	63 66	nfim	$⊢ Ⅎ k ((φ \land i + 1 \in Z) \to ⦋ (i + 1) / k ⦌ B \in ℝ)$
68		ovex	$⊢ i + 1 \in V$
69		eleq1	$⊢ k = i + 1 \to (k \in Z \leftrightarrow i + 1 \in Z)$
70	69	anbi2d	$⊢ k = i + 1 \to ((φ \land k \in Z) \leftrightarrow (φ \land i + 1 \in Z))$
71		csbeq1a	$⊢ k = i + 1 \to B = ⦋ (i + 1) / k ⦌ B$
72	71	eleq1d	$⊢ k = i + 1 \to (B \in ℝ \leftrightarrow ⦋ (i + 1) / k ⦌ B \in ℝ)$
73	70 72	imbi12d	$⊢ k = i + 1 \to (((φ \land k \in Z) \to B \in ℝ) \leftrightarrow ((φ \land i + 1 \in Z) \to ⦋ (i + 1) / k ⦌ B \in ℝ))$
74	67 68 73 5	vtoclf	$⊢ (φ \land i + 1 \in Z) \to ⦋ (i + 1) / k ⦌ B \in ℝ$
75	60 74	sylan2	$⊢ (φ \land i \in Z) \to ⦋ (i + 1) / k ⦌ B \in ℝ$
76		eqid	$⊢ (k \in Z ⟼ B) = (k \in Z ⟼ B)$
77	64 65 71 76	fvmptf	$⊢ (i + 1 \in Z \land ⦋ (i + 1) / k ⦌ B \in ℝ) \to (k \in Z ⟼ B) (i + 1) = ⦋ (i + 1) / k ⦌ B$
78	61 75 77	syl2anc	$⊢ (φ \land i \in Z) \to (k \in Z ⟼ B) (i + 1) = ⦋ (i + 1) / k ⦌ B$
79		simpr	$⊢ (φ \land i \in Z) \to i \in Z$
80		nfv	$⊢ Ⅎ j i \in Z$
81	2 80	nfan	$⊢ Ⅎ j (φ \land i \in Z)$
82		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ i / j ⦌ C$
83		nfcv	$⊢ \underline{Ⅎ} j ℝ$
84	82 83	nfel	$⊢ Ⅎ j ⦋ i / j ⦌ C \in ℝ$
85	81 84	nfim	$⊢ Ⅎ j ((φ \land i \in Z) \to ⦋ i / j ⦌ C \in ℝ)$
86		eleq1	$⊢ j = i \to (j \in Z \leftrightarrow i \in Z)$
87	86	anbi2d	$⊢ j = i \to ((φ \land j \in Z) \leftrightarrow (φ \land i \in Z))$
88		csbeq1a	$⊢ j = i \to C = ⦋ i / j ⦌ C$
89	88	eleq1d	$⊢ j = i \to (C \in ℝ \leftrightarrow ⦋ i / j ⦌ C \in ℝ)$
90	87 89	imbi12d	$⊢ j = i \to (((φ \land j \in Z) \to C \in ℝ) \leftrightarrow ((φ \land i \in Z) \to ⦋ i / j ⦌ C \in ℝ))$
91		nfv	$⊢ Ⅎ k j \in Z$
92	1 91	nfan	$⊢ Ⅎ k (φ \land j \in Z)$
93		nfv	$⊢ Ⅎ k C \in ℝ$
94	92 93	nfim	$⊢ Ⅎ k ((φ \land j \in Z) \to C \in ℝ)$
95		eleq1	$⊢ k = j \to (k \in Z \leftrightarrow j \in Z)$
96	95	anbi2d	$⊢ k = j \to ((φ \land k \in Z) \leftrightarrow (φ \land j \in Z))$
97	6	eleq1d	$⊢ k = j \to (B \in ℝ \leftrightarrow C \in ℝ)$
98	96 97	imbi12d	$⊢ k = j \to (((φ \land k \in Z) \to B \in ℝ) \leftrightarrow ((φ \land j \in Z) \to C \in ℝ))$
99	94 98 5	chvarfv	$⊢ (φ \land j \in Z) \to C \in ℝ$
100	85 90 99	chvarfv	$⊢ (φ \land i \in Z) \to ⦋ i / j ⦌ C \in ℝ$
101		nfcv	$⊢ \underline{Ⅎ} k i$
102		nfcv	$⊢ \underline{Ⅎ} k ⦋ i / j ⦌ C$
103	101 102 33 76	fvmptf	$⊢ (i \in Z \land ⦋ i / j ⦌ C \in ℝ) \to (k \in Z ⟼ B) (i) = ⦋ i / j ⦌ C$
104	79 100 103	syl2anc	$⊢ (φ \land i \in Z) \to (k \in Z ⟼ B) (i) = ⦋ i / j ⦌ C$
105	78 104	breq12d	$⊢ (φ \land i \in Z) \to ((k \in Z ⟼ B) (i + 1) \leq (k \in Z ⟼ B) (i) \leftrightarrow ⦋ (i + 1) / k ⦌ B \leq ⦋ i / j ⦌ C)$
106	59 105	mpbird	$⊢ (φ \land i \in Z) \to (k \in Z ⟼ B) (i + 1) \leq (k \in Z ⟼ B) (i)$
107		breq1	$⊢ x = y \to (x \leq B \leftrightarrow y \leq B)$
108	107	ralbidv	$⊢ x = y \to (\forall k \in Z x \leq B \leftrightarrow \forall k \in Z y \leq B)$
109	108	cbvrexvw	$⊢ \exists x \in ℝ \forall k \in Z x \leq B \leftrightarrow \exists y \in ℝ \forall k \in Z y \leq B$
110	8 109	sylib	$⊢ φ \to \exists y \in ℝ \forall k \in Z y \leq B$
111		nfcv	$⊢ \underline{Ⅎ} k y$
112		nfcv	$⊢ \underline{Ⅎ} k \leq$
113		nfmpt1	$⊢ \underline{Ⅎ} k (k \in Z ⟼ B)$
114	113 101	nffv	$⊢ \underline{Ⅎ} k (k \in Z ⟼ B) (i)$
115	111 112 114	nfbr	$⊢ Ⅎ k y \leq (k \in Z ⟼ B) (i)$
116		nfv	$⊢ Ⅎ i y \leq (k \in Z ⟼ B) (k)$
117		fveq2	$⊢ i = k \to (k \in Z ⟼ B) (i) = (k \in Z ⟼ B) (k)$
118	117	breq2d	$⊢ i = k \to (y \leq (k \in Z ⟼ B) (i) \leftrightarrow y \leq (k \in Z ⟼ B) (k))$
119	115 116 118	cbvralw	$⊢ \forall i \in Z y \leq (k \in Z ⟼ B) (i) \leftrightarrow \forall k \in Z y \leq (k \in Z ⟼ B) (k)$
120	119	a1i	$⊢ φ \to (\forall i \in Z y \leq (k \in Z ⟼ B) (i) \leftrightarrow \forall k \in Z y \leq (k \in Z ⟼ B) (k))$
121	76	a1i	$⊢ φ \to (k \in Z ⟼ B) = (k \in Z ⟼ B)$
122	121 5	fvmpt2d	$⊢ (φ \land k \in Z) \to (k \in Z ⟼ B) (k) = B$
123	122	breq2d	$⊢ (φ \land k \in Z) \to (y \leq (k \in Z ⟼ B) (k) \leftrightarrow y \leq B)$
124	1 123	ralbida	$⊢ φ \to (\forall k \in Z y \leq (k \in Z ⟼ B) (k) \leftrightarrow \forall k \in Z y \leq B)$
125	120 124	bitrd	$⊢ φ \to (\forall i \in Z y \leq (k \in Z ⟼ B) (i) \leftrightarrow \forall k \in Z y \leq B)$
126	125	rexbidv	$⊢ φ \to (\exists y \in ℝ \forall i \in Z y \leq (k \in Z ⟼ B) (i) \leftrightarrow \exists y \in ℝ \forall k \in Z y \leq B)$
127	110 126	mpbird	$⊢ φ \to \exists y \in ℝ \forall i \in Z y \leq (k \in Z ⟼ B) (i)$
128	9 10 4 3 11 106 127	climinf2	$⊢ φ \to (k \in Z ⟼ B) ⇝ sup (ran (k \in Z ⟼ B) ℝ^{*} <)$

Metamath Proof Explorer

Theorem climinfmpt

Proof