Step | Hyp | Ref
| Expression |
1 | | 2z 9284 |
. . . 4
 |
2 | | divides 11799 |
. . . 4
 
        |
3 | 1, 2 | mpan 424 |
. . 3
 
      |
4 | 3 | notbid 667 |
. 2
 
      |
5 | | elznn0 9271 |
. . . 4

 
     |
6 | | odd2np1lem 11880 |
. . . . . 6

      
     |
7 | 6 | adantl 277 |
. . . . 5
 
             |
8 | | odd2np1lem 11880 |
. . . . . . 7
 
 
            |
9 | | peano2z 9292 |
. . . . . . . . . . . . 13
     |
10 | | znegcl 9287 |
. . . . . . . . . . . . 13
        |
11 | 9, 10 | syl 14 |
. . . . . . . . . . . 12
      |
12 | 11 | ad2antlr 489 |
. . . . . . . . . . 11
               |
13 | | zcn 9261 |
. . . . . . . . . . . . . . . 16
   |
14 | | 2cn 8993 |
. . . . . . . . . . . . . . . . . 18
 |
15 | | mulcl 7941 |
. . . . . . . . . . . . . . . . . 18
 
     |
16 | 14, 15 | mpan 424 |
. . . . . . . . . . . . . . . . 17
     |
17 | | peano2cn 8095 |
. . . . . . . . . . . . . . . . 17
         |
18 | 16, 17 | syl 14 |
. . . . . . . . . . . . . . . 16
       |
19 | 13, 18 | syl 14 |
. . . . . . . . . . . . . . 15
       |
20 | 19 | adantl 277 |
. . . . . . . . . . . . . 14
 
       |
21 | | simpl 109 |
. . . . . . . . . . . . . . 15
 
   |
22 | 21 | recnd 7989 |
. . . . . . . . . . . . . 14
 
   |
23 | | negcon2 8213 |
. . . . . . . . . . . . . 14
     
               |
24 | 20, 22, 23 | syl2anc 411 |
. . . . . . . . . . . . 13
 
               |
25 | | eqcom 2179 |
. . . . . . . . . . . . . 14
     
       |
26 | 14, 13, 15 | sylancr 414 |
. . . . . . . . . . . . . . . . . . . . 21
     |
27 | | ax-1cn 7907 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
28 | 14, 27 | mulcli 7965 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
29 | | addsubass 8170 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                   |
30 | 28, 27, 29 | mp3an23 1329 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
31 | 26, 30 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
                   |
32 | | 2t1e2 9075 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
33 | 32 | oveq1i 5888 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
34 | | 2m1e1 9040 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
35 | 33, 34 | eqtri 2198 |
. . . . . . . . . . . . . . . . . . . . 21
     |
36 | 35 | oveq2i 5889 |
. . . . . . . . . . . . . . . . . . . 20
             |
37 | 31, 36 | eqtr2di 2227 |
. . . . . . . . . . . . . . . . . . 19
               |
38 | | adddi 7946 |
. . . . . . . . . . . . . . . . . . . . . 22
 
             |
39 | 14, 27, 38 | mp3an13 1328 |
. . . . . . . . . . . . . . . . . . . . 21
             |
40 | 13, 39 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
             |
41 | 40 | oveq1d 5893 |
. . . . . . . . . . . . . . . . . . 19
                 |
42 | 37, 41 | eqtr4d 2213 |
. . . . . . . . . . . . . . . . . 18
             |
43 | 42 | negeqd 8155 |
. . . . . . . . . . . . . . . . 17
               |
44 | 9 | zcnd 9379 |
. . . . . . . . . . . . . . . . . . . 20
     |
45 | | mulneg2 8356 |
. . . . . . . . . . . . . . . . . . . 20
  
              |
46 | 14, 44, 45 | sylancr 414 |
. . . . . . . . . . . . . . . . . . 19
             |
47 | 46 | oveq1d 5893 |
. . . . . . . . . . . . . . . . . 18
                 |
48 | | mulcl 7941 |
. . . . . . . . . . . . . . . . . . . 20
  
        |
49 | 14, 44, 48 | sylancr 414 |
. . . . . . . . . . . . . . . . . . 19
       |
50 | | negsubdi 8216 |
. . . . . . . . . . . . . . . . . . 19
     
                 |
51 | 49, 27, 50 | sylancl 413 |
. . . . . . . . . . . . . . . . . 18
                 |
52 | 47, 51 | eqtr4d 2213 |
. . . . . . . . . . . . . . . . 17
                 |
53 | 43, 52 | eqtr4d 2213 |
. . . . . . . . . . . . . . . 16
               |
54 | 53 | adantl 277 |
. . . . . . . . . . . . . . 15
 
               |
55 | 54 | eqeq1d 2186 |
. . . . . . . . . . . . . 14
 
                 |
56 | 25, 55 | bitrid 192 |
. . . . . . . . . . . . 13
 
                 |
57 | 24, 56 | bitrd 188 |
. . . . . . . . . . . 12
 
                 |
58 | 57 | biimpa 296 |
. . . . . . . . . . 11
                   |
59 | | oveq2 5886 |
. . . . . . . . . . . . . 14
             |
60 | 59 | oveq1d 5893 |
. . . . . . . . . . . . 13
                 |
61 | 60 | eqeq1d 2186 |
. . . . . . . . . . . 12
        
          |
62 | 61 | rspcev 2843 |
. . . . . . . . . . 11
                    |
63 | 12, 58, 62 | syl2anc 411 |
. . . . . . . . . 10
                 |
64 | 63 | ex 115 |
. . . . . . . . 9
 
               |
65 | 64 | rexlimdva 2594 |
. . . . . . . 8
  
             |
66 | | znegcl 9287 |
. . . . . . . . . . . 12
    |
67 | 66 | ad2antlr 489 |
. . . . . . . . . . 11
           |
68 | | zcn 9261 |
. . . . . . . . . . . . . . 15
   |
69 | | mulcl 7941 |
. . . . . . . . . . . . . . 15
 
     |
70 | 68, 14, 69 | sylancl 413 |
. . . . . . . . . . . . . 14
     |
71 | | recn 7947 |
. . . . . . . . . . . . . 14
   |
72 | | negcon2 8213 |
. . . . . . . . . . . . . 14
   
           |
73 | 70, 71, 72 | syl2anr 290 |
. . . . . . . . . . . . 13
 
           |
74 | | eqcom 2179 |
. . . . . . . . . . . . . 14
   
     |
75 | | mulneg1 8355 |
. . . . . . . . . . . . . . . . 17
 
         |
76 | 68, 14, 75 | sylancl 413 |
. . . . . . . . . . . . . . . 16
         |
77 | 76 | adantl 277 |
. . . . . . . . . . . . . . 15
 
         |
78 | 77 | eqeq1d 2186 |
. . . . . . . . . . . . . 14
 
           |
79 | 74, 78 | bitr4id 199 |
. . . . . . . . . . . . 13
 
           |
80 | 73, 79 | bitrd 188 |
. . . . . . . . . . . 12
 
           |
81 | 80 | biimpa 296 |
. . . . . . . . . . 11
             |
82 | | oveq1 5885 |
. . . . . . . . . . . . 13
         |
83 | 82 | eqeq1d 2186 |
. . . . . . . . . . . 12
    
      |
84 | 83 | rspcev 2843 |
. . . . . . . . . . 11
      
     |
85 | 67, 81, 84 | syl2anc 411 |
. . . . . . . . . 10
             |
86 | 85 | ex 115 |
. . . . . . . . 9
 
           |
87 | 86 | rexlimdva 2594 |
. . . . . . . 8
  
         |
88 | 65, 87 | orim12d 786 |
. . . . . . 7
        
      
           |
89 | 8, 88 | syl5 32 |
. . . . . 6
                |
90 | 89 | imp 124 |
. . . . 5
                |
91 | 7, 90 | jaodan 797 |
. . . 4
  

   
          |
92 | 5, 91 | sylbi 121 |
. . 3
  
          |
93 | | halfnz 9352 |
. . . 4
   |
94 | | reeanv 2647 |
. . . . 5
  
                    |
95 | | eqtr3 2197 |
. . . . . . 7
                 |
96 | | zcn 9261 |
. . . . . . . . . . 11
   |
97 | | mulcom 7943 |
. . . . . . . . . . 11
 
       |
98 | 96, 14, 97 | sylancl 413 |
. . . . . . . . . 10
       |
99 | 98 | eqeq2d 2189 |
. . . . . . . . 9
       
         |
100 | 99 | adantl 277 |
. . . . . . . 8
 
                 |
101 | | mulcl 7941 |
. . . . . . . . . . 11
 
     |
102 | 14, 96, 101 | sylancr 414 |
. . . . . . . . . 10
     |
103 | | zcn 9261 |
. . . . . . . . . . 11
   |
104 | | mulcl 7941 |
. . . . . . . . . . 11
 
     |
105 | 14, 103, 104 | sylancr 414 |
. . . . . . . . . 10
     |
106 | | subadd 8163 |
. . . . . . . . . . 11
     
                 |
107 | 27, 106 | mp3an3 1326 |
. . . . . . . . . 10
                       |
108 | 102, 105,
107 | syl2anr 290 |
. . . . . . . . 9
 
                 |
109 | | subcl 8159 |
. . . . . . . . . . . . . 14
 
     |
110 | | 2ap0 9015 |
. . . . . . . . . . . . . . . 16
#  |
111 | 14, 110 | pm3.2i 272 |
. . . . . . . . . . . . . . 15
 #   |
112 | | eqcom 2179 |
. . . . . . . . . . . . . . . 16
    
      |
113 | | divmulap 8635 |
. . . . . . . . . . . . . . . 16
     #               |
114 | 112, 113 | bitrid 192 |
. . . . . . . . . . . . . . 15
     #               |
115 | 27, 111, 114 | mp3an13 1328 |
. . . . . . . . . . . . . 14
       
       |
116 | 109, 115 | syl 14 |
. . . . . . . . . . . . 13
 
             |
117 | 116 | ancoms 268 |
. . . . . . . . . . . 12
 
             |
118 | | subdi 8345 |
. . . . . . . . . . . . . . 15
 
             |
119 | 14, 118 | mp3an1 1324 |
. . . . . . . . . . . . . 14
 
             |
120 | 119 | ancoms 268 |
. . . . . . . . . . . . 13
 
             |
121 | 120 | eqeq1d 2186 |
. . . . . . . . . . . 12
 
               |
122 | 117, 121 | bitrd 188 |
. . . . . . . . . . 11
 
               |
123 | 103, 96, 122 | syl2an 289 |
. . . . . . . . . 10
 
               |
124 | | zsubcl 9297 |
. . . . . . . . . . . 12
 
     |
125 | | eleq1 2240 |
. . . . . . . . . . . 12
       
     |
126 | 124, 125 | syl5ibcom 155 |
. . . . . . . . . . 11
 
           |
127 | 126 | ancoms 268 |
. . . . . . . . . 10
 
           |
128 | 123, 127 | sylbird 170 |
. . . . . . . . 9
 
             |
129 | 108, 128 | sylbird 170 |
. . . . . . . 8
 
             |
130 | 100, 129 | sylbid 150 |
. . . . . . 7
 
             |
131 | 95, 130 | syl5 32 |
. . . . . 6
 
               |
132 | 131 | rexlimivv 2600 |
. . . . 5
  
            |
133 | 94, 132 | sylbir 135 |
. . . 4
               |
134 | 93, 133 | mto 662 |
. . 3
 
         |
135 | | df-xor 1376 |
. . . . 5
          
  
                     |
136 | | xorbin 1384 |
. . . . 5
                       |
137 | 135, 136 | sylbir 135 |
. . . 4
             
                     |
138 | 137 | bicomd 141 |
. . 3
             
          
 
        |
139 | 92, 134, 138 | sylancl 413 |
. 2
    
        |
140 | 4, 139 | bitrd 188 |
1
 
        |