Step | Hyp | Ref
| Expression |
1 | | elfzoelz 12470 |
. . . . . . . 8
..^
|
2 | 1 | zred 11482 |
. . . . . . 7
..^
|
3 | 2 | 3ad2ant1 1082 |
. . . . . 6
..^ ..^ |
4 | | simp3 1063 |
. . . . . . 7
..^ ..^ |
5 | 4 | zred 11482 |
. . . . . 6
..^ ..^ |
6 | | elfzo0 12508 |
. . . . . . . . 9
..^
|
7 | 6 | simp2bi 1077 |
. . . . . . . 8
..^
|
8 | 7 | nnrpd 11870 |
. . . . . . 7
..^
|
9 | 8 | 3ad2ant1 1082 |
. . . . . 6
..^ ..^ |
10 | | modaddmod 12709 |
. . . . . 6
|
11 | 3, 5, 9, 10 | syl3anc 1326 |
. . . . 5
..^ ..^
|
12 | 11 | eqcomd 2628 |
. . . 4
..^ ..^ |
13 | | elfzoelz 12470 |
. . . . . . . 8
..^
|
14 | 13 | zred 11482 |
. . . . . . 7
..^
|
15 | 14 | 3ad2ant2 1083 |
. . . . . 6
..^ ..^ |
16 | | modaddmod 12709 |
. . . . . 6
|
17 | 15, 5, 9, 16 | syl3anc 1326 |
. . . . 5
..^ ..^
|
18 | 17 | eqcomd 2628 |
. . . 4
..^ ..^ |
19 | 12, 18 | eqeq12d 2637 |
. . 3
..^ ..^ |
20 | | nn0re 11301 |
. . . . . . . . . . . 12
|
21 | | nnrp 11842 |
. . . . . . . . . . . 12
|
22 | 20, 21 | anim12i 590 |
. . . . . . . . . . 11
|
23 | 22 | 3adant3 1081 |
. . . . . . . . . 10
|
24 | | modcl 12672 |
. . . . . . . . . 10
|
25 | 23, 24 | syl 17 |
. . . . . . . . 9
|
26 | 6, 25 | sylbi 207 |
. . . . . . . 8
..^
|
27 | 26 | 3ad2ant1 1082 |
. . . . . . 7
..^ ..^ |
28 | 27, 5 | readdcld 10069 |
. . . . . 6
..^ ..^ |
29 | | modcl 12672 |
. . . . . . 7
|
30 | 29 | recnd 10068 |
. . . . . 6
|
31 | 28, 9, 30 | syl2anc 693 |
. . . . 5
..^ ..^ |
32 | | elfzo0 12508 |
. . . . . . . . 9
..^
|
33 | | nn0re 11301 |
. . . . . . . . . . . 12
|
34 | 33, 21 | anim12i 590 |
. . . . . . . . . . 11
|
35 | 34 | 3adant3 1081 |
. . . . . . . . . 10
|
36 | | modcl 12672 |
. . . . . . . . . 10
|
37 | 35, 36 | syl 17 |
. . . . . . . . 9
|
38 | 32, 37 | sylbi 207 |
. . . . . . . 8
..^
|
39 | 38 | 3ad2ant2 1083 |
. . . . . . 7
..^ ..^ |
40 | 39, 5 | readdcld 10069 |
. . . . . 6
..^ ..^ |
41 | | modcl 12672 |
. . . . . . 7
|
42 | 41 | recnd 10068 |
. . . . . 6
|
43 | 40, 9, 42 | syl2anc 693 |
. . . . 5
..^ ..^ |
44 | 31, 43 | subeq0ad 10402 |
. . . 4
..^ ..^ |
45 | | oveq1 6657 |
. . . . 5
|
46 | | modsubmodmod 12729 |
. . . . . . . . 9
|
47 | 28, 40, 9, 46 | syl3anc 1326 |
. . . . . . . 8
..^ ..^ |
48 | 26 | recnd 10068 |
. . . . . . . . . . 11
..^
|
49 | 48 | 3ad2ant1 1082 |
. . . . . . . . . 10
..^ ..^ |
50 | 38 | recnd 10068 |
. . . . . . . . . . 11
..^
|
51 | 50 | 3ad2ant2 1083 |
. . . . . . . . . 10
..^ ..^ |
52 | 4 | zcnd 11483 |
. . . . . . . . . 10
..^ ..^ |
53 | 49, 51, 52 | pnpcan2d 10430 |
. . . . . . . . 9
..^ ..^ |
54 | 53 | oveq1d 6665 |
. . . . . . . 8
..^ ..^ |
55 | 47, 54 | eqtrd 2656 |
. . . . . . 7
..^ ..^ |
56 | 32 | simp2bi 1077 |
. . . . . . . . . 10
..^
|
57 | 56 | nnrpd 11870 |
. . . . . . . . 9
..^
|
58 | | 0mod 12701 |
. . . . . . . . 9
|
59 | 57, 58 | syl 17 |
. . . . . . . 8
..^
|
60 | 59 | 3ad2ant2 1083 |
. . . . . . 7
..^ ..^ |
61 | 55, 60 | eqeq12d 2637 |
. . . . . 6
..^ ..^ |
62 | | zmodidfzoimp 12700 |
. . . . . . . . . . 11
..^
|
63 | 62 | 3ad2ant1 1082 |
. . . . . . . . . 10
..^ ..^ |
64 | | zmodidfzoimp 12700 |
. . . . . . . . . . 11
..^
|
65 | 64 | 3ad2ant2 1083 |
. . . . . . . . . 10
..^ ..^ |
66 | 63, 65 | oveq12d 6668 |
. . . . . . . . 9
..^ ..^
|
67 | 66 | oveq1d 6665 |
. . . . . . . 8
..^ ..^ |
68 | 67 | eqeq1d 2624 |
. . . . . . 7
..^ ..^ |
69 | | zsubcl 11419 |
. . . . . . . . . . . 12
|
70 | 1, 13, 69 | syl2an 494 |
. . . . . . . . . . 11
..^ ..^
|
71 | 70 | zred 11482 |
. . . . . . . . . 10
..^ ..^
|
72 | 8 | adantr 481 |
. . . . . . . . . 10
..^ ..^
|
73 | | mod0 12675 |
. . . . . . . . . 10
|
74 | 71, 72, 73 | syl2anc 693 |
. . . . . . . . 9
..^ ..^
|
75 | | zdiv 11447 |
. . . . . . . . . . 11
|
76 | 7, 70, 75 | syl2an2r 876 |
. . . . . . . . . 10
..^ ..^
|
77 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
|
78 | | elfzoel2 12469 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
79 | 78 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
..^
|
80 | 79 | mul01d 10235 |
. . . . . . . . . . . . . . . . . 18
..^
|
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
82 | 81 | adantr 481 |
. . . . . . . . . . . . . . . 16
..^
..^
|
83 | 77, 82 | sylan9eq 2676 |
. . . . . . . . . . . . . . 15
..^ ..^
|
84 | 83 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
..^ ..^
|
85 | | eqcom 2629 |
. . . . . . . . . . . . . . . . 17
|
86 | 1 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
..^
|
87 | 13 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
..^
|
88 | | subeq0 10307 |
. . . . . . . . . . . . . . . . . . 19
|
89 | 86, 87, 88 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
90 | 89 | biimpd 219 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
91 | 85, 90 | syl5bi 232 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
92 | 91 | adantr 481 |
. . . . . . . . . . . . . . 15
..^
..^
|
93 | 92 | adantl 482 |
. . . . . . . . . . . . . 14
..^ ..^
|
94 | 84, 93 | sylbid 230 |
. . . . . . . . . . . . 13
..^ ..^
|
95 | 94 | ex 450 |
. . . . . . . . . . . 12
..^ ..^
|
96 | | subfzo0 12590 |
. . . . . . . . . . . . . . 15
..^ ..^
|
97 | 96 | adantr 481 |
. . . . . . . . . . . . . 14
..^
..^
|
98 | | elz 11379 |
. . . . . . . . . . . . . . . 16
|
99 | | pm2.24 121 |
. . . . . . . . . . . . . . . . . . . 20
|
100 | 99 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
|
101 | 100 | 2a1d 26 |
. . . . . . . . . . . . . . . . . 18
..^
..^
|
102 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
103 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
104 | 103 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
105 | 104 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
106 | 105 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
107 | 106 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
108 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
109 | 108 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
110 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
111 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
112 | 109, 110,
111 | ltmul2d 11914 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
113 | | nnge1 11046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
114 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
115 | 114, 108 | lenltd 10183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
116 | | pm2.21 120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
117 | 115, 116 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
118 | 113, 117 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
119 | 118 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
120 | 112, 119 | sylbird 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
121 | 107, 120 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
122 | 121 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
123 | 122 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
124 | 32, 123 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^
|
125 | 124 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^ ..^
|
126 | 125 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
..^
|
127 | 126 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ ..^
|
128 | 102, 127 | syl6bir 244 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ ..^
|
129 | 128 | com15 101 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^
|
130 | 129 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^
|
131 | 130 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^
|
132 | 131 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
..^
..^
|
133 | 132 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
..^
..^
|
134 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
135 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
136 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
137 | | remulcl 10021 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
138 | 135, 136,
137 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
139 | 135 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
140 | 138, 139 | possumd 10652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
141 | 103 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
142 | 141 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
143 | 142 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
144 | 143 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
145 | | recn 10026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
146 | 145 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
147 | 146 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
148 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
149 | 141, 147,
148 | adddid 10064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
150 | 144, 149 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
151 | 150 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
152 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
153 | 152 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
154 | 153 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
155 | 139, 154 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
156 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
157 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
158 | 157 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
159 | | nnge1 11046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
160 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
161 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
162 | 160, 161 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
163 | 161, 160 | subnegd 10399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
164 | 162, 163 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
165 | 145, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
166 | 165 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
167 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
168 | | renegcl 10344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
169 | 167, 168 | suble0d 10618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
170 | 169 | biimparc 504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
171 | 166, 170 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
172 | 159, 171 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
173 | 158, 172 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
174 | 173 | olcd 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
175 | | mulle0b 10894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
176 | 135, 153,
175 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
177 | 174, 176 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
178 | 155, 156,
177 | lensymd 10188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
179 | 178 | pm2.21d 118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
180 | 151, 179 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
181 | 140, 180 | sylbird 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
182 | 181 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
183 | 182 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
184 | 183 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
185 | 6, 184 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
186 | 185 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^ ..^
|
187 | 186 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
..^
|
188 | 134, 187 | syl6bir 244 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ ..^ |
189 | 188 | com15 101 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^
|
190 | 189 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^
|
191 | 190 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^
|
192 | 191 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
|
193 | 192 | ex 450 |
. . . . . . . . . . . . . . . . . 18
..^
..^
|
194 | 101, 133,
193 | 3jaoi 1391 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
195 | 194 | impcom 446 |
. . . . . . . . . . . . . . . 16
..^
..^
|
196 | 98, 195 | sylbi 207 |
. . . . . . . . . . . . . . 15
..^
..^
|
197 | 196 | impcom 446 |
. . . . . . . . . . . . . 14
..^
..^
|
198 | 97, 197 | mpd 15 |
. . . . . . . . . . . . 13
..^
..^
|
199 | 198 | com12 32 |
. . . . . . . . . . . 12
..^ ..^
|
200 | 95, 199 | pm2.61i 176 |
. . . . . . . . . . 11
..^
..^
|
201 | 200 | rexlimdva 3031 |
. . . . . . . . . 10
..^ ..^
|
202 | 76, 201 | sylbird 250 |
. . . . . . . . 9
..^ ..^
|
203 | 74, 202 | sylbid 230 |
. . . . . . . 8
..^ ..^
|
204 | 203 | 3adant3 1081 |
. . . . . . 7
..^ ..^
|
205 | 68, 204 | sylbid 230 |
. . . . . 6
..^ ..^
|
206 | 61, 205 | sylbid 230 |
. . . . 5
..^ ..^
|
207 | 45, 206 | syl5 34 |
. . . 4
..^ ..^ |
208 | 44, 207 | sylbird 250 |
. . 3
..^ ..^
|
209 | 19, 208 | sylbid 230 |
. 2
..^ ..^
|
210 | | oveq1 6657 |
. . 3
|
211 | 210 | oveq1d 6665 |
. 2
|
212 | 209, 211 | impbid1 215 |
1
..^ ..^
|