Step | Hyp | Ref
| Expression |
1 | | aalioulem2.d |
. . . . 5
|
2 | | 1re 10039 |
. . . . 5
|
3 | | resubcl 10345 |
. . . . 5
|
4 | 1, 2, 3 | sylancl 694 |
. . . 4
|
5 | | peano2re 10209 |
. . . . 5
|
6 | 1, 5 | syl 17 |
. . . 4
|
7 | | reelprrecn 10028 |
. . . . 5
|
8 | | ssid 3624 |
. . . . . . . . 9
|
9 | | fncpn 23696 |
. . . . . . . . 9
|
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
|
11 | | 1nn0 11308 |
. . . . . . . 8
|
12 | | fnfvelrn 6356 |
. . . . . . . 8
|
13 | 10, 11, 12 | mp2an 708 |
. . . . . . 7
|
14 | | intss1 4492 |
. . . . . . 7
|
15 | 13, 14 | ax-mp 5 |
. . . . . 6
|
16 | | aalioulem2.b |
. . . . . . 7
Poly |
17 | | plycpn 24044 |
. . . . . . 7
Poly |
18 | 16, 17 | syl 17 |
. . . . . 6
|
19 | 15, 18 | sseldi 3601 |
. . . . 5
|
20 | | cpnres 23700 |
. . . . 5
|
21 | 7, 19, 20 | sylancr 695 |
. . . 4
|
22 | | df-ima 5127 |
. . . . 5
|
23 | | zssre 11384 |
. . . . . . . . 9
|
24 | | ax-resscn 9993 |
. . . . . . . . 9
|
25 | | plyss 23955 |
. . . . . . . . 9
Poly Poly |
26 | 23, 24, 25 | mp2an 708 |
. . . . . . . 8
Poly
Poly |
27 | 26, 16 | sseldi 3601 |
. . . . . . 7
Poly |
28 | | plyreres 24038 |
. . . . . . 7
Poly |
29 | 27, 28 | syl 17 |
. . . . . 6
|
30 | | frn 6053 |
. . . . . 6
|
31 | 29, 30 | syl 17 |
. . . . 5
|
32 | 22, 31 | syl5eqss 3649 |
. . . 4
|
33 | | iccssre 12255 |
. . . . . . 7
|
34 | 4, 6, 33 | syl2anc 693 |
. . . . . 6
|
35 | 34, 24 | syl6ss 3615 |
. . . . 5
|
36 | | plyf 23954 |
. . . . . . 7
Poly |
37 | 16, 36 | syl 17 |
. . . . . 6
|
38 | | fdm 6051 |
. . . . . 6
|
39 | 37, 38 | syl 17 |
. . . . 5
|
40 | 35, 39 | sseqtr4d 3642 |
. . . 4
|
41 | 4, 6, 21, 32, 40 | c1lip3 23762 |
. . 3
|
42 | | simp2 1062 |
. . . . . . . . . . . . . 14
|
43 | 42 | recnd 10068 |
. . . . . . . . . . . . 13
|
44 | 1 | adantr 481 |
. . . . . . . . . . . . . . 15
|
45 | 44 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
|
46 | 45 | recnd 10068 |
. . . . . . . . . . . . 13
|
47 | 43, 46 | abssubd 14192 |
. . . . . . . . . . . 12
|
48 | | simp3 1063 |
. . . . . . . . . . . 12
|
49 | 47, 48 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
50 | | 1red 10055 |
. . . . . . . . . . . 12
|
51 | | elicc4abs 14059 |
. . . . . . . . . . . 12
|
52 | 45, 50, 42, 51 | syl3anc 1326 |
. . . . . . . . . . 11
|
53 | 49, 52 | mpbird 247 |
. . . . . . . . . 10
|
54 | 1 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | subidd 10380 |
. . . . . . . . . . . . . . 15
|
56 | 55 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
57 | | abs0 14025 |
. . . . . . . . . . . . . . 15
|
58 | | 0le1 10551 |
. . . . . . . . . . . . . . 15
|
59 | 57, 58 | eqbrtri 4674 |
. . . . . . . . . . . . . 14
|
60 | 56, 59 | syl6eqbr 4692 |
. . . . . . . . . . . . 13
|
61 | | 1red 10055 |
. . . . . . . . . . . . . 14
|
62 | | elicc4abs 14059 |
. . . . . . . . . . . . . 14
|
63 | 1, 61, 1, 62 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
64 | 60, 63 | mpbird 247 |
. . . . . . . . . . . 12
|
65 | 64 | adantr 481 |
. . . . . . . . . . 11
|
66 | 65 | 3ad2ant1 1082 |
. . . . . . . . . 10
|
67 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
68 | 67 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
69 | 68 | fveq2d 6195 |
. . . . . . . . . . . 12
|
70 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
71 | 70 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
72 | 71 | oveq2d 6666 |
. . . . . . . . . . . 12
|
73 | 69, 72 | breq12d 4666 |
. . . . . . . . . . 11
|
74 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
75 | 74 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
76 | 75 | fveq2d 6195 |
. . . . . . . . . . . 12
|
77 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
78 | 77 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
79 | 78 | oveq2d 6666 |
. . . . . . . . . . . 12
|
80 | 76, 79 | breq12d 4666 |
. . . . . . . . . . 11
|
81 | 73, 80 | rspc2v 3322 |
. . . . . . . . . 10
|
82 | 53, 66, 81 | syl2anc 693 |
. . . . . . . . 9
|
83 | | simp1l 1085 |
. . . . . . . . . . . . . 14
|
84 | | aalioulem3.e |
. . . . . . . . . . . . . 14
|
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . 13
|
86 | | 0cn 10032 |
. . . . . . . . . . . . 13
|
87 | 85, 86 | syl6eqel 2709 |
. . . . . . . . . . . 12
|
88 | 37 | adantr 481 |
. . . . . . . . . . . . . 14
|
89 | 88 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
90 | 89, 43 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
91 | 87, 90 | abssubd 14192 |
. . . . . . . . . . 11
|
92 | 85 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
93 | 90 | subid1d 10381 |
. . . . . . . . . . . . 13
|
94 | 92, 93 | eqtrd 2656 |
. . . . . . . . . . . 12
|
95 | 94 | fveq2d 6195 |
. . . . . . . . . . 11
|
96 | 91, 95 | eqtrd 2656 |
. . . . . . . . . 10
|
97 | 96 | breq1d 4663 |
. . . . . . . . 9
|
98 | 82, 97 | sylibd 229 |
. . . . . . . 8
|
99 | 98 | 3exp 1264 |
. . . . . . 7
|
100 | 99 | com34 91 |
. . . . . 6
|
101 | 100 | com23 86 |
. . . . 5
|
102 | 101 | ralrimdv 2968 |
. . . 4
|
103 | 102 | reximdva 3017 |
. . 3
|
104 | 41, 103 | mpd 15 |
. 2
|
105 | | 1rp 11836 |
. . . . . 6
|
106 | 105 | a1i 11 |
. . . . 5
|
107 | | recn 10026 |
. . . . . . . 8
|
108 | 107 | adantl 482 |
. . . . . . 7
|
109 | | df-ne 2795 |
. . . . . . . 8
|
110 | 109 | biimpri 218 |
. . . . . . 7
|
111 | | absrpcl 14028 |
. . . . . . 7
|
112 | 108, 110,
111 | syl2an 494 |
. . . . . 6
|
113 | 112 | rpreccld 11882 |
. . . . 5
|
114 | 106, 113 | ifclda 4120 |
. . . 4
|
115 | | eqid 2622 |
. . . . . . . . 9
|
116 | | eqif 4126 |
. . . . . . . . 9
|
117 | 115, 116 | mpbi 220 |
. . . . . . . 8
|
118 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
|
119 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
120 | 119 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
121 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
122 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
123 | 121, 122 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . . 22
|
124 | 123 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
|
125 | 124 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . 20
|
126 | 125 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
|
127 | 126 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
128 | 127 | mul02d 10234 |
. . . . . . . . . . . . . . . . 17
|
129 | 120, 128 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
130 | 118, 129 | breqtrd 4679 |
. . . . . . . . . . . . . . 15
|
131 | 37 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
132 | 122 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
133 | 131, 132 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
|
134 | 133 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
135 | 134 | absge0d 14183 |
. . . . . . . . . . . . . . 15
|
136 | 133 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
|
137 | 136 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
138 | | 0re 10040 |
. . . . . . . . . . . . . . . 16
|
139 | | letri3 10123 |
. . . . . . . . . . . . . . . 16
|
140 | 137, 138,
139 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
141 | 130, 135,
140 | mpbir2and 957 |
. . . . . . . . . . . . . 14
|
142 | 141 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
143 | | ax-1cn 9994 |
. . . . . . . . . . . . . 14
|
144 | 143 | mul01i 10226 |
. . . . . . . . . . . . 13
|
145 | 142, 144 | syl6eq 2672 |
. . . . . . . . . . . 12
|
146 | 124 | adantr 481 |
. . . . . . . . . . . . 13
|
147 | 146 | absge0d 14183 |
. . . . . . . . . . . 12
|
148 | 145, 147 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
149 | | oveq1 6657 |
. . . . . . . . . . . 12
|
150 | 149 | breq1d 4663 |
. . . . . . . . . . 11
|
151 | 148, 150 | syl5ibrcom 237 |
. . . . . . . . . 10
|
152 | 151 | expimpd 629 |
. . . . . . . . 9
|
153 | 136 | adantr 481 |
. . . . . . . . . . . . . . 15
|
154 | 153 | recnd 10068 |
. . . . . . . . . . . . . 14
|
155 | | simpllr 799 |
. . . . . . . . . . . . . . . . 17
|
156 | 155 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
157 | 156, 111 | sylancom 701 |
. . . . . . . . . . . . . . 15
|
158 | 157 | rpcnne0d 11881 |
. . . . . . . . . . . . . 14
|
159 | | divrec2 10702 |
. . . . . . . . . . . . . . 15
|
160 | 159 | 3expb 1266 |
. . . . . . . . . . . . . 14
|
161 | 154, 158,
160 | syl2anc 693 |
. . . . . . . . . . . . 13
|
162 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
|
163 | 162, 125 | remulcld 10070 |
. . . . . . . . . . . . . . . 16
|
164 | 162 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
165 | 164 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
|
166 | 165, 125 | remulcld 10070 |
. . . . . . . . . . . . . . . 16
|
167 | | simprr 796 |
. . . . . . . . . . . . . . . 16
|
168 | 124 | absge0d 14183 |
. . . . . . . . . . . . . . . . 17
|
169 | | leabs 14039 |
. . . . . . . . . . . . . . . . . 18
|
170 | 169 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
|
171 | 162, 165,
125, 168, 170 | lemul1ad 10963 |
. . . . . . . . . . . . . . . 16
|
172 | 136, 163,
166, 167, 171 | letrd 10194 |
. . . . . . . . . . . . . . 15
|
173 | 172 | adantr 481 |
. . . . . . . . . . . . . 14
|
174 | 125 | adantr 481 |
. . . . . . . . . . . . . . 15
|
175 | 153, 174,
157 | ledivmuld 11925 |
. . . . . . . . . . . . . 14
|
176 | 173, 175 | mpbird 247 |
. . . . . . . . . . . . 13
|
177 | 161, 176 | eqbrtrrd 4677 |
. . . . . . . . . . . 12
|
178 | 109, 177 | sylan2br 493 |
. . . . . . . . . . 11
|
179 | | oveq1 6657 |
. . . . . . . . . . . 12
|
180 | 179 | breq1d 4663 |
. . . . . . . . . . 11
|
181 | 178, 180 | syl5ibrcom 237 |
. . . . . . . . . 10
|
182 | 181 | expimpd 629 |
. . . . . . . . 9
|
183 | 152, 182 | jaod 395 |
. . . . . . . 8
|
184 | 117, 183 | mpi 20 |
. . . . . . 7
|
185 | 184 | expr 643 |
. . . . . 6
|
186 | 185 | imim2d 57 |
. . . . 5
|
187 | 186 | ralimdva 2962 |
. . . 4
|
188 | | oveq1 6657 |
. . . . . . . 8
|
189 | 188 | breq1d 4663 |
. . . . . . 7
|
190 | 189 | imbi2d 330 |
. . . . . 6
|
191 | 190 | ralbidv 2986 |
. . . . 5
|
192 | 191 | rspcev 3309 |
. . . 4
|
193 | 114, 187,
192 | syl6an 568 |
. . 3
|
194 | 193 | rexlimdva 3031 |
. 2
|
195 | 104, 194 | mpd 15 |
1
|