Step | Hyp | Ref
| Expression |
1 | | elfzoelz 10103 |
. . . . . . . 8
..^
|
2 | 1 | 3ad2ant1 1013 |
. . . . . . 7
..^ ..^ |
3 | | zq 9585 |
. . . . . . 7
|
4 | 2, 3 | syl 14 |
. . . . . 6
..^ ..^ |
5 | | simp3 994 |
. . . . . . 7
..^ ..^ |
6 | | zq 9585 |
. . . . . . 7
|
7 | 5, 6 | syl 14 |
. . . . . 6
..^ ..^ |
8 | | elfzo0 10138 |
. . . . . . . . . 10
..^
|
9 | 8 | biimpi 119 |
. . . . . . . . 9
..^
|
10 | 9 | 3ad2ant1 1013 |
. . . . . . . 8
..^ ..^
|
11 | 10 | simp2d 1005 |
. . . . . . 7
..^ ..^ |
12 | | nnq 9592 |
. . . . . . 7
|
13 | 11, 12 | syl 14 |
. . . . . 6
..^ ..^ |
14 | 11 | nngt0d 8922 |
. . . . . 6
..^ ..^ |
15 | | modqaddmod 10319 |
. . . . . 6
|
16 | 4, 7, 13, 14, 15 | syl22anc 1234 |
. . . . 5
..^ ..^
|
17 | 16 | eqcomd 2176 |
. . . 4
..^ ..^ |
18 | | elfzoelz 10103 |
. . . . . . . 8
..^
|
19 | 18 | 3ad2ant2 1014 |
. . . . . . 7
..^ ..^ |
20 | | zq 9585 |
. . . . . . 7
|
21 | 19, 20 | syl 14 |
. . . . . 6
..^ ..^ |
22 | | modqaddmod 10319 |
. . . . . 6
|
23 | 21, 7, 13, 14, 22 | syl22anc 1234 |
. . . . 5
..^ ..^
|
24 | 23 | eqcomd 2176 |
. . . 4
..^ ..^ |
25 | 17, 24 | eqeq12d 2185 |
. . 3
..^ ..^ |
26 | 2, 11 | zmodcld 10301 |
. . . . . . . . 9
..^ ..^ |
27 | 26 | nn0zd 9332 |
. . . . . . . 8
..^ ..^ |
28 | 27, 5 | zaddcld 9338 |
. . . . . . 7
..^ ..^ |
29 | 28, 11 | zmodcld 10301 |
. . . . . 6
..^ ..^ |
30 | 29 | nn0cnd 9190 |
. . . . 5
..^ ..^ |
31 | 19, 11 | zmodcld 10301 |
. . . . . . . . 9
..^ ..^ |
32 | 31 | nn0zd 9332 |
. . . . . . . 8
..^ ..^ |
33 | 32, 5 | zaddcld 9338 |
. . . . . . 7
..^ ..^ |
34 | 33, 11 | zmodcld 10301 |
. . . . . 6
..^ ..^ |
35 | 34 | nn0cnd 9190 |
. . . . 5
..^ ..^ |
36 | 30, 35 | subeq0ad 8240 |
. . . 4
..^ ..^ |
37 | | oveq1 5860 |
. . . . 5
|
38 | 4, 13, 14 | modqcld 10284 |
. . . . . . . . . 10
..^ ..^ |
39 | | qaddcl 9594 |
. . . . . . . . . 10
|
40 | 38, 7, 39 | syl2anc 409 |
. . . . . . . . 9
..^ ..^ |
41 | 21, 13, 14 | modqcld 10284 |
. . . . . . . . . 10
..^ ..^ |
42 | | qaddcl 9594 |
. . . . . . . . . 10
|
43 | 41, 7, 42 | syl2anc 409 |
. . . . . . . . 9
..^ ..^ |
44 | | modqsubmodmod 10339 |
. . . . . . . . 9
|
45 | 40, 43, 13, 14, 44 | syl22anc 1234 |
. . . . . . . 8
..^ ..^ |
46 | 26 | nn0cnd 9190 |
. . . . . . . . . 10
..^ ..^ |
47 | 31 | nn0cnd 9190 |
. . . . . . . . . 10
..^ ..^ |
48 | 5 | zcnd 9335 |
. . . . . . . . . 10
..^ ..^ |
49 | 46, 47, 48 | pnpcan2d 8268 |
. . . . . . . . 9
..^ ..^ |
50 | 49 | oveq1d 5868 |
. . . . . . . 8
..^ ..^ |
51 | 45, 50 | eqtrd 2203 |
. . . . . . 7
..^ ..^ |
52 | | q0mod 10311 |
. . . . . . . 8
|
53 | 13, 14, 52 | syl2anc 409 |
. . . . . . 7
..^ ..^ |
54 | 51, 53 | eqeq12d 2185 |
. . . . . 6
..^ ..^ |
55 | | zmodidfzoimp 10310 |
. . . . . . . . . . 11
..^
|
56 | 55 | 3ad2ant1 1013 |
. . . . . . . . . 10
..^ ..^ |
57 | | zmodidfzoimp 10310 |
. . . . . . . . . . 11
..^
|
58 | 57 | 3ad2ant2 1014 |
. . . . . . . . . 10
..^ ..^ |
59 | 56, 58 | oveq12d 5871 |
. . . . . . . . 9
..^ ..^
|
60 | 59 | oveq1d 5868 |
. . . . . . . 8
..^ ..^ |
61 | 60 | eqeq1d 2179 |
. . . . . . 7
..^ ..^ |
62 | | qsubcl 9597 |
. . . . . . . . . 10
|
63 | 4, 21, 62 | syl2anc 409 |
. . . . . . . . 9
..^ ..^ |
64 | | modq0 10285 |
. . . . . . . . 9
|
65 | 63, 13, 14, 64 | syl3anc 1233 |
. . . . . . . 8
..^ ..^ |
66 | 2, 19 | zsubcld 9339 |
. . . . . . . . . 10
..^ ..^ |
67 | | zdiv 9300 |
. . . . . . . . . 10
|
68 | 11, 66, 67 | syl2anc 409 |
. . . . . . . . 9
..^ ..^ |
69 | | simpr 109 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
70 | 69 | oveq2d 5869 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
71 | 11 | nncnd 8892 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
72 | 71 | mul01d 8312 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
73 | 72 | ad2antrr 485 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
74 | 70, 73 | eqtrd 2203 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
75 | 74 | eqeq1d 2179 |
. . . . . . . . . . . . . . 15
..^ ..^
|
76 | | eqcom 2172 |
. . . . . . . . . . . . . . . 16
|
77 | 10 | simp1d 1004 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
78 | 77 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
|
79 | 78 | nn0cnd 9190 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
80 | | elfzo0 10138 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
81 | 80 | biimpi 119 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
82 | 81 | 3ad2ant2 1014 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^
|
83 | 82 | simp1d 1004 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
84 | 83 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
|
85 | 84 | nn0cnd 9190 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
86 | 79, 85 | subeq0ad 8240 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
87 | 86 | biimpd 143 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
88 | 76, 87 | syl5bi 151 |
. . . . . . . . . . . . . . 15
..^ ..^
|
89 | 75, 88 | sylbid 149 |
. . . . . . . . . . . . . 14
..^ ..^
|
90 | 89 | imp 123 |
. . . . . . . . . . . . 13
..^ ..^ |
91 | 90 | an32s 563 |
. . . . . . . . . . . 12
..^ ..^ |
92 | | subfzo0 10198 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
93 | 92 | 3adant3 1012 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
94 | 93 | ad3antrrr 489 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
95 | 94 | simprd 113 |
. . . . . . . . . . . . . . 15
..^ ..^ |
96 | | simplr 525 |
. . . . . . . . . . . . . . 15
..^ ..^
|
97 | 71 | mulid1d 7937 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
98 | 97 | ad3antrrr 489 |
. . . . . . . . . . . . . . 15
..^ ..^
|
99 | 95, 96, 98 | 3brtr4d 4021 |
. . . . . . . . . . . . . 14
..^ ..^
|
100 | | simpllr 529 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
101 | 100 | zred 9334 |
. . . . . . . . . . . . . . 15
..^ ..^ |
102 | | 1red 7935 |
. . . . . . . . . . . . . . 15
..^ ..^ |
103 | 11 | nnrpd 9651 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
104 | 103 | ad3antrrr 489 |
. . . . . . . . . . . . . . 15
..^ ..^ |
105 | 101, 102,
104 | ltmul2d 9696 |
. . . . . . . . . . . . . 14
..^ ..^
|
106 | 99, 105 | mpbird 166 |
. . . . . . . . . . . . 13
..^ ..^ |
107 | | simpr 109 |
. . . . . . . . . . . . . . 15
..^ ..^ |
108 | 107 | nnge1d 8921 |
. . . . . . . . . . . . . 14
..^ ..^ |
109 | 102, 101,
108 | lensymd 8041 |
. . . . . . . . . . . . 13
..^ ..^ |
110 | 106, 109 | pm2.21dd 615 |
. . . . . . . . . . . 12
..^ ..^ |
111 | 93 | ad3antrrr 489 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
112 | 111 | simpld 111 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
113 | | simplr 525 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
114 | 112, 113 | breqtrrd 4017 |
. . . . . . . . . . . . . . 15
..^ ..^ |
115 | 11 | nnzd 9333 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
116 | 115 | adantr 274 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
117 | | simpr 109 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
118 | 116, 117 | zmulcld 9340 |
. . . . . . . . . . . . . . . . . 18
..^
..^
|
119 | 118 | zred 9334 |
. . . . . . . . . . . . . . . . 17
..^
..^
|
120 | 119 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
121 | 11 | nnred 8891 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
122 | 121 | ad3antrrr 489 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
123 | 120, 122 | possumd 8488 |
. . . . . . . . . . . . . . 15
..^ ..^
|
124 | 114, 123 | mpbird 166 |
. . . . . . . . . . . . . 14
..^ ..^ |
125 | 97 | eqcomd 2176 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
126 | 125 | oveq2d 5869 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
127 | 126 | ad3antrrr 489 |
. . . . . . . . . . . . . . 15
..^ ..^ |
128 | 71 | ad3antrrr 489 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
129 | 117 | zcnd 9335 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
130 | 129 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
131 | | 1cnd 7936 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
132 | 128, 130,
131 | adddid 7944 |
. . . . . . . . . . . . . . 15
..^ ..^
|
133 | 127, 132 | eqtr4d 2206 |
. . . . . . . . . . . . . 14
..^ ..^ |
134 | 124, 133 | breqtrd 4015 |
. . . . . . . . . . . . 13
..^ ..^ |
135 | 117 | peano2zd 9337 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
136 | 116, 135 | zmulcld 9340 |
. . . . . . . . . . . . . . . 16
..^
..^
|
137 | 136 | zred 9334 |
. . . . . . . . . . . . . . 15
..^
..^
|
138 | 137 | ad2antrr 485 |
. . . . . . . . . . . . . 14
..^ ..^
|
139 | | 0red 7921 |
. . . . . . . . . . . . . 14
..^ ..^ |
140 | 71 | adantr 274 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
141 | 135 | zcnd 9335 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
142 | 140, 141 | mulcomd 7941 |
. . . . . . . . . . . . . . . 16
..^
..^
|
143 | 142 | ad2antrr 485 |
. . . . . . . . . . . . . . 15
..^ ..^
|
144 | 135 | zred 9334 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
145 | 144 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
146 | | zcn 9217 |
. . . . . . . . . . . . . . . . . . . 20
|
147 | | 1cnd 7936 |
. . . . . . . . . . . . . . . . . . . 20
|
148 | 146, 147 | addcomd 8070 |
. . . . . . . . . . . . . . . . . . 19
|
149 | 147, 146 | subnegd 8237 |
. . . . . . . . . . . . . . . . . . 19
|
150 | 148, 149 | eqtr4d 2206 |
. . . . . . . . . . . . . . . . . 18
|
151 | 150 | ad3antlr 490 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
152 | | simpr 109 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
153 | 152 | nnge1d 8921 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
154 | | 1red 7935 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
155 | 152 | nnred 8891 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
156 | 154, 155 | suble0d 8455 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
157 | 153, 156 | mpbird 166 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
158 | 151, 157 | eqbrtrd 4011 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
159 | 11 | nnnn0d 9188 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
160 | 159 | nn0ge0d 9191 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
161 | 160 | ad3antrrr 489 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
162 | | mulle0r 8860 |
. . . . . . . . . . . . . . . 16
|
163 | 145, 122,
158, 161, 162 | syl22anc 1234 |
. . . . . . . . . . . . . . 15
..^ ..^ |
164 | 143, 163 | eqbrtrd 4011 |
. . . . . . . . . . . . . 14
..^ ..^
|
165 | 138, 139,
164 | lensymd 8041 |
. . . . . . . . . . . . 13
..^ ..^ |
166 | 134, 165 | pm2.21dd 615 |
. . . . . . . . . . . 12
..^ ..^ |
167 | | elz 9214 |
. . . . . . . . . . . . . 14
|
168 | 167 | simprbi 273 |
. . . . . . . . . . . . 13
|
169 | 168 | ad2antlr 486 |
. . . . . . . . . . . 12
..^ ..^
|
170 | 91, 110, 166, 169 | mpjao3dan 1302 |
. . . . . . . . . . 11
..^ ..^
|
171 | 170 | ex 114 |
. . . . . . . . . 10
..^
..^
|
172 | 171 | rexlimdva 2587 |
. . . . . . . . 9
..^ ..^ |
173 | 68, 172 | sylbird 169 |
. . . . . . . 8
..^ ..^
|
174 | 65, 173 | sylbid 149 |
. . . . . . 7
..^ ..^
|
175 | 61, 174 | sylbid 149 |
. . . . . 6
..^ ..^
|
176 | 54, 175 | sylbid 149 |
. . . . 5
..^ ..^
|
177 | 37, 176 | syl5 32 |
. . . 4
..^ ..^ |
178 | 36, 177 | sylbird 169 |
. . 3
..^ ..^
|
179 | 25, 178 | sylbid 149 |
. 2
..^ ..^
|
180 | | oveq1 5860 |
. . 3
|
181 | 180 | oveq1d 5868 |
. 2
|
182 | 179, 181 | impbid1 141 |
1
..^ ..^
|