Proof of Theorem acongeq
Step | Hyp | Ref
| Expression |
1 | | 2z 11409 |
. . . . . . 7
|
2 | | nnz 11399 |
. . . . . . . 8
|
3 | 2 | 3ad2ant1 1082 |
. . . . . . 7
|
4 | | zmulcl 11426 |
. . . . . . 7
|
5 | 1, 3, 4 | sylancr 695 |
. . . . . 6
|
6 | | elfzelz 12342 |
. . . . . . 7
|
7 | 6 | 3ad2ant2 1083 |
. . . . . 6
|
8 | | congid 37538 |
. . . . . 6
|
9 | 5, 7, 8 | syl2anc 693 |
. . . . 5
|
10 | 9 | adantr 481 |
. . . 4
|
11 | | oveq2 6658 |
. . . . 5
|
12 | 11 | adantl 482 |
. . . 4
|
13 | 10, 12 | breqtrd 4679 |
. . 3
|
14 | 13 | orcd 407 |
. 2
|
15 | | elfzelz 12342 |
. . . . . . . . . 10
|
16 | 15 | 3ad2ant3 1084 |
. . . . . . . . 9
|
17 | 7, 16 | zsubcld 11487 |
. . . . . . . 8
|
18 | 17 | zcnd 11483 |
. . . . . . 7
|
19 | 18 | abscld 14175 |
. . . . . 6
|
20 | | nnre 11027 |
. . . . . . . 8
|
21 | 20 | 3ad2ant1 1082 |
. . . . . . 7
|
22 | | 0re 10040 |
. . . . . . 7
|
23 | | resubcl 10345 |
. . . . . . 7
|
24 | 21, 22, 23 | sylancl 694 |
. . . . . 6
|
25 | | 2re 11090 |
. . . . . . 7
|
26 | | remulcl 10021 |
. . . . . . 7
|
27 | 25, 21, 26 | sylancr 695 |
. . . . . 6
|
28 | | simp2 1062 |
. . . . . . 7
|
29 | | simp3 1063 |
. . . . . . 7
|
30 | 24 | leidd 10594 |
. . . . . . 7
|
31 | | fzmaxdif 37548 |
. . . . . . 7
|
32 | 3, 28, 3, 29, 30, 31 | syl221anc 1337 |
. . . . . 6
|
33 | | nnrp 11842 |
. . . . . . . . 9
|
34 | 33 | 3ad2ant1 1082 |
. . . . . . . 8
|
35 | 21, 34 | ltaddrpd 11905 |
. . . . . . 7
|
36 | 21 | recnd 10068 |
. . . . . . . 8
|
37 | 36 | subid1d 10381 |
. . . . . . 7
|
38 | 36 | 2timesd 11275 |
. . . . . . 7
|
39 | 35, 37, 38 | 3brtr4d 4685 |
. . . . . 6
|
40 | 19, 24, 27, 32, 39 | lelttrd 10195 |
. . . . 5
|
41 | 40 | adantr 481 |
. . . 4
|
42 | | 2nn 11185 |
. . . . . 6
|
43 | | simpl1 1064 |
. . . . . 6
|
44 | | nnmulcl 11043 |
. . . . . 6
|
45 | 42, 43, 44 | sylancr 695 |
. . . . 5
|
46 | | simpl2 1065 |
. . . . . 6
|
47 | 46, 6 | syl 17 |
. . . . 5
|
48 | | simpl3 1066 |
. . . . . 6
|
49 | 48, 15 | syl 17 |
. . . . 5
|
50 | | simpr 477 |
. . . . 5
|
51 | | congabseq 37541 |
. . . . 5
|
52 | 45, 47, 49, 50, 51 | syl31anc 1329 |
. . . 4
|
53 | 41, 52 | mpbid 222 |
. . 3
|
54 | | simpll2 1101 |
. . . . . . . . . . 11
|
55 | | elfzle1 12344 |
. . . . . . . . . . 11
|
56 | 54, 55 | syl 17 |
. . . . . . . . . 10
|
57 | 7 | zred 11482 |
. . . . . . . . . . . . . . . 16
|
58 | 16 | zred 11482 |
. . . . . . . . . . . . . . . . 17
|
59 | 58 | renegcld 10457 |
. . . . . . . . . . . . . . . 16
|
60 | 57, 59 | resubcld 10458 |
. . . . . . . . . . . . . . 15
|
61 | 60 | recnd 10068 |
. . . . . . . . . . . . . 14
|
62 | 61 | abscld 14175 |
. . . . . . . . . . . . 13
|
63 | 62 | ad2antrr 762 |
. . . . . . . . . . . 12
|
64 | | 1re 10039 |
. . . . . . . . . . . . . . . 16
|
65 | | resubcl 10345 |
. . . . . . . . . . . . . . . 16
|
66 | 21, 64, 65 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
67 | 66 | renegcld 10457 |
. . . . . . . . . . . . . 14
|
68 | 21, 67 | resubcld 10458 |
. . . . . . . . . . . . 13
|
69 | 68 | ad2antrr 762 |
. . . . . . . . . . . 12
|
70 | 27 | ad2antrr 762 |
. . . . . . . . . . . 12
|
71 | 7 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
72 | 71 | zcnd 11483 |
. . . . . . . . . . . . . 14
|
73 | 16 | znegcld 11484 |
. . . . . . . . . . . . . . . 16
|
74 | 73 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
75 | 74 | zcnd 11483 |
. . . . . . . . . . . . . 14
|
76 | 72, 75 | abssubd 14192 |
. . . . . . . . . . . . 13
|
77 | | 0zd 11389 |
. . . . . . . . . . . . . 14
|
78 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
79 | | 0zd 11389 |
. . . . . . . . . . . . . . . . . 18
|
80 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . 19
|
81 | | zsubcl 11419 |
. . . . . . . . . . . . . . . . . . 19
|
82 | 3, 80, 81 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
|
83 | | fzneg 37549 |
. . . . . . . . . . . . . . . . . 18
|
84 | 16, 79, 82, 83 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
85 | 84 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
86 | 78, 85 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
87 | | neg0 10327 |
. . . . . . . . . . . . . . . . 17
|
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
89 | 88 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
90 | 86, 89 | eleqtrd 2703 |
. . . . . . . . . . . . . 14
|
91 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
92 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . 19
|
93 | 42, 92, 44 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
|
94 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . . 18
|
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
96 | 95 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . 16
|
97 | | 0m0e0 11130 |
. . . . . . . . . . . . . . . . 17
|
98 | 97 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
99 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . 18
|
100 | 36, 36, 99 | addsubassd 10412 |
. . . . . . . . . . . . . . . . 17
|
101 | 38 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
102 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . 19
|
103 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . 19
|
104 | 36, 102, 103 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
|
105 | 36, 104 | subnegd 10399 |
. . . . . . . . . . . . . . . . 17
|
106 | 100, 101,
105 | 3eqtr4rd 2667 |
. . . . . . . . . . . . . . . 16
|
107 | 96, 98, 106 | 3brtr4d 4685 |
. . . . . . . . . . . . . . 15
|
108 | 107 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
109 | | fzmaxdif 37548 |
. . . . . . . . . . . . . 14
|
110 | 77, 90, 91, 54, 108, 109 | syl221anc 1337 |
. . . . . . . . . . . . 13
|
111 | 76, 110 | eqbrtrd 4675 |
. . . . . . . . . . . 12
|
112 | 27 | ltm1d 10956 |
. . . . . . . . . . . . . 14
|
113 | 106, 112 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
|
114 | 113 | ad2antrr 762 |
. . . . . . . . . . . 12
|
115 | 63, 69, 70, 111, 114 | lelttrd 10195 |
. . . . . . . . . . 11
|
116 | 93 | ad2antrr 762 |
. . . . . . . . . . . 12
|
117 | | simplr 792 |
. . . . . . . . . . . 12
|
118 | | congabseq 37541 |
. . . . . . . . . . . 12
|
119 | 116, 71, 74, 117, 118 | syl31anc 1329 |
. . . . . . . . . . 11
|
120 | 115, 119 | mpbid 222 |
. . . . . . . . . 10
|
121 | 56, 120 | breqtrd 4679 |
. . . . . . . . 9
|
122 | | elfzelz 12342 |
. . . . . . . . . . . 12
|
123 | 122 | zred 11482 |
. . . . . . . . . . 11
|
124 | 123 | adantl 482 |
. . . . . . . . . 10
|
125 | 124 | le0neg1d 10599 |
. . . . . . . . 9
|
126 | 121, 125 | mpbird 247 |
. . . . . . . 8
|
127 | | elfzle1 12344 |
. . . . . . . . 9
|
128 | 127 | adantl 482 |
. . . . . . . 8
|
129 | | letri3 10123 |
. . . . . . . . 9
|
130 | 124, 22, 129 | sylancl 694 |
. . . . . . . 8
|
131 | 126, 128,
130 | mpbir2and 957 |
. . . . . . 7
|
132 | 131 | negeqd 10275 |
. . . . . 6
|
133 | 132, 88 | eqtrd 2656 |
. . . . 5
|
134 | 133, 120,
131 | 3eqtr4d 2666 |
. . . 4
|
135 | | oveq2 6658 |
. . . . . . . . 9
|
136 | 135 | adantl 482 |
. . . . . . . 8
|
137 | 136 | fveq2d 6195 |
. . . . . . 7
|
138 | 40 | ad2antrr 762 |
. . . . . . 7
|
139 | 137, 138 | eqbrtrrd 4677 |
. . . . . 6
|
140 | 93 | ad2antrr 762 |
. . . . . . 7
|
141 | 7 | ad2antrr 762 |
. . . . . . 7
|
142 | 3 | ad2antrr 762 |
. . . . . . 7
|
143 | | simplr 792 |
. . . . . . . . 9
|
144 | 7 | zcnd 11483 |
. . . . . . . . . . . . . 14
|
145 | 36, 36, 144 | ppncand 10432 |
. . . . . . . . . . . . 13
|
146 | 36, 144 | addcomd 10238 |
. . . . . . . . . . . . 13
|
147 | 145, 146 | eqtrd 2656 |
. . . . . . . . . . . 12
|
148 | 147 | ad2antrr 762 |
. . . . . . . . . . 11
|
149 | | oveq2 6658 |
. . . . . . . . . . . 12
|
150 | 149 | adantl 482 |
. . . . . . . . . . 11
|
151 | 148, 150 | eqtr4d 2659 |
. . . . . . . . . 10
|
152 | 38 | oveq1d 6665 |
. . . . . . . . . . 11
|
153 | 152 | ad2antrr 762 |
. . . . . . . . . 10
|
154 | 16 | zcnd 11483 |
. . . . . . . . . . . 12
|
155 | 144, 154 | subnegd 10399 |
. . . . . . . . . . 11
|
156 | 155 | ad2antrr 762 |
. . . . . . . . . 10
|
157 | 151, 153,
156 | 3eqtr4d 2666 |
. . . . . . . . 9
|
158 | 143, 157 | breqtrrd 4681 |
. . . . . . . 8
|
159 | 5 | ad2antrr 762 |
. . . . . . . . 9
|
160 | 7, 3 | zsubcld 11487 |
. . . . . . . . . 10
|
161 | 160 | ad2antrr 762 |
. . . . . . . . 9
|
162 | | dvdsadd 15024 |
. . . . . . . . 9
|
163 | 159, 161,
162 | syl2anc 693 |
. . . . . . . 8
|
164 | 158, 163 | mpbird 247 |
. . . . . . 7
|
165 | | congabseq 37541 |
. . . . . . 7
|
166 | 140, 141,
142, 164, 165 | syl31anc 1329 |
. . . . . 6
|
167 | 139, 166 | mpbid 222 |
. . . . 5
|
168 | | simpr 477 |
. . . . 5
|
169 | 167, 168 | eqtr4d 2659 |
. . . 4
|
170 | | nnnn0 11299 |
. . . . . . . 8
|
171 | 170 | 3ad2ant1 1082 |
. . . . . . 7
|
172 | | nn0uz 11722 |
. . . . . . 7
|
173 | 171, 172 | syl6eleq 2711 |
. . . . . 6
|
174 | | fzm1 12420 |
. . . . . . 7
|
175 | 174 | biimpa 501 |
. . . . . 6
|
176 | 173, 29, 175 | syl2anc 693 |
. . . . 5
|
177 | 176 | adantr 481 |
. . . 4
|
178 | 134, 169,
177 | mpjaodan 827 |
. . 3
|
179 | 53, 178 | jaodan 826 |
. 2
|
180 | 14, 179 | impbida 877 |
1
|