Step | Hyp | Ref
| Expression |
1 | | 2z 9252 |
. . . 4
|
2 | | divides 11762 |
. . . 4
|
3 | 1, 2 | mpan 424 |
. . 3
|
4 | 3 | notbid 667 |
. 2
|
5 | | elznn0 9239 |
. . . 4
|
6 | | odd2np1lem 11842 |
. . . . . 6
|
7 | 6 | adantl 277 |
. . . . 5
|
8 | | odd2np1lem 11842 |
. . . . . . 7
|
9 | | peano2z 9260 |
. . . . . . . . . . . . 13
|
10 | | znegcl 9255 |
. . . . . . . . . . . . 13
|
11 | 9, 10 | syl 14 |
. . . . . . . . . . . 12
|
12 | 11 | ad2antlr 489 |
. . . . . . . . . . 11
|
13 | | zcn 9229 |
. . . . . . . . . . . . . . . 16
|
14 | | 2cn 8961 |
. . . . . . . . . . . . . . . . . 18
|
15 | | mulcl 7913 |
. . . . . . . . . . . . . . . . . 18
|
16 | 14, 15 | mpan 424 |
. . . . . . . . . . . . . . . . 17
|
17 | | peano2cn 8066 |
. . . . . . . . . . . . . . . . 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 7960 |
. . . . . . . . . . . . . 14
|
23 | | negcon2 8184 |
. . . . . . . . . . . . . 14
|
24 | 20, 22, 23 | syl2anc 411 |
. . . . . . . . . . . . 13
|
25 | | eqcom 2177 |
. . . . . . . . . . . . . 14
|
26 | 14, 13, 15 | sylancr 414 |
. . . . . . . . . . . . . . . . . . . . 21
|
27 | | ax-1cn 7879 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
28 | 14, 27 | mulcli 7937 |
. . . . . . . . . . . . . . . . . . . . . 22
|
29 | | addsubass 8141 |
. . . . . . . . . . . . . . . . . . . . . 22
|
30 | 28, 27, 29 | mp3an23 1329 |
. . . . . . . . . . . . . . . . . . . . 21
|
31 | 26, 30 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
|
32 | | 2t1e2 9043 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
33 | 32 | oveq1i 5875 |
. . . . . . . . . . . . . . . . . . . . . 22
|
34 | | 2m1e1 9008 |
. . . . . . . . . . . . . . . . . . . . . 22
|
35 | 33, 34 | eqtri 2196 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | 35 | oveq2i 5876 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | 31, 36 | eqtr2di 2225 |
. . . . . . . . . . . . . . . . . . 19
|
38 | | adddi 7918 |
. . . . . . . . . . . . . . . . . . . . . 22
|
39 | 14, 27, 38 | mp3an13 1328 |
. . . . . . . . . . . . . . . . . . . . 21
|
40 | 13, 39 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | 40 | oveq1d 5880 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 37, 41 | eqtr4d 2211 |
. . . . . . . . . . . . . . . . . 18
|
43 | 42 | negeqd 8126 |
. . . . . . . . . . . . . . . . 17
|
44 | 9 | zcnd 9347 |
. . . . . . . . . . . . . . . . . . . 20
|
45 | | mulneg2 8327 |
. . . . . . . . . . . . . . . . . . . 20
|
46 | 14, 44, 45 | sylancr 414 |
. . . . . . . . . . . . . . . . . . 19
|
47 | 46 | oveq1d 5880 |
. . . . . . . . . . . . . . . . . 18
|
48 | | mulcl 7913 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 14, 44, 48 | sylancr 414 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | negsubdi 8187 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 49, 27, 50 | sylancl 413 |
. . . . . . . . . . . . . . . . . 18
|
52 | 47, 51 | eqtr4d 2211 |
. . . . . . . . . . . . . . . . 17
|
53 | 43, 52 | eqtr4d 2211 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | adantl 277 |
. . . . . . . . . . . . . . 15
|
55 | 54 | eqeq1d 2184 |
. . . . . . . . . . . . . 14
|
56 | 25, 55 | bitrid 192 |
. . . . . . . . . . . . 13
|
57 | 24, 56 | bitrd 188 |
. . . . . . . . . . . 12
|
58 | 57 | biimpa 296 |
. . . . . . . . . . 11
|
59 | | oveq2 5873 |
. . . . . . . . . . . . . 14
|
60 | 59 | oveq1d 5880 |
. . . . . . . . . . . . 13
|
61 | 60 | eqeq1d 2184 |
. . . . . . . . . . . 12
|
62 | 61 | rspcev 2839 |
. . . . . . . . . . 11
|
63 | 12, 58, 62 | syl2anc 411 |
. . . . . . . . . 10
|
64 | 63 | ex 115 |
. . . . . . . . 9
|
65 | 64 | rexlimdva 2592 |
. . . . . . . 8
|
66 | | znegcl 9255 |
. . . . . . . . . . . 12
|
67 | 66 | ad2antlr 489 |
. . . . . . . . . . 11
|
68 | | zcn 9229 |
. . . . . . . . . . . . . . 15
|
69 | | mulcl 7913 |
. . . . . . . . . . . . . . 15
|
70 | 68, 14, 69 | sylancl 413 |
. . . . . . . . . . . . . 14
|
71 | | recn 7919 |
. . . . . . . . . . . . . 14
|
72 | | negcon2 8184 |
. . . . . . . . . . . . . 14
|
73 | 70, 71, 72 | syl2anr 290 |
. . . . . . . . . . . . 13
|
74 | | eqcom 2177 |
. . . . . . . . . . . . . 14
|
75 | | mulneg1 8326 |
. . . . . . . . . . . . . . . . 17
|
76 | 68, 14, 75 | sylancl 413 |
. . . . . . . . . . . . . . . 16
|
77 | 76 | adantl 277 |
. . . . . . . . . . . . . . 15
|
78 | 77 | eqeq1d 2184 |
. . . . . . . . . . . . . 14
|
79 | 74, 78 | bitr4id 199 |
. . . . . . . . . . . . 13
|
80 | 73, 79 | bitrd 188 |
. . . . . . . . . . . 12
|
81 | 80 | biimpa 296 |
. . . . . . . . . . 11
|
82 | | oveq1 5872 |
. . . . . . . . . . . . 13
|
83 | 82 | eqeq1d 2184 |
. . . . . . . . . . . 12
|
84 | 83 | rspcev 2839 |
. . . . . . . . . . 11
|
85 | 67, 81, 84 | syl2anc 411 |
. . . . . . . . . 10
|
86 | 85 | ex 115 |
. . . . . . . . 9
|
87 | 86 | rexlimdva 2592 |
. . . . . . . 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 9320 |
. . . 4
|
94 | | reeanv 2644 |
. . . . 5
|
95 | | eqtr3 2195 |
. . . . . . 7
|
96 | | zcn 9229 |
. . . . . . . . . . 11
|
97 | | mulcom 7915 |
. . . . . . . . . . 11
|
98 | 96, 14, 97 | sylancl 413 |
. . . . . . . . . 10
|
99 | 98 | eqeq2d 2187 |
. . . . . . . . 9
|
100 | 99 | adantl 277 |
. . . . . . . 8
|
101 | | mulcl 7913 |
. . . . . . . . . . 11
|
102 | 14, 96, 101 | sylancr 414 |
. . . . . . . . . 10
|
103 | | zcn 9229 |
. . . . . . . . . . 11
|
104 | | mulcl 7913 |
. . . . . . . . . . 11
|
105 | 14, 103, 104 | sylancr 414 |
. . . . . . . . . 10
|
106 | | subadd 8134 |
. . . . . . . . . . 11
|
107 | 27, 106 | mp3an3 1326 |
. . . . . . . . . 10
|
108 | 102, 105,
107 | syl2anr 290 |
. . . . . . . . 9
|
109 | | subcl 8130 |
. . . . . . . . . . . . . 14
|
110 | | 2ap0 8983 |
. . . . . . . . . . . . . . . 16
# |
111 | 14, 110 | pm3.2i 272 |
. . . . . . . . . . . . . . 15
# |
112 | | eqcom 2177 |
. . . . . . . . . . . . . . . 16
|
113 | | divmulap 8604 |
. . . . . . . . . . . . . . . 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 8316 |
. . . . . . . . . . . . . . 15
|
119 | 14, 118 | mp3an1 1324 |
. . . . . . . . . . . . . 14
|
120 | 119 | ancoms 268 |
. . . . . . . . . . . . 13
|
121 | 120 | eqeq1d 2184 |
. . . . . . . . . . . 12
|
122 | 117, 121 | bitrd 188 |
. . . . . . . . . . 11
|
123 | 103, 96, 122 | syl2an 289 |
. . . . . . . . . 10
|
124 | | zsubcl 9265 |
. . . . . . . . . . . 12
|
125 | | eleq1 2238 |
. . . . . . . . . . . 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 2598 |
. . . . 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
|