Step | Hyp | Ref
| Expression |
1 | | fourierdlem68.f |
. . . . . 6
       |
2 | | fourierdlem68.xre |
. . . . . 6
   |
3 | | fourierdlem68.a |
. . . . . 6
   |
4 | | fourierdlem68.b |
. . . . . 6
   |
5 | | fourierdlem68.fdv |
. . . . . 6
                           |
6 | | ioossicc 11745 |
. . . . . . 7
      ![[,] [,]](_icc.gif)   |
7 | | fourierdlem68.ab |
. . . . . . 7
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)    |
8 | 6, 7 | syl5ss 3429 |
. . . . . 6
    
   ![[,] [,]](_icc.gif)    |
9 | | fourierdlem68.n0 |
. . . . . . 7
   ![[,] [,]](_icc.gif)    |
10 | 6 | sseli 3414 |
. . . . . . 7
       ![[,] [,]](_icc.gif)    |
11 | 9, 10 | nsyl 125 |
. . . . . 6
       |
12 | | fourierdlem68.c |
. . . . . 6
   |
13 | | fourierdlem68.o |
. . . . . 6
                         |
14 | 1, 2, 3, 4, 5, 8, 11, 12, 13 | fourierdlem57 38139 |
. . . . 5
                                                                                                                 |
15 | 14 | simpli 465 |
. . . 4
                                                                                   |
16 | 15 | simpld 466 |
. . 3
             |
17 | | fdm 5745 |
. . 3
                   |
18 | 16, 17 | syl 17 |
. 2
         |
19 | | eqid 2471 |
. . . . . 6
   ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)            |
20 | | fourierdlem68.altb |
. . . . . . 7
   |
21 | 3, 4, 20 | ltled 9800 |
. . . . . 6

  |
22 | | 2re 10701 |
. . . . . . . . . . 11
 |
23 | 22 | a1i 11 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
  |
24 | 3, 4 | iccssred 37698 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif) 
  |
25 | 24 | sselda 3418 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)  
  |
26 | 25 | rehalfcld 10882 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)  
    |
27 | 26 | resincld 14274 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
        |
28 | 23, 27 | remulcld 9689 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
          |
29 | | 2cnd 10704 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
  |
30 | 27 | recnd 9687 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
        |
31 | | 2ne0 10724 |
. . . . . . . . . . 11
 |
32 | 31 | a1i 11 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
  |
33 | 7 | sselda 3418 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)    |
34 | | eqcom 2478 |
. . . . . . . . . . . . . . . . 17

  |
35 | 34 | biimpi 199 |
. . . . . . . . . . . . . . . 16
   |
36 | 35 | adantl 473 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif) 
   |
37 | | simpl 464 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)    |
38 | 36, 37 | eqeltrd 2549 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)    |
39 | 38 | adantll 728 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
40 | 9 | ad2antrr 740 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)    |
41 | 39, 40 | pm2.65da 586 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)  
  |
42 | 41 | neqned 2650 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)  
  |
43 | | fourierdlem44 38127 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)           |
44 | 33, 42, 43 | syl2anc 673 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
        |
45 | 29, 30, 32, 44 | mulne0d 10286 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
          |
46 | | eldifsn 4088 |
. . . . . . . . 9
            
                    |
47 | 28, 45, 46 | sylanbrc 677 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)  
              |
48 | 47, 19 | fmptd 6061 |
. . . . . . 7
    ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          |
49 | | difss 3549 |
. . . . . . . . . 10
   
 |
50 | | ax-resscn 9614 |
. . . . . . . . . 10
 |
51 | 49, 50 | sstri 3427 |
. . . . . . . . 9
   
 |
52 | 51 | a1i 11 |
. . . . . . . 8
       |
53 | 24, 50 | syl6ss 3430 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif) 
  |
54 | | 2cnd 10704 |
. . . . . . . . . 10
   |
55 | | ssid 3437 |
. . . . . . . . . . 11
 |
56 | 55 | a1i 11 |
. . . . . . . . . 10

  |
57 | 53, 54, 56 | constcncfg 37845 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
58 | | sincn 23478 |
. . . . . . . . . . 11
     |
59 | 58 | a1i 11 |
. . . . . . . . . 10
       |
60 | 53, 56 | idcncfg 37846 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
61 | | eldifsn 4088 |
. . . . . . . . . . . . . 14
         |
62 | 29, 32, 61 | sylanbrc 677 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)  

     |
63 | | eqid 2471 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
64 | 62, 63 | fmptd 6061 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
65 | | difssd 3550 |
. . . . . . . . . . . . 13
       |
66 | | cncffvrn 22008 |
. . . . . . . . . . . . 13
         ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)           |
67 | 65, 57, 66 | syl2anc 673 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)           |
68 | 64, 67 | mpbird 240 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)           |
69 | 60, 68 | divcncf 37858 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
70 | 59, 69 | cncfmpt1f 22023 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)       |
71 | 57, 70 | mulcncf 22476 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)       |
72 | | cncffvrn 22008 |
. . . . . . . 8
         ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)        
   ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)           |
73 | 52, 71, 72 | syl2anc 673 |
. . . . . . 7
     ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)        
   ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)           |
74 | 48, 73 | mpbird 240 |
. . . . . 6
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)           |
75 | 19, 3, 4, 21, 74 | cncficcgt0 37863 |
. . . . 5
     ![[,] [,]](_icc.gif)                 |
76 | | reelprrecn 9649 |
. . . . . . . 8
    |
77 | 76 | a1i 11 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)  
                  |
78 | 1 | adantr 472 |
. . . . . . . . . . 11
 
    
      |
79 | 2 | adantr 472 |
. . . . . . . . . . . 12
 
    
  |
80 | | elioore 11691 |
. . . . . . . . . . . . 13
       |
81 | 80 | adantl 473 |
. . . . . . . . . . . 12
 
    
  |
82 | 79, 81 | readdcld 9688 |
. . . . . . . . . . 11
 
    
    |
83 | 78, 82 | ffvelrnd 6038 |
. . . . . . . . . 10
 
    
        |
84 | 12 | adantr 472 |
. . . . . . . . . 10
 
    
  |
85 | 83, 84 | resubcld 10068 |
. . . . . . . . 9
 
    
          |
86 | 85 | recnd 9687 |
. . . . . . . 8
 
    
          |
87 | 86 | 3ad2antl1 1192 |
. . . . . . 7
      ![[,] [,]](_icc.gif)                    
          |
88 | 76 | a1i 11 |
. . . . . . . . . 10
      |
89 | 83 | recnd 9687 |
. . . . . . . . . 10
 
    
        |
90 | 5 | adantr 472 |
. . . . . . . . . . 11
 
    
                          |
91 | 2, 3 | readdcld 9688 |
. . . . . . . . . . . . . 14
     |
92 | 91 | rexrd 9708 |
. . . . . . . . . . . . 13
     |
93 | 92 | adantr 472 |
. . . . . . . . . . . 12
 
    
    |
94 | 2, 4 | readdcld 9688 |
. . . . . . . . . . . . . 14
     |
95 | 94 | rexrd 9708 |
. . . . . . . . . . . . 13
     |
96 | 95 | adantr 472 |
. . . . . . . . . . . 12
 
    
    |
97 | 3 | adantr 472 |
. . . . . . . . . . . . 13
 
    
  |
98 | 97 | rexrd 9708 |
. . . . . . . . . . . . . 14
 
    
  |
99 | 4 | rexrd 9708 |
. . . . . . . . . . . . . . 15
   |
100 | 99 | adantr 472 |
. . . . . . . . . . . . . 14
 
    
  |
101 | | simpr 468 |
. . . . . . . . . . . . . 14
 
    
      |
102 | | ioogtlb 37688 |
. . . . . . . . . . . . . 14
         |
103 | 98, 100, 101, 102 | syl3anc 1292 |
. . . . . . . . . . . . 13
 
    
  |
104 | 97, 81, 79, 103 | ltadd2dd 9811 |
. . . . . . . . . . . 12
 
    
  
   |
105 | 4 | adantr 472 |
. . . . . . . . . . . . 13
 
    
  |
106 | | iooltub 37706 |
. . . . . . . . . . . . . 14
         |
107 | 98, 100, 101, 106 | syl3anc 1292 |
. . . . . . . . . . . . 13
 
    
  |
108 | 81, 105, 79, 107 | ltadd2dd 9811 |
. . . . . . . . . . . 12
 
    
      |
109 | 93, 96, 82, 104, 108 | eliood 37691 |
. . . . . . . . . . 11
 
    
       
    |
110 | 90, 109 | ffvelrnd 6038 |
. . . . . . . . . 10
 
    
        
      
    |
111 | | eqid 2471 |
. . . . . . . . . . 11
       
                 |
112 | 1, 2, 3, 4, 111, 5 | fourierdlem28 38109 |
. . . . . . . . . 10
                                         |
113 | 84 | recnd 9687 |
. . . . . . . . . 10
 
    
  |
114 | | 0red 9662 |
. . . . . . . . . 10
 
    
  |
115 | | iooretop 21864 |
. . . . . . . . . . . . 13
         |
116 | | eqid 2471 |
. . . . . . . . . . . . . 14
  ℂfld   ℂfld |
117 | 116 | tgioo2 21899 |
. . . . . . . . . . . . 13
       ℂfld
↾t   |
118 | 115, 117 | eleqtri 2547 |
. . . . . . . . . . . 12
       ℂfld
↾t   |
119 | 118 | a1i 11 |
. . . . . . . . . . 11
        ℂfld ↾t    |
120 | 12 | recnd 9687 |
. . . . . . . . . . 11
   |
121 | 88, 119, 120 | dvmptconst 37882 |
. . . . . . . . . 10
                 |
122 | 88, 89, 110, 112, 113, 114, 121 | dvmptsub 23000 |
. . . . . . . . 9
           
             
                   |
123 | 110 | recnd 9687 |
. . . . . . . . . . 11
 
    
        
      
    |
124 | 123 | subid1d 9994 |
. . . . . . . . . 10
 
    
                                        |
125 | 124 | mpteq2dva 4482 |
. . . . . . . . 9
               
      
                              |
126 | 122, 125 | eqtrd 2505 |
. . . . . . . 8
           
                               |
127 | 126 | 3ad2ant1 1051 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)  
                                          
      
     |
128 | 123 | 3ad2antl1 1192 |
. . . . . . 7
      ![[,] [,]](_icc.gif)                    
        
      
    |
129 | | 2cnd 10704 |
. . . . . . . . 9
       |
130 | 80 | recnd 9687 |
. . . . . . . . . . 11
       |
131 | 130 | halfcld 10880 |
. . . . . . . . . 10
         |
132 | 131 | sincld 14261 |
. . . . . . . . 9
             |
133 | 129, 132 | mulcld 9681 |
. . . . . . . 8
               |
134 | 133 | adantl 473 |
. . . . . . 7
      ![[,] [,]](_icc.gif)                    
          |
135 | | fourierdlem68.e |
. . . . . . . 8
   |
136 | 135 | 3ad2ant1 1051 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)  
               |
137 | | 1re 9660 |
. . . . . . . . 9
 |
138 | 22, 137 | remulcli 9675 |
. . . . . . . 8
   |
139 | 138 | a1i 11 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)  
                 |
140 | | 1red 9676 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)  
               |
141 | | fourierdlem68.d |
. . . . . . . . 9
   |
142 | 120 | abscld 13575 |
. . . . . . . . 9
       |
143 | 141, 142 | readdcld 9688 |
. . . . . . . 8
         |
144 | 143 | 3ad2ant1 1051 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)  
             
       |
145 | | simpl 464 |
. . . . . . . . . 10
 
    
  |
146 | 145, 109 | jca 541 |
. . . . . . . . 9
 
    
              |
147 | | eleq1 2537 |
. . . . . . . . . . . 12
           
       
     |
148 | 147 | anbi2d 718 |
. . . . . . . . . . 11
    
     
  
               |
149 | | fveq2 5879 |
. . . . . . . . . . . . 13
                     
                 |
150 | 149 | fveq2d 5883 |
. . . . . . . . . . . 12
              
                                |
151 | 150 | breq1d 4405 |
. . . . . . . . . . 11
                       
     
               
   |
152 | 148, 151 | imbi12d 327 |
. . . . . . . . . 10
     
 
                           
            
     
               
    |
153 | | fourierdlem68.fdvbd |
. . . . . . . . . 10
 
     
              
          |
154 | 152, 153 | vtoclg 3093 |
. . . . . . . . 9
    

      
              
      
      |
155 | 82, 146, 154 | sylc 61 |
. . . . . . . 8
 
    
     
               
  |
156 | 155 | 3ad2antl1 1192 |
. . . . . . 7
      ![[,] [,]](_icc.gif)                    
     
               
  |
157 | 129, 132 | absmuld 13593 |
. . . . . . . . 9
                                   |
158 | | 0le2 10722 |
. . . . . . . . . . . 12
 |
159 | | absid 13436 |
. . . . . . . . . . . 12
         |
160 | 22, 158, 159 | mp2an 686 |
. . . . . . . . . . 11
     |
161 | 160 | oveq1i 6318 |
. . . . . . . . . 10
                             |
162 | 132 | abscld 13575 |
. . . . . . . . . . 11
                 |
163 | | 1red 9676 |
. . . . . . . . . . 11
       |
164 | 22 | a1i 11 |
. . . . . . . . . . 11
       |
165 | 158 | a1i 11 |
. . . . . . . . . . 11
       |
166 | 80 | rehalfcld 10882 |
. . . . . . . . . . . 12
         |
167 | | abssinbd 37600 |
. . . . . . . . . . . 12
               |
168 | 166, 167 | syl 17 |
. . . . . . . . . . 11
                 |
169 | 162, 163,
164, 165, 168 | lemul2ad 10569 |
. . . . . . . . . 10
                     |
170 | 161, 169 | syl5eqbr 4429 |
. . . . . . . . 9
                         |
171 | 157, 170 | eqbrtrd 4416 |
. . . . . . . 8
                     |
172 | 171 | adantl 473 |
. . . . . . 7
      ![[,] [,]](_icc.gif)                    
           
    |
173 | | abscosbd 37578 |
. . . . . . . . 9
               |
174 | 101, 166,
173 | 3syl 18 |
. . . . . . . 8
 
    
            |
175 | 174 | 3ad2antl1 1192 |
. . . . . . 7
      ![[,] [,]](_icc.gif)                    
            |
176 | 86 | abscld 13575 |
. . . . . . . . 9
 
    
       
      |
177 | 89 | abscld 13575 |
. . . . . . . . . 10
 
    
      
     |
178 | 113 | abscld 13575 |
. . . . . . . . . 10
 
    
      |
179 | 177, 178 | readdcld 9688 |
. . . . . . . . 9
 
    
       
          |
180 | 141 | adantr 472 |
. . . . . . . . . 10
 
    
  |
181 | 180, 178 | readdcld 9688 |
. . . . . . . . 9
 
    
        |
182 | 89, 113 | abs2dif2d 13597 |
. . . . . . . . 9
 
    
       
                      |
183 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
          
    |
184 | 183 | fveq2d 5883 |
. . . . . . . . . . . . . 14
                       |
185 | 184 | breq1d 4405 |
. . . . . . . . . . . . 13
           
      
      |
186 | 148, 185 | imbi12d 327 |
. . . . . . . . . . . 12
     
 
              
   
      
         
       |
187 | | fourierdlem68.fbd |
. . . . . . . . . . . 12
 
     
             |
188 | 186, 187 | vtoclg 3093 |
. . . . . . . . . . 11
            

      
         
      |
189 | 109, 146,
188 | sylc 61 |
. . . . . . . . . 10
 
    
      
     |
190 | 177, 180,
178, 189 | leadd1dd 10248 |
. . . . . . . . 9
 
    
       
        
       |
191 | 176, 179,
181, 182, 190 | letrd 9809 |
. . . . . . . 8
 
    
       
    
       |
192 | 191 | 3ad2antl1 1192 |
. . . . . . 7
      ![[,] [,]](_icc.gif)                    
       
    
       |
193 | 14 | simpri 469 |
. . . . . . . 8
                             |
194 | 193 | a1i 11 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)  
                                           |
195 | 131 | coscld 14262 |
. . . . . . . 8
             |
196 | 195 | adantl 473 |
. . . . . . 7
      ![[,] [,]](_icc.gif)                    
        |
197 | | simp2 1031 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)  
               |
198 | | oveq1 6315 |
. . . . . . . . . . . . . 14
       |
199 | 198 | fveq2d 5883 |
. . . . . . . . . . . . 13
               |
200 | 199 | oveq2d 6324 |
. . . . . . . . . . . 12
                   |
201 | 200 | fveq2d 5883 |
. . . . . . . . . . 11
                           |
202 | 201 | breq2d 4407 |
. . . . . . . . . 10
 
                           |
203 | 202 | cbvralv 3005 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)               
  ![[,] [,]](_icc.gif)                 |
204 | | nfv 1769 |
. . . . . . . . . . 11
   |
205 | | nfra1 2785 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)  
             |
206 | 204, 205 | nfan 2031 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)                 |
207 | | simplr 770 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)                 |
208 | 6, 101 | sseldi 3416 |
. . . . . . . . . . . . 13
 
    
  ![[,] [,]](_icc.gif)    |
209 | 208 | adantlr 729 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif)    |
210 | | rspa 2774 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)  
              ![[,] [,]](_icc.gif)                 |
211 | 207, 209,
210 | syl2anc 673 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)                                   |
212 | 211 | ex 441 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)                    
               |
213 | 206, 212 | ralrimi 2800 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)                     
              |
214 | 203, 213 | sylan2b 483 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)                     
              |
215 | 214 | 3adant2 1049 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)  
                                 |
216 | | eqid 2471 |
. . . . . . 7
                                     
               |
217 | 77, 87, 127, 128, 134, 136, 139, 140, 144, 156, 172, 175, 192, 194, 196, 197, 215, 216 | dvdivbd 37892 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)  
                                   
                 
  |
218 | 217 | rexlimdv3a 2873 |
. . . . 5
      ![[,] [,]](_icc.gif)  
           
                      
                 
   |
219 | 75, 218 | mpd 15 |
. . . 4
                       
                 
  |
220 | | nfcv 2612 |
. . . . . . . . 9
   |
221 | | nfcv 2612 |
. . . . . . . . 9
  |
222 | | nfmpt1 4485 |
. . . . . . . . . 10
                           |
223 | 13, 222 | nfcxfr 2610 |
. . . . . . . . 9
   |
224 | 220, 221,
223 | nfov 6334 |
. . . . . . . 8
     |
225 | 224 | nfdm 5082 |
. . . . . . 7
     |
226 | | nfcv 2612 |
. . . . . . 7
       |
227 | 225, 226 | raleqf 2969 |
. . . . . 6
                                                                   
                 
   |
228 | 18, 227 | syl 17 |
. . . . 5
                                                             
                 
   |
229 | 228 | rexbidv 2892 |
. . . 4
                                          
                                          |
230 | 219, 229 | mpbird 240 |
. . 3
                     
                 
  |
231 | 13 | a1i 11 |
. . . . . . . 8
           
               |
232 | 231 | oveq2d 6324 |
. . . . . . 7
                               |
233 | 232 | fveq1d 5881 |
. . . . . 6
                   
                   |
234 | 233 | fveq2d 5883 |
. . . . 5
                                               |
235 | 234 | breq1d 4405 |
. . . 4
           
                                     |
236 | 235 | rexralbidv 2898 |
. . 3
                  
                  
                 
   |
237 | 230, 236 | mpbird 240 |
. 2
                  |
238 | 18, 237 | jca 541 |
1
       
                  |