Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem31 Structured version   Visualization version   Unicode version

Theorem fourierdlem31 38112
 Description: If is finite and for any element in there is a number such that a property holds for all numbers larger than , then there is a number such that the property holds for all numbers larger than and for all elements in . (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.)
Hypotheses
Ref Expression
fourierdlem31.i
fourierdlem31.r
fourierdlem31.iv
fourierdlem31.a
fourierdlem31.exm
fourierdlem31.m
fourierdlem31.v inf
fourierdlem31.n
Assertion
Ref Expression
fourierdlem31
Distinct variable groups:   ,,,   ,,,   ,   ,   ,
Allowed substitution hints:   (,,,)   (,)   (,,,)   (,,)   (,,,)

Proof of Theorem fourierdlem31
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1nn 10642 . . . 4
2 rzal 3862 . . . . 5
32ralrimivw 2810 . . . 4
4 oveq1 6315 . . . . . 6
54raleqdv 2979 . . . . 5
65rspcev 3136 . . . 4
71, 3, 6sylancr 676 . . 3
9 fourierdlem31.n . . . 4
10 fourierdlem31.i . . . . . . . 8
11 fourierdlem31.m . . . . . . . . . . . 12
1211a1i 11 . . . . . . . . . . 11
1312infeq1d 8011 . . . . . . . . . 10 inf inf
14 ssrab2 3500 . . . . . . . . . . 11
15 nnuz 11218 . . . . . . . . . . . . 13
1614, 15sseqtri 3450 . . . . . . . . . . . 12
17 fourierdlem31.exm . . . . . . . . . . . . . 14
1817r19.21bi 2776 . . . . . . . . . . . . 13
19 rabn0 3755 . . . . . . . . . . . . 13
2018, 19sylibr 217 . . . . . . . . . . . 12
21 infssuzcl 11268 . . . . . . . . . . . 12 inf
2216, 20, 21sylancr 676 . . . . . . . . . . 11 inf
2314, 22sseldi 3416 . . . . . . . . . 10 inf
2413, 23eqeltrd 2549 . . . . . . . . 9 inf
2524ex 441 . . . . . . . 8 inf
2610, 25ralrimi 2800 . . . . . . 7 inf
27 fourierdlem31.v . . . . . . . 8 inf
2827rnmptss 6068 . . . . . . 7 inf
2926, 28syl 17 . . . . . 6
3029adantr 472 . . . . 5
31 ltso 9732 . . . . . . 7
3231a1i 11 . . . . . 6
33 fourierdlem31.a . . . . . . . . . 10
34 mptfi 7891 . . . . . . . . . 10 inf
3533, 34syl 17 . . . . . . . . 9 inf
3627, 35syl5eqel 2553 . . . . . . . 8
37 rnfi 7875 . . . . . . . 8
3836, 37syl 17 . . . . . . 7
3938adantr 472 . . . . . 6
40 neqne 2651 . . . . . . . . 9
41 n0 3732 . . . . . . . . 9
4240, 41sylib 201 . . . . . . . 8
4342adantl 473 . . . . . . 7
44 nfv 1769 . . . . . . . . 9
4510, 44nfan 2031 . . . . . . . 8
46 fourierdlem31.iv . . . . . . . . . 10
4746nfrn 5083 . . . . . . . . 9
48 nfcv 2612 . . . . . . . . 9
4947, 48nfne 2742 . . . . . . . 8
50 simpr 468 . . . . . . . . . . . 12
5127elrnmpt1 5089 . . . . . . . . . . . 12 inf inf
5250, 24, 51syl2anc 673 . . . . . . . . . . 11 inf
53 ne0i 3728 . . . . . . . . . . 11 inf
5452, 53syl 17 . . . . . . . . . 10
5554ex 441 . . . . . . . . 9
5655adantr 472 . . . . . . . 8
5745, 49, 56exlimd 2017 . . . . . . 7
5843, 57mpd 15 . . . . . 6
59 nnssre 10635 . . . . . . 7
6030, 59syl6ss 3430 . . . . . 6
61 fisupcl 8003 . . . . . 6
6232, 39, 58, 60, 61syl13anc 1294 . . . . 5
6330, 62sseldd 3419 . . . 4
649, 63syl5eqel 2553 . . 3
65 fourierdlem31.r . . . . 5
66 nfcv 2612 . . . . . . . . . . . 12
67 nfcv 2612 . . . . . . . . . . . 12
6847, 66, 67nfsup 7983 . . . . . . . . . . 11
699, 68nfcxfr 2610 . . . . . . . . . 10
70 nfcv 2612 . . . . . . . . . 10
71 nfcv 2612 . . . . . . . . . 10
7269, 70, 71nfov 6334 . . . . . . . . 9
7372nfcri 2606 . . . . . . . 8
7410, 73nfan 2031 . . . . . . 7
7527fvmpt2 5972 . . . . . . . . . . . . . 14 inf inf
7650, 24, 75syl2anc 673 . . . . . . . . . . . . 13 inf
7724nnxrd 37426 . . . . . . . . . . . . 13 inf
7876, 77eqeltrd 2549 . . . . . . . . . . . 12
7978adantr 472 . . . . . . . . . . 11
80 pnfxr 11435 . . . . . . . . . . . 12
8180a1i 11 . . . . . . . . . . 11
82 elioore 11691 . . . . . . . . . . . 12
8382adantl 473 . . . . . . . . . . 11
8476, 24eqeltrd 2549 . . . . . . . . . . . . . 14
8584nnred 10646 . . . . . . . . . . . . 13
8685adantr 472 . . . . . . . . . . . 12
87 ne0i 3728 . . . . . . . . . . . . . . . . 17
8887adantl 473 . . . . . . . . . . . . . . . 16
8988neneqd 2648 . . . . . . . . . . . . . . 15
9089, 64syldan 478 . . . . . . . . . . . . . 14
9190nnred 10646 . . . . . . . . . . . . 13
9291adantr 472 . . . . . . . . . . . 12
9389, 60syldan 478 . . . . . . . . . . . . . . 15
9429, 59syl6ss 3430 . . . . . . . . . . . . . . . . 17
95 fimaxre2 10574 . . . . . . . . . . . . . . . . 17
9694, 38, 95syl2anc 673 . . . . . . . . . . . . . . . 16
9796adantr 472 . . . . . . . . . . . . . . 15
9876, 52eqeltrd 2549 . . . . . . . . . . . . . . 15
99 suprub 10592 . . . . . . . . . . . . . . 15
10093, 54, 97, 98, 99syl31anc 1295 . . . . . . . . . . . . . 14
101100, 9syl6breqr 4436 . . . . . . . . . . . . 13
102101adantr 472 . . . . . . . . . . . 12
10392rexrd 9708 . . . . . . . . . . . . 13
104 simpr 468 . . . . . . . . . . . . 13
105 ioogtlb 37688 . . . . . . . . . . . . 13
106103, 81, 104, 105syl3anc 1292 . . . . . . . . . . . 12
10786, 92, 83, 102, 106lelttrd 9810 . . . . . . . . . . 11
10883ltpnfd 11446 . . . . . . . . . . 11
10979, 81, 83, 107, 108eliood 37691 . . . . . . . . . 10
11013, 22eqeltrd 2549 . . . . . . . . . . . . . 14 inf
11176, 110eqeltrd 2549 . . . . . . . . . . . . 13
112 nfcv 2612 . . . . . . . . . . . . . . . . . 18
113 nfrab1 2957 . . . . . . . . . . . . . . . . . . . 20
11411, 113nfcxfr 2610 . . . . . . . . . . . . . . . . . . 19
115 nfcv 2612 . . . . . . . . . . . . . . . . . . 19
116 nfcv 2612 . . . . . . . . . . . . . . . . . . 19
117114, 115, 116nfinf 8016 . . . . . . . . . . . . . . . . . 18 inf
118112, 117nfmpt 4484 . . . . . . . . . . . . . . . . 17 inf
11927, 118nfcxfr 2610 . . . . . . . . . . . . . . . 16
120 nfcv 2612 . . . . . . . . . . . . . . . 16
121119, 120nffv 5886 . . . . . . . . . . . . . . 15
122121, 113nfel 2624 . . . . . . . . . . . . . . . 16
123121nfel1 2626 . . . . . . . . . . . . . . . . 17
124 nfcv 2612 . . . . . . . . . . . . . . . . . . 19
125 nfcv 2612 . . . . . . . . . . . . . . . . . . 19
126121, 124, 125nfov 6334 . . . . . . . . . . . . . . . . . 18
127 nfv 1769 . . . . . . . . . . . . . . . . . 18
128126, 127nfral 2789 . . . . . . . . . . . . . . . . 17
129123, 128nfan 2031 . . . . . . . . . . . . . . . 16
130122, 129nfbi 2037 . . . . . . . . . . . . . . 15
131 eleq1 2537 . . . . . . . . . . . . . . . 16
132 eleq1 2537 . . . . . . . . . . . . . . . . 17
133 oveq1 6315 . . . . . . . . . . . . . . . . . 18
134 nfcv 2612 . . . . . . . . . . . . . . . . . . 19
135 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . 23
136 nfra1 2785 . . . . . . . . . . . . . . . . . . . . . . . . . 26
137 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . . . 26
138136, 137nfrab 2958 . . . . . . . . . . . . . . . . . . . . . . . . 25
13911, 138nfcxfr 2610 . . . . . . . . . . . . . . . . . . . . . . . 24
140 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . 24
141 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . 24
142139, 140, 141nfinf 8016 . . . . . . . . . . . . . . . . . . . . . . 23 inf
143135, 142nfmpt 4484 . . . . . . . . . . . . . . . . . . . . . 22 inf
14427, 143nfcxfr 2610 . . . . . . . . . . . . . . . . . . . . 21
145 nfcv 2612 . . . . . . . . . . . . . . . . . . . . 21
146144, 145nffv 5886 . . . . . . . . . . . . . . . . . . . 20
147 nfcv 2612 . . . . . . . . . . . . . . . . . . . 20
148 nfcv 2612 . . . . . . . . . . . . . . . . . . . 20
149146, 147, 148nfov 6334 . . . . . . . . . . . . . . . . . . 19
150134, 149raleqf 2969 . . . . . . . . . . . . . . . . . 18
151133, 150syl 17 . . . . . . . . . . . . . . . . 17
152132, 151anbi12d 725 . . . . . . . . . . . . . . . 16
153131, 152bibi12d 328 . . . . . . . . . . . . . . 15
154 rabid 2953 . . . . . . . . . . . . . . 15
155121, 130, 153, 154vtoclgf 3091 . . . . . . . . . . . . . 14
15684, 155syl 17 . . . . . . . . . . . . 13
157111, 156mpbid 215 . . . . . . . . . . . 12
158157simprd 470 . . . . . . . . . . 11
159158r19.21bi 2776 . . . . . . . . . 10
160109, 159syldan 478 . . . . . . . . 9
161160an32s 821 . . . . . . . 8
162161ex 441 . . . . . . 7
16374, 162ralrimi 2800 . . . . . 6
164163ex 441 . . . . 5
16565, 164ralrimi 2800 . . . 4