Step | Hyp | Ref
| Expression |
1 | | stoweidlem14.1 |
. . . . . 6
     |
2 | | ssrab2 3526 |
. . . . . . 7
     |
3 | 2 | a1i 11 |
. . . . . 6
       |
4 | 1, 3 | syl5eqss 3488 |
. . . . 5

  |
5 | | stoweidlem14.2 |
. . . . . . 7
   |
6 | 5 | rprecred 11381 |
. . . . . 6
     |
7 | | arch 10895 |
. . . . . 6
        |
8 | | breq2 4420 |
. . . . . . . . . . 11
   
     |
9 | 8 | elrab 3208 |
. . . . . . . . . 10
    
      |
10 | 9 | biimpri 211 |
. . . . . . . . 9
   
       |
11 | 10, 1 | syl6eleqr 2551 |
. . . . . . . 8
   
   |
12 | | simpr 467 |
. . . . . . . 8
   
  
  |
13 | 11, 12 | jca 539 |
. . . . . . 7
   
   
   |
14 | 13 | reximi2 2866 |
. . . . . 6
    
    |
15 | | rexn0 3884 |
. . . . . 6
      |
16 | 6, 7, 14, 15 | 4syl 19 |
. . . . 5
   |
17 | | nnwo 11253 |
. . . . 5
 
 

  |
18 | 4, 16, 17 | syl2anc 671 |
. . . 4
  
  |
19 | | df-rex 2755 |
. . . 4
  
   
   |
20 | 18, 19 | sylib 201 |
. . 3
    
   |
21 | 8, 1 | elrab2 3210 |
. . . . . . . 8

      |
22 | 21 | simplbi 466 |
. . . . . . 7
   |
23 | 22 | ad2antrl 739 |
. . . . . 6
 


    |
24 | | simpl 463 |
. . . . . . 7
 


    |
25 | | simprl 769 |
. . . . . . 7
 


    |
26 | | simprr 771 |
. . . . . . . 8
 


  
  |
27 | | nfcv 2603 |
. . . . . . . . 9
   |
28 | | nfrab1 2983 |
. . . . . . . . . 10
       |
29 | 1, 28 | nfcxfr 2601 |
. . . . . . . . 9
   |
30 | | nfv 1772 |
. . . . . . . . 9

 |
31 | | nfv 1772 |
. . . . . . . . 9

 |
32 | | breq2 4420 |
. . . . . . . . 9
 
   |
33 | 27, 29, 30, 31, 32 | cbvralf 3025 |
. . . . . . . 8
 
   |
34 | 26, 33 | sylib 201 |
. . . . . . 7
 


  
  |
35 | 21 | simprbi 470 |
. . . . . . . . 9
     |
36 | 35 | ad2antrl 739 |
. . . . . . . 8
 


      |
37 | 22 | ad2antrl 739 |
. . . . . . . . 9
 


    |
38 | | 1red 9684 |
. . . . . . . . . 10
 

  |
39 | | nnre 10644 |
. . . . . . . . . . 11
   |
40 | 39 | adantl 472 |
. . . . . . . . . 10
 

  |
41 | 5 | rpregt0d 11376 |
. . . . . . . . . . 11
     |
42 | 41 | adantr 471 |
. . . . . . . . . 10
 

    |
43 | | ltdivmul2 10510 |
. . . . . . . . . 10
 

          |
44 | 38, 40, 42, 43 | syl3anc 1276 |
. . . . . . . . 9
 

  
     |
45 | 37, 44 | syldan 477 |
. . . . . . . 8
 


    
     |
46 | 36, 45 | mpbid 215 |
. . . . . . 7
 


      |
47 | 24, 25, 34, 46 | syl12anc 1274 |
. . . . . 6
 


      |
48 | | oveq1 6322 |
. . . . . . . . . . . 12
       |
49 | 48 | adantl 472 |
. . . . . . . . . . 11
 
       |
50 | 5 | rpcnd 11372 |
. . . . . . . . . . . . 13
   |
51 | 50 | adantr 471 |
. . . . . . . . . . . 12
 
   |
52 | 51 | mulid2d 9687 |
. . . . . . . . . . 11
 
     |
53 | 49, 52 | eqtrd 2496 |
. . . . . . . . . 10
 
     |
54 | 53 | oveq1d 6330 |
. . . . . . . . 9
 
         |
55 | 5 | rpred 11370 |
. . . . . . . . . . . 12
   |
56 | 55 | rehalfcld 10888 |
. . . . . . . . . . 11
     |
57 | | halfre 10857 |
. . . . . . . . . . . 12
   |
58 | 57 | a1i 11 |
. . . . . . . . . . 11
     |
59 | | 1red 9684 |
. . . . . . . . . . 11
   |
60 | | stoweidlem14.3 |
. . . . . . . . . . . 12
   |
61 | | 2re 10707 |
. . . . . . . . . . . . . 14
 |
62 | 61 | a1i 11 |
. . . . . . . . . . . . 13
   |
63 | | 2pos 10729 |
. . . . . . . . . . . . . 14
 |
64 | 63 | a1i 11 |
. . . . . . . . . . . . 13
   |
65 | | ltdiv1 10497 |
. . . . . . . . . . . . 13
 
           |
66 | 55, 59, 62, 64, 65 | syl112anc 1280 |
. . . . . . . . . . . 12
         |
67 | 60, 66 | mpbid 215 |
. . . . . . . . . . 11
  
    |
68 | | halflt1 10860 |
. . . . . . . . . . . 12
   |
69 | 68 | a1i 11 |
. . . . . . . . . . 11
  
  |
70 | 56, 58, 59, 67, 69 | lttrd 9822 |
. . . . . . . . . 10
  
  |
71 | 70 | adantr 471 |
. . . . . . . . 9
 
     |
72 | 54, 71 | eqbrtrd 4437 |
. . . . . . . 8
 
       |
73 | 72 | adantlr 726 |
. . . . . . 7
       
      |
74 | | simpll 765 |
. . . . . . . 8
          |
75 | | simplrl 775 |
. . . . . . . . . 10
          |
76 | 75, 22 | syl 17 |
. . . . . . . . 9
          |
77 | | neqne 2643 |
. . . . . . . . . 10
   |
78 | 77 | adantl 472 |
. . . . . . . . 9
          |
79 | | eluz2b3 11261 |
. . . . . . . . 9
         |
80 | 76, 78, 79 | sylanbrc 675 |
. . . . . . . 8
              |
81 | | peano2rem 9967 |
. . . . . . . . . 10
     |
82 | 75, 22, 39, 81 | 4syl 19 |
. . . . . . . . 9
            |
83 | 55 | ad2antrr 737 |
. . . . . . . . . 10
          |
84 | 5 | rpne0d 11375 |
. . . . . . . . . . 11
   |
85 | 84 | ad2antrr 737 |
. . . . . . . . . 10
          |
86 | 83, 85 | rereccld 10462 |
. . . . . . . . 9
            |
87 | | 1zzd 10997 |
. . . . . . . . . . 11
          |
88 | | df-2 10696 |
. . . . . . . . . . . . . . 15
   |
89 | 88 | fveq2i 5891 |
. . . . . . . . . . . . . 14
           |
90 | 89 | eleq2i 2532 |
. . . . . . . . . . . . 13
             |
91 | | eluzsub 11217 |
. . . . . . . . . . . . 13
 
      
        |
92 | 90, 91 | syl3an3b 1314 |
. . . . . . . . . . . 12
 
    
        |
93 | | nnuz 11223 |
. . . . . . . . . . . 12
     |
94 | 92, 93 | syl6eleqr 2551 |
. . . . . . . . . . 11
 
    
    |
95 | 87, 87, 80, 94 | syl3anc 1276 |
. . . . . . . . . 10
            |
96 | 22, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
97 | 96 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . 21
   
   |
98 | 97, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
99 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
   
   |
100 | 99 | ltm1d 10567 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
101 | | ltnle 9739 |
. . . . . . . . . . . . . . . . . . . . 21
   
   
     |
102 | 100, 101 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
103 | 98, 97, 102 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . 19
   
     |
104 | | breq2 4420 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
105 | 104 | notbid 300 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
106 | 105 | rspcev 3162 |
. . . . . . . . . . . . . . . . . . 19
   
   
  |
107 | 103, 106 | syldan 477 |
. . . . . . . . . . . . . . . . . 18
   
 
  |
108 | | rexnal 2848 |
. . . . . . . . . . . . . . . . . 18
 

  |
109 | 107, 108 | sylib 201 |
. . . . . . . . . . . . . . . . 17
   
    |
110 | 109 | ex 440 |
. . . . . . . . . . . . . . . 16
        |
111 | | imnan 428 |
. . . . . . . . . . . . . . . 16
   
     |
112 | 110, 111 | sylib 201 |
. . . . . . . . . . . . . . 15
        |
113 | 112 | con2i 125 |
. . . . . . . . . . . . . 14
        |
114 | 113 | ad2antlr 738 |
. . . . . . . . . . . . 13
            |
115 | | breq2 4420 |
. . . . . . . . . . . . . 14
     
       |
116 | 115, 1 | elrab2 3210 |
. . . . . . . . . . . . 13
  
          |
117 | 114, 116 | sylnib 310 |
. . . . . . . . . . . 12
            
     |
118 | | ianor 495 |
. . . . . . . . . . . 12
     
             |
119 | 117, 118 | sylib 201 |
. . . . . . . . . . 11
            
     |
120 | | imor 418 |
. . . . . . . . . . 11
     
             |
121 | 119, 120 | sylibr 217 |
. . . . . . . . . 10
            
     |
122 | 95, 121 | mpd 15 |
. . . . . . . . 9
         
    |
123 | 82, 86, 122 | nltled 9811 |
. . . . . . . 8
              |
124 | | eluzelre 11198 |
. . . . . . . . . . . . 13
    
  |
125 | 124 | adantl 472 |
. . . . . . . . . . . 12
 
    
  |
126 | 55 | adantr 471 |
. . . . . . . . . . . 12
 
    
  |
127 | 125, 126 | remulcld 9697 |
. . . . . . . . . . 11
 
    
    |
128 | 127 | rehalfcld 10888 |
. . . . . . . . . 10
 
    
      |
129 | 128 | 3adant3 1034 |
. . . . . . . . 9
 
     
         |
130 | 59, 55 | readdcld 9696 |
. . . . . . . . . . . 12
     |
131 | 130 | adantr 471 |
. . . . . . . . . . 11
 
    
    |
132 | 131 | rehalfcld 10888 |
. . . . . . . . . 10
 
    
      |
133 | 132 | 3adant3 1034 |
. . . . . . . . 9
 
     
         |
134 | | 1red 9684 |
. . . . . . . . 9
 
     
     |
135 | | eluzelcn 11199 |
. . . . . . . . . . . . . . 15
    
  |
136 | 135 | adantl 472 |
. . . . . . . . . . . . . 14
 
    
  |
137 | 50 | adantr 471 |
. . . . . . . . . . . . . 14
 
    
  |
138 | 136, 137 | mulcld 9689 |
. . . . . . . . . . . . 13
 
    
    |
139 | 138 | 3adant3 1034 |
. . . . . . . . . . . 12
 
     
       |
140 | 50 | 3ad2ant1 1035 |
. . . . . . . . . . . 12
 
     
     |
141 | 139, 140 | npcand 10016 |
. . . . . . . . . . 11
 
     
             |
142 | 127, 126 | resubcld 10075 |
. . . . . . . . . . . . 13
 
    
      |
143 | 142 | 3adant3 1034 |
. . . . . . . . . . . 12
 
     
         |
144 | 55 | 3ad2ant1 1035 |
. . . . . . . . . . . 12
 
     
     |
145 | | simp3 1016 |
. . . . . . . . . . . . . 14
 
     
         |
146 | | 1red 9684 |
. . . . . . . . . . . . . . . . 17
    
  |
147 | 124, 146 | resubcld 10075 |
. . . . . . . . . . . . . . . 16
    
    |
148 | 147 | 3ad2ant2 1036 |
. . . . . . . . . . . . . . 15
 
     
       |
149 | 6 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . 15
 
     
       |
150 | 41 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . 15
 
     
       |
151 | | lemul1 10485 |
. . . . . . . . . . . . . . 15
      
 
    
           |
152 | 148, 149,
150, 151 | syl3anc 1276 |
. . . . . . . . . . . . . 14
 
     
                   |
153 | 145, 152 | mpbid 215 |
. . . . . . . . . . . . 13
 
     
             |
154 | | 1cnd 9685 |
. . . . . . . . . . . . . . . 16
 
    
  |
155 | 136, 154,
137 | subdird 10103 |
. . . . . . . . . . . . . . 15
 
    
            |
156 | 137 | mulid2d 9687 |
. . . . . . . . . . . . . . . 16
 
    
    |
157 | 156 | oveq2d 6331 |
. . . . . . . . . . . . . . 15
 
    
            |
158 | 155, 157 | eqtrd 2496 |
. . . . . . . . . . . . . 14
 
    
          |
159 | 158 | 3adant3 1034 |
. . . . . . . . . . . . 13
 
     
             |
160 | | 1cnd 9685 |
. . . . . . . . . . . . . . . 16
   |
161 | 160, 50, 84 | 3jca 1194 |
. . . . . . . . . . . . . . 15
     |
162 | 161 | 3ad2ant1 1035 |
. . . . . . . . . . . . . 14
 
     
       |
163 | | divcan1 10307 |
. . . . . . . . . . . . . 14
 
       |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . 13
 
     
         |
165 | 153, 159,
164 | 3brtr3d 4446 |
. . . . . . . . . . . 12
 
     
         |
166 | 143, 134,
144, 165 | leadd1dd 10255 |
. . . . . . . . . . 11
 
     
             |
167 | 141, 166 | eqbrtrrd 4439 |
. . . . . . . . . 10
 
     
         |
168 | 127 | 3adant3 1034 |
. . . . . . . . . . 11
 
     
       |
169 | 130 | 3ad2ant1 1035 |
. . . . . . . . . . 11
 
     
       |
170 | 61, 63 | pm3.2i 461 |
. . . . . . . . . . . 12
   |
171 | 170 | a1i 11 |
. . . . . . . . . . 11
 
     
       |
172 | | lediv1 10498 |
. . . . . . . . . . 11
        
    
           |
173 | 168, 169,
171, 172 | syl3anc 1276 |
. . . . . . . . . 10
 
     
                   |
174 | 167, 173 | mpbid 215 |
. . . . . . . . 9
 
     
             |
175 | 55, 59, 59, 60 | ltadd2dd 9820 |
. . . . . . . . . . . . 13
  
    |
176 | | 1p1e2 10751 |
. . . . . . . . . . . . 13
   |
177 | 175, 176 | syl6breq 4456 |
. . . . . . . . . . . 12
  
  |
178 | | ltdiv1 10497 |
. . . . . . . . . . . . 13
   
               |
179 | 130, 62, 62, 64, 178 | syl112anc 1280 |
. . . . . . . . . . . 12
             |
180 | 177, 179 | mpbid 215 |
. . . . . . . . . . 11
    
    |
181 | | 2div2e1 10761 |
. . . . . . . . . . 11
   |
182 | 180, 181 | syl6breq 4456 |
. . . . . . . . . 10
    
  |
183 | 182 | 3ad2ant1 1035 |
. . . . . . . . 9
 
     
         |
184 | 129, 133,
134, 174, 183 | lelttrd 9819 |
. . . . . . . 8
 
     
         |
185 | 74, 80, 123, 184 | syl3anc 1276 |
. . . . . . 7
              |
186 | 73, 185 | pm2.61dan 805 |
. . . . . 6
 


        |
187 | 23, 47, 186 | jca32 542 |
. . . . 5
 


              |
188 | 187 | ex 440 |
. . . 4
   

             |
189 | 188 | eximdv 1775 |
. . 3
                      |
190 | 20, 189 | mpd 15 |
. 2
    
          |
191 | | df-rex 2755 |
. 2
  
      
              |
192 | 190, 191 | sylibr 217 |
1
            |