Step | Hyp | Ref
| Expression |
1 | | nnre 10638 |
. . . . . . . . . . . . 13
   |
2 | 1 | adantl 473 |
. . . . . . . . . . . 12
 

  |
3 | | stoweidlem60.17 |
. . . . . . . . . . . . . 14
   |
4 | 3 | rpred 11364 |
. . . . . . . . . . . . 13
   |
5 | 4 | adantr 472 |
. . . . . . . . . . . 12
 

  |
6 | 3 | rpne0d 11369 |
. . . . . . . . . . . . 13
   |
7 | 6 | adantr 472 |
. . . . . . . . . . . 12
 

  |
8 | 2, 5, 7 | redivcld 10457 |
. . . . . . . . . . 11
 

    |
9 | | 1red 9676 |
. . . . . . . . . . 11
 

  |
10 | 8, 9 | readdcld 9688 |
. . . . . . . . . 10
 

      |
11 | 10 | adantr 472 |
. . . . . . . . 9
    
           |
12 | | arch 10890 |
. . . . . . . . 9
            |
13 | 11, 12 | syl 17 |
. . . . . . . 8
    
            |
14 | | stoweidlem60.2 |
. . . . . . . . . . . . . . 15
   |
15 | | nfv 1769 |
. . . . . . . . . . . . . . 15
  |
16 | 14, 15 | nfan 2031 |
. . . . . . . . . . . . . 14
     |
17 | | nfra1 2785 |
. . . . . . . . . . . . . 14
        |
18 | 16, 17 | nfan 2031 |
. . . . . . . . . . . . 13
   
        |
19 | | nfv 1769 |
. . . . . . . . . . . . 13
  |
20 | 18, 19 | nfan 2031 |
. . . . . . . . . . . 12
           
  |
21 | | nfv 1769 |
. . . . . . . . . . . 12
       |
22 | 20, 21 | nfan 2031 |
. . . . . . . . . . 11
     


    

      |
23 | | simp-5l 786 |
. . . . . . . . . . . . . 14
     


    

    
   |
24 | | stoweidlem60.3 |
. . . . . . . . . . . . . . . 16
     |
25 | | stoweidlem60.4 |
. . . . . . . . . . . . . . . 16
  |
26 | | stoweidlem60.5 |
. . . . . . . . . . . . . . . 16
   |
27 | | stoweidlem60.15 |
. . . . . . . . . . . . . . . 16
   |
28 | 24, 25, 26, 27 | fcnre 37409 |
. . . . . . . . . . . . . . 15
       |
29 | 28 | fnvinran 37398 |
. . . . . . . . . . . . . 14
 
       |
30 | 23, 29 | sylancom 680 |
. . . . . . . . . . . . 13
     


    

    
       |
31 | | simp-5r 787 |
. . . . . . . . . . . . . 14
     


    

    
   |
32 | 31 | nnred 10646 |
. . . . . . . . . . . . 13
     


    

    
   |
33 | | simpllr 777 |
. . . . . . . . . . . . . . . 16
     


    

    
   |
34 | 33 | nnred 10646 |
. . . . . . . . . . . . . . 15
     


    

    
   |
35 | | 1red 9676 |
. . . . . . . . . . . . . . 15
     


    

    
   |
36 | 34, 35 | resubcld 10068 |
. . . . . . . . . . . . . 14
     


    

    
     |
37 | 23, 4 | syl 17 |
. . . . . . . . . . . . . 14
     


    

    
   |
38 | 36, 37 | remulcld 9689 |
. . . . . . . . . . . . 13
     


    

    
       |
39 | | simpllr 777 |
. . . . . . . . . . . . . 14
           

     
      |
40 | 39 | r19.21bi 2776 |
. . . . . . . . . . . . 13
     


    

    
    
  |
41 | | simplr 770 |
. . . . . . . . . . . . . 14
     


    

    
       |
42 | | simpr 468 |
. . . . . . . . . . . . . . . 16
               |
43 | | simpl1 1033 |
. . . . . . . . . . . . . . . . . 18
           |
44 | | simpl2 1034 |
. . . . . . . . . . . . . . . . . 18
        
  |
45 | 43, 44, 8 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
             |
46 | | 1red 9676 |
. . . . . . . . . . . . . . . . 17
           |
47 | | simpl3 1035 |
. . . . . . . . . . . . . . . . . 18
        
  |
48 | 47 | nnred 10646 |
. . . . . . . . . . . . . . . . 17
        
  |
49 | 45, 46, 48 | ltaddsubd 10234 |
. . . . . . . . . . . . . . . 16
                     |
50 | 42, 49 | mpbid 215 |
. . . . . . . . . . . . . . 15
          
    |
51 | 1 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . 17
 
   |
52 | 51 | adantr 472 |
. . . . . . . . . . . . . . . 16
        
  |
53 | 48, 46 | resubcld 10068 |
. . . . . . . . . . . . . . . 16
             |
54 | 4 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . 17
 
   |
55 | 54 | adantr 472 |
. . . . . . . . . . . . . . . 16
        
  |
56 | 3 | rpgt0d 11367 |
. . . . . . . . . . . . . . . . 17
   |
57 | 43, 56 | syl 17 |
. . . . . . . . . . . . . . . 16
        
  |
58 | | ltdivmul2 10504 |
. . . . . . . . . . . . . . . 16
  
 
 
    
       |
59 | 52, 53, 55, 57, 58 | syl112anc 1296 |
. . . . . . . . . . . . . . 15
             
       |
60 | 50, 59 | mpbid 215 |
. . . . . . . . . . . . . 14
               |
61 | 23, 31, 33, 41, 60 | syl31anc 1295 |
. . . . . . . . . . . . 13
     


    

    
       |
62 | 30, 32, 38, 40, 61 | lttrd 9813 |
. . . . . . . . . . . 12
     


    

    
    
      |
63 | 62 | ex 441 |
. . . . . . . . . . 11
           

         
       |
64 | 22, 63 | ralrimi 2800 |
. . . . . . . . . 10
           

     
          |
65 | 64 | ex 441 |
. . . . . . . . 9
   
      
                  |
66 | 65 | reximdva 2858 |
. . . . . . . 8
    
      
    
            |
67 | 13, 66 | mpd 15 |
. . . . . . 7
    
                 |
68 | | stoweidlem60.1 |
. . . . . . . 8
   |
69 | | stoweidlem60.8 |
. . . . . . . 8
   |
70 | | stoweidlem60.9 |
. . . . . . . 8
   |
71 | 68, 14, 24, 69, 25, 70, 26, 27 | rfcnnnub 37420 |
. . . . . . 7
         |
72 | 67, 71 | r19.29a 2918 |
. . . . . 6
             |
73 | | df-rex 2762 |
. . . . . 6
  
           
           |
74 | 72, 73 | sylib 201 |
. . . . 5
    
           |
75 | | simpr 468 |
. . . . . . . . 9
 
 
                       |
76 | 14, 19 | nfan 2031 |
. . . . . . . . . . 11
     |
77 | | stoweidlem60.6 |
. . . . . . . . . . 11
                   |
78 | | stoweidlem60.7 |
. . . . . . . . . . 11
                   |
79 | | eqid 2471 |
. . . . . . . . . . 11
 

                    
   |
80 | | eqid 2471 |
. . . . . . . . . . 11
       
                                                
                                          |
81 | 69 | adantr 472 |
. . . . . . . . . . 11
 

  |
82 | | stoweidlem60.10 |
. . . . . . . . . . . 12

  |
83 | 82 | adantr 472 |
. . . . . . . . . . 11
 

  |
84 | | stoweidlem60.11 |
. . . . . . . . . . . 12
 


             |
85 | 84 | 3adant1r 1285 |
. . . . . . . . . . 11
   
               |
86 | | stoweidlem60.12 |
. . . . . . . . . . . 12
 


             |
87 | 86 | 3adant1r 1285 |
. . . . . . . . . . 11
   
               |
88 | | stoweidlem60.13 |
. . . . . . . . . . . 12
 

    |
89 | 88 | adantlr 729 |
. . . . . . . . . . 11
         |
90 | | stoweidlem60.14 |
. . . . . . . . . . . 12
 

  
          |
91 | 90 | adantlr 729 |
. . . . . . . . . . 11
    
             |
92 | 27 | adantr 472 |
. . . . . . . . . . 11
 

  |
93 | 3 | adantr 472 |
. . . . . . . . . . 11
 

  |
94 | | stoweidlem60.18 |
. . . . . . . . . . . 12
     |
95 | 94 | adantr 472 |
. . . . . . . . . . 11
 

    |
96 | | simpr 468 |
. . . . . . . . . . 11
 

  |
97 | 68, 76, 24, 25, 26, 77, 78, 79, 80, 81, 83, 85, 87, 89, 91, 92, 93, 95, 96 | stoweidlem59 38032 |
. . . . . . . . . 10
 

                  
                  
              
                      |
98 | 97 | adantrr 731 |
. . . . . . . . 9
 
 
                            
                  
              
                      |
99 | | 19.42v 1842 |
. . . . . . . . 9
     
                         
                  
              
                    
                       
                       
                                        |
100 | 75, 98, 99 | sylanbrc 677 |
. . . . . . . 8
 
 
              
                                          
                                        |
101 | | 3anass 1011 |
. . . . . . . . 9
                                             
                                       
                                          
                                        |
102 | 101 | exbii 1726 |
. . . . . . . 8
     
                                         
                                         
                         
                  
              
                       |
103 | 100, 102 | sylibr 217 |
. . . . . . 7
 
 
              
                 
                       
                                       |
104 | 103 | ex 441 |
. . . . . 6
   
        
    
                 
                       
                                        |
105 | 104 | eximdv 1772 |
. . . . 5
                                                               
                                        |
106 | 74, 105 | mpd 15 |
. . . 4
       
                 
                       
                                       |
107 | | simpl 464 |
. . . . . . . 8
 
                                            
                                     
  |
108 | | simpr1l 1087 |
. . . . . . . 8
 
                                            
                                     
  |
109 | | simpr2 1037 |
. . . . . . . 8
 
                                            
                                     
          |
110 | | nfv 1769 |
. . . . . . . . . 10
          |
111 | 14, 19, 110 | nf3an 2033 |
. . . . . . . . 9
             |
112 | | simp2 1031 |
. . . . . . . . 9
 
           |
113 | | simp3 1032 |
. . . . . . . . 9
 
                   |
114 | | simp1 1030 |
. . . . . . . . . 10
 
           |
115 | 114, 84 | syl3an1 1325 |
. . . . . . . . 9
           
               |
116 | 114, 86 | syl3an1 1325 |
. . . . . . . . 9
           
               |
117 | 88 | 3ad2antl1 1192 |
. . . . . . . . 9
           
     |
118 | 3 | 3ad2ant1 1051 |
. . . . . . . . . 10
 
           |
119 | 118 | rpred 11364 |
. . . . . . . . 9
 
           |
120 | 82 | sselda 3418 |
. . . . . . . . . . 11
 
   |
121 | 24, 25, 26, 120 | fcnre 37409 |
. . . . . . . . . 10
 
       |
122 | 121 | 3ad2antl1 1192 |
. . . . . . . . 9
           
       |
123 | 111, 112,
113, 115, 116, 117, 119, 122 | stoweidlem17 37989 |
. . . . . . . 8
 
                             |
124 | 107, 108,
109, 123 | syl3anc 1292 |
. . . . . . 7
 
                                            
                                     

                   |
125 | | nfv 1769 |
. . . . . . . . 9
   |
126 | | nfv 1769 |
. . . . . . . . . 10
              |
127 | | nfv 1769 |
. . . . . . . . . 10
          |
128 | | nfra1 2785 |
. . . . . . . . . 10
                  
        
                                    |
129 | 126, 127,
128 | nf3an 2033 |
. . . . . . . . 9
    
                 
                       
                                      |
130 | 125, 129 | nfan 2031 |
. . . . . . . 8
                                               
                                       |
131 | | nfra1 2785 |
. . . . . . . . . . 11
            |
132 | 19, 131 | nfan 2031 |
. . . . . . . . . 10
              |
133 | | nfcv 2612 |
. . . . . . . . . . 11
       |
134 | | nfra1 2785 |
. . . . . . . . . . . 12
                   
  |
135 | | nfra1 2785 |
. . . . . . . . . . . 12
               
   |
136 | | nfra1 2785 |
. . . . . . . . . . . 12
                     |
137 | 134, 135,
136 | nf3an 2033 |
. . . . . . . . . . 11
            
        
                                    |
138 | 133, 137 | nfral 2789 |
. . . . . . . . . 10
                  
        
                                    |
139 | 132, 110,
138 | nf3an 2033 |
. . . . . . . . 9
    
                 
                       
                                      |
140 | 14, 139 | nfan 2031 |
. . . . . . . 8
                                               
                                       |
141 | | eqid 2471 |
. . . . . . . 8
                         |
142 | | uniexg 6607 |
. . . . . . . . . . 11

   |
143 | 69, 142 | syl 17 |
. . . . . . . . . 10
    |
144 | 25, 143 | syl5eqel 2553 |
. . . . . . . . 9
   |
145 | 144 | adantr 472 |
. . . . . . . 8
 
                                            
                                     
  |
146 | 28 | adantr 472 |
. . . . . . . 8
 
                                            
                                     
      |
147 | | stoweidlem60.16 |
. . . . . . . . . 10
 
      |
148 | 147 | r19.21bi 2776 |
. . . . . . . . 9
 
       |
149 | 148 | adantlr 729 |
. . . . . . . 8
                                               
                                             |
150 | | simpr1r 1088 |
. . . . . . . . 9
 
                                            
                                     

          |
151 | 150 | r19.21bi 2776 |
. . . . . . . 8
                                               
                                                 |
152 | 3 | adantr 472 |
. . . . . . . 8
 
                                            
                                     
  |
153 | 94 | adantr 472 |
. . . . . . . 8
 
                                            
                                     
    |
154 | | simpll 768 |
. . . . . . . . 9
                                               
                                             |
155 | | simplr2 1073 |
. . . . . . . . 9
                                               
                                                     |
156 | | simpr 468 |
. . . . . . . . 9
                                               
                                                 |
157 | | simp1 1030 |
. . . . . . . . . 10
 
               |
158 | | ffvelrn 6035 |
. . . . . . . . . . 11
              
      |
159 | 158 | 3adant1 1048 |
. . . . . . . . . 10
 
                   |
160 | 82 | sselda 3418 |
. . . . . . . . . . 11
 
    
      |
161 | 24, 25, 26, 160 | fcnre 37409 |
. . . . . . . . . 10
 
    
          |
162 | 157, 159,
161 | syl2anc 673 |
. . . . . . . . 9
 
                       |
163 | 154, 155,
156, 162 | syl3anc 1292 |
. . . . . . . 8
                                               
                                                     |
164 | | simp1r3 1128 |
. . . . . . . . . 10
                                               
                                         
        
                  
              
                     |
165 | | r19.26-3 2906 |
. . . . . . . . . . 11
 
                       
                                   
 
     

                 
     
              
                           |
166 | 165 | simp1bi 1045 |
. . . . . . . . . 10
 
                       
                                    
     

                   |
167 | | simpl 464 |
. . . . . . . . . . . 12
 
                           |
168 | 167 | ralimi 2796 |
. . . . . . . . . . 11
 

                 
          |
169 | 168 | ralimi 2796 |
. . . . . . . . . 10
 
     

                                  |
170 | 164, 166,
169 | 3syl 18 |
. . . . . . . . 9
                                               
                                         
                  |
171 | | simp2 1031 |
. . . . . . . . 9
                                               
                                         
       |
172 | | simp3 1032 |
. . . . . . . . 9
                                               
                                         
   |
173 | | rspa 2774 |
. . . . . . . . . 10
        
             
          |
174 | 173 | r19.21bi 2776 |
. . . . . . . . 9
                 
     
          |
175 | 170, 171,
172, 174 | syl21anc 1291 |
. . . . . . . 8
                                               
                                         
           |
176 | | simpr 468 |
. . . . . . . . . . . 12
 
                           |
177 | 176 | ralimi 2796 |
. . . . . . . . . . 11
 

                 
          |
178 | 177 | ralimi 2796 |
. . . . . . . . . 10
 
     

                                  |
179 | 164, 166,
178 | 3syl 18 |
. . . . . . . . 9
                                               
                                         
                  |
180 | | rspa 2774 |
. . . . . . . . . 10
                
             
  |
181 | 180 | r19.21bi 2776 |
. . . . . . . . 9
                 
     
          |
182 | 179, 171,
172, 181 | syl21anc 1291 |
. . . . . . . 8
                                               
                                         
           |
183 | | simp1r3 1128 |
. . . . . . . . . 10
                                               
                                         
    
       
                  
              
                     |
184 | 165 | simp2bi 1046 |
. . . . . . . . . 10
 
                       
                                    
     
                 |
185 | 183, 184 | syl 17 |
. . . . . . . . 9
                                               
                                         
    
                        |
186 | | simp2 1031 |
. . . . . . . . 9
                                               
                                         
    
      |
187 | | simp3 1032 |
. . . . . . . . 9
                                               
                                         
    
      |
188 | | rspa 2774 |
. . . . . . . . . 10
                     
                         |
189 | 188 | r19.21bi 2776 |
. . . . . . . . 9
                        
         
            |
190 | 185, 186,
187, 189 | syl21anc 1291 |
. . . . . . . 8
                                               
                                         
    
            |
191 | | simp1r3 1128 |
. . . . . . . . . 10
                                               
                                         
    
       
                  
              
                     |
192 | 165 | simp3bi 1047 |
. . . . . . . . . 10
 
                       
                                    
     
                   |
193 | 191, 192 | syl 17 |
. . . . . . . . 9
                                               
                                         
    
                          |
194 | | simp2 1031 |
. . . . . . . . 9
                                               
                                         
    
      |
195 | | simp3 1032 |
. . . . . . . . 9
                                               
                                         
    
      |
196 | | rspa 2774 |
. . . . . . . . . 10
                                                   |
197 | 196 | r19.21bi 2776 |
. . . . . . . . 9
                          
         
              |
198 | 193, 194,
195, 197 | syl21anc 1291 |
. . . . . . . 8
                                               
                                         
    
              |
199 | 68, 130, 140, 77, 78, 141, 108, 145, 146, 149, 151, 152, 153, 163, 175, 182, 190, 198 | stoweidlem34 38007 |
. . . . . . 7
 
                                            
                                     

                                              
           
                          |
200 | | nfmpt1 4485 |
. . . . . . . . . 10
                     |
201 | 200 | nfeq2 2627 |
. . . . . . . . 9
                    |
202 | | fveq1 5878 |
. . . . . . . . . . . . 13
                                               |
203 | 202 | breq1d 4405 |
. . . . . . . . . . . 12
                       
     
                               |
204 | 202 | breq2d 4407 |
. . . . . . . . . . . 12
                         
   
                               |
205 | 203, 204 | anbi12d 725 |
. . . . . . . . . . 11
                                                                                                       |
206 | 205 | anbi2d 718 |
. . . . . . . . . 10
                               
                                             
                                 
           
                           |
207 | 206 | rexbidv 2892 |
. . . . . . . . 9
                    
           
                                  
           
                                 
           
                           |
208 | 201, 207 | ralbid 2826 |
. . . . . . . 8
                    

           
                                  

           
                                 
           
                           |
209 | 208 | rspcev 3136 |
. . . . . . 7
                     
           
                                 
           
                         


           
                                    |
210 | 124, 199,
209 | syl2anc 673 |
. . . . . 6
 
                                            
                                     


                            
           
        |
211 | 210 | ex 441 |
. . . . 5
    
                                         
                                      

           
                                     |
212 | 211 | 2eximdv 1774 |
. . . 4
        
                                         
                                         


           
                                     |
213 | 106, 212 | mpd 15 |
. . 3
     


           
                                    |
214 | | idd 24 |
. . . 4
    


               
                 
                                            
           
         |
215 | 214 | exlimdv 1787 |
. . 3
       

      |