Step | Hyp | Ref
| Expression |
1 | | fourierdlem12.4 |
. . . 4
   |
2 | | fourierdlem12.3 |
. . . . . . . 8
       |
3 | | fourierdlem12.2 |
. . . . . . . . 9
   |
4 | | fourierdlem12.1 |
. . . . . . . . . 10
 
                 
 ..^                |
5 | 4 | fourierdlem2 38083 |
. . . . . . . . 9
 
   
                  
 ..^                 |
6 | 3, 5 | syl 17 |
. . . . . . . 8
                        
 ..^                 |
7 | 2, 6 | mpbid 215 |
. . . . . . 7
                   
 ..^                |
8 | 7 | simpld 466 |
. . . . . 6
         |
9 | | elmapi 7511 |
. . . . . 6
                 |
10 | | ffn 5739 |
. . . . . 6
               |
11 | 8, 9, 10 | 3syl 18 |
. . . . 5
       |
12 | | fvelrnb 5926 |
. . . . 5
     
             |
13 | 11, 12 | syl 17 |
. . . 4
  
            |
14 | 1, 13 | mpbid 215 |
. . 3
             |
15 | 14 | adantr 472 |
. 2
 
 ..^              |
16 | 8, 9 | syl 17 |
. . . . . . . . . . . 12
           |
17 | 16 | adantr 472 |
. . . . . . . . . . 11
 
 ..^            |
18 | | fzofzp1 12037 |
. . . . . . . . . . . 12
  ..^
        |
19 | 18 | adantl 473 |
. . . . . . . . . . 11
 
 ..^          |
20 | 17, 19 | ffvelrnd 6038 |
. . . . . . . . . 10
 
 ..^          |
21 | 20 | adantr 472 |
. . . . . . . . 9
    ..^           |
22 | 21 | 3ad2antl1 1192 |
. . . . . . . 8
   
 ..^ 
                  |
23 | | frn 5747 |
. . . . . . . . . . . 12
        
  |
24 | 16, 23 | syl 17 |
. . . . . . . . . . 11
   |
25 | 24, 1 | sseldd 3419 |
. . . . . . . . . 10
   |
26 | 25 | ad2antrr 740 |
. . . . . . . . 9
    ..^     |
27 | 26 | 3ad2antl1 1192 |
. . . . . . . 8
   
 ..^ 
         
  |
28 | 17 | ffvelrnda 6037 |
. . . . . . . . . . 11
    ..^             |
29 | 28 | 3adant3 1050 |
. . . . . . . . . 10
    ..^     
    
      |
30 | 29 | adantr 472 |
. . . . . . . . 9
   
 ..^ 
                |
31 | | simpr 468 |
. . . . . . . . . . . . . 14
    ..^
     
  |
32 | | elfzoelz 11947 |
. . . . . . . . . . . . . . . 16
  ..^
  |
33 | 32 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
    ..^
     
  |
34 | | elfzelz 11826 |
. . . . . . . . . . . . . . . 16
       |
35 | 34 | ad2antlr 741 |
. . . . . . . . . . . . . . 15
    ..^
     
  |
36 | | zltp1le 11010 |
. . . . . . . . . . . . . . 15
 
       |
37 | 33, 35, 36 | syl2anc 673 |
. . . . . . . . . . . . . 14
    ..^
     
      |
38 | 31, 37 | mpbid 215 |
. . . . . . . . . . . . 13
    ..^
     
    |
39 | 33 | peano2zd 11066 |
. . . . . . . . . . . . . 14
    ..^
     
    |
40 | | eluz 11196 |
. . . . . . . . . . . . . 14
   
       
     |
41 | 39, 35, 40 | syl2anc 673 |
. . . . . . . . . . . . 13
    ..^
     
        
   |
42 | 38, 41 | mpbird 240 |
. . . . . . . . . . . 12
    ..^
     
        |
43 | 42 | adantlll 732 |
. . . . . . . . . . 11
   
 ..^ 
     
        |
44 | 17 | ad2antrr 740 |
. . . . . . . . . . . . 13
   
 ..^ 
           
          |
45 | | 0red 9662 |
. . . . . . . . . . . . . . . . 17
   ..^          |
46 | | elfzelz 11826 |
. . . . . . . . . . . . . . . . . . 19
         |
47 | 46 | zred 11063 |
. . . . . . . . . . . . . . . . . 18
         |
48 | 47 | adantl 473 |
. . . . . . . . . . . . . . . . 17
   ..^          |
49 | 32 | peano2zd 11066 |
. . . . . . . . . . . . . . . . . . . 20
  ..^
    |
50 | 49 | zred 11063 |
. . . . . . . . . . . . . . . . . . 19
  ..^
    |
51 | 50 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
   ..^            |
52 | 32 | zred 11063 |
. . . . . . . . . . . . . . . . . . . 20
  ..^
  |
53 | 52 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
   ..^          |
54 | | elfzole1 11955 |
. . . . . . . . . . . . . . . . . . . 20
  ..^
  |
55 | 54 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
   ..^          |
56 | 53 | ltp1d 10559 |
. . . . . . . . . . . . . . . . . . 19
   ..^            |
57 | 45, 53, 51, 55, 56 | lelttrd 9810 |
. . . . . . . . . . . . . . . . . 18
   ..^            |
58 | | elfzle1 11828 |
. . . . . . . . . . . . . . . . . . 19
           |
59 | 58 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
   ..^            |
60 | 45, 51, 48, 57, 59 | ltletrd 9812 |
. . . . . . . . . . . . . . . . 17
   ..^          |
61 | 45, 48, 60 | ltled 9800 |
. . . . . . . . . . . . . . . 16
   ..^          |
62 | 61 | adantlr 729 |
. . . . . . . . . . . . . . 15
    ..^
           
  |
63 | 47 | adantl 473 |
. . . . . . . . . . . . . . . . 17
     
         |
64 | 34 | zred 11063 |
. . . . . . . . . . . . . . . . . 18
       |
65 | 64 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     
         |
66 | | elfzel2 11824 |
. . . . . . . . . . . . . . . . . . 19
       |
67 | 66 | zred 11063 |
. . . . . . . . . . . . . . . . . 18
       |
68 | 67 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     
         |
69 | | elfzle2 11829 |
. . . . . . . . . . . . . . . . . 18
         |
70 | 69 | adantl 473 |
. . . . . . . . . . . . . . . . 17
     
         |
71 | | elfzle2 11829 |
. . . . . . . . . . . . . . . . . 18
       |
72 | 71 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     
         |
73 | 63, 65, 68, 70, 72 | letrd 9809 |
. . . . . . . . . . . . . . . 16
     
         |
74 | 73 | adantll 728 |
. . . . . . . . . . . . . . 15
    ..^
           
  |
75 | 46 | adantl 473 |
. . . . . . . . . . . . . . . 16
    ..^
           
  |
76 | | 0zd 10973 |
. . . . . . . . . . . . . . . 16
    ..^
           
  |
77 | 66 | ad2antlr 741 |
. . . . . . . . . . . . . . . 16
    ..^
           
  |
78 | | elfz 11816 |
. . . . . . . . . . . . . . . 16
 
     
     |
79 | 75, 76, 77, 78 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
    ..^
           
          |
80 | 62, 74, 79 | mpbir2and 936 |
. . . . . . . . . . . . . 14
    ..^
           
      |
81 | 80 | adantlll 732 |
. . . . . . . . . . . . 13
   
 ..^ 
           
      |
82 | 44, 81 | ffvelrnd 6038 |
. . . . . . . . . . . 12
   
 ..^ 
           
      |
83 | 82 | adantlr 729 |
. . . . . . . . . . 11
      ..^ 
     
             |
84 | | simp-4l 784 |
. . . . . . . . . . . 12
      ..^ 
     
           |
85 | | 0red 9662 |
. . . . . . . . . . . . . . . 16
    ..^
             
  |
86 | | elfzelz 11826 |
. . . . . . . . . . . . . . . . . 18
           |
87 | 86 | zred 11063 |
. . . . . . . . . . . . . . . . 17
           |
88 | 87 | adantl 473 |
. . . . . . . . . . . . . . . 16
    ..^
             
  |
89 | | 0red 9662 |
. . . . . . . . . . . . . . . . . 18
   ..^            |
90 | 50 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
   ..^              |
91 | 87 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
   ..^            |
92 | | 0red 9662 |
. . . . . . . . . . . . . . . . . . . 20
  ..^
  |
93 | 52 | ltp1d 10559 |
. . . . . . . . . . . . . . . . . . . 20
  ..^
    |
94 | 92, 52, 50, 54, 93 | lelttrd 9810 |
. . . . . . . . . . . . . . . . . . 19
  ..^
    |
95 | 94 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
   ..^              |
96 | | elfzle1 11828 |
. . . . . . . . . . . . . . . . . . 19
             |
97 | 96 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
   ..^              |
98 | 89, 90, 91, 95, 97 | ltletrd 9812 |
. . . . . . . . . . . . . . . . 17
   ..^            |
99 | 98 | adantlr 729 |
. . . . . . . . . . . . . . . 16
    ..^
             
  |
100 | 85, 88, 99 | ltled 9800 |
. . . . . . . . . . . . . . 15
    ..^
             
  |
101 | 100 | adantlll 732 |
. . . . . . . . . . . . . 14
   
 ..^ 
             
  |
102 | 101 | adantlr 729 |
. . . . . . . . . . . . 13
      ..^ 
     
           |
103 | 87 | adantl 473 |
. . . . . . . . . . . . . . . 16
     
           |
104 | | peano2rem 9961 |
. . . . . . . . . . . . . . . . . 18
     |
105 | 64, 104 | syl 17 |
. . . . . . . . . . . . . . . . 17
         |
106 | 105 | adantr 472 |
. . . . . . . . . . . . . . . 16
     
             |
107 | 67 | adantr 472 |
. . . . . . . . . . . . . . . 16
     
           |
108 | | elfzle2 11829 |
. . . . . . . . . . . . . . . . 17
             |
109 | 108 | adantl 473 |
. . . . . . . . . . . . . . . 16
     
             |
110 | | zlem1lt 11012 |
. . . . . . . . . . . . . . . . . . 19
 
       |
111 | 34, 66, 110 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
     
     |
112 | 71, 111 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
         |
113 | 112 | adantr 472 |
. . . . . . . . . . . . . . . 16
     
             |
114 | 103, 106,
107, 109, 113 | lelttrd 9810 |
. . . . . . . . . . . . . . 15
     
           |
115 | 114 | adantlr 729 |
. . . . . . . . . . . . . 14
       
           |
116 | 115 | adantlll 732 |
. . . . . . . . . . . . 13
      ..^ 
     
           |
117 | 86 | adantl 473 |
. . . . . . . . . . . . . 14
      ..^ 
     
           |
118 | | 0zd 10973 |
. . . . . . . . . . . . . 14
      ..^ 
     
           |
119 | 66 | ad3antlr 745 |
. . . . . . . . . . . . . 14
      ..^ 
     
           |
120 | | elfzo 11949 |
. . . . . . . . . . . . . 14
 
   ..^
     |
121 | 117, 118,
119, 120 | syl3anc 1292 |
. . . . . . . . . . . . 13
      ..^ 
     
           ..^
     |
122 | 102, 116,
121 | mpbir2and 936 |
. . . . . . . . . . . 12
      ..^ 
     
          ..^   |
123 | 16 | adantr 472 |
. . . . . . . . . . . . . 14
 
 ..^            |
124 | | elfzofz 11962 |
. . . . . . . . . . . . . . 15
  ..^
      |
125 | 124 | adantl 473 |
. . . . . . . . . . . . . 14
 
 ..^        |
126 | 123, 125 | ffvelrnd 6038 |
. . . . . . . . . . . . 13
 
 ..^        |
127 | | fzofzp1 12037 |
. . . . . . . . . . . . . . 15
  ..^
        |
128 | 127 | adantl 473 |
. . . . . . . . . . . . . 14
 
 ..^          |
129 | 123, 128 | ffvelrnd 6038 |
. . . . . . . . . . . . 13
 
 ..^     
    |
130 | | eleq1 2537 |
. . . . . . . . . . . . . . . 16
   ..^
 ..^    |
131 | 130 | anbi2d 718 |
. . . . . . . . . . . . . . 15
  
 ..^  
 ..^     |
132 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
           |
133 | | oveq1 6315 |
. . . . . . . . . . . . . . . . 17
       |
134 | 133 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
          
    |
135 | 132, 134 | breq12d 4408 |
. . . . . . . . . . . . . . 15
     
     
             |
136 | 131, 135 | imbi12d 327 |
. . . . . . . . . . . . . 14
   
 ..^     
      
   ..^                |
137 | 7 | simprrd 775 |
. . . . . . . . . . . . . . 15
   ..^              |
138 | 137 | r19.21bi 2776 |
. . . . . . . . . . . . . 14
 
 ..^              |
139 | 136, 138 | chvarv 2120 |
. . . . . . . . . . . . 13
 
 ..^              |
140 | 126, 129,
139 | ltled 9800 |
. . . . . . . . . . . 12
 
 ..^              |
141 | 84, 122, 140 | syl2anc 673 |
. . . . . . . . . . 11
      ..^ 
     
                     |
142 | 43, 83, 141 | monoord 12281 |
. . . . . . . . . 10
   
 ..^ 
     
            |
143 | 142 | 3adantl3 1188 |
. . . . . . . . 9
   
 ..^ 
               
      |
144 | 16 | ffvelrnda 6037 |
. . . . . . . . . . . . 13
 
           |
145 | 144 | 3adant3 1050 |
. . . . . . . . . . . 12
 
   
    
      |
146 | | simp3 1032 |
. . . . . . . . . . . 12
 
   
    
      |
147 | 145, 146 | eqled 9755 |
. . . . . . . . . . 11
 
   
    
      |
148 | 147 | 3adant1r 1285 |
. . . . . . . . . 10
    ..^     
    
      |
149 | 148 | adantr 472 |
. . . . . . . . 9
   
 ..^ 
             
  |
150 | 22, 30, 27, 143, 149 | letrd 9809 |
. . . . . . . 8
   
 ..^ 
               
  |
151 | 22, 27, 150 | lensymd 9803 |
. . . . . . 7
   
 ..^ 
         
        |
152 | 151 | intnand 930 |
. . . . . 6
   
 ..^ 
              
         |
153 | 64 | ad2antlr 741 |
. . . . . . . . . 10
   
 ..^ 
        |
154 | 52 | ad3antlr 745 |
. . . . . . . . . 10
   
 ..^ 
        |
155 | | simpr 468 |
. . . . . . . . . 10
   
 ..^ 
        |
156 | 153, 154,
155 | nltled 9802 |
. . . . . . . . 9
   
 ..^ 
        |
157 | 156 | 3adantl3 1188 |
. . . . . . . 8
   
 ..^ 
        
   |
158 | | eqcom 2478 |
. . . . . . . . . . . . 13
    
      |
159 | 158 | biimpi 199 |
. . . . . . . . . . . 12
           |
160 | 159 | adantr 472 |
. . . . . . . . . . 11
      
      |
161 | 160 | 3ad2antl3 1194 |
. . . . . . . . . 10
   
 ..^ 
         
      |
162 | 34 | ad2antlr 741 |
. . . . . . . . . . . . . 14
    ..^
     
  |
163 | 32 | ad2antrr 740 |
. . . . . . . . . . . . . 14
    ..^
     
  |
164 | | simpr 468 |
. . . . . . . . . . . . . 14
    ..^
     
  |
165 | | eluz2 11188 |
. . . . . . . . . . . . . 14
         |
166 | 162, 163,
164, 165 | syl3anbrc 1214 |
. . . . . . . . . . . . 13
    ..^
     
      |
167 | 166 | adantlll 732 |
. . . . . . . . . . . 12
   
 ..^ 
     
      |
168 | 17 | ad2antrr 740 |
. . . . . . . . . . . . . 14
   
 ..^ 
         
          |
169 | | 0zd 10973 |
. . . . . . . . . . . . . . . . . 18
    ..^
         
  |
170 | 66 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . 18
    ..^
         
  |
171 | | elfzelz 11826 |
. . . . . . . . . . . . . . . . . . 19
       |
172 | 171 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
    ..^
         
  |
173 | 169, 170,
172 | 3jca 1210 |
. . . . . . . . . . . . . . . . 17
    ..^
         
    |
174 | | 0red 9662 |
. . . . . . . . . . . . . . . . . . 19
     
       |
175 | 64 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
     
       |
176 | 171 | zred 11063 |
. . . . . . . . . . . . . . . . . . . 20
       |
177 | 176 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
     
    
  |
178 | | elfzle1 11828 |
. . . . . . . . . . . . . . . . . . . 20
       |
179 | 178 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
     
    
  |
180 | | elfzle1 11828 |
. . . . . . . . . . . . . . . . . . . 20
       |
181 | 180 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
     
    
  |
182 | 174, 175,
177, 179, 181 | letrd 9809 |
. . . . . . . . . . . . . . . . . 18
     
    
  |
183 | 182 | adantll 728 |
. . . . . . . . . . . . . . . . 17
    ..^
         
  |
184 | 176 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
   ..^        |
185 | | elfzoel2 11946 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^
  |
186 | 185 | zred 11063 |
. . . . . . . . . . . . . . . . . . . 20
  ..^
  |
187 | 186 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
   ..^        |
188 | 52 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
   ..^        |
189 | | elfzle2 11829 |
. . . . . . . . . . . . . . . . . . . . 21
       |
190 | 189 | adantl 473 |
. . . . . . . . . . . . . . . . . . . 20
   ..^        |
191 | | elfzolt2 11956 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^
  |
192 | 191 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
   ..^        |
193 | 184, 188,
187, 190, 192 | lelttrd 9810 |
. . . . . . . . . . . . . . . . . . 19
   ..^        |
194 | 184, 187,
193 | ltled 9800 |
. . . . . . . . . . . . . . . . . 18
   ..^        |
195 | 194 | adantlr 729 |
. . . . . . . . . . . . . . . . 17
    ..^
         
  |
196 | 173, 183,
195 | jca32 544 |
. . . . . . . . . . . . . . . 16
    ..^
         
 
 
    |
197 | 196 | adantlll 732 |
. . . . . . . . . . . . . . 15
   
 ..^ 
         
 
 
    |
198 | | elfz2 11817 |
. . . . . . . . . . . . . . 15
    
 
 
    |
199 | 197, 198 | sylibr 217 |
. . . . . . . . . . . . . 14
   
 ..^ 
         
      |
200 | 168, 199 | ffvelrnd 6038 |
. . . . . . . . . . . . 13
   
 ..^ 
         
      |
201 | 200 | adantlr 729 |
. . . . . . . . . . . 12
      ..^ 
     
           |
202 | | simplll 776 |
. . . . . . . . . . . . . 14
   
 ..^ 
           
  |
203 | | 0red 9662 |
. . . . . . . . . . . . . . . . 17
    ..^
           
  |
204 | 64 | ad2antlr 741 |
. . . . . . . . . . . . . . . . 17
    ..^
           
  |
205 | | elfzelz 11826 |
. . . . . . . . . . . . . . . . . . 19
         |
206 | 205 | zred 11063 |
. . . . . . . . . . . . . . . . . 18
         |
207 | 206 | adantl 473 |
. . . . . . . . . . . . . . . . 17
    ..^
           
  |
208 | 178 | ad2antlr 741 |
. . . . . . . . . . . . . . . . 17
    ..^
           
  |
209 | | elfzle1 11828 |
. . . . . . . . . . . . . . . . . 18
         |
210 | 209 | adantl 473 |
. . . . . . . . . . . . . . . . 17
    ..^
           
  |
211 | 203, 204,
207, 208, 210 | letrd 9809 |
. . . . . . . . . . . . . . . 16
    ..^
           
  |
212 | 206 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
   ..^          |
213 | 52 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
   ..^          |
214 | 186 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
   ..^          |
215 | | peano2rem 9961 |
. . . . . . . . . . . . . . . . . . . 20
     |
216 | 213, 215 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
   ..^            |
217 | | elfzle2 11829 |
. . . . . . . . . . . . . . . . . . . 20
           |
218 | 217 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
   ..^            |
219 | 213 | ltm1d 10561 |
. . . . . . . . . . . . . . . . . . 19
   ..^            |
220 | 212, 216,
213, 218, 219 | lelttrd 9810 |
. . . . . . . . . . . . . . . . . 18
   ..^          |
221 | 191 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
   ..^          |
222 | 212, 213,
214, 220, 221 | lttrd 9813 |
. . . . . . . . . . . . . . . . 17
   ..^          |
223 | 222 | adantlr 729 |
. . . . . . . . . . . . . . . 16
    ..^
           
  |
224 | 205 | adantl 473 |
. . . . . . . . . . . . . . . . 17
    ..^
           
  |
225 | | 0zd 10973 |
. . . . . . . . . . . . . . . . 17
    ..^
           
  |
226 | 185 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
    ..^
           
  |
227 | 224, 225,
226, 120 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
    ..^
           
  ..^ 
    |
228 | 211, 223,
227 | mpbir2and 936 |
. . . . . . . . . . . . . . 15
    ..^
           
 ..^   |
229 | 228 | adantlll 732 |
. . . . . . . . . . . . . 14
   
 ..^ 
           
 ..^   |
230 | 202, 229,
140 | syl2anc 673 |
. . . . . . . . . . . . 13
   
 ..^ 
           
            |
231 | 230 | adantlr 729 |
. . . . . . . . . . . 12
      ..^ 
     
                   |
232 | 167, 201,
231 | monoord 12281 |
. . . . . . . . . . 11
   
 ..^ 
     
          |
233 | 232 | 3adantl3 1188 |
. . . . . . . . . 10
   
 ..^ 
             
      |
234 | 161, 233 | eqbrtrd 4416 |
. . . . . . . . 9
   
 ..^ 
                |
235 | 25 | adantr 472 |
. . . . . . . . . . . 12
 
 ..^    |
236 | | elfzofz 11962 |
. . . . . . . . . . . . . 14
  ..^
      |
237 | 236 | adantl 473 |
. . . . . . . . . . . . 13
 
 ..^        |
238 | 17, 237 | ffvelrnd 6038 |
. . . . . . . . . . . 12
 
 ..^        |
239 | 235, 238 | lenltd 9798 |
. . . . . . . . . . 11
 
 ..^      
       |
240 | 239 | adantr 472 |
. . . . . . . . . 10
    ..^       
       |
241 | 240 | 3ad2antl1 1192 |
. . . . . . . . 9
   
 ..^ 
                  
   |
242 | 234, 241 | mpbid 215 |
. . . . . . . 8
   
 ..^ 
             
  |
243 | 157, 242 | syldan 478 |
. . . . . . 7
   
 ..^ 
        

      |
244 | 243 | intnanrd 931 |
. . . . . 6
   
 ..^ 
        

              |
245 | 152, 244 | pm2.61dan 808 |
. . . . 5
    ..^     
    
    
         |
246 | 245 | intnand 930 |
. . . 4
    ..^     
    
                 
          |
247 | | elioo3g 11690 |
. . . 4
              
           
     
          |
248 | 246, 247 | sylnibr 312 |
. . 3
    ..^     
    
                |
249 | 248 | rexlimdv3a 2873 |
. 2
 
 ..^            
                 |
250 | 15, 249 | mpd 15 |
1
 
 ..^ 
                |