Metamath Proof Explorer


Theorem 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 𝑘 𝜑
climinfmpt.j 𝑗 𝜑
climinfmpt.m ( 𝜑𝑀 ∈ ℤ )
climinfmpt.z 𝑍 = ( ℤ𝑀 )
climinfmpt.b ( ( 𝜑𝑘𝑍 ) → 𝐵 ∈ ℝ )
climinfmpt.c ( 𝑘 = 𝑗𝐵 = 𝐶 )
climinfmpt.l ( ( 𝜑𝑘𝑍𝑗 = ( 𝑘 + 1 ) ) → 𝐶𝐵 )
climinfmpt.e ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍 𝑥𝐵 )
Assertion climinfmpt ( 𝜑 → ( 𝑘𝑍𝐵 ) ⇝ inf ( ran ( 𝑘𝑍𝐵 ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 climinfmpt.p 𝑘 𝜑
2 climinfmpt.j 𝑗 𝜑
3 climinfmpt.m ( 𝜑𝑀 ∈ ℤ )
4 climinfmpt.z 𝑍 = ( ℤ𝑀 )
5 climinfmpt.b ( ( 𝜑𝑘𝑍 ) → 𝐵 ∈ ℝ )
6 climinfmpt.c ( 𝑘 = 𝑗𝐵 = 𝐶 )
7 climinfmpt.l ( ( 𝜑𝑘𝑍𝑗 = ( 𝑘 + 1 ) ) → 𝐶𝐵 )
8 climinfmpt.e ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍 𝑥𝐵 )
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 breq1 ( 𝑥 = 𝑦 → ( 𝑥𝐵𝑦𝐵 ) )
108 107 ralbidv ( 𝑥 = 𝑦 → ( ∀ 𝑘𝑍 𝑥𝐵 ↔ ∀ 𝑘𝑍 𝑦𝐵 ) )
109 108 cbvrexvw ( ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍 𝑥𝐵 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑘𝑍 𝑦𝐵 )
110 8 109 sylib ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑘𝑍 𝑦𝐵 )
111 nfcv 𝑘 𝑦
112 nfcv 𝑘
113 nfmpt1 𝑘 ( 𝑘𝑍𝐵 )
114 113 101 nffv 𝑘 ( ( 𝑘𝑍𝐵 ) ‘ 𝑖 )
115 111 112 114 nfbr 𝑘 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑖 )
116 nfv 𝑖 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑘 )
117 fveq2 ( 𝑖 = 𝑘 → ( ( 𝑘𝑍𝐵 ) ‘ 𝑖 ) = ( ( 𝑘𝑍𝐵 ) ‘ 𝑘 ) )
118 117 breq2d ( 𝑖 = 𝑘 → ( 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑖 ) ↔ 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑘 ) ) )
119 115 116 118 cbvralw ( ∀ 𝑖𝑍 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑖 ) ↔ ∀ 𝑘𝑍 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑘 ) )
120 119 a1i ( 𝜑 → ( ∀ 𝑖𝑍 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑖 ) ↔ ∀ 𝑘𝑍 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑘 ) ) )
121 76 a1i ( 𝜑 → ( 𝑘𝑍𝐵 ) = ( 𝑘𝑍𝐵 ) )
122 121 5 fvmpt2d ( ( 𝜑𝑘𝑍 ) → ( ( 𝑘𝑍𝐵 ) ‘ 𝑘 ) = 𝐵 )
123 122 breq2d ( ( 𝜑𝑘𝑍 ) → ( 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑘 ) ↔ 𝑦𝐵 ) )
124 1 123 ralbida ( 𝜑 → ( ∀ 𝑘𝑍 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑘 ) ↔ ∀ 𝑘𝑍 𝑦𝐵 ) )
125 120 124 bitrd ( 𝜑 → ( ∀ 𝑖𝑍 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑖 ) ↔ ∀ 𝑘𝑍 𝑦𝐵 ) )
126 125 rexbidv ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑖𝑍 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑖 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑘𝑍 𝑦𝐵 ) )
127 110 126 mpbird ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑖𝑍 𝑦 ≤ ( ( 𝑘𝑍𝐵 ) ‘ 𝑖 ) )
128 9 10 4 3 11 106 127 climinf2 ( 𝜑 → ( 𝑘𝑍𝐵 ) ⇝ inf ( ran ( 𝑘𝑍𝐵 ) , ℝ* , < ) )