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 
|- F/ i ph
fourierdlem31.r 
|- F/ r ph
fourierdlem31.iv 
|- F/_ i V
fourierdlem31.a 
|- ( ph -> A e. Fin )
fourierdlem31.exm 
|- ( ph -> A. i e. A E. m e. NN A. r e. ( m (,) +oo ) ch )
fourierdlem31.m 
|- M = { m e. NN | A. r e. ( m (,) +oo ) ch }
fourierdlem31.v 
|- V = ( i e. A |-> inf ( M , RR , < ) )
fourierdlem31.n 
|- N = sup ( ran V , RR , < )
Assertion fourierdlem31 
|- ( ph -> E. n e. NN A. r e. ( n (,) +oo ) A. i e. A ch )

Proof

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