Proof of Theorem fourierdlem47
Step | Hyp | Ref
| Expression |
1 | | fourierdlem47.m |
. . 3
|
2 | | fourierdlem47.x |
. . . . . . . . . . 11
|
3 | | fourierdlem47.a |
. . . . . . . . . . . 12
|
4 | 3 | abscld 14175 |
. . . . . . . . . . 11
|
5 | 2, 4 | syl5eqel 2705 |
. . . . . . . . . 10
|
6 | | fourierdlem47.y |
. . . . . . . . . . 11
|
7 | | fourierdlem47.c |
. . . . . . . . . . . 12
|
8 | 7 | abscld 14175 |
. . . . . . . . . . 11
|
9 | 6, 8 | syl5eqel 2705 |
. . . . . . . . . 10
|
10 | 5, 9 | readdcld 10069 |
. . . . . . . . 9
|
11 | | fourierdlem47.z |
. . . . . . . . . 10
|
12 | | fourierdlem47.f |
. . . . . . . . . . . 12
|
13 | 12 | abscld 14175 |
. . . . . . . . . . 11
|
14 | | fourierdlem47.ibl |
. . . . . . . . . . . 12
|
15 | 12, 14 | iblabs 23595 |
. . . . . . . . . . 11
|
16 | 13, 15 | itgrecl 23564 |
. . . . . . . . . 10
|
17 | 11, 16 | syl5eqel 2705 |
. . . . . . . . 9
|
18 | 10, 17 | readdcld 10069 |
. . . . . . . 8
|
19 | | fourierdlem47.e |
. . . . . . . . 9
|
20 | 19 | rpred 11872 |
. . . . . . . 8
|
21 | 19 | rpne0d 11877 |
. . . . . . . 8
|
22 | 18, 20, 21 | redivcld 10853 |
. . . . . . 7
|
23 | | 1red 10055 |
. . . . . . 7
|
24 | 22, 23 | readdcld 10069 |
. . . . . 6
|
25 | 24 | flcld 12599 |
. . . . 5
|
26 | | 0red 10041 |
. . . . . 6
|
27 | | reflcl 12597 |
. . . . . . 7
|
28 | 24, 27 | syl 17 |
. . . . . 6
|
29 | | 0lt1 10550 |
. . . . . . 7
|
30 | 29 | a1i 11 |
. . . . . 6
|
31 | 3 | absge0d 14183 |
. . . . . . . . . . . . 13
|
32 | 31, 2 | syl6breqr 4695 |
. . . . . . . . . . . 12
|
33 | 7 | absge0d 14183 |
. . . . . . . . . . . . 13
|
34 | 33, 6 | syl6breqr 4695 |
. . . . . . . . . . . 12
|
35 | 5, 9, 32, 34 | addge0d 10603 |
. . . . . . . . . . 11
|
36 | 12 | absge0d 14183 |
. . . . . . . . . . . . 13
|
37 | 15, 13, 36 | itgge0 23577 |
. . . . . . . . . . . 12
|
38 | 37, 11 | syl6breqr 4695 |
. . . . . . . . . . 11
|
39 | 10, 17, 35, 38 | addge0d 10603 |
. . . . . . . . . 10
|
40 | 18, 19, 39 | divge0d 11912 |
. . . . . . . . 9
|
41 | | flge0nn0 12621 |
. . . . . . . . 9
|
42 | 22, 40, 41 | syl2anc 693 |
. . . . . . . 8
|
43 | | nn0addge1 11339 |
. . . . . . . 8
|
44 | 23, 42, 43 | syl2anc 693 |
. . . . . . 7
|
45 | | 1z 11407 |
. . . . . . . . 9
|
46 | | fladdz 12626 |
. . . . . . . . 9
|
47 | 22, 45, 46 | sylancl 694 |
. . . . . . . 8
|
48 | 42 | nn0cnd 11353 |
. . . . . . . . 9
|
49 | 23 | recnd 10068 |
. . . . . . . . 9
|
50 | 48, 49 | addcomd 10238 |
. . . . . . . 8
|
51 | 47, 50 | eqtr2d 2657 |
. . . . . . 7
|
52 | 44, 51 | breqtrd 4679 |
. . . . . 6
|
53 | 26, 23, 28, 30, 52 | ltletrd 10197 |
. . . . 5
|
54 | | elnnz 11387 |
. . . . 5
|
55 | 25, 53, 54 | sylanbrc 698 |
. . . 4
|
56 | 55 | peano2nnd 11037 |
. . 3
|
57 | 1, 56 | syl5eqel 2705 |
. 2
|
58 | | elioore 12205 |
. . . . 5
|
59 | | fourierdlem47.iblmul |
. . . . 5
|
60 | 58, 59 | sylan2 491 |
. . . 4
|
61 | 12 | adantlr 751 |
. . . 4
|
62 | | simpll 790 |
. . . . 5
|
63 | | simpr 477 |
. . . . 5
|
64 | 58 | ad2antlr 763 |
. . . . . 6
|
65 | 64 | recnd 10068 |
. . . . 5
|
66 | | fourierdlem47.g |
. . . . 5
|
67 | 62, 63, 65, 66 | syl21anc 1325 |
. . . 4
|
68 | 3 | adantr 481 |
. . . 4
|
69 | 7 | adantr 481 |
. . . 4
|
70 | | eqid 2622 |
. . . 4
|
71 | 19 | adantr 481 |
. . . 4
|
72 | 58 | adantl 482 |
. . . 4
|
73 | 2 | eqcomi 2631 |
. . . . . . . . . 10
|
74 | 6 | eqcomi 2631 |
. . . . . . . . . 10
|
75 | 73, 74 | oveq12i 6662 |
. . . . . . . . 9
|
76 | 75 | oveq1i 6660 |
. . . . . . . 8
|
77 | 4 | adantr 481 |
. . . . . . . . . 10
|
78 | 8 | adantr 481 |
. . . . . . . . . 10
|
79 | 77, 78 | readdcld 10069 |
. . . . . . . . 9
|
80 | 67 | negcld 10379 |
. . . . . . . . . . . 12
|
81 | 61, 80 | mulcld 10060 |
. . . . . . . . . . 11
|
82 | 81, 60 | itgcl 23550 |
. . . . . . . . . 10
|
83 | 82 | abscld 14175 |
. . . . . . . . 9
|
84 | 79, 83 | readdcld 10069 |
. . . . . . . 8
|
85 | 76, 84 | syl5eqelr 2706 |
. . . . . . 7
|
86 | 20 | adantr 481 |
. . . . . . 7
|
87 | 21 | adantr 481 |
. . . . . . 7
|
88 | 85, 86, 87 | redivcld 10853 |
. . . . . 6
|
89 | | 1red 10055 |
. . . . . 6
|
90 | 88, 89 | readdcld 10069 |
. . . . 5
|
91 | 2, 77 | syl5eqel 2705 |
. . . . . . . . . . . . 13
|
92 | 6, 78 | syl5eqel 2705 |
. . . . . . . . . . . . 13
|
93 | 91, 92 | readdcld 10069 |
. . . . . . . . . . . 12
|
94 | 17 | adantr 481 |
. . . . . . . . . . . 12
|
95 | 93, 94 | readdcld 10069 |
. . . . . . . . . . 11
|
96 | 95, 86, 87 | redivcld 10853 |
. . . . . . . . . 10
|
97 | 96, 89 | readdcld 10069 |
. . . . . . . . 9
|
98 | 97, 27 | syl 17 |
. . . . . . . 8
|
99 | 98, 89 | readdcld 10069 |
. . . . . . 7
|
100 | 1, 99 | syl5eqel 2705 |
. . . . . 6
|
101 | 81 | abscld 14175 |
. . . . . . . . . . . . 13
|
102 | 81, 60 | iblabs 23595 |
. . . . . . . . . . . . 13
|
103 | 101, 102 | itgrecl 23564 |
. . . . . . . . . . . 12
|
104 | 81, 60 | itgabs 23601 |
. . . . . . . . . . . 12
|
105 | 15 | adantr 481 |
. . . . . . . . . . . . . 14
|
106 | 61 | abscld 14175 |
. . . . . . . . . . . . . 14
|
107 | 61, 80 | absmuld 14193 |
. . . . . . . . . . . . . . 15
|
108 | 80 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
|
109 | | 1red 10055 |
. . . . . . . . . . . . . . . . 17
|
110 | 61 | absge0d 14183 |
. . . . . . . . . . . . . . . . 17
|
111 | | recn 10026 |
. . . . . . . . . . . . . . . . . . . . 21
|
112 | 111, 66 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . 20
|
113 | 112 | absnegd 14188 |
. . . . . . . . . . . . . . . . . . 19
|
114 | | fourierdlem47.absg |
. . . . . . . . . . . . . . . . . . 19
|
115 | 113, 114 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . 18
|
116 | 62, 63, 64, 115 | syl21anc 1325 |
. . . . . . . . . . . . . . . . 17
|
117 | 108, 109,
106, 110, 116 | lemul2ad 10964 |
. . . . . . . . . . . . . . . 16
|
118 | 106 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
119 | 118 | mulid1d 10057 |
. . . . . . . . . . . . . . . 16
|
120 | 117, 119 | breqtrd 4679 |
. . . . . . . . . . . . . . 15
|
121 | 107, 120 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
|
122 | 102, 105,
101, 106, 121 | itgle 23576 |
. . . . . . . . . . . . 13
|
123 | 122, 11 | syl6breqr 4695 |
. . . . . . . . . . . 12
|
124 | 83, 103, 94, 104, 123 | letrd 10194 |
. . . . . . . . . . 11
|
125 | 83, 94, 93, 124 | leadd2dd 10642 |
. . . . . . . . . 10
|
126 | 85, 95, 71, 125 | lediv1dd 11930 |
. . . . . . . . 9
|
127 | | flltp1 12601 |
. . . . . . . . . . 11
|
128 | 96, 127 | syl 17 |
. . . . . . . . . 10
|
129 | 96, 45, 46 | sylancl 694 |
. . . . . . . . . 10
|
130 | 128, 129 | breqtrrd 4681 |
. . . . . . . . 9
|
131 | 88, 96, 98, 126, 130 | lelttrd 10195 |
. . . . . . . 8
|
132 | 88, 98, 89, 131 | ltadd1dd 10638 |
. . . . . . 7
|
133 | 132, 1 | syl6breqr 4695 |
. . . . . 6
|
134 | 100 | rexrd 10089 |
. . . . . . 7
|
135 | | pnfxr 10092 |
. . . . . . . 8
|
136 | 135 | a1i 11 |
. . . . . . 7
|
137 | | simpr 477 |
. . . . . . 7
|
138 | | ioogtlb 39717 |
. . . . . . 7
|
139 | 134, 136,
137, 138 | syl3anc 1326 |
. . . . . 6
|
140 | 90, 100, 72, 133, 139 | lttrd 10198 |
. . . . 5
|
141 | 90, 72, 140 | ltled 10185 |
. . . 4
|
142 | 72 | recnd 10068 |
. . . . 5
|
143 | | fourierdlem47.b |
. . . . 5
|
144 | 142, 143 | syldan 487 |
. . . 4
|
145 | | fourierdlem47.absb |
. . . . 5
|
146 | 58, 145 | sylan2 491 |
. . . 4
|
147 | | fourierdlem47.d |
. . . . 5
|
148 | 142, 147 | syldan 487 |
. . . 4
|
149 | | fourierdlem47.absd |
. . . . 5
|
150 | 58, 149 | sylan2 491 |
. . . 4
|
151 | 60, 61, 67, 68, 2, 69, 6, 70, 71, 72, 141, 144, 146, 148, 150 | fourierdlem30 40354 |
. . 3
|
152 | 151 | ralrimiva 2966 |
. 2
|
153 | | oveq1 6657 |
. . . 4
|
154 | 153 | raleqdv 3144 |
. . 3
|
155 | 154 | rspcev 3309 |
. 2
|
156 | 57, 152, 155 | syl2anc 693 |
1
|