Metamath Proof Explorer


Theorem aalioulem3

Description: Lemma for aaliou . (Contributed by Stefan O'Rear, 15-Nov-2014)

Ref Expression
Hypotheses aalioulem2.a N = deg F
aalioulem2.b φ F Poly
aalioulem2.c φ N
aalioulem2.d φ A
aalioulem3.e φ F A = 0
Assertion aalioulem3 φ x + r A r 1 x F r A r

Proof

Step Hyp Ref Expression
1 aalioulem2.a N = deg F
2 aalioulem2.b φ F Poly
3 aalioulem2.c φ N
4 aalioulem2.d φ A
5 aalioulem3.e φ F A = 0
6 1re 1
7 resubcl A 1 A 1
8 4 6 7 sylancl φ A 1
9 peano2re A A + 1
10 4 9 syl φ A + 1
11 reelprrecn
12 ssid
13 fncpn C n Fn 0
14 12 13 ax-mp C n Fn 0
15 1nn0 1 0
16 fnfvelrn C n Fn 0 1 0 C n 1 ran C n
17 14 15 16 mp2an C n 1 ran C n
18 intss1 C n 1 ran C n ran C n C n 1
19 17 18 ax-mp ran C n C n 1
20 plycpn F Poly F ran C n
21 2 20 syl φ F ran C n
22 19 21 sseldi φ F C n 1
23 cpnres F C n 1 F C n 1
24 11 22 23 sylancr φ F C n 1
25 df-ima F = ran F
26 zssre
27 ax-resscn
28 plyss Poly Poly
29 26 27 28 mp2an Poly Poly
30 29 2 sseldi φ F Poly
31 plyreres F Poly F :
32 30 31 syl φ F :
33 32 frnd φ ran F
34 25 33 eqsstrid φ F
35 iccssre A 1 A + 1 A 1 A + 1
36 8 10 35 syl2anc φ A 1 A + 1
37 36 27 sstrdi φ A 1 A + 1
38 plyf F Poly F :
39 2 38 syl φ F :
40 39 fdmd φ dom F =
41 37 40 sseqtrrd φ A 1 A + 1 dom F
42 8 10 24 34 41 c1lip3 φ a b A 1 A + 1 c A 1 A + 1 F c F b a c b
43 simp2 φ a r A r 1 r
44 43 recnd φ a r A r 1 r
45 4 adantr φ a A
46 45 3ad2ant1 φ a r A r 1 A
47 46 recnd φ a r A r 1 A
48 44 47 abssubd φ a r A r 1 r A = A r
49 simp3 φ a r A r 1 A r 1
50 48 49 eqbrtrd φ a r A r 1 r A 1
51 1red φ a r A r 1 1
52 elicc4abs A 1 r r A 1 A + 1 r A 1
53 46 51 43 52 syl3anc φ a r A r 1 r A 1 A + 1 r A 1
54 50 53 mpbird φ a r A r 1 r A 1 A + 1
55 4 recnd φ A
56 55 subidd φ A A = 0
57 56 fveq2d φ A A = 0
58 abs0 0 = 0
59 0le1 0 1
60 58 59 eqbrtri 0 1
61 57 60 eqbrtrdi φ A A 1
62 1red φ 1
63 elicc4abs A 1 A A A 1 A + 1 A A 1
64 4 62 4 63 syl3anc φ A A 1 A + 1 A A 1
65 61 64 mpbird φ A A 1 A + 1
66 65 adantr φ a A A 1 A + 1
67 66 3ad2ant1 φ a r A r 1 A A 1 A + 1
68 fveq2 b = r F b = F r
69 68 oveq2d b = r F c F b = F c F r
70 69 fveq2d b = r F c F b = F c F r
71 oveq2 b = r c b = c r
72 71 fveq2d b = r c b = c r
73 72 oveq2d b = r a c b = a c r
74 70 73 breq12d b = r F c F b a c b F c F r a c r
75 fveq2 c = A F c = F A
76 75 fvoveq1d c = A F c F r = F A F r
77 fvoveq1 c = A c r = A r
78 77 oveq2d c = A a c r = a A r
79 76 78 breq12d c = A F c F r a c r F A F r a A r
80 74 79 rspc2v r A 1 A + 1 A A 1 A + 1 b A 1 A + 1 c A 1 A + 1 F c F b a c b F A F r a A r
81 54 67 80 syl2anc φ a r A r 1 b A 1 A + 1 c A 1 A + 1 F c F b a c b F A F r a A r
82 simp1l φ a r A r 1 φ
83 82 5 syl φ a r A r 1 F A = 0
84 0cn 0
85 83 84 eqeltrdi φ a r A r 1 F A
86 39 adantr φ a F :
87 86 3ad2ant1 φ a r A r 1 F :
88 87 44 ffvelrnd φ a r A r 1 F r
89 85 88 abssubd φ a r A r 1 F A F r = F r F A
90 83 oveq2d φ a r A r 1 F r F A = F r 0
91 88 subid1d φ a r A r 1 F r 0 = F r
92 90 91 eqtrd φ a r A r 1 F r F A = F r
93 92 fveq2d φ a r A r 1 F r F A = F r
94 89 93 eqtrd φ a r A r 1 F A F r = F r
95 94 breq1d φ a r A r 1 F A F r a A r F r a A r
96 81 95 sylibd φ a r A r 1 b A 1 A + 1 c A 1 A + 1 F c F b a c b F r a A r
97 96 3exp φ a r A r 1 b A 1 A + 1 c A 1 A + 1 F c F b a c b F r a A r
98 97 com34 φ a r b A 1 A + 1 c A 1 A + 1 F c F b a c b A r 1 F r a A r
99 98 com23 φ a b A 1 A + 1 c A 1 A + 1 F c F b a c b r A r 1 F r a A r
100 99 ralrimdv φ a b A 1 A + 1 c A 1 A + 1 F c F b a c b r A r 1 F r a A r
101 100 reximdva φ a b A 1 A + 1 c A 1 A + 1 F c F b a c b a r A r 1 F r a A r
102 42 101 mpd φ a r A r 1 F r a A r
103 1rp 1 +
104 103 a1i φ a a = 0 1 +
105 recn a a
106 105 adantl φ a a
107 neqne ¬ a = 0 a 0
108 absrpcl a a 0 a +
109 106 107 108 syl2an φ a ¬ a = 0 a +
110 109 rpreccld φ a ¬ a = 0 1 a +
111 104 110 ifclda φ a if a = 0 1 1 a +
112 eqid if a = 0 1 1 a = if a = 0 1 1 a
113 eqif if a = 0 1 1 a = if a = 0 1 1 a a = 0 if a = 0 1 1 a = 1 ¬ a = 0 if a = 0 1 1 a = 1 a
114 112 113 mpbi a = 0 if a = 0 1 1 a = 1 ¬ a = 0 if a = 0 1 1 a = 1 a
115 simplrr φ a r F r a A r a = 0 F r a A r
116 oveq1 a = 0 a A r = 0 A r
117 116 adantl φ a r F r a A r a = 0 a A r = 0 A r
118 4 ad2antrr φ a r F r a A r A
119 simprl φ a r F r a A r r
120 118 119 resubcld φ a r F r a A r A r
121 120 recnd φ a r F r a A r A r
122 121 abscld φ a r F r a A r A r
123 122 recnd φ a r F r a A r A r
124 123 adantr φ a r F r a A r a = 0 A r
125 124 mul02d φ a r F r a A r a = 0 0 A r = 0
126 117 125 eqtrd φ a r F r a A r a = 0 a A r = 0
127 115 126 breqtrd φ a r F r a A r a = 0 F r 0
128 39 ad2antrr φ a r F r a A r F :
129 119 recnd φ a r F r a A r r
130 128 129 ffvelrnd φ a r F r a A r F r
131 130 adantr φ a r F r a A r a = 0 F r
132 131 absge0d φ a r F r a A r a = 0 0 F r
133 130 abscld φ a r F r a A r F r
134 133 adantr φ a r F r a A r a = 0 F r
135 0re 0
136 letri3 F r 0 F r = 0 F r 0 0 F r
137 134 135 136 sylancl φ a r F r a A r a = 0 F r = 0 F r 0 0 F r
138 127 132 137 mpbir2and φ a r F r a A r a = 0 F r = 0
139 138 oveq2d φ a r F r a A r a = 0 1 F r = 1 0
140 ax-1cn 1
141 140 mul01i 1 0 = 0
142 139 141 syl6eq φ a r F r a A r a = 0 1 F r = 0
143 121 adantr φ a r F r a A r a = 0 A r
144 143 absge0d φ a r F r a A r a = 0 0 A r
145 142 144 eqbrtrd φ a r F r a A r a = 0 1 F r A r
146 oveq1 if a = 0 1 1 a = 1 if a = 0 1 1 a F r = 1 F r
147 146 breq1d if a = 0 1 1 a = 1 if a = 0 1 1 a F r A r 1 F r A r
148 145 147 syl5ibrcom φ a r F r a A r a = 0 if a = 0 1 1 a = 1 if a = 0 1 1 a F r A r
149 148 expimpd φ a r F r a A r a = 0 if a = 0 1 1 a = 1 if a = 0 1 1 a F r A r
150 df-ne a 0 ¬ a = 0
151 133 adantr φ a r F r a A r a 0 F r
152 151 recnd φ a r F r a A r a 0 F r
153 simpllr φ a r F r a A r a 0 a
154 153 recnd φ a r F r a A r a 0 a
155 154 108 sylancom φ a r F r a A r a 0 a +
156 155 rpcnne0d φ a r F r a A r a 0 a a 0
157 divrec2 F r a a 0 F r a = 1 a F r
158 157 3expb F r a a 0 F r a = 1 a F r
159 152 156 158 syl2anc φ a r F r a A r a 0 F r a = 1 a F r
160 simplr φ a r F r a A r a
161 160 122 remulcld φ a r F r a A r a A r
162 160 recnd φ a r F r a A r a
163 162 abscld φ a r F r a A r a
164 163 122 remulcld φ a r F r a A r a A r
165 simprr φ a r F r a A r F r a A r
166 121 absge0d φ a r F r a A r 0 A r
167 leabs a a a
168 167 ad2antlr φ a r F r a A r a a
169 160 163 122 166 168 lemul1ad φ a r F r a A r a A r a A r
170 133 161 164 165 169 letrd φ a r F r a A r F r a A r
171 170 adantr φ a r F r a A r a 0 F r a A r
172 122 adantr φ a r F r a A r a 0 A r
173 151 172 155 ledivmuld φ a r F r a A r a 0 F r a A r F r a A r
174 171 173 mpbird φ a r F r a A r a 0 F r a A r
175 159 174 eqbrtrrd φ a r F r a A r a 0 1 a F r A r
176 150 175 sylan2br φ a r F r a A r ¬ a = 0 1 a F r A r
177 oveq1 if a = 0 1 1 a = 1 a if a = 0 1 1 a F r = 1 a F r
178 177 breq1d if a = 0 1 1 a = 1 a if a = 0 1 1 a F r A r 1 a F r A r
179 176 178 syl5ibrcom φ a r F r a A r ¬ a = 0 if a = 0 1 1 a = 1 a if a = 0 1 1 a F r A r
180 179 expimpd φ a r F r a A r ¬ a = 0 if a = 0 1 1 a = 1 a if a = 0 1 1 a F r A r
181 149 180 jaod φ a r F r a A r a = 0 if a = 0 1 1 a = 1 ¬ a = 0 if a = 0 1 1 a = 1 a if a = 0 1 1 a F r A r
182 114 181 mpi φ a r F r a A r if a = 0 1 1 a F r A r
183 182 expr φ a r F r a A r if a = 0 1 1 a F r A r
184 183 imim2d φ a r A r 1 F r a A r A r 1 if a = 0 1 1 a F r A r
185 184 ralimdva φ a r A r 1 F r a A r r A r 1 if a = 0 1 1 a F r A r
186 oveq1 x = if a = 0 1 1 a x F r = if a = 0 1 1 a F r
187 186 breq1d x = if a = 0 1 1 a x F r A r if a = 0 1 1 a F r A r
188 187 imbi2d x = if a = 0 1 1 a A r 1 x F r A r A r 1 if a = 0 1 1 a F r A r
189 188 ralbidv x = if a = 0 1 1 a r A r 1 x F r A r r A r 1 if a = 0 1 1 a F r A r
190 189 rspcev if a = 0 1 1 a + r A r 1 if a = 0 1 1 a F r A r x + r A r 1 x F r A r
191 111 185 190 syl6an φ a r A r 1 F r a A r x + r A r 1 x F r A r
192 191 rexlimdva φ a r A r 1 F r a A r x + r A r 1 x F r A r
193 102 192 mpd φ x + r A r 1 x F r A r