Proof of Theorem modfzo0difsn
Step | Hyp | Ref
| Expression |
1 | | eldifi 3732 |
. . . . . 6
..^ ..^ |
2 | | elfzoelz 12470 |
. . . . . . 7
..^
|
3 | 2 | zred 11482 |
. . . . . 6
..^
|
4 | 1, 3 | syl 17 |
. . . . 5
..^ |
5 | | elfzoelz 12470 |
. . . . . 6
..^
|
6 | 5 | zred 11482 |
. . . . 5
..^
|
7 | | leloe 10124 |
. . . . 5
|
8 | 4, 6, 7 | syl2anr 495 |
. . . 4
..^ ..^
|
9 | | elfzo0 12508 |
. . . . . . . . . . . 12
..^
|
10 | | elfzo0 12508 |
. . . . . . . . . . . . . . 15
..^
|
11 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . 22
|
12 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
13 | 12 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
14 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . 22
|
15 | 14 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . 21
|
16 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
17 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . 22
|
18 | 17 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . 21
|
19 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
20 | 13, 16, 19 | subadd23d 10414 |
. . . . . . . . . . . . . . . . . . 19
|
21 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
|
22 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . 22
|
23 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . 22
|
24 | | znnsub 11423 |
. . . . . . . . . . . . . . . . . . . . . 22
|
25 | 22, 23, 24 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . 21
|
26 | 25 | biimp3a 1432 |
. . . . . . . . . . . . . . . . . . . 20
|
27 | | nn0nnaddcl 11324 |
. . . . . . . . . . . . . . . . . . . 20
|
28 | 21, 26, 27 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . 19
|
29 | 20, 28 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . 18
|
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
31 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . 19
|
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
34 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
36 | 35 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
37 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
38 | 37 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . 22
|
39 | 38 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
40 | 36, 39 | sublt0d 10653 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | 40 | bicomd 213 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 41 | biimpa 501 |
. . . . . . . . . . . . . . . . . 18
|
43 | | resubcl 10345 |
. . . . . . . . . . . . . . . . . . . . . 22
|
44 | 35, 38, 43 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . 21
|
45 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
46 | 45 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . 22
|
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
48 | 44, 47 | jca 554 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 48 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | ltaddnegr 10252 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
52 | 42, 51 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
53 | | elfzo1 12517 |
. . . . . . . . . . . . . . . . 17
..^ |
54 | 30, 33, 52, 53 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . 16
..^ |
55 | 54 | exp31 630 |
. . . . . . . . . . . . . . 15
..^ |
56 | 10, 55 | sylbi 207 |
. . . . . . . . . . . . . 14
..^
..^ |
57 | 56 | com12 32 |
. . . . . . . . . . . . 13
..^ ..^ |
58 | 57 | 3adant2 1080 |
. . . . . . . . . . . 12
..^ ..^ |
59 | 9, 58 | sylbi 207 |
. . . . . . . . . . 11
..^
..^
..^ |
60 | 1, 59 | syl 17 |
. . . . . . . . . 10
..^
..^ ..^ |
61 | 60 | impcom 446 |
. . . . . . . . 9
..^ ..^ ..^ |
62 | 61 | impcom 446 |
. . . . . . . 8
..^
..^
..^ |
63 | | oveq1 6657 |
. . . . . . . . . . 11
|
64 | 2 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
65 | 64 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
66 | 14 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
67 | 66 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
68 | 17 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
69 | 68 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
70 | 65, 67, 69 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . 19
..^
|
71 | 70 | ex 450 |
. . . . . . . . . . . . . . . . . 18
..^
|
72 | 1, 71 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^ |
73 | 72 | com12 32 |
. . . . . . . . . . . . . . . 16
..^
|
74 | 73 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
..^
|
75 | 10, 74 | sylbi 207 |
. . . . . . . . . . . . . 14
..^
..^
|
76 | 75 | imp 445 |
. . . . . . . . . . . . 13
..^ ..^
|
77 | 76 | adantl 482 |
. . . . . . . . . . . 12
..^
..^
|
78 | | nppcan 10303 |
. . . . . . . . . . . 12
|
79 | 77, 78 | syl 17 |
. . . . . . . . . . 11
..^
..^
|
80 | 63, 79 | sylan9eqr 2678 |
. . . . . . . . . 10
..^
..^ |
81 | 80 | oveq1d 6665 |
. . . . . . . . 9
..^
..^
|
82 | 81 | eqeq2d 2632 |
. . . . . . . 8
..^
..^
|
83 | 9 | biimpi 206 |
. . . . . . . . . . . . 13
..^
|
84 | 83 | a1d 25 |
. . . . . . . . . . . 12
..^
..^
|
85 | 1, 84 | syl 17 |
. . . . . . . . . . 11
..^
..^
|
86 | 85 | impcom 446 |
. . . . . . . . . 10
..^ ..^ |
87 | 86 | adantl 482 |
. . . . . . . . 9
..^
..^
|
88 | | addmodidr 12719 |
. . . . . . . . . 10
|
89 | 88 | eqcomd 2628 |
. . . . . . . . 9
|
90 | 87, 89 | syl 17 |
. . . . . . . 8
..^
..^
|
91 | 62, 82, 90 | rspcedvd 3317 |
. . . . . . 7
..^
..^
..^ |
92 | 91 | ex 450 |
. . . . . 6
..^
..^ ..^ |
93 | | eldifsn 4317 |
. . . . . . . . 9
..^
..^ |
94 | | eqneqall 2805 |
. . . . . . . . . . 11
..^ |
95 | 94 | com12 32 |
. . . . . . . . . 10
..^ |
96 | 95 | adantl 482 |
. . . . . . . . 9
..^
..^ |
97 | 93, 96 | sylbi 207 |
. . . . . . . 8
..^
..^ |
98 | 97 | adantl 482 |
. . . . . . 7
..^ ..^ ..^ |
99 | 98 | com12 32 |
. . . . . 6
..^
..^ ..^ |
100 | 92, 99 | jaoi 394 |
. . . . 5
..^ ..^ ..^ |
101 | 100 | com12 32 |
. . . 4
..^ ..^ ..^ |
102 | 8, 101 | sylbid 230 |
. . 3
..^ ..^ ..^ |
103 | 102 | com12 32 |
. 2
..^
..^ ..^ |
104 | | ltnle 10117 |
. . . . . . . . 9
|
105 | 6, 4, 104 | syl2an 494 |
. . . . . . . 8
..^ ..^
|
106 | 105 | bicomd 213 |
. . . . . . 7
..^ ..^ |
107 | 22 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . 17
|
108 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . 18
|
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
110 | | znnsub 11423 |
. . . . . . . . . . . . . . . . 17
|
111 | 107, 109,
110 | syl2anr 495 |
. . . . . . . . . . . . . . . 16
|
112 | 111 | biimpa 501 |
. . . . . . . . . . . . . . 15
|
113 | 31 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
114 | 113 | adantr 481 |
. . . . . . . . . . . . . . 15
|
115 | | nn0ge0 11318 |
. . . . . . . . . . . . . . . . . . . . . 22
|
116 | 115 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . 21
|
117 | 116 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
118 | | subge02 10544 |
. . . . . . . . . . . . . . . . . . . . 21
|
119 | 34, 38, 118 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
|
120 | 117, 119 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
|
121 | 38 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
122 | 34 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
123 | 46 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
124 | 121, 122,
123 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . 21
|
125 | 43 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
126 | 125 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . 22
|
127 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . . . 22
|
128 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . 22
|
129 | 126, 127,
128 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . 21
|
130 | 124, 129 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
131 | | lelttr 10128 |
. . . . . . . . . . . . . . . . . . . 20
|
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
133 | 120, 132 | mpand 711 |
. . . . . . . . . . . . . . . . . 18
|
134 | 133 | impancom 456 |
. . . . . . . . . . . . . . . . 17
|
135 | 134 | imp 445 |
. . . . . . . . . . . . . . . 16
|
136 | 135 | adantr 481 |
. . . . . . . . . . . . . . 15
|
137 | 112, 114,
136 | 3jca 1242 |
. . . . . . . . . . . . . 14
|
138 | 137 | exp31 630 |
. . . . . . . . . . . . 13
|
139 | 138 | 3adant2 1080 |
. . . . . . . . . . . 12
|
140 | 9, 139 | sylbi 207 |
. . . . . . . . . . 11
..^
|
141 | 1, 140 | syl 17 |
. . . . . . . . . 10
..^
|
142 | 141 | com12 32 |
. . . . . . . . 9
..^
|
143 | 10, 142 | sylbi 207 |
. . . . . . . 8
..^
..^
|
144 | 143 | imp 445 |
. . . . . . 7
..^ ..^
|
145 | 106, 144 | sylbid 230 |
. . . . . 6
..^ ..^ |
146 | 145 | impcom 446 |
. . . . 5
..^
..^
|
147 | | elfzo1 12517 |
. . . . 5
..^ |
148 | 146, 147 | sylibr 224 |
. . . 4
..^
..^
..^ |
149 | | oveq1 6657 |
. . . . . . 7
|
150 | 1, 64 | syl 17 |
. . . . . . . . 9
..^ |
151 | 5 | zcnd 11483 |
. . . . . . . . 9
..^
|
152 | | npcan 10290 |
. . . . . . . . 9
|
153 | 150, 151,
152 | syl2anr 495 |
. . . . . . . 8
..^ ..^ |
154 | 153 | adantl 482 |
. . . . . . 7
..^
..^
|
155 | 149, 154 | sylan9eqr 2678 |
. . . . . 6
..^ ..^
|
156 | 155 | oveq1d 6665 |
. . . . 5
..^ ..^
|
157 | 156 | eqeq2d 2632 |
. . . 4
..^ ..^
|
158 | | zmodidfzoimp 12700 |
. . . . . . . 8
..^
|
159 | 1, 158 | syl 17 |
. . . . . . 7
..^ |
160 | 159 | adantl 482 |
. . . . . 6
..^ ..^ |
161 | 160 | adantl 482 |
. . . . 5
..^
..^
|
162 | 161 | eqcomd 2628 |
. . . 4
..^
..^
|
163 | 148, 157,
162 | rspcedvd 3317 |
. . 3
..^
..^
..^ |
164 | 163 | ex 450 |
. 2
..^
..^ ..^ |
165 | 103, 164 | pm2.61i 176 |
1
..^ ..^
..^ |