Step | Hyp | Ref
| Expression |
1 | | eqid 2471 |
. . 3
         |
2 | | 1zzd 10992 |
. . 3
   |
3 | | nfv 1769 |
. . . . 5
   |
4 | | nfmpt1 4485 |
. . . . 5
                |
5 | | nfmpt1 4485 |
. . . . 5
     |
6 | | fourierdlem104.e |
. . . . . 6
                |
7 | | nfmpt1 4485 |
. . . . . 6
                  |
8 | 6, 7 | nfcxfr 2610 |
. . . . 5
   |
9 | | nnuz 11218 |
. . . . 5
     |
10 | | elioore 11691 |
. . . . . . . . . . . . . . . 16
       |
11 | 10 | adantl 473 |
. . . . . . . . . . . . . . 15
 
       |
12 | | pire 23492 |
. . . . . . . . . . . . . . . 16
 |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
 
       |
14 | | fourierdlem104.f |
. . . . . . . . . . . . . . . . . . . 20
       |
15 | | fourierdlem104.xre |
. . . . . . . . . . . . . . . . . . . 20
   |
16 | | ioossre 11721 |
. . . . . . . . . . . . . . . . . . . . . . 23
    |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
      |
18 | 14, 17 | fssresd 5762 |
. . . . . . . . . . . . . . . . . . . . 21
               |
19 | | ioosscn 37687 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
      |
21 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . 22
  ℂfld   ℂfld |
22 | | pnfxr 11435 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
24 | 15 | ltpnfd 11446 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
25 | 21, 23, 15, 24 | lptioo1cn 37824 |
. . . . . . . . . . . . . . . . . . . . 21
       ℂfld         |
26 | | fourierdlem104.y |
. . . . . . . . . . . . . . . . . . . . 21
  
    lim    |
27 | 18, 20, 25, 26 | limcrecl 37806 |
. . . . . . . . . . . . . . . . . . . 20
   |
28 | | ioossre 11721 |
. . . . . . . . . . . . . . . . . . . . . . 23
    |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
   
  |
30 | 14, 29 | fssresd 5762 |
. . . . . . . . . . . . . . . . . . . . 21
               |
31 | | ioosscn 37687 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
   
  |
33 | | mnfxr 11437 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
35 | 15 | mnfltd 11449 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
36 | 21, 34, 15, 35 | lptioo2cn 37823 |
. . . . . . . . . . . . . . . . . . . . 21
       ℂfld         |
37 | | fourierdlem104.w |
. . . . . . . . . . . . . . . . . . . . 21
  
    lim    |
38 | 30, 32, 36, 37 | limcrecl 37806 |
. . . . . . . . . . . . . . . . . . . 20
   |
39 | | fourierdlem104.h |
. . . . . . . . . . . . . . . . . . . 20
    ![[,] [,]](_icc.gif)                        |
40 | | fourierdlem104.k |
. . . . . . . . . . . . . . . . . . . 20
    ![[,] [,]](_icc.gif)                   |
41 | | fourierdlem104.u |
. . . . . . . . . . . . . . . . . . . 20
    ![[,] [,]](_icc.gif)              |
42 | 14, 15, 27, 38, 39, 40, 41 | fourierdlem55 38137 |
. . . . . . . . . . . . . . . . . . 19
      ![[,] [,]](_icc.gif)      |
43 | | ax-resscn 9614 |
. . . . . . . . . . . . . . . . . . . 20
 |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19

  |
45 | 42, 44 | fssd 5750 |
. . . . . . . . . . . . . . . . . 18
      ![[,] [,]](_icc.gif)      |
46 | 45 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
          ![[,] [,]](_icc.gif)      |
47 | 12 | renegcli 9955 |
. . . . . . . . . . . . . . . . . . 19
  |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
 
        |
49 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
        |
50 | | 0red 9662 |
. . . . . . . . . . . . . . . . . . . . 21
       |
51 | | negpilt0 37580 |
. . . . . . . . . . . . . . . . . . . . . 22
  |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
        |
53 | | 0xr 9705 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
54 | 12 | rexri 9711 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
55 | | ioogtlb 37688 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
56 | 53, 54, 55 | mp3an12 1380 |
. . . . . . . . . . . . . . . . . . . . 21
       |
57 | 49, 50, 10, 52, 56 | lttrd 9813 |
. . . . . . . . . . . . . . . . . . . 20
        |
58 | 49, 10, 57 | ltled 9800 |
. . . . . . . . . . . . . . . . . . 19
        |
59 | 58 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
 
        |
60 | 13 | leidd 10201 |
. . . . . . . . . . . . . . . . . 18
 
       |
61 | | iccss 11727 |
. . . . . . . . . . . . . . . . . 18
           ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
62 | 48, 13, 59, 60, 61 | syl22anc 1293 |
. . . . . . . . . . . . . . . . 17
 
       ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
63 | 46, 62 | fssresd 5762 |
. . . . . . . . . . . . . . . 16
 
        ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
64 | | fourierdlem104.o |
. . . . . . . . . . . . . . . . . 18
   ![[,] [,]](_icc.gif)    |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
        ![[,] [,]](_icc.gif)     |
66 | 65 | feq1d 5724 |
. . . . . . . . . . . . . . . 16
 
          ![[,] [,]](_icc.gif)   
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)       |
67 | 63, 66 | mpbird 240 |
. . . . . . . . . . . . . . 15
 
         ![[,] [,]](_icc.gif)      |
68 | | fourierdlem104.n |
. . . . . . . . . . . . . . . . . 18
       |
69 | 12 | elexi 3041 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
70 | 69 | prid2 4072 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    |
71 | | elun1 3592 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
72 | 70, 71 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
        |
73 | | fourierdlem104.t |
. . . . . . . . . . . . . . . . . . . . . . 23
            |
74 | 72, 73 | eleqtrri 2548 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
75 | 74 | ne0ii 3729 |
. . . . . . . . . . . . . . . . . . . . 21
 |
76 | 75 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   |
77 | | prfi 7864 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
  |
79 | | fzfi 12223 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
80 | | fourierdlem104.q |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
81 | 80 | rnmptfi 37508 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
82 | 79, 81 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
83 | | infi 7813 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
84 | 82, 83 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
85 | | unfi 7856 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                    |
86 | 78, 84, 85 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . 22
              |
87 | 73, 86 | syl5eqel 2553 |
. . . . . . . . . . . . . . . . . . . . 21
   |
88 | | hashnncl 12585 |
. . . . . . . . . . . . . . . . . . . . 21
     
   |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
     
   |
90 | 76, 89 | mpbird 240 |
. . . . . . . . . . . . . . . . . . 19
       |
91 | | nnm1nn0 10935 |
. . . . . . . . . . . . . . . . . . 19
    
        |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         |
93 | 68, 92 | syl5eqel 2553 |
. . . . . . . . . . . . . . . . 17
   |
94 | 93 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
       |
95 | | 0red 9662 |
. . . . . . . . . . . . . . . . . 18
 
       |
96 | | 1red 9676 |
. . . . . . . . . . . . . . . . . 18
 
       |
97 | 94 | nn0red 10950 |
. . . . . . . . . . . . . . . . . 18
 
       |
98 | | 0lt1 10157 |
. . . . . . . . . . . . . . . . . . 19
 |
99 | 98 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
 
       |
100 | | 2re 10701 |
. . . . . . . . . . . . . . . . . . . . 21
 |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
102 | 90 | nnred 10646 |
. . . . . . . . . . . . . . . . . . . . 21
       |
103 | 102 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
           |
104 | | iooltub 37706 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
105 | 53, 54, 104 | mp3an12 1380 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
106 | 10, 105 | ltned 9788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
107 | 106 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       |
108 | | hashprg 12610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              |
109 | 11, 12, 108 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     
          |
110 | 107, 109 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . 22
 
              |
111 | 110 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . 21
 
              |
112 | 87 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
113 | | ssun1 3588 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
        |
114 | 113, 73 | sseqtr4i 3451 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
115 | | hashssle 37603 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
116 | 112, 114,
115 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . 21
 
                  |
117 | 111, 116 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . . . . . 20
 
           |
118 | 101, 103,
96, 117 | lesub1dd 10250 |
. . . . . . . . . . . . . . . . . . 19
 
               |
119 | | 1e2m1 10747 |
. . . . . . . . . . . . . . . . . . 19
   |
120 | 118, 119,
68 | 3brtr4g 4428 |
. . . . . . . . . . . . . . . . . 18
 
       |
121 | 95, 96, 97, 99, 120 | ltletrd 9812 |
. . . . . . . . . . . . . . . . 17
 
       |
122 | 121 | gt0ne0d 10199 |
. . . . . . . . . . . . . . . 16
 
       |
123 | | elnnne0 10907 |
. . . . . . . . . . . . . . . 16

    |
124 | 94, 122, 123 | sylanbrc 677 |
. . . . . . . . . . . . . . 15
 
       |
125 | | fourierdlem104.j |
. . . . . . . . . . . . . . . . 17
            |
126 | 11 | leidd 10201 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
127 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
128 | 10, 127, 105 | ltled 9800 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
129 | 128 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
130 | 11, 13, 11, 126, 129 | eliccd 37697 |
. . . . . . . . . . . . . . . . . . . . 21
 
       ![[,] [,]](_icc.gif)    |
131 | 11, 13, 13, 129, 60 | eliccd 37697 |
. . . . . . . . . . . . . . . . . . . . 21
 
       ![[,] [,]](_icc.gif)    |
132 | 130, 131 | jca 541 |
. . . . . . . . . . . . . . . . . . . 20
 
        ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
133 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . 21
 |
134 | 133, 69 | prss 4117 |
. . . . . . . . . . . . . . . . . . . 20
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
     ![[,] [,]](_icc.gif)    |
135 | 132, 134 | sylib 201 |
. . . . . . . . . . . . . . . . . . 19
 
          ![[,] [,]](_icc.gif)    |
136 | | inss2 3644 |
. . . . . . . . . . . . . . . . . . . . 21

          |
137 | 136 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
                 |
138 | | ioossicc 11745 |
. . . . . . . . . . . . . . . . . . . 20
      ![[,] [,]](_icc.gif)   |
139 | 137, 138 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . 19
 
             ![[,] [,]](_icc.gif)    |
140 | 135, 139 | unssd 3601 |
. . . . . . . . . . . . . . . . . 18
 
        
         ![[,] [,]](_icc.gif)    |
141 | 73, 140 | syl5eqss 3462 |
. . . . . . . . . . . . . . . . 17
 
       ![[,] [,]](_icc.gif)    |
142 | 133 | prid1 4071 |
. . . . . . . . . . . . . . . . . . . 20
    |
143 | | elun1 3592 |
. . . . . . . . . . . . . . . . . . . 20
                 |
144 | 142, 143 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
            |
145 | 144, 73 | eleqtrri 2548 |
. . . . . . . . . . . . . . . . . 18
 |
146 | 145 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
       |
147 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
       |
148 | 112, 68, 125, 11, 13, 141, 146, 147 | fourierdlem52 38134 |
. . . . . . . . . . . . . . . 16
 
                 ![[,] [,]](_icc.gif)              |
149 | 148 | simplld 769 |
. . . . . . . . . . . . . . 15
 
               ![[,] [,]](_icc.gif)    |
150 | 148 | simplrd 771 |
. . . . . . . . . . . . . . 15
 
           |
151 | 148 | simprd 470 |
. . . . . . . . . . . . . . 15
 
           |
152 | | elfzoelz 11947 |
. . . . . . . . . . . . . . . . . . 19
  ..^
  |
153 | 152 | zred 11063 |
. . . . . . . . . . . . . . . . . 18
  ..^
  |
154 | 153 | adantl 473 |
. . . . . . . . . . . . . . . . 17
         ..^ 
  |
155 | 154 | ltp1d 10559 |
. . . . . . . . . . . . . . . 16
         ..^ 
    |
156 | 10, 127 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
157 | 133, 69 | prss 4117 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
     |
158 | 156, 157 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . 22
          |
159 | 158 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . 21
 
          |
160 | | ioossre 11721 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
161 | 136, 160 | sstri 3427 |
. . . . . . . . . . . . . . . . . . . . . 22

      |
162 | 161 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
 
             |
163 | 159, 162 | unssd 3601 |
. . . . . . . . . . . . . . . . . . . 20
 
        
         |
164 | 73, 163 | syl5eqss 3462 |
. . . . . . . . . . . . . . . . . . 19
 
       |
165 | 112, 164,
125, 68 | fourierdlem36 38118 |
. . . . . . . . . . . . . . . . . 18
 
              |
166 | 165 | adantr 472 |
. . . . . . . . . . . . . . . . 17
         ..^ 
         |
167 | | elfzofz 11962 |
. . . . . . . . . . . . . . . . . 18
  ..^
      |
168 | 167 | adantl 473 |
. . . . . . . . . . . . . . . . 17
         ..^ 
      |
169 | | fzofzp1 12037 |
. . . . . . . . . . . . . . . . . 18
  ..^
        |
170 | 169 | adantl 473 |
. . . . . . . . . . . . . . . . 17
         ..^ 
        |
171 | | isorel 6235 |
. . . . . . . . . . . . . . . . 17
 
           
              
         |
172 | 166, 168,
170, 171 | syl12anc 1290 |
. . . . . . . . . . . . . . . 16
         ..^ 
                |
173 | 155, 172 | mpbid 215 |
. . . . . . . . . . . . . . 15
         ..^ 
            |
174 | 42 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
          ![[,] [,]](_icc.gif)      |
175 | 174, 62 | feqresmpt 5933 |
. . . . . . . . . . . . . . . . . . 19
 
        ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)         |
176 | 62 | sselda 3418 |
. . . . . . . . . . . . . . . . . . . . . 22
          ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
177 | 14, 15, 27, 38, 39 | fourierdlem9 38090 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      ![[,] [,]](_icc.gif)      |
178 | 177 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)      |
179 | 178, 176 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . . . 23
          ![[,] [,]](_icc.gif)         |
180 | 40 | fourierdlem43 38126 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     ![[,] [,]](_icc.gif)     |
181 | 180 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)      |
182 | 181, 176 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . . . 23
          ![[,] [,]](_icc.gif)         |
183 | 179, 182 | remulcld 9689 |
. . . . . . . . . . . . . . . . . . . . . 22
          ![[,] [,]](_icc.gif)               |
184 | 41 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . . . . . 22
     ![[,] [,]](_icc.gif)                             |
185 | 176, 183,
184 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . 21
          ![[,] [,]](_icc.gif)                   |
186 | | 0red 9662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
  ![[,] [,]](_icc.gif)     |
187 | 10 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
  ![[,] [,]](_icc.gif)     |
188 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
  ![[,] [,]](_icc.gif)     |
189 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
190 | | eliccre 37699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    ![[,] [,]](_icc.gif)     |
191 | 187, 188,
189, 190 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
  ![[,] [,]](_icc.gif)     |
192 | 56 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
  ![[,] [,]](_icc.gif)  
  |
193 | 187 | rexrd 9708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
  ![[,] [,]](_icc.gif)     |
194 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
  ![[,] [,]](_icc.gif)     |
195 | | iccgelb 11716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    ![[,] [,]](_icc.gif)     |
196 | 193, 194,
189, 195 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
  ![[,] [,]](_icc.gif)  
  |
197 | 186, 187,
191, 192, 196 | ltletrd 9812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
  ![[,] [,]](_icc.gif)  
  |
198 | 197 | gt0ne0d 10199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
  ![[,] [,]](_icc.gif)     |
199 | 198 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          ![[,] [,]](_icc.gif)     |
200 | 199 | neneqd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          ![[,] [,]](_icc.gif)  
  |
201 | 200 | iffalsed 3883 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          ![[,] [,]](_icc.gif)            
               
           |
202 | 197 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          ![[,] [,]](_icc.gif)     |
203 | 202 | iftrued 3880 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          ![[,] [,]](_icc.gif)          |
204 | 203 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          ![[,] [,]](_icc.gif)       
                  |
205 | 204 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          ![[,] [,]](_icc.gif)        
                     |
206 | 201, 205 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          ![[,] [,]](_icc.gif)            
               
      |
207 | 14 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          ![[,] [,]](_icc.gif)         |
208 | 15 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          ![[,] [,]](_icc.gif)     |
209 | | iccssre 11741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       ![[,] [,]](_icc.gif)    |
210 | 47, 12, 209 | mp2an 686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   ![[,] [,]](_icc.gif)   |
211 | 210, 176 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          ![[,] [,]](_icc.gif)     |
212 | 208, 211 | readdcld 9688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          ![[,] [,]](_icc.gif)   
   |
213 | 207, 212 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          ![[,] [,]](_icc.gif)           |
214 | 27 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          ![[,] [,]](_icc.gif)     |
215 | 213, 214 | resubcld 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          ![[,] [,]](_icc.gif)       
     |
216 | 215, 211,
199 | redivcld 10457 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          ![[,] [,]](_icc.gif)        
      |
217 | 206, 216 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          ![[,] [,]](_icc.gif)            
            |
218 | 39 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     ![[,] [,]](_icc.gif)           
                        
            |
219 | 176, 217,
218 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . 23
          ![[,] [,]](_icc.gif)                             |
220 | 219, 201,
205 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . . . . . . 22
          ![[,] [,]](_icc.gif)                   |
221 | 188 | renegcld 10067 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
  ![[,] [,]](_icc.gif)      |
222 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
  ![[,] [,]](_icc.gif)      |
223 | 221, 186,
191, 222, 197 | lttrd 9813 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
  ![[,] [,]](_icc.gif)      |
224 | 221, 191,
223 | ltled 9800 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
  ![[,] [,]](_icc.gif)   
  |
225 | | iccleub 11715 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    ![[,] [,]](_icc.gif)     |
226 | 193, 194,
189, 225 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
  ![[,] [,]](_icc.gif)  
  |
227 | 221, 188,
191, 224, 226 | eliccd 37697 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
228 | 198 | neneqd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
  ![[,] [,]](_icc.gif)  
  |
229 | 228 | iffalsed 3883 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
  ![[,] [,]](_icc.gif)                              |
230 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
  ![[,] [,]](_icc.gif)     |
231 | 191 | rehalfcld 10882 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
  ![[,] [,]](_icc.gif)       |
232 | 231 | resincld 14274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
  ![[,] [,]](_icc.gif)           |
233 | 230, 232 | remulcld 9689 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
  ![[,] [,]](_icc.gif)             |
234 | | 2cnd 10704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
  ![[,] [,]](_icc.gif)     |
235 | 191 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
  ![[,] [,]](_icc.gif)     |
236 | 235 | halfcld 10880 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
  ![[,] [,]](_icc.gif)       |
237 | 236 | sincld 14261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
  ![[,] [,]](_icc.gif)           |
238 | | 2ne0 10724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 |
239 | 238 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
  ![[,] [,]](_icc.gif)     |
240 | | fourierdlem44 38127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     ![[,] [,]](_icc.gif)           |
241 | 227, 198,
240 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
  ![[,] [,]](_icc.gif)           |
242 | 234, 237,
239, 241 | mulne0d 10286 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
  ![[,] [,]](_icc.gif)             |
243 | 191, 233,
242 | redivcld 10457 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
  ![[,] [,]](_icc.gif)               |
244 | 229, 243 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
  ![[,] [,]](_icc.gif)                    |
245 | 40 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     ![[,] [,]](_icc.gif)                                       |
246 | 227, 244,
245 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
  ![[,] [,]](_icc.gif)                        |
247 | 246 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . 22
          ![[,] [,]](_icc.gif)                        |
248 | 220, 247 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . 21
          ![[,] [,]](_icc.gif)                   
                      |
249 | 200 | iffalsed 3883 |
. . . . . . . . . . . . . . . . . . . . . 22
          ![[,] [,]](_icc.gif)                              |
250 | 249 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . 21
          ![[,] [,]](_icc.gif)                                    
                 |
251 | 185, 248,
250 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . . . . 20
          ![[,] [,]](_icc.gif)             
                 |
252 | 251 | mpteq2dva 4482 |
. . . . . . . . . . . . . . . . . . 19
 
        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)        
                  |
253 | 65, 175, 252 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . . 18
 
        ![[,] [,]](_icc.gif)        
                  |
254 | 253 | adantr 472 |
. . . . . . . . . . . . . . . . 17
         ..^ 
   ![[,] [,]](_icc.gif)                           |
255 | 254 | reseq1d 5110 |
. . . . . . . . . . . . . . . 16
         ..^ 
                    ![[,] [,]](_icc.gif)                        
                 |
256 | 14 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
           |
257 | 15 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
       |
258 | | fourierdlem104.p |
. . . . . . . . . . . . . . . . . 18
 
                        ..^                |
259 | | fourierdlem104.m |
. . . . . . . . . . . . . . . . . . 19
   |
260 | 259 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
       |
261 | | fourierdlem104.v |
. . . . . . . . . . . . . . . . . . 19
       |
262 | 261 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
           |
263 | | fourierdlem104.fcn |
. . . . . . . . . . . . . . . . . . 19
 
 ..^                                      |
264 | 263 | adantlr 729 |
. . . . . . . . . . . . . . . . . 18
         ..^ 
                                    |
265 | | fourierdlem104.r |
. . . . . . . . . . . . . . . . . . 19
 
 ..^                   lim        |
266 | 265 | adantlr 729 |
. . . . . . . . . . . . . . . . . 18
         ..^ 
                 lim        |
267 | | fourierdlem104.l |
. . . . . . . . . . . . . . . . . . 19
 
 ..^                   lim          |
268 | 267 | adantlr 729 |
. . . . . . . . . . . . . . . . . 18
         ..^ 
                 lim          |
269 | 105 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
 
       |
270 | 50, 10 | ltnled 9799 |
. . . . . . . . . . . . . . . . . . . . . 22
     
   |
271 | 56, 270 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . 21
       |
272 | 271 | intn3an2d 1408 |
. . . . . . . . . . . . . . . . . . . 20
     
   |
273 | | elicc2 11724 |
. . . . . . . . . . . . . . . . . . . . 21
      ![[,] [,]](_icc.gif)  
    |
274 | 10, 12, 273 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . 20
        ![[,] [,]](_icc.gif) 
     |
275 | 272, 274 | mtbird 308 |
. . . . . . . . . . . . . . . . . . 19
    
  ![[,] [,]](_icc.gif)    |
276 | 275 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
 
    
  ![[,] [,]](_icc.gif)    |
277 | 27 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
       |
278 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
   ![[,] [,]](_icc.gif)        
                   ![[,] [,]](_icc.gif)                          |
279 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
                  ..^               
                      ..^               
                ![]_ ]_](_urbrack.gif)                                                                ..^               
                      ..^               
                ![]_ ]_](_urbrack.gif)                                               |
280 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
               ..^                                     ..^                                ![]_ ]_](_urbrack.gif) 
                                                   ..^                                     ..^               
                ![]_ ]_](_urbrack.gif)                                       |
281 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . 21
           |
282 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
283 | 282 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
               |
284 | 281, 283 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . 20
                               |
285 | 284 | sseq2d 3446 |
. . . . . . . . . . . . . . . . . . 19
               
             
                               |
286 | 285 | cbvriotav 6281 |
. . . . . . . . . . . . . . . . . 18
   ..^                                  ..^                                |
287 | 256, 257,
258, 260, 262, 264, 266, 268, 11, 13, 269, 62, 276, 277, 278, 80, 73, 68, 125, 279, 280, 286 | fourierdlem86 38168 |
. . . . . . . . . . . . . . . . 17
         ..^ 
                  
 ..^                                      ..^               
                ![]_ ]_](_urbrack.gif)                                                   ![[,] [,]](_icc.gif)                        
               lim                       ..^                                     ..^                                ![]_ ]_](_urbrack.gif) 
                                         ![[,] [,]](_icc.gif)                        
               lim           ![[,] [,]](_icc.gif)                        
                                    |
288 | 287 | simprd 470 |
. . . . . . . . . . . . . . . 16
         ..^ 
    ![[,] [,]](_icc.gif)                        
                                   |
289 | 255, 288 | eqeltrd 2549 |
. . . . . . . . . . . . . . 15
         ..^ 
                                    |
290 | 287 | simplld 769 |
. . . . . . . . . . . . . . . 16
         ..^ 
                  ..^               
                      ..^               
                ![]_ ]_](_urbrack.gif)                                                   ![[,] [,]](_icc.gif)                        
               lim          |
291 | 254 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . 18
         ..^ 
   ![[,] [,]](_icc.gif)        
                  |
292 | 291 | reseq1d 5110 |
. . . . . . . . . . . . . . . . 17
         ..^ 
    ![[,] [,]](_icc.gif)                        
                                 |
293 | 292 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
         ..^ 
     ![[,] [,]](_icc.gif)                        
               lim         
               lim          |
294 | 290, 293 | eleqtrd 2551 |
. . . . . . . . . . . . . . 15
         ..^ 
                  ..^               
                      ..^               
                ![]_ ]_](_urbrack.gif)                                               
               lim          |
295 | 287 | simplrd 771 |
. . . . . . . . . . . . . . . 16
         ..^ 
               ..^                                     ..^                                ![]_ ]_](_urbrack.gif) 
                                         ![[,] [,]](_icc.gif)                        
               lim        |
296 | 292 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
         ..^ 
     ![[,] [,]](_icc.gif)                        
               lim       
               lim        |
297 | 295, 296 | eleqtrd 2551 |
. . . . . . . . . . . . . . 15
         ..^ 
               ..^                                     ..^                                ![]_ ]_](_urbrack.gif) 
                                                     lim        |
298 | | eqid 2471 |
. . . . . . . . . . . . . . 15
     |
299 | 67 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
         ..^ 
    ![[,] [,]](_icc.gif)      |
300 | 11 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      ..^                
  |
301 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      ..^                
  |
302 | | elioore 11691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
303 | 302 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      ..^                
  |
304 | 62, 210 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
       ![[,] [,]](_icc.gif)    |
305 | 304 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         ..^ 
  ![[,] [,]](_icc.gif)    |
306 | 149 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         ..^ 
          ![[,] [,]](_icc.gif)    |
307 | 306, 168 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         ..^ 
      ![[,] [,]](_icc.gif)    |
308 | 305, 307 | sseldd 3419 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         ..^ 
      |
309 | 308 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
      ..^                
      |
310 | 11 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         ..^ 
  |
311 | 310 | rexrd 9708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         ..^ 
  |
312 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         ..^ 
  |
313 | | iccgelb 11716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        ![[,] [,]](_icc.gif)         |
314 | 311, 312,
307, 313 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         ..^ 
      |
315 | 314 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
      ..^                
      |
316 | 309 | rexrd 9708 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
      ..^                
      |
317 | 306, 170 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         ..^ 
        ![[,] [,]](_icc.gif)    |
318 | 305, 317 | sseldd 3419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         ..^ 
        |
319 | 318 | rexrd 9708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         ..^ 
        |
320 | 319 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
      ..^                
        |
321 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
      ..^                
                |
322 | | ioogtlb 37688 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           
                     |
323 | 316, 320,
321, 322 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
      ..^                
      |
324 | 300, 309,
303, 315, 323 | lelttrd 9810 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
      ..^                
  |
325 | 300, 303,
324 | ltled 9800 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      ..^                
  |
326 | 318 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
      ..^                
        |
327 | | iooltub 37706 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           
                       |
328 | 316, 320,
321, 327 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
      ..^                
        |
329 | | iccleub 11715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          ![[,] [,]](_icc.gif)           |
330 | 311, 312,
317, 329 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         ..^ 
        |
331 | 330 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
      ..^                
        |
332 | 303, 326,
301, 328, 331 | ltletrd 9812 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
      ..^                
  |
333 | 303, 301,
332 | ltled 9800 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      ..^                
  |
334 | 300, 301,
303, 325, 333 | eliccd 37697 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      ..^                
  ![[,] [,]](_icc.gif)    |
335 | 334 | ralrimiva 2809 |
. . . . . . . . . . . . . . . . . . . . 21
         ..^ 
                  ![[,] [,]](_icc.gif)    |
336 | | dfss3 3408 |
. . . . . . . . . . . . . . . . . . . . 21
                 ![[,] [,]](_icc.gif) 
                  ![[,] [,]](_icc.gif)    |
337 | 335, 336 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . 20
         ..^ 
                ![[,] [,]](_icc.gif)    |
338 | 299, 337 | feqresmpt 5933 |
. . . . . . . . . . . . . . . . . . 19
         ..^ 
                                      |
339 | | simplll 776 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      ..^                
  |
340 | | simpllr 777 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      ..^                
      |
341 | 64 | fveq1i 5880 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        ![[,] [,]](_icc.gif)       |
342 | 341 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
          ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)        |
343 | | fvres 5893 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            |
344 | 343 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
          ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)            |
345 | 247, 249 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          ![[,] [,]](_icc.gif)                   |
346 | 220, 345 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          ![[,] [,]](_icc.gif)                   
                 |
347 | 215 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          ![[,] [,]](_icc.gif)       
     |
348 | 235 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          ![[,] [,]](_icc.gif)     |
349 | | 2cnd 10704 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          ![[,] [,]](_icc.gif)     |
350 | 348 | halfcld 10880 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          ![[,] [,]](_icc.gif)       |
351 | 350 | sincld 14261 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          ![[,] [,]](_icc.gif)           |
352 | 349, 351 | mulcld 9681 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          ![[,] [,]](_icc.gif)             |
353 | 242 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          ![[,] [,]](_icc.gif)             |
354 | 347, 348,
352, 199, 353 | dmdcan2d 10435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          ![[,] [,]](_icc.gif)                                             |
355 | 185, 346,
354 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . . . . . . . 23
          ![[,] [,]](_icc.gif)                           |
356 | 342, 344,
355 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . . . . . . 22
          ![[,] [,]](_icc.gif)                           |
357 | 339, 340,
334, 356 | syl21anc 1291 |
. . . . . . . . . . . . . . . . . . . . 21
   
      ..^                
         
              |
358 | 339, 340,
334, 354 | syl21anc 1291 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      ..^                
      
                    
              |
359 | 358 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . 21
   
      ..^                
     
                                    |
360 | | eqidd 2472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ..^                                     
                         
       |
361 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
     |
362 | 361 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          
    |
363 | 362 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
             |
364 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
365 | 363, 364 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
                |
366 | 365 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 ..^ 
              
                
      |
367 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ..^                                 |
368 | | ovex 6336 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
     |
369 | 368 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ..^                      
      |
370 | 360, 366,
367, 369 | fvmptd 5969 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    ..^                                                    
      |
371 | | eqidd 2472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ..^                                                                       |
372 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       |
373 | 372 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
               |
374 | 373 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                   |
375 | 364, 374 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                       |
376 | 375 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 ..^ 
              
       ![]() |