Step | Hyp | Ref
| Expression |
1 | | nnre 10430 |
. . . . . . . . . . . . 13
   |
2 | 1 | adantl 466 |
. . . . . . . . . . . 12
 

  |
3 | | stoweidlem60.17 |
. . . . . . . . . . . . . 14
   |
4 | 3 | rpred 11128 |
. . . . . . . . . . . . 13
   |
5 | 4 | adantr 465 |
. . . . . . . . . . . 12
 

  |
6 | 3 | rpne0d 11133 |
. . . . . . . . . . . . 13
   |
7 | 6 | adantr 465 |
. . . . . . . . . . . 12
 

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

    |
9 | | 1red 9502 |
. . . . . . . . . . 11
 

  |
10 | 8, 9 | readdcld 9514 |
. . . . . . . . . 10
 

      |
11 | 10 | adantr 465 |
. . . . . . . . 9
    
           |
12 | | arch 10677 |
. . . . . . . . 9
            |
13 | 11, 12 | syl 16 |
. . . . . . . 8
    
            |
14 | | stoweidlem60.2 |
. . . . . . . . . . . . . . 15
   |
15 | | nfv 1674 |
. . . . . . . . . . . . . . 15
  |
16 | 14, 15 | nfan 1863 |
. . . . . . . . . . . . . 14
     |
17 | | nfra1 2875 |
. . . . . . . . . . . . . 14
        |
18 | 16, 17 | nfan 1863 |
. . . . . . . . . . . . 13
   
        |
19 | | nfv 1674 |
. . . . . . . . . . . . 13
  |
20 | 18, 19 | nfan 1863 |
. . . . . . . . . . . 12
           
  |
21 | | nfv 1674 |
. . . . . . . . . . . 12
       |
22 | 20, 21 | nfan 1863 |
. . . . . . . . . . 11
     


    

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


    

    
   |
24 | | stoweidlem60.3 |
. . . . . . . . . . . . . . . 16
     |
25 | | stoweidlem60.4 |
. . . . . . . . . . . . . . . 16
  |
26 | | stoweidlem60.5 |
. . . . . . . . . . . . . . . 16
   |
27 | | stoweidlem60.15 |
. . . . . . . . . . . . . . . 16
   |
28 | 24, 25, 26, 27 | fcnre 29885 |
. . . . . . . . . . . . . . 15
       |
29 | 28 | fnvinran 29874 |
. . . . . . . . . . . . . 14
 
       |
30 | 23, 29 | sylancom 667 |
. . . . . . . . . . . . 13
     


    

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


    

    
   |
32 | 31 | nnred 10438 |
. . . . . . . . . . . . 13
     


    

    
   |
33 | | simpllr 758 |
. . . . . . . . . . . . . . . 16
     


    

    
   |
34 | 33 | nnred 10438 |
. . . . . . . . . . . . . . 15
     


    

    
   |
35 | | 1red 9502 |
. . . . . . . . . . . . . . 15
     


    

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


    

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


    

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


    

    
       |
39 | | simpllr 758 |
. . . . . . . . . . . . . 14
           

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


    

    
    
  |
41 | | simplr 754 |
. . . . . . . . . . . . . 14
     


    

    
       |
42 | | simpr 461 |
. . . . . . . . . . . . . . . 16
               |
43 | | simpl1 991 |
. . . . . . . . . . . . . . . . . 18
           |
44 | | simpl2 992 |
. . . . . . . . . . . . . . . . . 18
        
  |
45 | 43, 44, 8 | syl2anc 661 |
. . . . . . . . . . . . . . . . 17
             |
46 | | 1red 9502 |
. . . . . . . . . . . . . . . . 17
           |
47 | | simpl3 993 |
. . . . . . . . . . . . . . . . . 18
        
  |
48 | 47 | nnred 10438 |
. . . . . . . . . . . . . . . . 17
        
  |
49 | 45, 46, 48 | ltaddsubd 10040 |
. . . . . . . . . . . . . . . 16
                     |
50 | 42, 49 | mpbid 210 |
. . . . . . . . . . . . . . 15
          
    |
51 | 1 | 3ad2ant2 1010 |
. . . . . . . . . . . . . . . . 17
 
   |
52 | 51 | adantr 465 |
. . . . . . . . . . . . . . . 16
        
  |
53 | 48, 46 | resubcld 9877 |
. . . . . . . . . . . . . . . 16
             |
54 | 4 | 3ad2ant1 1009 |
. . . . . . . . . . . . . . . . 17
 
   |
55 | 54 | adantr 465 |
. . . . . . . . . . . . . . . 16
        
  |
56 | 3 | rpgt0d 11131 |
. . . . . . . . . . . . . . . . 17
   |
57 | 43, 56 | syl 16 |
. . . . . . . . . . . . . . . 16
        
  |
58 | | ltdivmul2 10308 |
. . . . . . . . . . . . . . . 16
  
 
 
    
       |
59 | 52, 53, 55, 57, 58 | syl112anc 1223 |
. . . . . . . . . . . . . . 15
             
       |
60 | 50, 59 | mpbid 210 |
. . . . . . . . . . . . . 14
               |
61 | 23, 31, 33, 41, 60 | syl31anc 1222 |
. . . . . . . . . . . . 13
     


    

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


    

    
    
      |
63 | 62 | ex 434 |
. . . . . . . . . . 11
           

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

     
          |
65 | 64 | ex 434 |
. . . . . . . . 9
   
      
                  |
66 | 65 | reximdva 2924 |
. . . . . . . 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 29896 |
. . . . . . 7
         |
72 | 67, 71 | r19.29a 2958 |
. . . . . 6
             |
73 | | df-rex 2801 |
. . . . . 6
  
           
           |
74 | 72, 73 | sylib 196 |
. . . . 5
    
           |
75 | | simpr 461 |
. . . . . . . . 9
 
 
                       |
76 | 14, 19 | nfan 1863 |
. . . . . . . . . . 11
     |
77 | | stoweidlem60.6 |
. . . . . . . . . . 11
                   |
78 | | stoweidlem60.7 |
. . . . . . . . . . 11
                   |
79 | | eqid 2451 |
. . . . . . . . . . 11
 

                    
   |
80 | | eqid 2451 |
. . . . . . . . . . 11
       
                                                
                                          |
81 | 69 | adantr 465 |
. . . . . . . . . . 11
 

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

  |
83 | 82 | adantr 465 |
. . . . . . . . . . 11
 

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


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


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

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

  
          |
91 | 90 | adantlr 714 |
. . . . . . . . . . 11
    
             |
92 | 27 | adantr 465 |
. . . . . . . . . . 11
 

  |
93 | 3 | adantr 465 |
. . . . . . . . . . 11
 

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

    |
96 | | simpr 461 |
. . . . . . . . . . 11
 

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

                  
                  
              
                      |
98 | 97 | adantrr 716 |
. . . . . . . . 9
 
 
                            
                  
              
                      |
99 | | 19.42v 1933 |
. . . . . . . . 9
     
                         
                  
              
                    
                       
                       
                                        |
100 | 75, 98, 99 | sylanbrc 664 |
. . . . . . . 8
 
 
              
                                          
                                        |
101 | | 3anass 969 |
. . . . . . . . 9
                                             
                                       
                                          
                                        |
102 | 101 | exbii 1635 |
. . . . . . . 8
     
                                         
                                         
                         
                  
              
                       |
103 | 100, 102 | sylibr 212 |
. . . . . . 7
 
 
              
                 
                       
                                       |
104 | 103 | ex 434 |
. . . . . 6
   
        
    
                 
                       
                                        |
105 | 104 | eximdv 1677 |
. . . . 5
                                                               
                                        |
106 | 74, 105 | mpd 15 |
. . . 4
       
                 
                       
                                       |
107 | | simpl 457 |
. . . . . . . 8
 
                                            
                                     
  |
108 | | simpr1l 1045 |
. . . . . . . 8
 
                                            
                                     
  |
109 | | simpr2 995 |
. . . . . . . 8
 
                                            
                                     
          |
110 | | nfv 1674 |
. . . . . . . . . 10
          |
111 | 14, 19, 110 | nf3an 1865 |
. . . . . . . . 9
             |
112 | | simp2 989 |
. . . . . . . . 9
 
           |
113 | | simp3 990 |
. . . . . . . . 9
 
                   |
114 | | simp1 988 |
. . . . . . . . . 10
 
           |
115 | 114, 84 | syl3an1 1252 |
. . . . . . . . 9
           
               |
116 | 114, 86 | syl3an1 1252 |
. . . . . . . . 9
           
               |
117 | 88 | 3ad2antl1 1150 |
. . . . . . . . 9
           
     |
118 | 3 | 3ad2ant1 1009 |
. . . . . . . . . 10
 
           |
119 | 118 | rpred 11128 |
. . . . . . . . 9
 
           |
120 | 82 | sselda 3454 |
. . . . . . . . . . 11
 
   |
121 | 24, 25, 26, 120 | fcnre 29885 |
. . . . . . . . . 10
 
       |
122 | 121 | 3ad2antl1 1150 |
. . . . . . . . 9
           
       |
123 | 111, 112,
113, 115, 116, 117, 119, 122 | stoweidlem17 29950 |
. . . . . . . 8
 
                             |
124 | 107, 108,
109, 123 | syl3anc 1219 |
. . . . . . 7
 
                                            
                                     

                   |
125 | | nfv 1674 |
. . . . . . . . 9
   |
126 | | nfv 1674 |
. . . . . . . . . 10
              |
127 | | nfv 1674 |
. . . . . . . . . 10
          |
128 | | nfra1 2875 |
. . . . . . . . . 10
                  
        
                                    |
129 | 126, 127,
128 | nf3an 1865 |
. . . . . . . . 9
    
                 
                       
                                      |
130 | 125, 129 | nfan 1863 |
. . . . . . . 8
                                               
                                       |
131 | | nfra1 2875 |
. . . . . . . . . . 11
            |
132 | 19, 131 | nfan 1863 |
. . . . . . . . . 10
              |
133 | | nfcv 2613 |
. . . . . . . . . . 11
       |
134 | | nfra1 2875 |
. . . . . . . . . . . 12
                   
  |
135 | | nfra1 2875 |
. . . . . . . . . . . 12
               
   |
136 | | nfra1 2875 |
. . . . . . . . . . . 12
                     |
137 | 134, 135,
136 | nf3an 1865 |
. . . . . . . . . . 11
            
        
                                    |
138 | 133, 137 | nfral 2878 |
. . . . . . . . . 10
                  
        
                                    |
139 | 132, 110,
138 | nf3an 1865 |
. . . . . . . . 9
    
                 
                       
                                      |
140 | 14, 139 | nfan 1863 |
. . . . . . . 8
                                               
                                       |
141 | | eqid 2451 |
. . . . . . . 8
                         |
142 | | uniexg 6477 |
. . . . . . . . . . 11

   |
143 | 69, 142 | syl 16 |
. . . . . . . . . 10
    |
144 | 25, 143 | syl5eqel 2543 |
. . . . . . . . 9
   |
145 | 144 | adantr 465 |
. . . . . . . 8
 
                                            
                                     
  |
146 | 28 | adantr 465 |
. . . . . . . 8
 
                                            
                                     
      |
147 | | stoweidlem60.16 |
. . . . . . . . . 10
 
      |
148 | 147 | r19.21bi 2910 |
. . . . . . . . 9
 
       |
149 | 148 | adantlr 714 |
. . . . . . . 8
                                               
                                             |
150 | | simpr1r 1046 |
. . . . . . . . 9
 
                                            
                                     

          |
151 | 150 | r19.21bi 2910 |
. . . . . . . 8
                                               
                                                 |
152 | 3 | adantr 465 |
. . . . . . . 8
 
                                            
                                     
  |
153 | 94 | adantr 465 |
. . . . . . . 8
 
                                            
                                     
    |
154 | | simpll 753 |
. . . . . . . . 9
                                               
                                             |
155 | | simplr2 1031 |
. . . . . . . . 9
                                               
                                                     |
156 | | simpr 461 |
. . . . . . . . 9
                                               
                                                 |
157 | | simp1 988 |
. . . . . . . . . 10
 
               |
158 | | ffvelrn 5940 |
. . . . . . . . . . 11
              
      |
159 | 158 | 3adant1 1006 |
. . . . . . . . . 10
 
                   |
160 | 82 | sselda 3454 |
. . . . . . . . . . 11
 
    
      |
161 | 24, 25, 26, 160 | fcnre 29885 |
. . . . . . . . . 10
 
    
          |
162 | 157, 159,
161 | syl2anc 661 |
. . . . . . . . 9
 
                       |
163 | 154, 155,
156, 162 | syl3anc 1219 |
. . . . . . . 8
                                               
                                                     |
164 | | simp1r3 1086 |
. . . . . . . . . 10
                                               
                                         
        
                  
              
                     |
165 | | r19.26-3 2947 |
. . . . . . . . . . 11
 
                       
                                   
 
     

                 
     
              
                           |
166 | 165 | simp1bi 1003 |
. . . . . . . . . 10
 
                       
                                    
     

                   |
167 | | simpl 457 |
. . . . . . . . . . . 12
 
                           |
168 | 167 | ralimi 2811 |
. . . . . . . . . . 11
 

                 
          |
169 | 168 | ralimi 2811 |
. . . . . . . . . 10
 
     

                                  |
170 | 164, 166,
169 | 3syl 20 |
. . . . . . . . 9
                                               
                                         
                  |
171 | | simp2 989 |
. . . . . . . . 9
                                               
                                         
       |
172 | | simp3 990 |
. . . . . . . . 9
                                               
                                         
   |
173 | | rsp 2884 |
. . . . . . . . . . 11
 
     
       
    

           |
174 | 173 | imp 429 |
. . . . . . . . . 10
        
             
          |
175 | 174 | r19.21bi 2910 |
. . . . . . . . 9
                 
     
          |
176 | 170, 171,
172, 175 | syl21anc 1218 |
. . . . . . . 8
                                               
                                         
           |
177 | | simpr 461 |
. . . . . . . . . . . 12
 
                           |
178 | 177 | ralimi 2811 |
. . . . . . . . . . 11
 

                 
          |
179 | 178 | ralimi 2811 |
. . . . . . . . . 10
 
     

                                  |
180 | 164, 166,
179 | 3syl 20 |
. . . . . . . . 9
                                               
                                         
                  |
181 | | rsp 2884 |
. . . . . . . . . . 11
 
     
       
    

           |
182 | 181 | imp 429 |
. . . . . . . . . 10
                
             
  |
183 | 182 | r19.21bi 2910 |
. . . . . . . . 9
                 
     
          |
184 | 180, 171,
172, 183 | syl21anc 1218 |
. . . . . . . 8
                                               
                                         
           |
185 | | simp1r3 1086 |
. . . . . . . . . 10
                                               
                                         
    
       
                  
              
                     |
186 | 165 | simp2bi 1004 |
. . . . . . . . . 10
 
                       
                                    
     
                 |
187 | 185, 186 | syl 16 |
. . . . . . . . 9
                                               
                                         
    
                        |
188 | | simp2 989 |
. . . . . . . . 9
                                               
                                         
    
      |
189 | | simp3 990 |
. . . . . . . . 9
                                               
                                         
    
      |
190 | | rsp 2884 |
. . . . . . . . . . 11
 
     
              
    
                   |
191 | 190 | imp 429 |
. . . . . . . . . 10
                     
                         |
192 | 191 | r19.21bi 2910 |
. . . . . . . . 9
                        
         
            |
193 | 187, 188,
189, 192 | syl21anc 1218 |
. . . . . . . 8
                                               
                                         
    
            |
194 | | simp1r3 1086 |
. . . . . . . . . 10
                                               
                                         
    
       
                  
              
                     |
195 | 165 | simp3bi 1005 |
. . . . . . . . . 10
 
                       
                                    
     
                   |
196 | 194, 195 | syl 16 |
. . . . . . . . 9
                                               
                                         
    
                          |
197 | | simp2 989 |
. . . . . . . . 9
                                               
                                         
    
      |
198 | | simp3 990 |
. . . . . . . . 9
                                               
                                         
    
      |
199 | | rsp 2884 |
. . . . . . . . . . 11
 
     
                
    
                     |
200 | 199 | imp 429 |
. . . . . . . . . 10
                                                   |
201 | 200 | r19.21bi 2910 |
. . . . . . . . 9
                          
         
              |
202 | 196, 197,
198, 201 | syl21anc 1218 |
. . . . . . . 8
                                               
                                         
    
              |
203 | 68, 130, 140, 77, 78, 141, 108, 145, 146, 149, 151, 152, 153, 163, 176, 184, 193, 202 | stoweidlem34 29967 |
. . . . . . 7
 
                                            
                                     

                                              
           
                          |
204 | | nfmpt1 4479 |
. . . . . . . . . 10
                     |
205 | 204 | nfeq2 2629 |
. . . . . . . . 9
                    |
206 | | fveq1 5788 |
. . . . . . . . . . . . 13
                                               |
207 | 206 | breq1d 4400 |
. . . . . . . . . . . 12
                       
     
                               |
208 | 206 | breq2d 4402 |
. . . . . . . . . . . 12
                         
   
                               |
209 | 207, 208 | anbi12d 710 |
. . . . . . . . . . 11
                                                                                                       |
210 | 209 | anbi2d 703 |
. . . . . . . . . 10
                               
                                             
                                 
           
                           |
211 | 210 | rexbidv 2844 |
. . . . . . . . 9
                    
           
                                  
           
                                 
           
                           |
212 | 205, 211 | ralbid 2836 |
. . . . . . . 8
                    

           
                                  

           
                                 
           
                           |
213 | 212 | rspcev 3169 |
. . . . . . 7
                     
           
                                 
           
                         


           
                                    |
214 | 124, 203,
213 | syl2anc 661 |
. . . . . 6
 
                                            
                                     


                            
           
        |
215 | 214 | ex 434 |
. . . . 5
    
                                         
                                      

           
                                     |
216 | 215 | 2eximdv 1679 |
. . . 4
        
                                         
                                         


           
                                     |
217 | 106, 216 | mpd 15 |
. . 3
     


           
                       |