Step | Hyp | Ref
| Expression |
1 | | 1zzd 9226 |
. . . 4
|
2 | | 0zd 9211 |
. . . 4
|
3 | | zsqcl 10533 |
. . . . . 6
|
4 | 3 | ad2antrr 485 |
. . . . 5
|
5 | | zdceq 9274 |
. . . . 5
DECID |
6 | 4, 1, 5 | syl2anc 409 |
. . . 4
DECID |
7 | 1, 2, 6 | ifcldcd 3560 |
. . 3
|
8 | | neg1z 9231 |
. . . . . 6
|
9 | 8 | a1i 9 |
. . . . 5
|
10 | | 1zzd 9226 |
. . . . 5
|
11 | | simpr 109 |
. . . . . . 7
|
12 | | 0zd 9211 |
. . . . . . 7
|
13 | | zdclt 9276 |
. . . . . . 7
DECID |
14 | 11, 12, 13 | syl2an2r 590 |
. . . . . 6
DECID
|
15 | | simpl 108 |
. . . . . . 7
|
16 | | zdclt 9276 |
. . . . . . 7
DECID |
17 | 15, 12, 16 | syl2an2r 590 |
. . . . . 6
DECID
|
18 | | dcan2 929 |
. . . . . 6
DECID
DECID
DECID
|
19 | 14, 17, 18 | sylc 62 |
. . . . 5
DECID
|
20 | 9, 10, 19 | ifcldcd 3560 |
. . . 4
|
21 | | nnuz 9509 |
. . . . . 6
|
22 | | lgsval.1 |
. . . . . . . 8
|
23 | | eleq1w 2231 |
. . . . . . . . 9
|
24 | | eqeq1 2177 |
. . . . . . . . . . 11
|
25 | | oveq1 5857 |
. . . . . . . . . . . . . . . 16
|
26 | 25 | oveq1d 5865 |
. . . . . . . . . . . . . . 15
|
27 | 26 | oveq2d 5866 |
. . . . . . . . . . . . . 14
|
28 | 27 | oveq1d 5865 |
. . . . . . . . . . . . 13
|
29 | | id 19 |
. . . . . . . . . . . . 13
|
30 | 28, 29 | oveq12d 5868 |
. . . . . . . . . . . 12
|
31 | 30 | oveq1d 5865 |
. . . . . . . . . . 11
|
32 | 24, 31 | ifbieq2d 3549 |
. . . . . . . . . 10
|
33 | | oveq1 5857 |
. . . . . . . . . 10
|
34 | 32, 33 | oveq12d 5868 |
. . . . . . . . 9
|
35 | 23, 34 | ifbieq1d 3547 |
. . . . . . . 8
|
36 | | simpr 109 |
. . . . . . . 8
|
37 | | 0zd 9211 |
. . . . . . . . . . . 12
|
38 | | 1zzd 9226 |
. . . . . . . . . . . . 13
|
39 | 38 | znegcld 9323 |
. . . . . . . . . . . . 13
|
40 | | id 19 |
. . . . . . . . . . . . . . . . . . 19
|
41 | | 8nn 9032 |
. . . . . . . . . . . . . . . . . . . 20
|
42 | 41 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
|
43 | 40, 42 | zmodcld 10288 |
. . . . . . . . . . . . . . . . . 18
|
44 | 43 | nn0zd 9319 |
. . . . . . . . . . . . . . . . 17
|
45 | | 1zzd 9226 |
. . . . . . . . . . . . . . . . 17
|
46 | | zdceq 9274 |
. . . . . . . . . . . . . . . . 17
DECID |
47 | 44, 45, 46 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
DECID |
48 | | 7nn 9031 |
. . . . . . . . . . . . . . . . . 18
|
49 | 48 | nnzi 9220 |
. . . . . . . . . . . . . . . . 17
|
50 | | zdceq 9274 |
. . . . . . . . . . . . . . . . 17
DECID |
51 | 44, 49, 50 | sylancl 411 |
. . . . . . . . . . . . . . . 16
DECID |
52 | | dcor 930 |
. . . . . . . . . . . . . . . 16
DECID
DECID
DECID |
53 | 47, 51, 52 | sylc 62 |
. . . . . . . . . . . . . . 15
DECID |
54 | | elprg 3601 |
. . . . . . . . . . . . . . . . 17
|
55 | 43, 54 | syl 14 |
. . . . . . . . . . . . . . . 16
|
56 | 55 | dcbid 833 |
. . . . . . . . . . . . . . 15
DECID DECID |
57 | 53, 56 | mpbird 166 |
. . . . . . . . . . . . . 14
DECID |
58 | 57 | ad5antr 493 |
. . . . . . . . . . . . 13
DECID |
59 | 38, 39, 58 | ifcldcd 3560 |
. . . . . . . . . . . 12
|
60 | | 2nn 9026 |
. . . . . . . . . . . . . 14
|
61 | 60 | a1i 9 |
. . . . . . . . . . . . 13
|
62 | | simp-5l 538 |
. . . . . . . . . . . . 13
|
63 | | dvdsdc 11747 |
. . . . . . . . . . . . 13
DECID |
64 | 61, 62, 63 | syl2anc 409 |
. . . . . . . . . . . 12
DECID |
65 | 37, 59, 64 | ifcldcd 3560 |
. . . . . . . . . . 11
|
66 | | simp-5l 538 |
. . . . . . . . . . . . . . . 16
|
67 | | simpr 109 |
. . . . . . . . . . . . . . . . . 18
|
68 | | prm2orodd 12067 |
. . . . . . . . . . . . . . . . . . . 20
|
69 | 68 | orcomd 724 |
. . . . . . . . . . . . . . . . . . 19
|
70 | 69 | ad2antlr 486 |
. . . . . . . . . . . . . . . . . 18
|
71 | 67, 70 | ecased 1344 |
. . . . . . . . . . . . . . . . 17
|
72 | | prmnn 12051 |
. . . . . . . . . . . . . . . . . . . 20
|
73 | 72 | nnnn0d 9175 |
. . . . . . . . . . . . . . . . . . 19
|
74 | | nn0oddm1d2 11855 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 73, 74 | syl 14 |
. . . . . . . . . . . . . . . . . 18
|
76 | 75 | ad2antlr 486 |
. . . . . . . . . . . . . . . . 17
|
77 | 71, 76 | mpbid 146 |
. . . . . . . . . . . . . . . 16
|
78 | | zexpcl 10478 |
. . . . . . . . . . . . . . . 16
|
79 | 66, 77, 78 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
80 | 79 | peano2zd 9324 |
. . . . . . . . . . . . . 14
|
81 | 36 | ad2antrr 485 |
. . . . . . . . . . . . . 14
|
82 | 80, 81 | zmodcld 10288 |
. . . . . . . . . . . . 13
|
83 | 82 | nn0zd 9319 |
. . . . . . . . . . . 12
|
84 | | 1zzd 9226 |
. . . . . . . . . . . 12
|
85 | 83, 84 | zsubcld 9326 |
. . . . . . . . . . 11
|
86 | | nnz 9218 |
. . . . . . . . . . . . 13
|
87 | 86 | ad2antlr 486 |
. . . . . . . . . . . 12
|
88 | | 2z 9227 |
. . . . . . . . . . . 12
|
89 | | zdceq 9274 |
. . . . . . . . . . . 12
DECID |
90 | 87, 88, 89 | sylancl 411 |
. . . . . . . . . . 11
DECID |
91 | 65, 85, 90 | ifcldadc 3554 |
. . . . . . . . . 10
|
92 | | simpr 109 |
. . . . . . . . . . 11
|
93 | | simp-4r 537 |
. . . . . . . . . . 11
|
94 | | neqne 2348 |
. . . . . . . . . . . 12
|
95 | 94 | ad3antlr 490 |
. . . . . . . . . . 11
|
96 | | pczcl 12239 |
. . . . . . . . . . 11
|
97 | 92, 93, 95, 96 | syl12anc 1231 |
. . . . . . . . . 10
|
98 | | zexpcl 10478 |
. . . . . . . . . 10
|
99 | 91, 97, 98 | syl2anc 409 |
. . . . . . . . 9
|
100 | | 1zzd 9226 |
. . . . . . . . 9
|
101 | | prmdc 12071 |
. . . . . . . . . 10
DECID
|
102 | 101 | adantl 275 |
. . . . . . . . 9
DECID |
103 | 99, 100, 102 | ifcldadc 3554 |
. . . . . . . 8
|
104 | 22, 35, 36, 103 | fvmptd3 5587 |
. . . . . . 7
|
105 | 104, 103 | eqeltrd 2247 |
. . . . . 6
|
106 | | zmulcl 9252 |
. . . . . . 7
|
107 | 106 | adantl 275 |
. . . . . 6
|
108 | 21, 10, 105, 107 | seqf 10404 |
. . . . 5
|
109 | | simplr 525 |
. . . . . 6
|
110 | 94 | adantl 275 |
. . . . . 6
|
111 | | nnabscl 11051 |
. . . . . 6
|
112 | 109, 110,
111 | syl2anc 409 |
. . . . 5
|
113 | 108, 112 | ffvelrnd 5629 |
. . . 4
|
114 | 20, 113 | zmulcld 9327 |
. . 3
|
115 | | 0zd 9211 |
. . . 4
|
116 | | zdceq 9274 |
. . . 4
DECID |
117 | 11, 115, 116 | syl2anc 409 |
. . 3
DECID |
118 | 7, 114, 117 | ifcldadc 3554 |
. 2
|
119 | | simpr 109 |
. . . . 5
|
120 | 119 | eqeq1d 2179 |
. . . 4
|
121 | | simpl 108 |
. . . . . . 7
|
122 | 121 | oveq1d 5865 |
. . . . . 6
|
123 | 122 | eqeq1d 2179 |
. . . . 5
|
124 | 123 | ifbid 3546 |
. . . 4
|
125 | 119 | breq1d 3997 |
. . . . . . 7
|
126 | 121 | breq1d 3997 |
. . . . . . 7
|
127 | 125, 126 | anbi12d 470 |
. . . . . 6
|
128 | 127 | ifbid 3546 |
. . . . 5
|
129 | 121 | breq2d 3999 |
. . . . . . . . . . . . 13
|
130 | 121 | oveq1d 5865 |
. . . . . . . . . . . . . . 15
|
131 | 130 | eleq1d 2239 |
. . . . . . . . . . . . . 14
|
132 | 131 | ifbid 3546 |
. . . . . . . . . . . . 13
|
133 | 129, 132 | ifbieq2d 3549 |
. . . . . . . . . . . 12
|
134 | 121 | oveq1d 5865 |
. . . . . . . . . . . . . . 15
|
135 | 134 | oveq1d 5865 |
. . . . . . . . . . . . . 14
|
136 | 135 | oveq1d 5865 |
. . . . . . . . . . . . 13
|
137 | 136 | oveq1d 5865 |
. . . . . . . . . . . 12
|
138 | 133, 137 | ifeq12d 3544 |
. . . . . . . . . . 11
|
139 | 119 | oveq2d 5866 |
. . . . . . . . . . 11
|
140 | 138, 139 | oveq12d 5868 |
. . . . . . . . . 10
|
141 | 140 | ifeq1d 3542 |
. . . . . . . . 9
|
142 | 141 | mpteq2dv 4078 |
. . . . . . . 8
|
143 | 142, 22 | eqtr4di 2221 |
. . . . . . 7
|
144 | 143 | seqeq3d 10396 |
. . . . . 6
|
145 | 119 | fveq2d 5498 |
. . . . . 6
|
146 | 144, 145 | fveq12d 5501 |
. . . . 5
|
147 | 128, 146 | oveq12d 5868 |
. . . 4
|
148 | 120, 124,
147 | ifbieq12d 3551 |
. . 3
|
149 | | df-lgs 13614 |
. . 3
|
150 | 148, 149 | ovmpoga 5979 |
. 2
|
151 | 118, 150 | mpd3an3 1333 |
1
|