Proof of Theorem fourierdlem30
Step | Hyp | Ref
| Expression |
1 | | fourierdlem30.b |
. . . . . . . . . . 11
|
2 | | fourierdlem30.r |
. . . . . . . . . . . 12
|
3 | 2 | recnd 10068 |
. . . . . . . . . . 11
|
4 | | 0red 10041 |
. . . . . . . . . . . . 13
|
5 | | 1red 10055 |
. . . . . . . . . . . . 13
|
6 | | 0lt1 10550 |
. . . . . . . . . . . . . 14
|
7 | 6 | a1i 11 |
. . . . . . . . . . . . 13
|
8 | | fourierdlem30.x |
. . . . . . . . . . . . . . . . . . 19
|
9 | | fourierdlem30.a |
. . . . . . . . . . . . . . . . . . . 20
|
10 | 9 | abscld 14175 |
. . . . . . . . . . . . . . . . . . 19
|
11 | 8, 10 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . 18
|
12 | | fourierdlem30.y |
. . . . . . . . . . . . . . . . . . 19
|
13 | | fourierdlem30.c |
. . . . . . . . . . . . . . . . . . . 20
|
14 | 13 | abscld 14175 |
. . . . . . . . . . . . . . . . . . 19
|
15 | 12, 14 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . 18
|
16 | 11, 15 | readdcld 10069 |
. . . . . . . . . . . . . . . . 17
|
17 | | fourierdlem30.z |
. . . . . . . . . . . . . . . . . 18
|
18 | | fourierlemreimleblemlte22.f |
. . . . . . . . . . . . . . . . . . . . 21
|
19 | | fourierdlem30.g |
. . . . . . . . . . . . . . . . . . . . . 22
|
20 | 19 | negcld 10379 |
. . . . . . . . . . . . . . . . . . . . 21
|
21 | 18, 20 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . 20
|
22 | | fourierdlem30.ibl |
. . . . . . . . . . . . . . . . . . . 20
|
23 | 21, 22 | itgcl 23550 |
. . . . . . . . . . . . . . . . . . 19
|
24 | 23 | abscld 14175 |
. . . . . . . . . . . . . . . . . 18
|
25 | 17, 24 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . 17
|
26 | 16, 25 | readdcld 10069 |
. . . . . . . . . . . . . . . 16
|
27 | | fourierdlem30.e |
. . . . . . . . . . . . . . . . 17
|
28 | 27 | rpred 11872 |
. . . . . . . . . . . . . . . 16
|
29 | 27 | rpne0d 11877 |
. . . . . . . . . . . . . . . 16
|
30 | 26, 28, 29 | redivcld 10853 |
. . . . . . . . . . . . . . 15
|
31 | 30, 5 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
32 | 9 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . 19
|
33 | 32, 8 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . . 18
|
34 | 13 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . 19
|
35 | 34, 12 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . . 18
|
36 | 11, 15, 33, 35 | addge0d 10603 |
. . . . . . . . . . . . . . . . 17
|
37 | 23 | absge0d 14183 |
. . . . . . . . . . . . . . . . . 18
|
38 | 37, 17 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . 17
|
39 | 16, 25, 36, 38 | addge0d 10603 |
. . . . . . . . . . . . . . . 16
|
40 | 26, 27, 39 | divge0d 11912 |
. . . . . . . . . . . . . . 15
|
41 | 5, 30 | addge02d 10616 |
. . . . . . . . . . . . . . 15
|
42 | 40, 41 | mpbid 222 |
. . . . . . . . . . . . . 14
|
43 | | fourierdlem30.ler |
. . . . . . . . . . . . . 14
|
44 | 5, 31, 2, 42, 43 | letrd 10194 |
. . . . . . . . . . . . 13
|
45 | 4, 5, 2, 7, 44 | ltletrd 10197 |
. . . . . . . . . . . 12
|
46 | 45 | gt0ne0d 10592 |
. . . . . . . . . . 11
|
47 | 1, 3, 46 | divnegd 10814 |
. . . . . . . . . 10
|
48 | 47 | oveq2d 6666 |
. . . . . . . . 9
|
49 | 1 | negcld 10379 |
. . . . . . . . . 10
|
50 | 9, 49, 3, 46 | divassd 10836 |
. . . . . . . . 9
|
51 | 48, 50 | eqtr4d 2659 |
. . . . . . . 8
|
52 | | fourierdlem30.d |
. . . . . . . . . . 11
|
53 | 52, 3, 46 | divnegd 10814 |
. . . . . . . . . 10
|
54 | 53 | oveq2d 6666 |
. . . . . . . . 9
|
55 | 52 | negcld 10379 |
. . . . . . . . . 10
|
56 | 13, 55, 3, 46 | divassd 10836 |
. . . . . . . . 9
|
57 | 54, 56 | eqtr4d 2659 |
. . . . . . . 8
|
58 | 51, 57 | oveq12d 6668 |
. . . . . . 7
|
59 | 9, 49 | mulcld 10060 |
. . . . . . . 8
|
60 | 13, 55 | mulcld 10060 |
. . . . . . . 8
|
61 | 59, 60, 3, 46 | divsubdird 10840 |
. . . . . . 7
|
62 | 58, 61 | eqtr4d 2659 |
. . . . . 6
|
63 | 3, 46 | reccld 10794 |
. . . . . . . 8
|
64 | 63, 21, 22 | itgmulc2 23600 |
. . . . . . 7
|
65 | 23, 3, 46 | divrec2d 10805 |
. . . . . . 7
|
66 | 3 | adantr 481 |
. . . . . . . . . . 11
|
67 | 46 | adantr 481 |
. . . . . . . . . . 11
|
68 | 19, 66, 67 | divnegd 10814 |
. . . . . . . . . 10
|
69 | 68 | oveq2d 6666 |
. . . . . . . . 9
|
70 | 18, 20, 66, 67 | divassd 10836 |
. . . . . . . . 9
|
71 | 21, 66, 67 | divrec2d 10805 |
. . . . . . . . 9
|
72 | 69, 70, 71 | 3eqtr2d 2662 |
. . . . . . . 8
|
73 | 72 | itgeq2dv 23548 |
. . . . . . 7
|
74 | 64, 65, 73 | 3eqtr4rd 2667 |
. . . . . 6
|
75 | 62, 74 | oveq12d 6668 |
. . . . 5
|
76 | 59, 60 | subcld 10392 |
. . . . . 6
|
77 | 76, 23, 3, 46 | divsubdird 10840 |
. . . . 5
|
78 | 75, 77 | eqtr4d 2659 |
. . . 4
|
79 | 78 | fveq2d 6195 |
. . 3
|
80 | 76, 23 | subcld 10392 |
. . . 4
|
81 | 80, 3, 46 | absdivd 14194 |
. . 3
|
82 | 4, 2, 45 | ltled 10185 |
. . . . 5
|
83 | 2, 82 | absidd 14161 |
. . . 4
|
84 | 83 | oveq2d 6666 |
. . 3
|
85 | 79, 81, 84 | 3eqtrd 2660 |
. 2
|
86 | 80 | abscld 14175 |
. . . 4
|
87 | 86, 2, 46 | redivcld 10853 |
. . 3
|
88 | 10, 14 | readdcld 10069 |
. . . . 5
|
89 | 88, 24 | readdcld 10069 |
. . . 4
|
90 | 89, 2, 46 | redivcld 10853 |
. . 3
|
91 | 2, 45 | elrpd 11869 |
. . . 4
|
92 | 76 | abscld 14175 |
. . . . . 6
|
93 | 92, 24 | readdcld 10069 |
. . . . 5
|
94 | 76, 23 | abs2dif2d 14197 |
. . . . 5
|
95 | 59 | abscld 14175 |
. . . . . . . 8
|
96 | 60 | abscld 14175 |
. . . . . . . 8
|
97 | 95, 96 | readdcld 10069 |
. . . . . . 7
|
98 | 59, 60 | abs2dif2d 14197 |
. . . . . . 7
|
99 | 9, 49 | absmuld 14193 |
. . . . . . . . 9
|
100 | 49 | abscld 14175 |
. . . . . . . . . . 11
|
101 | 1 | absnegd 14188 |
. . . . . . . . . . . 12
|
102 | | fourierdlem30.12 |
. . . . . . . . . . . 12
|
103 | 101, 102 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
104 | 100, 5, 10, 32, 103 | lemul2ad 10964 |
. . . . . . . . . 10
|
105 | 10 | recnd 10068 |
. . . . . . . . . . 11
|
106 | 105 | mulid1d 10057 |
. . . . . . . . . 10
|
107 | 104, 106 | breqtrd 4679 |
. . . . . . . . 9
|
108 | 99, 107 | eqbrtrd 4675 |
. . . . . . . 8
|
109 | 13, 55 | absmuld 14193 |
. . . . . . . . 9
|
110 | 55 | abscld 14175 |
. . . . . . . . . . 11
|
111 | 52 | absnegd 14188 |
. . . . . . . . . . . 12
|
112 | | fourierdlem30.14 |
. . . . . . . . . . . 12
|
113 | 111, 112 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
114 | 110, 5, 14, 34, 113 | lemul2ad 10964 |
. . . . . . . . . 10
|
115 | 14 | recnd 10068 |
. . . . . . . . . . 11
|
116 | 115 | mulid1d 10057 |
. . . . . . . . . 10
|
117 | 114, 116 | breqtrd 4679 |
. . . . . . . . 9
|
118 | 109, 117 | eqbrtrd 4675 |
. . . . . . . 8
|
119 | 95, 96, 10, 14, 108, 118 | le2addd 10646 |
. . . . . . 7
|
120 | 92, 97, 88, 98, 119 | letrd 10194 |
. . . . . 6
|
121 | 92, 88, 24, 120 | leadd1dd 10641 |
. . . . 5
|
122 | 86, 93, 89, 94, 121 | letrd 10194 |
. . . 4
|
123 | 86, 89, 91, 122 | lediv1dd 11930 |
. . 3
|
124 | 30 | ltp1d 10954 |
. . . . . . 7
|
125 | 4, 30, 31, 40, 124 | lelttrd 10195 |
. . . . . 6
|
126 | 125 | gt0ne0d 10592 |
. . . . 5
|
127 | 89, 31, 126 | redivcld 10853 |
. . . 4
|
128 | 30, 40 | ge0p1rpd 11902 |
. . . . 5
|
129 | 8 | eqcomi 2631 |
. . . . . . . 8
|
130 | 12 | eqcomi 2631 |
. . . . . . . 8
|
131 | 129, 130 | oveq12i 6662 |
. . . . . . 7
|
132 | 17 | eqcomi 2631 |
. . . . . . 7
|
133 | 131, 132 | oveq12i 6662 |
. . . . . 6
|
134 | 39, 133 | syl6breqr 4695 |
. . . . 5
|
135 | 128, 91, 89, 134, 43 | lediv2ad 11894 |
. . . 4
|
136 | 133 | oveq1i 6660 |
. . . . 5
|
137 | | oveq1 6657 |
. . . . . . . . 9
|
138 | 137 | adantl 482 |
. . . . . . . 8
|
139 | 30 | recnd 10068 |
. . . . . . . . . . 11
|
140 | 5 | recnd 10068 |
. . . . . . . . . . 11
|
141 | 139, 140 | addcld 10059 |
. . . . . . . . . 10
|
142 | 141 | adantr 481 |
. . . . . . . . 9
|
143 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
144 | 143 | adantl 482 |
. . . . . . . . . . . . 13
|
145 | 27 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
|
146 | 145 | adantr 481 |
. . . . . . . . . . . . . 14
|
147 | 29 | adantr 481 |
. . . . . . . . . . . . . 14
|
148 | 146, 147 | div0d 10800 |
. . . . . . . . . . . . 13
|
149 | 144, 148 | eqtrd 2656 |
. . . . . . . . . . . 12
|
150 | 149 | oveq1d 6665 |
. . . . . . . . . . 11
|
151 | | 0p1e1 11132 |
. . . . . . . . . . 11
|
152 | 150, 151 | syl6eq 2672 |
. . . . . . . . . 10
|
153 | | ax-1ne0 10005 |
. . . . . . . . . . 11
|
154 | 153 | a1i 11 |
. . . . . . . . . 10
|
155 | 152, 154 | eqnetrd 2861 |
. . . . . . . . 9
|
156 | 142, 155 | div0d 10800 |
. . . . . . . 8
|
157 | 138, 156 | eqtrd 2656 |
. . . . . . 7
|
158 | 27 | rpgt0d 11875 |
. . . . . . . 8
|
159 | 158 | adantr 481 |
. . . . . . 7
|
160 | 157, 159 | eqbrtrd 4675 |
. . . . . 6
|
161 | 26 | adantr 481 |
. . . . . . 7
|
162 | 27 | adantr 481 |
. . . . . . 7
|
163 | 39 | adantr 481 |
. . . . . . . . . . 11
|
164 | | neqne 2802 |
. . . . . . . . . . . 12
|
165 | 164 | adantl 482 |
. . . . . . . . . . 11
|
166 | 161, 163,
165 | ne0gt0d 10174 |
. . . . . . . . . 10
|
167 | 161, 166 | elrpd 11869 |
. . . . . . . . 9
|
168 | 167, 162 | rpdivcld 11889 |
. . . . . . . 8
|
169 | | 1rp 11836 |
. . . . . . . . 9
|
170 | 169 | a1i 11 |
. . . . . . . 8
|
171 | 168, 170 | rpaddcld 11887 |
. . . . . . 7
|
172 | 124 | adantr 481 |
. . . . . . 7
|
173 | 161, 162,
171, 172 | ltdiv23d 11937 |
. . . . . 6
|
174 | 160, 173 | pm2.61dan 832 |
. . . . 5
|
175 | 136, 174 | syl5eqbr 4688 |
. . . 4
|
176 | 90, 127, 28, 135, 175 | lelttrd 10195 |
. . 3
|
177 | 87, 90, 28, 123, 176 | lelttrd 10195 |
. 2
|
178 | 85, 177 | eqbrtrd 4675 |
1
|