Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elaa2lem Structured version   Visualization version   GIF version

Theorem elaa2lem 44369
Description: Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 44370. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 1-Oct-2020.)
Hypotheses
Ref Expression
elaa2lem.a (𝜑𝐴 ∈ 𝔸)
elaa2lem.an0 (𝜑𝐴 ≠ 0)
elaa2lem.g (𝜑𝐺 ∈ (Poly‘ℤ))
elaa2lem.gn0 (𝜑𝐺 ≠ 0𝑝)
elaa2lem.ga (𝜑 → (𝐺𝐴) = 0)
elaa2lem.m 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )
elaa2lem.i 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀)))
elaa2lem.f 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘)))
Assertion
Ref Expression
elaa2lem (𝜑 → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓𝐴) = 0))
Distinct variable groups:   𝐴,𝑓   𝐴,𝑘,𝑧   𝑓,𝐹   𝑘,𝐺   𝑛,𝐺   𝑧,𝐺   𝑘,𝐼,𝑧   𝑘,𝑀   𝑛,𝑀   𝑧,𝑀   𝜑,𝑘,𝑧
Allowed substitution hints:   𝜑(𝑓,𝑛)   𝐴(𝑛)   𝐹(𝑧,𝑘,𝑛)   𝐺(𝑓)   𝐼(𝑓,𝑛)   𝑀(𝑓)

Proof of Theorem elaa2lem
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 elaa2lem.f . . . 4 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘)))
21a1i 11 . . 3 (𝜑𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘))))
3 zsscn 12465 . . . . 5 ℤ ⊆ ℂ
43a1i 11 . . . 4 (𝜑 → ℤ ⊆ ℂ)
5 elaa2lem.g . . . . . . . . 9 (𝜑𝐺 ∈ (Poly‘ℤ))
6 dgrcl 25540 . . . . . . . . 9 (𝐺 ∈ (Poly‘ℤ) → (deg‘𝐺) ∈ ℕ0)
75, 6syl 17 . . . . . . . 8 (𝜑 → (deg‘𝐺) ∈ ℕ0)
87nn0zd 12483 . . . . . . 7 (𝜑 → (deg‘𝐺) ∈ ℤ)
9 elaa2lem.m . . . . . . . . 9 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )
10 ssrab2 4035 . . . . . . . . . 10 {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ ℕ0
11 nn0uz 12759 . . . . . . . . . . . . 13 0 = (ℤ‘0)
1210, 11sseqtri 3978 . . . . . . . . . . . 12 {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ‘0)
1312a1i 11 . . . . . . . . . . 11 (𝜑 → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ‘0))
14 elaa2lem.gn0 . . . . . . . . . . . . . . . . 17 (𝜑𝐺 ≠ 0𝑝)
1514neneqd 2946 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ 𝐺 = 0𝑝)
16 eqid 2736 . . . . . . . . . . . . . . . . . 18 (deg‘𝐺) = (deg‘𝐺)
17 eqid 2736 . . . . . . . . . . . . . . . . . 18 (coeff‘𝐺) = (coeff‘𝐺)
1816, 17dgreq0 25572 . . . . . . . . . . . . . . . . 17 (𝐺 ∈ (Poly‘ℤ) → (𝐺 = 0𝑝 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) = 0))
195, 18syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺 = 0𝑝 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) = 0))
2015, 19mtbid 323 . . . . . . . . . . . . . . 15 (𝜑 → ¬ ((coeff‘𝐺)‘(deg‘𝐺)) = 0)
2120neqned 2948 . . . . . . . . . . . . . 14 (𝜑 → ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)
227, 21jca 512 . . . . . . . . . . . . 13 (𝜑 → ((deg‘𝐺) ∈ ℕ0 ∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
23 fveq2 6839 . . . . . . . . . . . . . . 15 (𝑛 = (deg‘𝐺) → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘(deg‘𝐺)))
2423neeq1d 3001 . . . . . . . . . . . . . 14 (𝑛 = (deg‘𝐺) → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
2524elrab 3643 . . . . . . . . . . . . 13 ((deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ ((deg‘𝐺) ∈ ℕ0 ∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
2622, 25sylibr 233 . . . . . . . . . . . 12 (𝜑 → (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
2726ne0d 4293 . . . . . . . . . . 11 (𝜑 → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅)
28 infssuzcl 12811 . . . . . . . . . . 11 (({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ‘0) ∧ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
2913, 27, 28syl2anc 584 . . . . . . . . . 10 (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
3010, 29sselid 3940 . . . . . . . . 9 (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ ℕ0)
319, 30eqeltrid 2842 . . . . . . . 8 (𝜑𝑀 ∈ ℕ0)
3231nn0zd 12483 . . . . . . 7 (𝜑𝑀 ∈ ℤ)
338, 32zsubcld 12570 . . . . . 6 (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℤ)
349a1i 11 . . . . . . . 8 (𝜑𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ))
35 infssuzle 12810 . . . . . . . . 9 (({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ‘0) ∧ (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ (deg‘𝐺))
3613, 26, 35syl2anc 584 . . . . . . . 8 (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ (deg‘𝐺))
3734, 36eqbrtrd 5125 . . . . . . 7 (𝜑𝑀 ≤ (deg‘𝐺))
387nn0red 12432 . . . . . . . 8 (𝜑 → (deg‘𝐺) ∈ ℝ)
3931nn0red 12432 . . . . . . . 8 (𝜑𝑀 ∈ ℝ)
4038, 39subge0d 11703 . . . . . . 7 (𝜑 → (0 ≤ ((deg‘𝐺) − 𝑀) ↔ 𝑀 ≤ (deg‘𝐺)))
4137, 40mpbird 256 . . . . . 6 (𝜑 → 0 ≤ ((deg‘𝐺) − 𝑀))
4233, 41jca 512 . . . . 5 (𝜑 → (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤ ((deg‘𝐺) − 𝑀)))
43 elnn0z 12470 . . . . 5 (((deg‘𝐺) − 𝑀) ∈ ℕ0 ↔ (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤ ((deg‘𝐺) − 𝑀)))
4442, 43sylibr 233 . . . 4 (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℕ0)
45 0zd 12469 . . . . . . . 8 (𝐺 ∈ (Poly‘ℤ) → 0 ∈ ℤ)
4617coef2 25538 . . . . . . . 8 ((𝐺 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → (coeff‘𝐺):ℕ0⟶ℤ)
475, 45, 46syl2anc2 585 . . . . . . 7 (𝜑 → (coeff‘𝐺):ℕ0⟶ℤ)
4847adantr 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (coeff‘𝐺):ℕ0⟶ℤ)
49 simpr 485 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
5031adantr 481 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝑀 ∈ ℕ0)
5149, 50nn0addcld 12435 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑘 + 𝑀) ∈ ℕ0)
5248, 51ffvelcdmd 7032 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ)
53 elaa2lem.i . . . . 5 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀)))
5452, 53fmptd 7058 . . . 4 (𝜑𝐼:ℕ0⟶ℤ)
55 elplyr 25508 . . . 4 ((ℤ ⊆ ℂ ∧ ((deg‘𝐺) − 𝑀) ∈ ℕ0𝐼:ℕ0⟶ℤ) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘))) ∈ (Poly‘ℤ))
564, 44, 54, 55syl3anc 1371 . . 3 (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘))) ∈ (Poly‘ℤ))
572, 56eqeltrd 2838 . 2 (𝜑𝐹 ∈ (Poly‘ℤ))
58 simpr 485 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ≤ ((deg‘𝐺) − 𝑀))
5958iftrued 4492 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
60 iffalse 4493 . . . . . . . . . . 11 𝑘 ≤ ((deg‘𝐺) − 𝑀) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0)
6160adantl 482 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0)
62 simpr 485 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀))
6338ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) ∈ ℝ)
6439ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑀 ∈ ℝ)
6563, 64resubcld 11541 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) ∈ ℝ)
66 nn0re 12380 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
6766ad2antlr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℝ)
6865, 67ltnled 11260 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)))
6962, 68mpbird 256 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) < 𝑘)
7063, 64, 67ltsubaddd 11709 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ (deg‘𝐺) < (𝑘 + 𝑀)))
7169, 70mpbid 231 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) < (𝑘 + 𝑀))
72 olc 866 . . . . . . . . . . . . 13 ((deg‘𝐺) < (𝑘 + 𝑀) → (𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)))
7371, 72syl 17 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)))
745ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝐺 ∈ (Poly‘ℤ))
7551adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝑘 + 𝑀) ∈ ℕ0)
7616, 17dgrlt 25573 . . . . . . . . . . . . 13 ((𝐺 ∈ (Poly‘ℤ) ∧ (𝑘 + 𝑀) ∈ ℕ0) → ((𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)))
7774, 75, 76syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)))
7873, 77mpbid 231 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0))
7978simprd 496 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)
8061, 79eqtr4d 2779 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
8159, 80pm2.61dan 811 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
8281mpteq2dva 5203 . . . . . . 7 (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)) = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))))
8347, 4fssd 6683 . . . . . . . . . 10 (𝜑 → (coeff‘𝐺):ℕ0⟶ℂ)
8483adantr 481 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (coeff‘𝐺):ℕ0⟶ℂ)
85 elfznn0 13488 . . . . . . . . . . 11 (𝑘 ∈ (0...((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℕ0)
8685adantl 482 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑘 ∈ ℕ0)
8731adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑀 ∈ ℕ0)
8886, 87nn0addcld 12435 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑘 + 𝑀) ∈ ℕ0)
8984, 88ffvelcdmd 7032 . . . . . . . 8 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℂ)
90 eqidd 2737 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ℂ) → (0...((deg‘𝐺) − 𝑀)) = (0...((deg‘𝐺) − 𝑀)))
91 simpl 483 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝜑)
9253a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))))
9392, 52fvmpt2d 6958 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → (𝐼𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
9491, 86, 93syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
9594adantlr 713 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
9695oveq1d 7366 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼𝑘) · (𝑧𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧𝑘)))
9790, 96sumeq12rdv 15546 . . . . . . . . . 10 ((𝜑𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧𝑘)))
9897mpteq2dva 5203 . . . . . . . . 9 (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧𝑘))))
992, 98eqtrd 2776 . . . . . . . 8 (𝜑𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧𝑘))))
10057, 44, 89, 99coeeq2 25549 . . . . . . 7 (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)))
10182, 100, 923eqtr4d 2786 . . . . . 6 (𝜑 → (coeff‘𝐹) = 𝐼)
102101fveq1d 6841 . . . . 5 (𝜑 → ((coeff‘𝐹)‘0) = (𝐼‘0))
103 oveq1 7358 . . . . . . . . 9 (𝑘 = 0 → (𝑘 + 𝑀) = (0 + 𝑀))
104103adantl 482 . . . . . . . 8 ((𝜑𝑘 = 0) → (𝑘 + 𝑀) = (0 + 𝑀))
1053, 32sselid 3940 . . . . . . . . . 10 (𝜑𝑀 ∈ ℂ)
106105addid2d 11314 . . . . . . . . 9 (𝜑 → (0 + 𝑀) = 𝑀)
107106adantr 481 . . . . . . . 8 ((𝜑𝑘 = 0) → (0 + 𝑀) = 𝑀)
108104, 107eqtrd 2776 . . . . . . 7 ((𝜑𝑘 = 0) → (𝑘 + 𝑀) = 𝑀)
109108fveq2d 6843 . . . . . 6 ((𝜑𝑘 = 0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘𝑀))
110 0nn0 12386 . . . . . . 7 0 ∈ ℕ0
111110a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℕ0)
11247, 31ffvelcdmd 7032 . . . . . 6 (𝜑 → ((coeff‘𝐺)‘𝑀) ∈ ℤ)
11392, 109, 111, 112fvmptd 6952 . . . . 5 (𝜑 → (𝐼‘0) = ((coeff‘𝐺)‘𝑀))
114 eqidd 2737 . . . . 5 (𝜑 → ((coeff‘𝐺)‘𝑀) = ((coeff‘𝐺)‘𝑀))
115102, 113, 1143eqtrd 2780 . . . 4 (𝜑 → ((coeff‘𝐹)‘0) = ((coeff‘𝐺)‘𝑀))
11634, 29eqeltrd 2838 . . . . . 6 (𝜑𝑀 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
117 fveq2 6839 . . . . . . . 8 (𝑛 = 𝑀 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑀))
118117neeq1d 3001 . . . . . . 7 (𝑛 = 𝑀 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑀) ≠ 0))
119118elrab 3643 . . . . . 6 (𝑀 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑀 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑀) ≠ 0))
120116, 119sylib 217 . . . . 5 (𝜑 → (𝑀 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑀) ≠ 0))
121120simprd 496 . . . 4 (𝜑 → ((coeff‘𝐺)‘𝑀) ≠ 0)
122115, 121eqnetrd 3009 . . 3 (𝜑 → ((coeff‘𝐹)‘0) ≠ 0)
1235, 45syl 17 . . . . . . 7 (𝜑 → 0 ∈ ℤ)
124 aasscn 25624 . . . . . . . . . . 11 𝔸 ⊆ ℂ
125 elaa2lem.a . . . . . . . . . . 11 (𝜑𝐴 ∈ 𝔸)
126124, 125sselid 3940 . . . . . . . . . 10 (𝜑𝐴 ∈ ℂ)
12791, 126syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝐴 ∈ ℂ)
128127, 86expcld 14005 . . . . . . . 8 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐴𝑘) ∈ ℂ)
12989, 128mulcld 11133 . . . . . . 7 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)) ∈ ℂ)
130 fvoveq1 7374 . . . . . . . 8 (𝑘 = (𝑗𝑀) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)))
131 oveq2 7359 . . . . . . . 8 (𝑘 = (𝑗𝑀) → (𝐴𝑘) = (𝐴↑(𝑗𝑀)))
132130, 131oveq12d 7369 . . . . . . 7 (𝑘 = (𝑗𝑀) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)) = (((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))))
13332, 123, 33, 129, 132fsumshft 15619 . . . . . 6 (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)) = Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))))
1343, 8sselid 3940 . . . . . . . . . 10 (𝜑 → (deg‘𝐺) ∈ ℂ)
135134, 105npcand 11474 . . . . . . . . 9 (𝜑 → (((deg‘𝐺) − 𝑀) + 𝑀) = (deg‘𝐺))
136106, 135oveq12d 7369 . . . . . . . 8 (𝜑 → ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀)) = (𝑀...(deg‘𝐺)))
137136sumeq1d 15540 . . . . . . 7 (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))))
138 elfzelz 13395 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑗 ∈ ℤ)
139138adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ)
1403, 139sselid 3940 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℂ)
141105adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℂ)
142140, 141npcand 11474 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → ((𝑗𝑀) + 𝑀) = 𝑗)
143142fveq2d 6843 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) = ((coeff‘𝐺)‘𝑗))
144143oveq1d 7366 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗𝑀))))
145126adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝐴 ∈ ℂ)
146 elaa2lem.an0 . . . . . . . . . . . . 13 (𝜑𝐴 ≠ 0)
147146adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝐴 ≠ 0)
14832adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℤ)
149145, 147, 148, 139expsubd 14016 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑(𝑗𝑀)) = ((𝐴𝑗) / (𝐴𝑀)))
150149oveq2d 7367 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗𝑀))) = (((coeff‘𝐺)‘𝑗) · ((𝐴𝑗) / (𝐴𝑀))))
15183adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ)
152 0red 11116 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ∈ ℝ)
15339adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℝ)
154139zred 12565 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ)
15531nn0ge0d 12434 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ 𝑀)
156155adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑀)
157 elfzle1 13398 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑀𝑗)
158157adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀𝑗)
159152, 153, 154, 156, 158letrd 11270 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑗)
160139, 159jca 512 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
161 elnn0z 12470 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
162160, 161sylibr 233 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0)
163151, 162ffvelcdmd 7032 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ)
164145, 162expcld 14005 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴𝑗) ∈ ℂ)
165126, 31expcld 14005 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝑀) ∈ ℂ)
166165adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴𝑀) ∈ ℂ)
167145, 147, 148expne0d 14011 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴𝑀) ≠ 0)
168163, 164, 166, 167divassd 11924 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) = (((coeff‘𝐺)‘𝑗) · ((𝐴𝑗) / (𝐴𝑀))))
169168eqcomd 2742 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · ((𝐴𝑗) / (𝐴𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
170150, 169eqtr2d 2777 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗𝑀))))
171144, 170eqtr4d 2779 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
172171sumeq2dv 15542 . . . . . . 7 (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
173137, 172eqtrd 2776 . . . . . 6 (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
17431, 11eleqtrdi 2848 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘0))
175 fzss1 13434 . . . . . . . 8 (𝑀 ∈ (ℤ‘0) → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺)))
176174, 175syl 17 . . . . . . 7 (𝜑 → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺)))
177163, 164mulcld 11133 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) ∈ ℂ)
178177, 166, 167divcld 11889 . . . . . . 7 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) ∈ ℂ)
17932ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℤ)
1808ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (deg‘𝐺) ∈ ℤ)
181 eldifi 4084 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ (0...(deg‘𝐺)))
182181elfzelzd 13396 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ)
183182ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℤ)
184 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 < 𝑀)
18539ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℝ)
186183zred 12565 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℝ)
187185, 186lenltd 11259 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (𝑀𝑗 ↔ ¬ 𝑗 < 𝑀))
188184, 187mpbird 256 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀𝑗)
189 elfzle2 13399 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ≤ (deg‘𝐺))
190181, 189syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ≤ (deg‘𝐺))
191190ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ≤ (deg‘𝐺))
192179, 180, 183, 188, 191elfzd 13386 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ (𝑀...(deg‘𝐺)))
193 eldifn 4085 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺)))
194193ad2antlr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺)))
195192, 194condan 816 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 < 𝑀)
196195adantr 481 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 < 𝑀)
1979a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ))
19812a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ‘0))
199 elfznn0 13488 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ∈ ℕ0)
200181, 199syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0)
201200adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℕ0)
202 neqne 2949 . . . . . . . . . . . . . . . . . . 19 (¬ ((coeff‘𝐺)‘𝑗) = 0 → ((coeff‘𝐺)‘𝑗) ≠ 0)
203202adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ((coeff‘𝐺)‘𝑗) ≠ 0)
204201, 203jca 512 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑗 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑗) ≠ 0))
205 fveq2 6839 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑗 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑗))
206205neeq1d 3001 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑗 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑗) ≠ 0))
207206elrab 3643 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑗 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑗) ≠ 0))
208204, 207sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
209208adantll 712 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
210 infssuzle 12810 . . . . . . . . . . . . . . 15 (({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ‘0) ∧ 𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗)
211198, 209, 210syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗)
212197, 211eqbrtrd 5125 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀𝑗)
21339ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ∈ ℝ)
214182zred 12565 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ)
215214ad2antlr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℝ)
216213, 215lenltd 11259 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑀𝑗 ↔ ¬ 𝑗 < 𝑀))
217212, 216mpbid 231 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ¬ 𝑗 < 𝑀)
218196, 217condan 816 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((coeff‘𝐺)‘𝑗) = 0)
219218oveq1d 7366 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) = (0 · (𝐴𝑗)))
220126adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝐴 ∈ ℂ)
221200adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 ∈ ℕ0)
222220, 221expcld 14005 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (𝐴𝑗) ∈ ℂ)
223222mul02d 11311 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 · (𝐴𝑗)) = 0)
224219, 223eqtrd 2776 . . . . . . . . 9 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) = 0)
225224oveq1d 7366 . . . . . . . 8 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) = (0 / (𝐴𝑀)))
226126, 146, 32expne0d 14011 . . . . . . . . . 10 (𝜑 → (𝐴𝑀) ≠ 0)
227165, 226div0d 11888 . . . . . . . . 9 (𝜑 → (0 / (𝐴𝑀)) = 0)
228227adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 / (𝐴𝑀)) = 0)
229225, 228eqtrd 2776 . . . . . . 7 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) = 0)
230 fzfid 13832 . . . . . . 7 (𝜑 → (0...(deg‘𝐺)) ∈ Fin)
231176, 178, 229, 230fsumss 15564 . . . . . 6 (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
232133, 173, 2313eqtrd 2780 . . . . 5 (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
23386, 52syldan 591 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ)
23453fvmpt2 6956 . . . . . . . . . 10 ((𝑘 ∈ ℕ0 ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) → (𝐼𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
23586, 233, 234syl2anc 584 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
236235adantlr 713 . . . . . . . 8 (((𝜑𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
237 oveq1 7358 . . . . . . . . 9 (𝑧 = 𝐴 → (𝑧𝑘) = (𝐴𝑘))
238237ad2antlr 725 . . . . . . . 8 (((𝜑𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑧𝑘) = (𝐴𝑘))
239236, 238oveq12d 7369 . . . . . . 7 (((𝜑𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼𝑘) · (𝑧𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)))
240239sumeq2dv 15542 . . . . . 6 ((𝜑𝑧 = 𝐴) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)))
241 fzfid 13832 . . . . . . 7 (𝜑 → (0...((deg‘𝐺) − 𝑀)) ∈ Fin)
242241, 129fsumcl 15572 . . . . . 6 (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)) ∈ ℂ)
2432, 240, 126, 242fvmptd 6952 . . . . 5 (𝜑 → (𝐹𝐴) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)))
24417, 16coeid2 25546 . . . . . . . 8 ((𝐺 ∈ (Poly‘ℤ) ∧ 𝐴 ∈ ℂ) → (𝐺𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴𝑗)))
2455, 126, 244syl2anc 584 . . . . . . 7 (𝜑 → (𝐺𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴𝑗)))
246245oveq1d 7366 . . . . . 6 (𝜑 → ((𝐺𝐴) / (𝐴𝑀)) = (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
24783adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ)
248199adantl 482 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(deg‘𝐺))) → 𝑗 ∈ ℕ0)
249247, 248ffvelcdmd 7032 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ)
250126adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(deg‘𝐺))) → 𝐴 ∈ ℂ)
251250, 248expcld 14005 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(deg‘𝐺))) → (𝐴𝑗) ∈ ℂ)
252249, 251mulcld 11133 . . . . . . 7 ((𝜑𝑗 ∈ (0...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) ∈ ℂ)
253230, 165, 252, 226fsumdivc 15625 . . . . . 6 (𝜑 → (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
254246, 253eqtrd 2776 . . . . 5 (𝜑 → ((𝐺𝐴) / (𝐴𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
255232, 243, 2543eqtr4d 2786 . . . 4 (𝜑 → (𝐹𝐴) = ((𝐺𝐴) / (𝐴𝑀)))
256 elaa2lem.ga . . . . 5 (𝜑 → (𝐺𝐴) = 0)
257256oveq1d 7366 . . . 4 (𝜑 → ((𝐺𝐴) / (𝐴𝑀)) = (0 / (𝐴𝑀)))
258255, 257, 2273eqtrd 2780 . . 3 (𝜑 → (𝐹𝐴) = 0)
259122, 258jca 512 . 2 (𝜑 → (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹𝐴) = 0))
260 fveq2 6839 . . . . . 6 (𝑓 = 𝐹 → (coeff‘𝑓) = (coeff‘𝐹))
261260fveq1d 6841 . . . . 5 (𝑓 = 𝐹 → ((coeff‘𝑓)‘0) = ((coeff‘𝐹)‘0))
262261neeq1d 3001 . . . 4 (𝑓 = 𝐹 → (((coeff‘𝑓)‘0) ≠ 0 ↔ ((coeff‘𝐹)‘0) ≠ 0))
263 fveq1 6838 . . . . 5 (𝑓 = 𝐹 → (𝑓𝐴) = (𝐹𝐴))
264263eqeq1d 2738 . . . 4 (𝑓 = 𝐹 → ((𝑓𝐴) = 0 ↔ (𝐹𝐴) = 0))
265262, 264anbi12d 631 . . 3 (𝑓 = 𝐹 → ((((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓𝐴) = 0) ↔ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹𝐴) = 0)))
266265rspcev 3579 . 2 ((𝐹 ∈ (Poly‘ℤ) ∧ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹𝐴) = 0)) → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓𝐴) = 0))
26757, 259, 266syl2anc 584 1 (𝜑 → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓𝐴) = 0))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  wne 2941  wrex 3071  {crab 3405  cdif 3905  wss 3908  c0 4280  ifcif 4484   class class class wbr 5103  cmpt 5186  wf 6489  cfv 6493  (class class class)co 7351  infcinf 9335  cc 11007  cr 11008  0cc0 11009   + caddc 11012   · cmul 11014   < clt 11147  cle 11148  cmin 11343   / cdiv 11770  0cn0 12371  cz 12457  cuz 12721  ...cfz 13378  cexp 13921  Σcsu 15524  0𝑝c0p 24979  Polycply 25491  coeffccoe 25493  degcdgr 25494  𝔸caa 25620
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664  ax-inf2 9535  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7307  df-ov 7354  df-oprab 7355  df-mpo 7356  df-of 7609  df-om 7795  df-1st 7913  df-2nd 7914  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-1o 8404  df-er 8606  df-map 8725  df-pm 8726  df-en 8842  df-dom 8843  df-sdom 8844  df-fin 8845  df-sup 9336  df-inf 9337  df-oi 9404  df-card 9833  df-pnf 11149  df-mnf 11150  df-xr 11151  df-ltxr 11152  df-le 11153  df-sub 11345  df-neg 11346  df-div 11771  df-nn 12112  df-2 12174  df-3 12175  df-n0 12372  df-z 12458  df-uz 12722  df-rp 12870  df-fz 13379  df-fzo 13522  df-fl 13651  df-seq 13861  df-exp 13922  df-hash 14185  df-cj 14938  df-re 14939  df-im 14940  df-sqrt 15074  df-abs 15075  df-clim 15324  df-rlim 15325  df-sum 15525  df-0p 24980  df-ply 25495  df-coe 25497  df-dgr 25498  df-aa 25621
This theorem is referenced by:  elaa2  44370
  Copyright terms: Public domain W3C validator