Step | Hyp | Ref
| Expression |
1 | | 2z 11409 |
. . . 4
|
2 | | divides 14985 |
. . . 4
|
3 | 1, 2 | mpan 706 |
. . 3
|
4 | 3 | notbid 308 |
. 2
|
5 | | elznn0 11392 |
. . . 4
|
6 | | odd2np1lem 15064 |
. . . . . 6
|
7 | 6 | adantl 482 |
. . . . 5
|
8 | | odd2np1lem 15064 |
. . . . . . 7
|
9 | | peano2z 11418 |
. . . . . . . . . . . . 13
|
10 | | znegcl 11412 |
. . . . . . . . . . . . 13
|
11 | 9, 10 | syl 17 |
. . . . . . . . . . . 12
|
12 | 11 | ad2antlr 763 |
. . . . . . . . . . 11
|
13 | | zcn 11382 |
. . . . . . . . . . . . . . . 16
|
14 | | 2cn 11091 |
. . . . . . . . . . . . . . . . . 18
|
15 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . 18
|
16 | 14, 15 | mpan 706 |
. . . . . . . . . . . . . . . . 17
|
17 | | peano2cn 10208 |
. . . . . . . . . . . . . . . . 17
|
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
|
19 | 13, 18 | syl 17 |
. . . . . . . . . . . . . . 15
|
20 | 19 | adantl 482 |
. . . . . . . . . . . . . 14
|
21 | | simpl 473 |
. . . . . . . . . . . . . . 15
|
22 | 21 | recnd 10068 |
. . . . . . . . . . . . . 14
|
23 | | negcon2 10334 |
. . . . . . . . . . . . . 14
|
24 | 20, 22, 23 | syl2anc 693 |
. . . . . . . . . . . . 13
|
25 | | eqcom 2629 |
. . . . . . . . . . . . . 14
|
26 | 14, 13, 15 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . 21
|
27 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
28 | 14, 27 | mulcli 10045 |
. . . . . . . . . . . . . . . . . . . . . 22
|
29 | | addsubass 10291 |
. . . . . . . . . . . . . . . . . . . . . 22
|
30 | 28, 27, 29 | mp3an23 1416 |
. . . . . . . . . . . . . . . . . . . . 21
|
31 | 26, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
32 | | 2t1e2 11176 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
33 | 32 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . 22
|
34 | | 2m1e1 11135 |
. . . . . . . . . . . . . . . . . . . . . 22
|
35 | 33, 34 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | 35 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | 31, 36 | syl6req 2673 |
. . . . . . . . . . . . . . . . . . 19
|
38 | | adddi 10025 |
. . . . . . . . . . . . . . . . . . . . . 22
|
39 | 14, 27, 38 | mp3an13 1415 |
. . . . . . . . . . . . . . . . . . . . 21
|
40 | 13, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | 40 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 37, 41 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . 18
|
43 | 42 | negeqd 10275 |
. . . . . . . . . . . . . . . . 17
|
44 | 9 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
|
45 | | mulneg2 10467 |
. . . . . . . . . . . . . . . . . . . 20
|
46 | 14, 44, 45 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
|
47 | 46 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
48 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 14, 44, 48 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | negsubdi 10337 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 49, 27, 50 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
|
52 | 47, 51 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . 17
|
53 | 43, 52 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | adantl 482 |
. . . . . . . . . . . . . . 15
|
55 | 54 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
56 | 25, 55 | syl5bb 272 |
. . . . . . . . . . . . 13
|
57 | 24, 56 | bitrd 268 |
. . . . . . . . . . . 12
|
58 | 57 | biimpa 501 |
. . . . . . . . . . 11
|
59 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
60 | 59 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
61 | 60 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
62 | 61 | rspcev 3309 |
. . . . . . . . . . 11
|
63 | 12, 58, 62 | syl2anc 693 |
. . . . . . . . . 10
|
64 | 63 | ex 450 |
. . . . . . . . 9
|
65 | 64 | rexlimdva 3031 |
. . . . . . . 8
|
66 | | znegcl 11412 |
. . . . . . . . . . . 12
|
67 | 66 | ad2antlr 763 |
. . . . . . . . . . 11
|
68 | | zcn 11382 |
. . . . . . . . . . . . . . 15
|
69 | | mulcl 10020 |
. . . . . . . . . . . . . . 15
|
70 | 68, 14, 69 | sylancl 694 |
. . . . . . . . . . . . . 14
|
71 | | recn 10026 |
. . . . . . . . . . . . . 14
|
72 | | negcon2 10334 |
. . . . . . . . . . . . . 14
|
73 | 70, 71, 72 | syl2anr 495 |
. . . . . . . . . . . . 13
|
74 | | mulneg1 10466 |
. . . . . . . . . . . . . . . . 17
|
75 | 68, 14, 74 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
76 | 75 | adantl 482 |
. . . . . . . . . . . . . . 15
|
77 | 76 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
78 | | eqcom 2629 |
. . . . . . . . . . . . . 14
|
79 | 77, 78 | syl6rbbr 279 |
. . . . . . . . . . . . 13
|
80 | 73, 79 | bitrd 268 |
. . . . . . . . . . . 12
|
81 | 80 | biimpa 501 |
. . . . . . . . . . 11
|
82 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
83 | 82 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
84 | 83 | rspcev 3309 |
. . . . . . . . . . 11
|
85 | 67, 81, 84 | syl2anc 693 |
. . . . . . . . . 10
|
86 | 85 | ex 450 |
. . . . . . . . 9
|
87 | 86 | rexlimdva 3031 |
. . . . . . . 8
|
88 | 65, 87 | orim12d 883 |
. . . . . . 7
|
89 | 8, 88 | syl5 34 |
. . . . . 6
|
90 | 89 | imp 445 |
. . . . 5
|
91 | 7, 90 | jaodan 826 |
. . . 4
|
92 | 5, 91 | sylbi 207 |
. . 3
|
93 | | halfnz 11455 |
. . . 4
|
94 | | reeanv 3107 |
. . . . 5
|
95 | | eqtr3 2643 |
. . . . . . 7
|
96 | | zcn 11382 |
. . . . . . . . . . 11
|
97 | | mulcom 10022 |
. . . . . . . . . . 11
|
98 | 96, 14, 97 | sylancl 694 |
. . . . . . . . . 10
|
99 | 98 | eqeq2d 2632 |
. . . . . . . . 9
|
100 | 99 | adantl 482 |
. . . . . . . 8
|
101 | | mulcl 10020 |
. . . . . . . . . . 11
|
102 | 14, 96, 101 | sylancr 695 |
. . . . . . . . . 10
|
103 | | zcn 11382 |
. . . . . . . . . . 11
|
104 | | mulcl 10020 |
. . . . . . . . . . 11
|
105 | 14, 103, 104 | sylancr 695 |
. . . . . . . . . 10
|
106 | | subadd 10284 |
. . . . . . . . . . 11
|
107 | 27, 106 | mp3an3 1413 |
. . . . . . . . . 10
|
108 | 102, 105,
107 | syl2anr 495 |
. . . . . . . . 9
|
109 | | subcl 10280 |
. . . . . . . . . . . . . 14
|
110 | | 2cnne0 11242 |
. . . . . . . . . . . . . . 15
|
111 | | eqcom 2629 |
. . . . . . . . . . . . . . . 16
|
112 | | divmul 10688 |
. . . . . . . . . . . . . . . 16
|
113 | 111, 112 | syl5bb 272 |
. . . . . . . . . . . . . . 15
|
114 | 27, 110, 113 | mp3an13 1415 |
. . . . . . . . . . . . . 14
|
115 | 109, 114 | syl 17 |
. . . . . . . . . . . . 13
|
116 | 115 | ancoms 469 |
. . . . . . . . . . . 12
|
117 | | subdi 10463 |
. . . . . . . . . . . . . . 15
|
118 | 14, 117 | mp3an1 1411 |
. . . . . . . . . . . . . 14
|
119 | 118 | ancoms 469 |
. . . . . . . . . . . . 13
|
120 | 119 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
121 | 116, 120 | bitrd 268 |
. . . . . . . . . . 11
|
122 | 103, 96, 121 | syl2an 494 |
. . . . . . . . . 10
|
123 | | zsubcl 11419 |
. . . . . . . . . . . 12
|
124 | | eleq1 2689 |
. . . . . . . . . . . 12
|
125 | 123, 124 | syl5ibcom 235 |
. . . . . . . . . . 11
|
126 | 125 | ancoms 469 |
. . . . . . . . . 10
|
127 | 122, 126 | sylbird 250 |
. . . . . . . . 9
|
128 | 108, 127 | sylbird 250 |
. . . . . . . 8
|
129 | 100, 128 | sylbid 230 |
. . . . . . 7
|
130 | 95, 129 | syl5 34 |
. . . . . 6
|
131 | 130 | rexlimivv 3036 |
. . . . 5
|
132 | 94, 131 | sylbir 225 |
. . . 4
|
133 | 93, 132 | mto 188 |
. . 3
|
134 | | pm5.17 932 |
. . . 4
|
135 | | bicom 212 |
. . . 4
|
136 | 134, 135 | bitri 264 |
. . 3
|
137 | 92, 133, 136 | sylanblc 696 |
. 2
|
138 | 4, 137 | bitrd 268 |
1
|