Proof of Theorem fourierdlem37
Step | Hyp | Ref
| Expression |
1 | | ssrab2 3687 |
. . . 4
..^ ..^ |
2 | | ltso 10118 |
. . . . . 6
|
3 | 2 | a1i 11 |
. . . . 5
|
4 | | fzfi 12771 |
. . . . . . 7
|
5 | | fzossfz 12488 |
. . . . . . . 8
..^ |
6 | 1, 5 | sstri 3612 |
. . . . . . 7
..^ |
7 | | ssfi 8180 |
. . . . . . 7
..^ ..^ |
8 | 4, 6, 7 | mp2an 708 |
. . . . . 6
..^ |
9 | 8 | a1i 11 |
. . . . 5
..^ |
10 | | 0zd 11389 |
. . . . . . . . 9
|
11 | | fourierdlem37.m |
. . . . . . . . . 10
|
12 | 11 | nnzd 11481 |
. . . . . . . . 9
|
13 | 11 | nngt0d 11064 |
. . . . . . . . 9
|
14 | | fzolb 12476 |
. . . . . . . . 9
..^ |
15 | 10, 12, 13, 14 | syl3anbrc 1246 |
. . . . . . . 8
..^ |
16 | 15 | adantr 481 |
. . . . . . 7
..^ |
17 | | fourierdlem37.q |
. . . . . . . . . . . . . . . 16
|
18 | | fourierdlem37.p |
. . . . . . . . . . . . . . . . . 18
..^ |
19 | 18 | fourierdlem2 40326 |
. . . . . . . . . . . . . . . . 17
..^ |
20 | 11, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
..^ |
21 | 17, 20 | mpbid 222 |
. . . . . . . . . . . . . . 15
..^ |
22 | 21 | simprd 479 |
. . . . . . . . . . . . . 14
..^ |
23 | 22 | simplld 791 |
. . . . . . . . . . . . 13
|
24 | 18, 11, 17 | fourierdlem11 40335 |
. . . . . . . . . . . . . 14
|
25 | 24 | simp1d 1073 |
. . . . . . . . . . . . 13
|
26 | 23, 25 | eqeltrd 2701 |
. . . . . . . . . . . 12
|
27 | 26, 23 | eqled 10140 |
. . . . . . . . . . 11
|
28 | 27 | ad2antrr 762 |
. . . . . . . . . 10
|
29 | | iftrue 4092 |
. . . . . . . . . . . 12
|
30 | 29 | eqcomd 2628 |
. . . . . . . . . . 11
|
31 | 30 | adantl 482 |
. . . . . . . . . 10
|
32 | 28, 31 | breqtrd 4679 |
. . . . . . . . 9
|
33 | 26 | adantr 481 |
. . . . . . . . . . . 12
|
34 | 25 | adantr 481 |
. . . . . . . . . . . . . . 15
|
35 | 34 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
36 | 24 | simp2d 1074 |
. . . . . . . . . . . . . . 15
|
37 | 36 | adantr 481 |
. . . . . . . . . . . . . 14
|
38 | | iocssre 12253 |
. . . . . . . . . . . . . 14
|
39 | 35, 37, 38 | syl2anc 693 |
. . . . . . . . . . . . 13
|
40 | 24 | simp3d 1075 |
. . . . . . . . . . . . . . 15
|
41 | | fourierdlem37.t |
. . . . . . . . . . . . . . 15
|
42 | | fourierdlem37.e |
. . . . . . . . . . . . . . 15
|
43 | 25, 36, 40, 41, 42 | fourierdlem4 40328 |
. . . . . . . . . . . . . 14
|
44 | 43 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
45 | 39, 44 | sseldd 3604 |
. . . . . . . . . . . 12
|
46 | 23 | adantr 481 |
. . . . . . . . . . . . 13
|
47 | | elioc2 12236 |
. . . . . . . . . . . . . . . 16
|
48 | 35, 37, 47 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
49 | 44, 48 | mpbid 222 |
. . . . . . . . . . . . . 14
|
50 | 49 | simp2d 1074 |
. . . . . . . . . . . . 13
|
51 | 46, 50 | eqbrtrd 4675 |
. . . . . . . . . . . 12
|
52 | 33, 45, 51 | ltled 10185 |
. . . . . . . . . . 11
|
53 | 52 | adantr 481 |
. . . . . . . . . 10
|
54 | | iffalse 4095 |
. . . . . . . . . . . 12
|
55 | 54 | eqcomd 2628 |
. . . . . . . . . . 11
|
56 | 55 | adantl 482 |
. . . . . . . . . 10
|
57 | 53, 56 | breqtrd 4679 |
. . . . . . . . 9
|
58 | 32, 57 | pm2.61dan 832 |
. . . . . . . 8
|
59 | | fourierdlem37.l |
. . . . . . . . . 10
|
60 | 59 | a1i 11 |
. . . . . . . . 9
|
61 | | eqeq1 2626 |
. . . . . . . . . . 11
|
62 | | id 22 |
. . . . . . . . . . 11
|
63 | 61, 62 | ifbieq2d 4111 |
. . . . . . . . . 10
|
64 | 63 | adantl 482 |
. . . . . . . . 9
|
65 | 34, 45 | ifcld 4131 |
. . . . . . . . 9
|
66 | 60, 64, 44, 65 | fvmptd 6288 |
. . . . . . . 8
|
67 | 58, 66 | breqtrrd 4681 |
. . . . . . 7
|
68 | | fveq2 6191 |
. . . . . . . . 9
|
69 | 68 | breq1d 4663 |
. . . . . . . 8
|
70 | 69 | elrab 3363 |
. . . . . . 7
..^ ..^ |
71 | 16, 67, 70 | sylanbrc 698 |
. . . . . 6
..^
|
72 | | ne0i 3921 |
. . . . . 6
..^ ..^ |
73 | 71, 72 | syl 17 |
. . . . 5
..^ |
74 | | fzssz 12343 |
. . . . . . . . 9
|
75 | 5, 74 | sstri 3612 |
. . . . . . . 8
..^ |
76 | | zssre 11384 |
. . . . . . . 8
|
77 | 75, 76 | sstri 3612 |
. . . . . . 7
..^ |
78 | 1, 77 | sstri 3612 |
. . . . . 6
..^ |
79 | 78 | a1i 11 |
. . . . 5
..^ |
80 | | fisupcl 8375 |
. . . . 5
..^
..^ ..^ ..^
..^
|
81 | 3, 9, 73, 79, 80 | syl13anc 1328 |
. . . 4
..^
..^
|
82 | 1, 81 | sseldi 3601 |
. . 3
..^
..^ |
83 | | fourierdlem37.i |
. . 3
..^ |
84 | 82, 83 | fmptd 6385 |
. 2
..^ |
85 | 81 | ex 450 |
. 2
..^ ..^ |
86 | 84, 85 | jca 554 |
1
..^
..^ ..^ |