Step | Hyp | Ref
| Expression |
1 | | nfcv 2592 |
. . 3
     |
2 | | stoweidlem52.3 |
. . 3
   |
3 | | stoweidlem52.2 |
. . 3
   |
4 | | stoweidlem52.4 |
. . 3
     |
5 | | stoweidlem52.7 |
. . 3
  |
6 | | stoweidlem52.5 |
. . 3
         |
7 | | stoweidlem52.13 |
. . . . . 6
   |
8 | 7 | rpred 11341 |
. . . . 5
   |
9 | 8 | rehalfcld 10859 |
. . . 4
     |
10 | 9 | rexrd 9690 |
. . 3
     |
11 | | stoweidlem52.9 |
. . . . 5

  |
12 | | stoweidlem52.8 |
. . . . 5
   |
13 | 11, 12 | syl6sseq 3478 |
. . . 4

    |
14 | | stoweidlem52.17 |
. . . 4
   |
15 | 13, 14 | sseldd 3433 |
. . 3
     |
16 | 1, 2, 3, 4, 5, 6, 10, 15 | rfcnpre2 37352 |
. 2
   |
17 | | stoweidlem52.15 |
. . . . . . . 8
   |
18 | | elssuni 4227 |
. . . . . . . 8
    |
19 | 17, 18 | syl 17 |
. . . . . . 7

   |
20 | 19, 5 | syl6sseqr 3479 |
. . . . . 6

  |
21 | | stoweidlem52.16 |
. . . . . 6
   |
22 | 20, 21 | sseldd 3433 |
. . . . 5
   |
23 | | stoweidlem52.19 |
. . . . . 6
       |
24 | | 2re 10679 |
. . . . . . . 8
 |
25 | 24 | a1i 11 |
. . . . . . 7
   |
26 | 7 | rpgt0d 11344 |
. . . . . . 7
   |
27 | | 2pos 10701 |
. . . . . . . 8
 |
28 | 27 | a1i 11 |
. . . . . . 7
   |
29 | 8, 25, 26, 28 | divgt0d 10542 |
. . . . . 6
     |
30 | 23, 29 | eqbrtrd 4423 |
. . . . 5
    
    |
31 | | nfcv 2592 |
. . . . . 6
   |
32 | | nfcv 2592 |
. . . . . 6
   |
33 | 2, 31 | nffv 5872 |
. . . . . . 7
       |
34 | | nfcv 2592 |
. . . . . . 7
  |
35 | 33, 34, 1 | nfbr 4447 |
. . . . . 6
     
   |
36 | | fveq2 5865 |
. . . . . . 7
           |
37 | 36 | breq1d 4412 |
. . . . . 6
     
 
         |
38 | 31, 32, 35, 37 | elrabf 3194 |
. . . . 5
        

         |
39 | 22, 30, 38 | sylanbrc 670 |
. . . 4
           |
40 | 39, 6 | syl6eleqr 2540 |
. . 3
   |
41 | | nfrab1 2971 |
. . . . 5
           |
42 | 6, 41 | nfcxfr 2590 |
. . . 4
   |
43 | | stoweidlem52.1 |
. . . 4
   |
44 | 11, 14 | sseldd 3433 |
. . . . . . . . . . 11
   |
45 | 4, 5, 12, 44 | fcnre 37346 |
. . . . . . . . . 10
       |
46 | 45 | adantr 467 |
. . . . . . . . 9
 
       |
47 | 6 | rabeq2i 3042 |
. . . . . . . . . . . 12


         |
48 | 47 | biimpi 198 |
. . . . . . . . . . 11
           |
49 | 48 | adantl 468 |
. . . . . . . . . 10
 
           |
50 | 49 | simpld 461 |
. . . . . . . . 9
 
   |
51 | 46, 50 | ffvelrnd 6023 |
. . . . . . . 8
 
       |
52 | 9 | adantr 467 |
. . . . . . . 8
 
     |
53 | 8 | adantr 467 |
. . . . . . . 8
 
   |
54 | 49 | simprd 465 |
. . . . . . . 8
 
         |
55 | | halfpos 10843 |
. . . . . . . . . . 11
 
     |
56 | 8, 55 | syl 17 |
. . . . . . . . . 10
       |
57 | 26, 56 | mpbid 214 |
. . . . . . . . 9
  
  |
58 | 57 | adantr 467 |
. . . . . . . 8
 
     |
59 | 51, 52, 53, 54, 58 | lttrd 9796 |
. . . . . . 7
 
       |
60 | 59 | adantr 467 |
. . . . . 6
   
    
  |
61 | 8 | ad2antrr 732 |
. . . . . . 7
   
   |
62 | 51 | adantr 467 |
. . . . . . 7
   
       |
63 | | stoweidlem52.20 |
. . . . . . . . 9
    
      |
64 | 63 | ad2antrr 732 |
. . . . . . . 8
   
    
      |
65 | 50 | anim1i 572 |
. . . . . . . . 9
   
     |
66 | | eldif 3414 |
. . . . . . . . 9
  

   |
67 | 65, 66 | sylibr 216 |
. . . . . . . 8
   
     |
68 | | rsp 2754 |
. . . . . . . 8
 
      
  
       |
69 | 64, 67, 68 | sylc 62 |
. . . . . . 7
   

      |
70 | 61, 62, 69 | lensymd 9786 |
. . . . . 6
   
       |
71 | 60, 70 | condan 803 |
. . . . 5
 
   |
72 | 71 | ex 436 |
. . . 4
     |
73 | 3, 42, 43, 72 | ssrd 3437 |
. . 3

  |
74 | | nfv 1761 |
. . . . . . . . 9
  |
75 | 3, 74 | nfan 2011 |
. . . . . . . 8
     |
76 | | nfv 1761 |
. . . . . . . 8
  |
77 | 75, 76 | nfan 2011 |
. . . . . . 7
   

  |
78 | | nfra1 2769 |
. . . . . . . 8
           
  |
79 | | nfra1 2769 |
. . . . . . . 8
    
     |
80 | | nfra1 2769 |
. . . . . . . 8
         
 |
81 | 78, 79, 80 | nf3an 2013 |
. . . . . . 7
        
    

     
          |
82 | 77, 81 | nfan 2011 |
. . . . . 6
     

 

         
      
          |
83 | | eqid 2451 |
. . . . . 6
                 |
84 | | eqid 2451 |
. . . . . 6
     |
85 | | ssrab2 3514 |
. . . . . . 7
         |
86 | 6, 85 | eqsstri 3462 |
. . . . . 6
 |
87 | | simplr 762 |
. . . . . 6
   

       
    

     
            |
88 | | simplll 768 |
. . . . . . 7
   

       
    

     
            |
89 | 11 | sselda 3432 |
. . . . . . . 8
 
   |
90 | 4, 5, 12, 89 | fcnre 37346 |
. . . . . . 7
 
       |
91 | 88, 87, 90 | syl2anc 667 |
. . . . . 6
   

       
    

     
                |
92 | 11 | sselda 3432 |
. . . . . . . 8
 
   |
93 | 4, 5, 12, 92 | fcnre 37346 |
. . . . . . 7
 
       |
94 | 88, 93 | sylan 474 |
. . . . . 6
     

 

         
      
        
       |
95 | | stoweidlem52.10 |
. . . . . . 7
 


             |
96 | 88, 95 | syl3an1 1301 |
. . . . . 6
     

 

         
      
        
               |
97 | | stoweidlem52.11 |
. . . . . . 7
 


             |
98 | 88, 97 | syl3an1 1301 |
. . . . . 6
     

 

         
      
        
               |
99 | | stoweidlem52.12 |
. . . . . . 7
 

    |
100 | 88, 99 | sylan 474 |
. . . . . 6
     

 

         
      
        
     |
101 | | simpllr 769 |
. . . . . 6
   

       
    

     
            |
102 | | simpr1 1014 |
. . . . . 6
   

       
    

     
          
            |
103 | | simpr2 1015 |
. . . . . 6
   

       
    

     
          
        |
104 | | simpr3 1016 |
. . . . . 6
   

       
    

     
                    |
105 | 82, 83, 84, 86, 87, 91, 94, 96, 98, 100, 101, 102, 103, 104 | stoweidlem41 37902 |
. . . . 5
   

       
    

     
          
 

         
                 |
106 | 7 | adantr 467 |
. . . . . 6
 

  |
107 | | stoweidlem52.14 |
. . . . . . 7
   |
108 | 107 | adantr 467 |
. . . . . 6
 

  |
109 | 14 | adantr 467 |
. . . . . 6
 

  |
110 | 45 | adantr 467 |
. . . . . 6
 

      |
111 | | stoweidlem52.18 |
. . . . . . 7
          
   |
112 | 111 | adantr 467 |
. . . . . 6
 


            |
113 | 63 | adantr 467 |
. . . . . 6
 

          |
114 | 93 | adantlr 721 |
. . . . . 6
           |
115 | 95 | 3adant1r 1261 |
. . . . . 6
   
               |
116 | 97 | 3adant1r 1261 |
. . . . . 6
   
               |
117 | 99 | adantlr 721 |
. . . . . 6
         |
118 | | simpr 463 |
. . . . . 6
 

  |
119 | 2, 75, 6, 106, 108, 109, 110, 112, 113, 114, 115, 116, 117, 118 | stoweidlem49 37910 |
. . . . 5
 


 

         
      
          |
120 | 105, 119 | r19.29a 2932 |
. . . 4
 


 

         
                 |
121 | 120 | ralrimiva 2802 |
. . 3
             
           
       |
122 | 40, 73, 121 | jca31 537 |
. 2
    

 

         
                  |
123 | | eleq2 2518 |
. . . . 5
 
   |
124 | | sseq1 3453 |
. . . . 5
 
   |
125 | 123, 124 | anbi12d 717 |
. . . 4
         |
126 | | nfcv 2592 |
. . . . . . . 8
   |
127 | 126, 42 | raleqf 2983 |
. . . . . . 7
  
   

       |
128 | 127 | 3anbi2d 1344 |
. . . . . 6
        
    

         
    
 

         
                  |
129 | 128 | rexbidv 2901 |
. . . . 5
  
          
           
    

 

         
                  |
130 | 129 | ralbidv 2827 |
. . . 4
  

 

         
                           
           
        |
131 | 125, 130 | anbi12d 717 |
. . 3
     

 

         
               
 
  
 

         
                   |
132 | 131 | rspcev 3150 |
. 2
     

 

         
                 
   

 

         
                  |
133 | 16, 122, 132 | syl2anc 667 |
1
     

 

         
                  |