This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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