Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.r |
. . . . 5
                      |
2 | 1 | elrnmpt 4905 |
. . . 4
                   
      |
3 | 2 | elv 2764 |
. . 3

                       |
4 | | iftrue 3562 |
. . . . . . . . . 10
                        |
5 | 4 | eqeq2d 2205 |
. . . . . . . . 9
                          |
6 | 5 | adantr 276 |
. . . . . . . 8
                                  |
7 | | elfz1b 10146 |
. . . . . . . . . . . . 13
    
    |
8 | | id 19 |
. . . . . . . . . . . . . . . . . 18
   |
9 | | 2nn 9133 |
. . . . . . . . . . . . . . . . . . 19
 |
10 | 9 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
   |
11 | 8, 10 | nnmulcld 9021 |
. . . . . . . . . . . . . . . . 17
     |
12 | 11 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . 16
 
     |
13 | 12 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . 15
             |
14 | | gausslemma2d.h |
. . . . . . . . . . . . . . . . . . 19
     |
15 | 14 | eleq1i 2259 |
. . . . . . . . . . . . . . . . . 18

 
    |
16 | 15 | biimpi 120 |
. . . . . . . . . . . . . . . . 17
       |
17 | 16 | 3ad2ant2 1021 |
. . . . . . . . . . . . . . . 16
 
       |
18 | 17 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . 15
               |
19 | | gausslemma2d.p |
. . . . . . . . . . . . . . . . . . 19
       |
20 | | nnoddn2prm 12388 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
21 | | nnz 9326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
22 | 21 | anim1i 340 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
23 | 20, 22 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
24 | | nnz 9326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
25 | | 2z 9335 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
26 | 25 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
27 | 24, 26 | zmulcld 9435 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
28 | 27 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     |
29 | 23, 28 | anim12i 338 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
30 | | df-3an 982 |
. . . . . . . . . . . . . . . . . . . . 21
 

          |
31 | 29, 30 | sylibr 134 |
. . . . . . . . . . . . . . . . . . . 20
               |
32 | 31 | ex 115 |
. . . . . . . . . . . . . . . . . . 19
        
      |
33 | 19, 32 | syl 14 |
. . . . . . . . . . . . . . . . . 18
    
      |
34 | 33 | impcom 125 |
. . . . . . . . . . . . . . . . 17
    

     |
35 | | ltoddhalfle 12024 |
. . . . . . . . . . . . . . . . 17
 

                |
36 | 34, 35 | syl 14 |
. . . . . . . . . . . . . . . 16
    
    
         |
37 | 36 | biimp3a 1356 |
. . . . . . . . . . . . . . 15
                 |
38 | 13, 18, 37 | 3jca 1179 |
. . . . . . . . . . . . . 14
                         |
39 | 38 | 3exp 1204 |
. . . . . . . . . . . . 13
 
      
                  |
40 | 7, 39 | sylbi 121 |
. . . . . . . . . . . 12
          
                  |
41 | 40 | impcom 125 |
. . . . . . . . . . 11
 
                 

 
      |
42 | 41 | impcom 125 |
. . . . . . . . . 10
                    

 
     |
43 | 14 | oveq2i 5921 |
. . . . . . . . . . . 12
             |
44 | 43 | eleq2i 2260 |
. . . . . . . . . . 11
      
            |
45 | | elfz1b 10146 |
. . . . . . . . . . 11
          
                |
46 | 44, 45 | bitri 184 |
. . . . . . . . . 10
      
                |
47 | 42, 46 | sylibr 134 |
. . . . . . . . 9
                     |
48 | | eleq1 2256 |
. . . . . . . . 9
       
         |
49 | 47, 48 | syl5ibrcom 157 |
. . . . . . . 8
                       |
50 | 6, 49 | sylbid 150 |
. . . . . . 7
                                    |
51 | 50 | ancoms 268 |
. . . . . 6
                                    |
52 | | iffalse 3565 |
. . . . . . . . . 10
                     
    |
53 | 52 | eqeq2d 2205 |
. . . . . . . . 9
                            |
54 | 53 | adantr 276 |
. . . . . . . 8
                                    |
55 | | eldifi 3281 |
. . . . . . . . . . . . . 14
    
  |
56 | | prmz 12239 |
. . . . . . . . . . . . . 14

  |
57 | 19, 55, 56 | 3syl 17 |
. . . . . . . . . . . . 13
   |
58 | 57 | ad2antrl 490 |
. . . . . . . . . . . 12
            
  |
59 | | elfzelz 10081 |
. . . . . . . . . . . . . 14
       |
60 | 25 | a1i 9 |
. . . . . . . . . . . . . 14
       |
61 | 59, 60 | zmulcld 9435 |
. . . . . . . . . . . . 13
         |
62 | 61 | ad2antll 491 |
. . . . . . . . . . . 12
                 |
63 | 58, 62 | zsubcld 9434 |
. . . . . . . . . . 11
                   |
64 | 56 | zred 9429 |
. . . . . . . . . . . . . 14

  |
65 | 14 | breq2i 4037 |
. . . . . . . . . . . . . . . . . . . 20

      |
66 | | nnre 8979 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
67 | 66 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
68 | | peano2rem 8276 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
69 | 68 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
70 | | 2re 9042 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
71 | | 2pos 9063 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
72 | 70, 71 | pm3.2i 272 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
73 | 72 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
74 | | lemuldiv 8890 |
. . . . . . . . . . . . . . . . . . . . 21
  
   
    
       |
75 | 67, 69, 73, 74 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . 20
 
    

 
     |
76 | 65, 75 | bitr4id 199 |
. . . . . . . . . . . . . . . . . . 19
 
         |
77 | 11 | nnred 8985 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
78 | 77 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
79 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
80 | 78, 69, 79 | lesub2d 8562 |
. . . . . . . . . . . . . . . . . . . 20
 
    
  
 
       |
81 | | recn 7995 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
82 | | 1cnd 8025 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
83 | 81, 82 | nncand 8325 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
84 | 83 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
    |
85 | 84 | breq1d 4039 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
  
  
       |
86 | 85 | biimpd 144 |
. . . . . . . . . . . . . . . . . . . 20
 
   
  
  
       |
87 | 80, 86 | sylbid 150 |
. . . . . . . . . . . . . . . . . . 19
 
    
 
      |
88 | 76, 87 | sylbid 150 |
. . . . . . . . . . . . . . . . . 18
 
 
       |
89 | 88 | impancom 260 |
. . . . . . . . . . . . . . . . 17
   
       |
90 | 89 | 3adant2 1018 |
. . . . . . . . . . . . . . . 16
 
 
 
     |
91 | 7, 90 | sylbi 121 |
. . . . . . . . . . . . . . 15
     
 
     |
92 | 91 | com12 30 |
. . . . . . . . . . . . . 14
     
       |
93 | 19, 55, 64, 92 | 4syl 18 |
. . . . . . . . . . . . 13
      
      |
94 | 93 | imp 124 |
. . . . . . . . . . . 12
 
           |
95 | 94 | adantl 277 |
. . . . . . . . . . 11
            
      |
96 | | elnnz1 9330 |
. . . . . . . . . . 11
    
 
          |
97 | 63, 95, 96 | sylanbrc 417 |
. . . . . . . . . 10
                   |
98 | 7 | simp2bi 1015 |
. . . . . . . . . . 11
       |
99 | 98 | ad2antll 491 |
. . . . . . . . . 10
            
  |
100 | | nnre 8979 |
. . . . . . . . . . . . . . . . . 18
   |
101 | 100 | rehalfcld 9219 |
. . . . . . . . . . . . . . . . 17
     |
102 | 101 | adantr 276 |
. . . . . . . . . . . . . . . 16
 
     |
103 | 61 | zred 9429 |
. . . . . . . . . . . . . . . 16
         |
104 | | lenlt 8085 |
. . . . . . . . . . . . . . . 16
    
      
       |
105 | 102, 103,
104 | syl2an 289 |
. . . . . . . . . . . . . . 15
   
       
 
       |
106 | 22, 61 | anim12i 338 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
       
     |
107 | 106, 30 | sylibr 134 |
. . . . . . . . . . . . . . . . . . . . . 22
   
     
     |
108 | | halfleoddlt 12025 |
. . . . . . . . . . . . . . . . . . . . . 22
 

              |
109 | 107, 108 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
   
       
 
       |
110 | 109 | biimpa 296 |
. . . . . . . . . . . . . . . . . . . 20
                     |
111 | | nncn 8980 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
112 | | subhalfhalf 9207 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       |
113 | 111, 112 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
114 | 113 | breq1d 4039 |
. . . . . . . . . . . . . . . . . . . . 21
       
       |
115 | 114 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . . . 20
                     
       |
116 | 110, 115 | mpbird 167 |
. . . . . . . . . . . . . . . . . . 19
               
       |
117 | 100 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
   
       |
118 | 101 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
   
         |
119 | 103 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
   
         |
120 | 117, 118,
119 | 3jca 1179 |
. . . . . . . . . . . . . . . . . . . . 21
   
     
       |
121 | 120 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
               
       |
122 | | ltsub23 8451 |
. . . . . . . . . . . . . . . . . . . 20
  
 
          
       |
123 | 121, 122 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
                     
         |
124 | 116, 123 | mpbid 147 |
. . . . . . . . . . . . . . . . . 18
               
       |
125 | 21 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . 21
   
       |
126 | | simplr 528 |
. . . . . . . . . . . . . . . . . . . . 21
   
       |
127 | 61 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
   
         |
128 | 125, 127 | zsubcld 9434 |
. . . . . . . . . . . . . . . . . . . . 21
   
     
     |
129 | 125, 126,
128 | 3jca 1179 |
. . . . . . . . . . . . . . . . . . . 20
   
     

      |
130 | 129 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
               

      |
131 | | ltoddhalfle 12024 |
. . . . . . . . . . . . . . . . . . 19
 

            
         |
132 | 130, 131 | syl 14 |
. . . . . . . . . . . . . . . . . 18
                     
           |
133 | 124, 132 | mpbid 147 |
. . . . . . . . . . . . . . . . 17
               
         |
134 | 133 | ex 115 |
. . . . . . . . . . . . . . . 16
   
       
  
          |
135 | 14 | breq2i 4037 |
. . . . . . . . . . . . . . . 16
    
          |
136 | 134, 135 | imbitrrdi 162 |
. . . . . . . . . . . . . . 15
   
       
  
      |
137 | 105, 136 | sylbird 170 |
. . . . . . . . . . . . . 14
   
             
   |
138 | 137 | ex 115 |
. . . . . . . . . . . . 13
 
     
 

     
    |
139 | 19, 20, 138 | 3syl 17 |
. . . . . . . . . . . 12
           
       |
140 | 139 | imp 124 |
. . . . . . . . . . 11
 
             
   |
141 | 140 | impcom 125 |
. . . . . . . . . 10
                
  |
142 | | elfz1b 10146 |
. . . . . . . . . 10
        
 
          |
143 | 97, 99, 141, 142 | syl3anbrc 1183 |
. . . . . . . . 9
                       |
144 | | eleq1 2256 |
. . . . . . . . 9
  
      
           |
145 | 143, 144 | syl5ibrcom 157 |
. . . . . . . 8
                         |
146 | 54, 145 | sylbid 150 |
. . . . . . 7
                                    |
147 | 146 | ancoms 268 |
. . . . . 6
        

                          |
148 | 61 | adantl 277 |
. . . . . . . . 9
 
         |
149 | | zq 9681 |
. . . . . . . . 9
       |
150 | 148, 149 | syl 14 |
. . . . . . . 8
 
         |
151 | 57 | adantr 276 |
. . . . . . . . 9
 
       |
152 | | znq 9679 |
. . . . . . . . 9
 
     |
153 | 151, 9, 152 | sylancl 413 |
. . . . . . . 8
 
         |
154 | | qdclt 10305 |
. . . . . . . 8
    
  DECID       |
155 | 150, 153,
154 | syl2anc 411 |
. . . . . . 7
 
    
DECID       |
156 | | exmiddc 837 |
. . . . . . 7
DECID    
     

     |
157 | 155, 156 | syl 14 |
. . . . . 6
 
                 |
158 | 51, 147, 157 | mpjaodan 799 |
. . . . 5
 
                            |
159 | 158 | rexlimdva 2611 |
. . . 4
                              |
160 | | elfz1b 10146 |
. . . . . . . . . . . 12
    
    |
161 | | simp1 999 |
. . . . . . . . . . . . . . 15
 
   |
162 | | simpl 109 |
. . . . . . . . . . . . . . 15
  
  |
163 | | nnehalf 12035 |
. . . . . . . . . . . . . . 15
       |
164 | 161, 162,
163 | syl2anr 290 |
. . . . . . . . . . . . . 14
    
      |
165 | | simpr2 1006 |
. . . . . . . . . . . . . 14
    
 
  |
166 | | nnre 8979 |
. . . . . . . . . . . . . . . . . . . 20
   |
167 | 166 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
         |
168 | | nnrp 9719 |
. . . . . . . . . . . . . . . . . . . . 21
   |
169 | 168 | adantl 277 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
170 | 169 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
         |
171 | | 2rp 9714 |
. . . . . . . . . . . . . . . . . . . . 21
 |
172 | | 1le2 9180 |
. . . . . . . . . . . . . . . . . . . . 21
 |
173 | 171, 172 | pm3.2i 272 |
. . . . . . . . . . . . . . . . . . . 20

  |
174 | 173 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
           |
175 | | ledivge1le 9782 |
. . . . . . . . . . . . . . . . . . 19
 
     
   |
176 | 167, 170,
174, 175 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . 18
             |
177 | 176 | ex 115 |
. . . . . . . . . . . . . . . . 17
 
      
    |
178 | 177 | com23 78 |
. . . . . . . . . . . . . . . 16
 
      
    |
179 | 178 | 3impia 1202 |
. . . . . . . . . . . . . . 15
 
         |
180 | 179 | impcom 125 |
. . . . . . . . . . . . . 14
    
   
  |
181 | 164, 165,
180 | 3jca 1179 |
. . . . . . . . . . . . 13
    
      
   |
182 | 181 | ex 115 |
. . . . . . . . . . . 12
  
 
   
      |
183 | 160, 182 | biimtrid 152 |
. . . . . . . . . . 11
  
    
         |
184 | 183 | 3impia 1202 |
. . . . . . . . . 10
      
        |
185 | | elfz1b 10146 |
. . . . . . . . . 10
      
        |
186 | 184, 185 | sylibr 134 |
. . . . . . . . 9
      
        |
187 | | oveq1 5917 |
. . . . . . . . . . . . 13
           |
188 | 187 | breq1d 4039 |
. . . . . . . . . . . 12
       
         |
189 | 187 | oveq2d 5926 |
. . . . . . . . . . . 12
   
           |
190 | 188, 187,
189 | ifbieq12d 3583 |
. . . . . . . . . . 11
                                         |
191 | 190 | eqeq2d 2205 |
. . . . . . . . . 10
                                           |
192 | 191 | adantl 277 |
. . . . . . . . 9
                                                   |
193 | | elfzelz 10081 |
. . . . . . . . . . . . . . 15
       |
194 | 193 | zcnd 9430 |
. . . . . . . . . . . . . 14
       |
195 | 194 | 3ad2ant3 1022 |
. . . . . . . . . . . . 13
      
  |
196 | | 2cnd 9045 |
. . . . . . . . . . . . 13
      
  |
197 | | 2ap0 9065 |
. . . . . . . . . . . . . 14
#  |
198 | 197 | a1i 9 |
. . . . . . . . . . . . 13
      
#   |
199 | 195, 196,
198 | divcanap1d 8800 |
. . . . . . . . . . . 12
      
      |
200 | 14 | breq2i 4037 |
. . . . . . . . . . . . . . . . . 18

      |
201 | | nnz 9326 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
202 | 19, 20, 22 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
203 | 202 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
    |
204 | 201, 203 | anim12ci 339 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
205 | | df-3an 982 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   
   |
206 | 204, 205 | sylibr 134 |
. . . . . . . . . . . . . . . . . . . . 21
     
   |
207 | | ltoddhalfle 12024 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
       |
208 | 206, 207 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
       
       |
209 | 208 | exbiri 382 |
. . . . . . . . . . . . . . . . . . 19
    
 
 
      |
210 | 209 | com23 78 |
. . . . . . . . . . . . . . . . . 18
 
 
    
      |
211 | 200, 210 | biimtrid 152 |
. . . . . . . . . . . . . . . . 17
 
         |
212 | 211 | a1d 22 |
. . . . . . . . . . . . . . . 16
 

          |
213 | 212 | 3imp 1195 |
. . . . . . . . . . . . . . 15
 
         |
214 | 160, 213 | sylbi 121 |
. . . . . . . . . . . . . 14
             |
215 | 214 | com12 30 |
. . . . . . . . . . . . 13
  
    
     |
216 | 215 | 3impia 1202 |
. . . . . . . . . . . 12
      
    |
217 | 199, 216 | eqbrtrd 4051 |
. . . . . . . . . . 11
      
        |
218 | 217 | iftrued 3564 |
. . . . . . . . . 10
      
                           |
219 | 218, 199 | eqtr2d 2227 |
. . . . . . . . 9
      
                       |
220 | 186, 192,
219 | rspcedvd 2870 |
. . . . . . . 8
      
                       |
221 | 220 | 3expb 1206 |
. . . . . . 7
         
                
     |
222 | 221 | ancoms 268 |
. . . . . 6
                                |
223 | 55, 56 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
    
  |
224 | 223 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
   
         |
225 | 201 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . . . . 19
 
   |
226 | 225 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
   
         |
227 | 224, 226 | zsubcld 9434 |
. . . . . . . . . . . . . . . . 17
   
           |
228 | 166 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
  |
229 | 68 | rehalfcld 9219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       |
230 | 229 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
 
    |
231 | | simpl 109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
  |
232 | 228, 230,
231 | 3jca 1179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
        |
233 | 232 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             |
234 | 55, 64, 233 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            
    |
235 | 234 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
236 | 235 | impcom 125 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
             |
237 | | lesub2 8466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
           
     |
238 | 236, 237 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
                
    |
239 | 56 | zcnd 9430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  |
240 | | id 19 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
241 | | 1cnd 8025 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
242 | | 2cnd 9045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
243 | 197 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 #   |
244 | 240, 241,
242, 243 | divsubdirapd 8839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             |
245 | 244 | oveq2d 5926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
 
             |
246 | | halfcl 9198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
247 | | halfcn 9186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
248 | 247 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
249 | 240, 246,
248 | subsubd 8348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
         
       |
250 | 112 | oveq1d 5925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 |
251 | 245, 249,
250 | 3eqtrd 2230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
 
           |
252 | 55, 239, 251 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
253 | 252 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
                   |
254 | 253 | breq1d 4039 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
                    
    |
255 | | prmnn 12238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  |
256 | | halfre 9185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
257 | 256 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
258 | | nngt0 8997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
259 | 72 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
260 | | divgt0 8881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
    |
261 | 100, 258,
259, 260 | syl21anc 1248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
262 | | halfgt0 9187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
263 | 262 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
264 | 101, 257,
261, 263 | addgt0d 8530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
265 | 55, 255, 264 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
        |
266 | 265 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
             |
267 | | 0red 8010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   |
268 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
   |
269 | 268 | rehalfcld 9219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
     |
270 | 256 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
     |
271 | 269, 270 | readdcld 8039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
         |
272 | | resubcl 8273 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
     |
273 | 272 | ancoms 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
     |
274 | 267, 271,
273 | 3jca 1179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
        
    |
275 | 274 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
       
     |
276 | 166, 275 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
       
     |
277 | 276 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
         
     |
278 | 277 | com12 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                 |
279 | 55, 64, 278 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
               
     |
280 | 279 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                       |
281 | 280 | impcom 125 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
                 |
282 | | ltletr 8099 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
                  
     |
283 | 281, 282 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
                     
     |
284 | 266, 283 | mpand 429 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
             
     |
285 | 254, 284 | sylbid 150 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
             
     |
286 | 238, 285 | sylbid 150 |
. . . . . . . . . . . . . . . . . . . . . 22
     
         
     |
287 | 286 | ex 115 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
         
     |
288 | 287 | com23 78 |
. . . . . . . . . . . . . . . . . . . 20
 
           
 
     |
289 | 200, 288 | biimtrid 152 |
. . . . . . . . . . . . . . . . . . 19
 
    
   
      |
290 | 289 | 3impia 1202 |
. . . . . . . . . . . . . . . . . 18
 
   
   
     |
291 | 290 | impcom 125 |
. . . . . . . . . . . . . . . . 17
   
       
   |
292 | | elnnz 9317 |
. . . . . . . . . . . . . . . . 17
  
 
      |
293 | 227, 291,
292 | sylanbrc 417 |
. . . . . . . . . . . . . . . 16
   
           |
294 | 23 | adantr 276 |
. . . . . . . . . . . . . . . . 17
       
   |
295 | | simpr 110 |
. . . . . . . . . . . . . . . . . 18
         |
296 | 295, 225 | anim12ci 339 |
. . . . . . . . . . . . . . . . 17
   
           |
297 | | omoe 12027 |
. . . . . . . . . . . . . . . . 17
   
  
    |
298 | 294, 296,
297 | syl2an2r 595 |
. . . . . . . . . . . . . . . 16
   
       
   |
299 | | nnehalf 12035 |
. . . . . . . . . . . . . . . 16
             |
300 | 293, 298,
299 | syl2anc 411 |
. . . . . . . . . . . . . . 15
   
             |
301 | | simpr2 1006 |
. . . . . . . . . . . . . . 15
   
         |
302 | | 1red 8024 |
. . . . . . . . . . . . . . . . . 18
   
         |
303 | 166 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . . . . 19
 
   |
304 | 303 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
   
         |
305 | 55, 64 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
    
  |
306 | 305 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
   
         |
307 | | nnge1 8995 |
. . . . . . . . . . . . . . . . . . . 20
   |
308 | 307 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . . . . 19
 
   |
309 | 308 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
   
         |
310 | 302, 304,
306, 309 | lesub2dd 8571 |
. . . . . . . . . . . . . . . . 17
   
         
   |
311 | 306, 304 | resubcld 8390 |
. . . . . . . . . . . . . . . . . 18
   
           |
312 | 55, 64, 68 | 3syl 17 |
. . . . . . . . . . . . . . . . . . 19
         |
313 | 312 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
   
           |
314 | 72 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
   
           |
315 | | lediv1 8878 |
. . . . . . . . . . . . . . . . . 18
    
   
 
              |
316 | 311, 313,
314, 315 | syl3anc 1249 |
. . . . . . . . . . . . . . . . 17
   
                       |
317 | 310, 316 | mpbid 147 |
. . . . . . . . . . . . . . . 16
   
                 |
318 | 14 | breq2i 4037 |
. . . . . . . . . . . . . . . 16
    
 
        |
319 | 317, 318 | sylibr 134 |
. . . . . . . . . . . . . . 15
   
             |
320 | 300, 301,
319 | 3jca 1179 |
. . . . . . . . . . . . . 14
   
                   |
321 | 320 | ex 115 |
. . . . . . . . . . . . 13
                  
    |
322 | | elfz1b 10146 |
. . . . . . . . . . . . 13
        
            |
323 | 321, 160,
322 | 3imtr4g 205 |
. . . . . . . . . . . 12
                       |
324 | 323 | ex 115 |
. . . . . . . . . . 11
          
 
          |
325 | 19, 324 | syl 14 |
. . . . . . . . . 10
      
 
          |
326 | 325 | 3imp21 1200 |
. . . . . . . . 9
                 |
327 | | oveq1 5917 |
. . . . . . . . . . . . 13
               |
328 | 327 | breq1d 4039 |
. . . . . . . . . . . 12
         
           |
329 | 327 | oveq2d 5926 |
. . . . . . . . . . . 12
     
             |
330 | 328, 327,
329 | ifbieq12d 3583 |
. . . . . . . . . . 11
                                                 |
331 | 330 | eqeq2d 2205 |
. . . . . . . . . 10
                                                   |
332 | 331 | adantl 277 |
. . . . . . . . 9
  
                                                        |
333 | 19, 55, 239 | 3syl 17 |
. . . . . . . . . . . . . . 15
   |
334 | 333 | 3ad2ant2 1021 |
. . . . . . . . . . . . . 14
         |
335 | 194 | 3ad2ant3 1022 |
. . . . . . . . . . . . . 14
         |
336 | 334, 335 | subcld 8320 |
. . . . . . . . . . . . 13
       
   |
337 | | 2cnd 9045 |
. . . . . . . . . . . . 13
         |
338 | 197 | a1i 9 |
. . . . . . . . . . . . 13
       #   |
339 | 336, 337,
338 | divcanap1d 8800 |
. . . . . . . . . . . 12
                 |
340 | | zre 9311 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
341 | | halfge0 9188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
342 | | rehalfcl 9199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     |
343 | 342 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
     |
344 | 343, 270 | subge02d 8546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
         
     |
345 | 341, 344 | mpbii 148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
      
    |
346 | | simpl 109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
347 | 256 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     |
348 | 342, 347 | resubcld 8390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         |
349 | 348 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
         |
350 | | letr 8092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        
                  
     |
351 | 346, 349,
343, 350 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
                       |
352 | 345, 351 | mpan2d 428 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
             |
353 | 81 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
354 | 353, 244 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
             |
355 | 354 | breq2d 4041 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
     
         |
356 | | lesub 8450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
   
 
       |
357 | 343, 268,
346, 356 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
    
  
     |
358 | 269, 273 | lenltd 8127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
    
  
     |
359 | | 2cnd 9045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
360 | 197 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 #   |
361 | 81, 359, 360 | divcanap1d 8800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
362 | 361 | eqcomd 2199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
363 | 362 | oveq1d 5925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
        
    |
364 | 342 | recnd 8038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
365 | 364, 359 | mulcomd 8031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
366 | 365 | oveq1d 5925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
              
    |
367 | 359, 364 | mulsubfacd 8427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                 |
368 | | 2m1e1 9090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
369 | 368 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
370 | 369 | oveq1d 5925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
371 | 364 | mullidd 8027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         |
372 | 367, 370,
371 | 3eqtrd 2230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             |
373 | 363, 366,
372 | 3eqtrd 2230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
       |
374 | 373 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
         |
375 | 374 | breq2d 4041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  
  
     |
376 | 357, 358,
375 | 3bitr3d 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
           |
377 | 352, 355,
376 | 3imtr4d 203 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
     
       |
378 | 377 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

 
   
      |
379 | 166, 378 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

 
   
      |
380 | 379 | com3l 81 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
           |
381 | 340, 380 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
 
 
           |
382 | 19, 55, 56, 381 | 4syl 18 |
. . . . . . . . . . . . . . . . . . . 20
      

       |
383 | 382 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
   
 
           |
384 | 383 | com13 80 |
. . . . . . . . . . . . . . . . . 18
 
 
   
         |
385 | 200, 384 | biimtrid 152 |
. . . . . . . . . . . . . . . . 17
 
    
      |
386 | 385 | a1d 22 |
. . . . . . . . . . . . . . . 16
 

    
       |
387 | 386 | 3imp 1195 |
. . . . . . . . . . . . . . 15
 
     
     |
388 | 387 | com12 30 |
. . . . . . . . . . . . . 14
       
     |
389 | 160, 388 | biimtrid 152 |
. . . . . . . . . . . . 13
         
     |
390 | 389 | 3impia 1202 |
. . . . . . . . . . . 12
       

    |
391 | 339, 390 | eqnbrtrd 4047 |
. . . . . . . . . . 11
                 |
392 | 391 | iffalsed 3567 |
. . . . . . . . . 10
                                            |
393 | 339 | oveq2d 5926 |
. . . . . . . . . 10
       
        
    |
394 | 333, 194 | anim12i 338 |
. . . . . . . . . . . 12
 
     
   |
395 | 394 | 3adant1 1017 |
. . . . . . . . . . 11
       
   |
396 | | nncan 8238 |
. . . . . . . . . . 11
 
  
    |
397 | 395, 396 | syl 14 |
. . . . . . . . . 10
       
     |
398 | 392, 393,
397 | 3eqtrrd 2231 |
. . . . . . . . 9
                                    |
399 | 326, 332,
398 | rspcedvd 2870 |
. . . . . . . 8
                              |
400 | 399 | 3expb 1206 |
. . . . . . 7
         
                
     |
401 | 400 | ancoms 268 |
. . . . . 6
         
                
     |
402 | 9 | a1i 9 |
. . . . . . . 8
 
       |
403 | 193 | adantl 277 |
. . . . . . . 8
 
       |
404 | | dvdsdc 11931 |
. . . . . . . 8
 
 DECID   |
405 | 402, 403,
404 | syl2anc 411 |
. . . . . . 7
 
    
DECID
  |
406 | | exmiddc 837 |
. . . . . . 7
DECID 
   |
407 | 405, 406 | syl 14 |
. . . . . 6
 
     
   |
408 | 222, 401,
407 | mpjaodan 799 |
. . . . 5
 
                            |
409 | 408 | ex 115 |
. . . 4
                              |
410 | 159, 409 | impbid 129 |
. . 3
                              |
411 | 3, 410 | bitrid 192 |
. 2
         |
412 | 411 | eqrdv 2191 |
1
       |