Metamath Proof Explorer


Theorem fourierdlem31

Description: If A is finite and for any element in A there is a number m such that a property holds for all numbers larger than m , then there is a number n such that the property holds for all numbers larger than n and for all elements in A . (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 29-Sep-2020)

Ref Expression
Hypotheses fourierdlem31.i i φ
fourierdlem31.r r φ
fourierdlem31.iv _ i V
fourierdlem31.a φ A Fin
fourierdlem31.exm φ i A m r m +∞ χ
fourierdlem31.m M = m | r m +∞ χ
fourierdlem31.v V = i A sup M <
fourierdlem31.n N = sup ran V <
Assertion fourierdlem31 φ n r n +∞ i A χ

Proof

Step Hyp Ref Expression
1 fourierdlem31.i i φ
2 fourierdlem31.r r φ
3 fourierdlem31.iv _ i V
4 fourierdlem31.a φ A Fin
5 fourierdlem31.exm φ i A m r m +∞ χ
6 fourierdlem31.m M = m | r m +∞ χ
7 fourierdlem31.v V = i A sup M <
8 fourierdlem31.n N = sup ran V <
9 1nn 1
10 rzal A = i A χ
11 10 ralrimivw A = r 1 +∞ i A χ
12 oveq1 n = 1 n +∞ = 1 +∞
13 12 raleqdv n = 1 r n +∞ i A χ r 1 +∞ i A χ
14 13 rspcev 1 r 1 +∞ i A χ n r n +∞ i A χ
15 9 11 14 sylancr A = n r n +∞ i A χ
16 15 adantl φ A = n r n +∞ i A χ
17 6 a1i φ i A M = m | r m +∞ χ
18 17 infeq1d φ i A sup M < = sup m | r m +∞ χ <
19 ssrab2 m | r m +∞ χ
20 nnuz = 1
21 19 20 sseqtri m | r m +∞ χ 1
22 5 r19.21bi φ i A m r m +∞ χ
23 rabn0 m | r m +∞ χ m r m +∞ χ
24 22 23 sylibr φ i A m | r m +∞ χ
25 infssuzcl m | r m +∞ χ 1 m | r m +∞ χ sup m | r m +∞ χ < m | r m +∞ χ
26 21 24 25 sylancr φ i A sup m | r m +∞ χ < m | r m +∞ χ
27 19 26 sseldi φ i A sup m | r m +∞ χ <
28 18 27 eqeltrd φ i A sup M <
29 28 ex φ i A sup M <
30 1 29 ralrimi φ i A sup M <
31 7 rnmptss i A sup M < ran V
32 30 31 syl φ ran V
33 32 adantr φ ¬ A = ran V
34 ltso < Or
35 34 a1i φ ¬ A = < Or
36 mptfi A Fin i A sup M < Fin
37 4 36 syl φ i A sup M < Fin
38 7 37 eqeltrid φ V Fin
39 rnfi V Fin ran V Fin
40 38 39 syl φ ran V Fin
41 40 adantr φ ¬ A = ran V Fin
42 neqne ¬ A = A
43 n0 A i i A
44 42 43 sylib ¬ A = i i A
45 44 adantl φ ¬ A = i i A
46 nfv i ¬ A =
47 1 46 nfan i φ ¬ A =
48 3 nfrn _ i ran V
49 nfcv _ i
50 48 49 nfne i ran V
51 simpr φ i A i A
52 7 elrnmpt1 i A sup M < sup M < ran V
53 51 28 52 syl2anc φ i A sup M < ran V
54 53 ne0d φ i A ran V
55 54 ex φ i A ran V
56 55 adantr φ ¬ A = i A ran V
57 47 50 56 exlimd φ ¬ A = i i A ran V
58 45 57 mpd φ ¬ A = ran V
59 nnssre
60 33 59 sstrdi φ ¬ A = ran V
61 fisupcl < Or ran V Fin ran V ran V sup ran V < ran V
62 35 41 58 60 61 syl13anc φ ¬ A = sup ran V < ran V
63 33 62 sseldd φ ¬ A = sup ran V <
64 8 63 eqeltrid φ ¬ A = N
65 nfcv _ i
66 nfcv _ i <
67 48 65 66 nfsup _ i sup ran V <
68 8 67 nfcxfr _ i N
69 nfcv _ i .
70 nfcv _ i +∞
71 68 69 70 nfov _ i N +∞
72 71 nfcri i r N +∞
73 1 72 nfan i φ r N +∞
74 7 fvmpt2 i A sup M < V i = sup M <
75 51 28 74 syl2anc φ i A V i = sup M <
76 28 nnxrd φ i A sup M < *
77 75 76 eqeltrd φ i A V i *
78 77 adantr φ i A r N +∞ V i *
79 pnfxr +∞ *
80 79 a1i φ i A r N +∞ +∞ *
81 elioore r N +∞ r
82 81 adantl φ i A r N +∞ r
83 75 28 eqeltrd φ i A V i
84 83 nnred φ i A V i
85 84 adantr φ i A r N +∞ V i
86 ne0i i A A
87 86 adantl φ i A A
88 87 neneqd φ i A ¬ A =
89 88 64 syldan φ i A N
90 89 nnred φ i A N
91 90 adantr φ i A r N +∞ N
92 88 60 syldan φ i A ran V
93 32 59 sstrdi φ ran V
94 fimaxre2 ran V ran V Fin x y ran V y x
95 93 40 94 syl2anc φ x y ran V y x
96 95 adantr φ i A x y ran V y x
97 75 53 eqeltrd φ i A V i ran V
98 suprub ran V ran V x y ran V y x V i ran V V i sup ran V <
99 92 54 96 97 98 syl31anc φ i A V i sup ran V <
100 99 8 breqtrrdi φ i A V i N
101 100 adantr φ i A r N +∞ V i N
102 91 rexrd φ i A r N +∞ N *
103 simpr φ i A r N +∞ r N +∞
104 ioogtlb N * +∞ * r N +∞ N < r
105 102 80 103 104 syl3anc φ i A r N +∞ N < r
106 85 91 82 101 105 lelttrd φ i A r N +∞ V i < r
107 82 ltpnfd φ i A r N +∞ r < +∞
108 78 80 82 106 107 eliood φ i A r N +∞ r V i +∞
109 18 26 eqeltrd φ i A sup M < m | r m +∞ χ
110 75 109 eqeltrd φ i A V i m | r m +∞ χ
111 nfcv _ m A
112 nfrab1 _ m m | r m +∞ χ
113 6 112 nfcxfr _ m M
114 nfcv _ m
115 nfcv _ m <
116 113 114 115 nfinf _ m sup M <
117 111 116 nfmpt _ m i A sup M <
118 7 117 nfcxfr _ m V
119 nfcv _ m i
120 118 119 nffv _ m V i
121 120 112 nfel m V i m | r m +∞ χ
122 120 nfel1 m V i
123 nfcv _ m .
124 nfcv _ m +∞
125 120 123 124 nfov _ m V i +∞
126 nfv m χ
127 125 126 nfral m r V i +∞ χ
128 122 127 nfan m V i r V i +∞ χ
129 121 128 nfbi m V i m | r m +∞ χ V i r V i +∞ χ
130 eleq1 m = V i m m | r m +∞ χ V i m | r m +∞ χ
131 eleq1 m = V i m V i
132 oveq1 m = V i m +∞ = V i +∞
133 nfcv _ r m +∞
134 nfcv _ r A
135 nfra1 r r m +∞ χ
136 nfcv _ r
137 135 136 nfrab _ r m | r m +∞ χ
138 6 137 nfcxfr _ r M
139 nfcv _ r
140 nfcv _ r <
141 138 139 140 nfinf _ r sup M <
142 134 141 nfmpt _ r i A sup M <
143 7 142 nfcxfr _ r V
144 nfcv _ r i
145 143 144 nffv _ r V i
146 nfcv _ r .
147 nfcv _ r +∞
148 145 146 147 nfov _ r V i +∞
149 133 148 raleqf m +∞ = V i +∞ r m +∞ χ r V i +∞ χ
150 132 149 syl m = V i r m +∞ χ r V i +∞ χ
151 131 150 anbi12d m = V i m r m +∞ χ V i r V i +∞ χ
152 130 151 bibi12d m = V i m m | r m +∞ χ m r m +∞ χ V i m | r m +∞ χ V i r V i +∞ χ
153 rabid m m | r m +∞ χ m r m +∞ χ
154 120 129 152 153 vtoclgf V i V i m | r m +∞ χ V i r V i +∞ χ
155 83 154 syl φ i A V i m | r m +∞ χ V i r V i +∞ χ
156 110 155 mpbid φ i A V i r V i +∞ χ
157 156 simprd φ i A r V i +∞ χ
158 157 r19.21bi φ i A r V i +∞ χ
159 108 158 syldan φ i A r N +∞ χ
160 159 an32s φ r N +∞ i A χ
161 160 ex φ r N +∞ i A χ
162 73 161 ralrimi φ r N +∞ i A χ
163 162 ex φ r N +∞ i A χ
164 2 163 ralrimi φ r N +∞ i A χ
165 164 adantr φ ¬ A = r N +∞ i A χ
166 oveq1 n = N n +∞ = N +∞
167 nfcv _ r n +∞
168 143 nfrn _ r ran V
169 168 139 140 nfsup _ r sup ran V <
170 8 169 nfcxfr _ r N
171 170 146 147 nfov _ r N +∞
172 167 171 raleqf n +∞ = N +∞ r n +∞ i A χ r N +∞ i A χ
173 166 172 syl n = N r n +∞ i A χ r N +∞ i A χ
174 173 rspcev N r N +∞ i A χ n r n +∞ i A χ
175 64 165 174 syl2anc φ ¬ A = n r n +∞ i A χ
176 16 175 pm2.61dan φ n r n +∞ i A χ