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 39031
Description: Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 39033. (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 11126 . . . . 5 ℤ ⊆ ℂ
43a1i 11 . . . 4 (𝜑 → ℤ ⊆ ℂ)
5 elaa2lem.g . . . . . . . . 9 (𝜑𝐺 ∈ (Poly‘ℤ))
6 dgrcl 23677 . . . . . . . . 9 (𝐺 ∈ (Poly‘ℤ) → (deg‘𝐺) ∈ ℕ0)
75, 6syl 17 . . . . . . . 8 (𝜑 → (deg‘𝐺) ∈ ℕ0)
87nn0zd 11220 . . . . . . 7 (𝜑 → (deg‘𝐺) ∈ ℤ)
9 elaa2lem.m . . . . . . . . 9 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < )
10 ssrab2 3554 . . . . . . . . . 10 {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ ℕ0
11 nn0uz 11462 . . . . . . . . . . . . 13 0 = (ℤ‘0)
1210, 11sseqtri 3504 . . . . . . . . . . . 12 {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ‘0)
1312a1i 11 . . . . . . . . . . 11 (𝜑 → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ‘0))
14 elaa2lem.gn0 . . . . . . . . . . . . . . . . 17 (𝜑𝐺 ≠ 0𝑝)
1514neneqd 2691 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ 𝐺 = 0𝑝)
16 eqid 2514 . . . . . . . . . . . . . . . . . 18 (deg‘𝐺) = (deg‘𝐺)
17 eqid 2514 . . . . . . . . . . . . . . . . . 18 (coeff‘𝐺) = (coeff‘𝐺)
1816, 17dgreq0 23709 . . . . . . . . . . . . . . . . 17 (𝐺 ∈ (Poly‘ℤ) → (𝐺 = 0𝑝 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) = 0))
195, 18syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺 = 0𝑝 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) = 0))
2015, 19mtbid 312 . . . . . . . . . . . . . . 15 (𝜑 → ¬ ((coeff‘𝐺)‘(deg‘𝐺)) = 0)
2120neqned 2693 . . . . . . . . . . . . . 14 (𝜑 → ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0)
227, 21jca 552 . . . . . . . . . . . . 13 (𝜑 → ((deg‘𝐺) ∈ ℕ0 ∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
23 fveq2 5987 . . . . . . . . . . . . . . 15 (𝑛 = (deg‘𝐺) → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘(deg‘𝐺)))
2423neeq1d 2745 . . . . . . . . . . . . . 14 (𝑛 = (deg‘𝐺) → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
2524elrab 3235 . . . . . . . . . . . . 13 ((deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ ((deg‘𝐺) ∈ ℕ0 ∧ ((coeff‘𝐺)‘(deg‘𝐺)) ≠ 0))
2622, 25sylibr 222 . . . . . . . . . . . 12 (𝜑 → (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
27 ne0i 3783 . . . . . . . . . . . 12 ((deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅)
2826, 27syl 17 . . . . . . . . . . 11 (𝜑 → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅)
29 infssuzcl 11512 . . . . . . . . . . 11 (({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ‘0) ∧ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
3013, 28, 29syl2anc 690 . . . . . . . . . 10 (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
3110, 30sseldi 3470 . . . . . . . . 9 (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ∈ ℕ0)
329, 31syl5eqel 2596 . . . . . . . 8 (𝜑𝑀 ∈ ℕ0)
3332nn0zd 11220 . . . . . . 7 (𝜑𝑀 ∈ ℤ)
348, 33zsubcld 11227 . . . . . 6 (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℤ)
359a1i 11 . . . . . . . 8 (𝜑𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ))
36 infssuzle 11511 . . . . . . . . 9 (({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ‘0) ∧ (deg‘𝐺) ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ (deg‘𝐺))
3713, 26, 36syl2anc 690 . . . . . . . 8 (𝜑 → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ (deg‘𝐺))
3835, 37eqbrtrd 4503 . . . . . . 7 (𝜑𝑀 ≤ (deg‘𝐺))
397nn0red 11107 . . . . . . . 8 (𝜑 → (deg‘𝐺) ∈ ℝ)
4032nn0red 11107 . . . . . . . 8 (𝜑𝑀 ∈ ℝ)
4139, 40subge0d 10366 . . . . . . 7 (𝜑 → (0 ≤ ((deg‘𝐺) − 𝑀) ↔ 𝑀 ≤ (deg‘𝐺)))
4238, 41mpbird 245 . . . . . 6 (𝜑 → 0 ≤ ((deg‘𝐺) − 𝑀))
4334, 42jca 552 . . . . 5 (𝜑 → (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤ ((deg‘𝐺) − 𝑀)))
44 elnn0z 11131 . . . . 5 (((deg‘𝐺) − 𝑀) ∈ ℕ0 ↔ (((deg‘𝐺) − 𝑀) ∈ ℤ ∧ 0 ≤ ((deg‘𝐺) − 𝑀)))
4543, 44sylibr 222 . . . 4 (𝜑 → ((deg‘𝐺) − 𝑀) ∈ ℕ0)
46 id 22 . . . . . . . . 9 (𝐺 ∈ (Poly‘ℤ) → 𝐺 ∈ (Poly‘ℤ))
47 0zd 11130 . . . . . . . . 9 (𝐺 ∈ (Poly‘ℤ) → 0 ∈ ℤ)
4817coef2 23675 . . . . . . . . 9 ((𝐺 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → (coeff‘𝐺):ℕ0⟶ℤ)
4946, 47, 48syl2anc 690 . . . . . . . 8 (𝐺 ∈ (Poly‘ℤ) → (coeff‘𝐺):ℕ0⟶ℤ)
505, 49syl 17 . . . . . . 7 (𝜑 → (coeff‘𝐺):ℕ0⟶ℤ)
5150adantr 479 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (coeff‘𝐺):ℕ0⟶ℤ)
52 simpr 475 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
5332adantr 479 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝑀 ∈ ℕ0)
5452, 53nn0addcld 11110 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑘 + 𝑀) ∈ ℕ0)
5551, 54ffvelrnd 6152 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ)
56 elaa2lem.i . . . . 5 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀)))
5755, 56fmptd 6176 . . . 4 (𝜑𝐼:ℕ0⟶ℤ)
58 elplyr 23645 . . . 4 ((ℤ ⊆ ℂ ∧ ((deg‘𝐺) − 𝑀) ∈ ℕ0𝐼:ℕ0⟶ℤ) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘))) ∈ (Poly‘ℤ))
594, 45, 57, 58syl3anc 1317 . . 3 (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘))) ∈ (Poly‘ℤ))
602, 59eqeltrd 2592 . 2 (𝜑𝐹 ∈ (Poly‘ℤ))
61 simpr 475 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ≤ ((deg‘𝐺) − 𝑀))
6261iftrued 3947 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
63 iffalse 3948 . . . . . . . . . . 11 𝑘 ≤ ((deg‘𝐺) − 𝑀) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0)
6463adantl 480 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = 0)
65 simpr 475 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀))
6639ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) ∈ ℝ)
6740ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑀 ∈ ℝ)
6866, 67resubcld 10209 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) ∈ ℝ)
69 nn0re 11056 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
7069ad2antlr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℝ)
7168, 70ltnled 9935 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)))
7265, 71mpbird 245 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) − 𝑀) < 𝑘)
7366, 67, 70ltsubaddd 10372 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (((deg‘𝐺) − 𝑀) < 𝑘 ↔ (deg‘𝐺) < (𝑘 + 𝑀)))
7472, 73mpbid 220 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (deg‘𝐺) < (𝑘 + 𝑀))
75 olc 397 . . . . . . . . . . . . 13 ((deg‘𝐺) < (𝑘 + 𝑀) → (𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)))
7674, 75syl 17 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)))
775ad2antrr 757 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → 𝐺 ∈ (Poly‘ℤ))
7854adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → (𝑘 + 𝑀) ∈ ℕ0)
7916, 17dgrlt 23710 . . . . . . . . . . . . 13 ((𝐺 ∈ (Poly‘ℤ) ∧ (𝑘 + 𝑀) ∈ ℕ0) → ((𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)))
8077, 78, 79syl2anc 690 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((𝐺 = 0𝑝 ∨ (deg‘𝐺) < (𝑘 + 𝑀)) ↔ ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)))
8176, 80mpbid 220 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((deg‘𝐺) ≤ (𝑘 + 𝑀) ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0))
8281simprd 477 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = 0)
8364, 82eqtr4d 2551 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ ¬ 𝑘 ≤ ((deg‘𝐺) − 𝑀)) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
8462, 83pm2.61dan 827 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
8584mpteq2dva 4570 . . . . . . 7 (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)) = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))))
8650, 4fssd 5855 . . . . . . . . . 10 (𝜑 → (coeff‘𝐺):ℕ0⟶ℂ)
8786adantr 479 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (coeff‘𝐺):ℕ0⟶ℂ)
88 elfznn0 12170 . . . . . . . . . . 11 (𝑘 ∈ (0...((deg‘𝐺) − 𝑀)) → 𝑘 ∈ ℕ0)
8988adantl 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑘 ∈ ℕ0)
9032adantr 479 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝑀 ∈ ℕ0)
9189, 90nn0addcld 11110 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑘 + 𝑀) ∈ ℕ0)
9287, 91ffvelrnd 6152 . . . . . . . 8 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℂ)
93 eqidd 2515 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ℂ) → (0...((deg‘𝐺) − 𝑀)) = (0...((deg‘𝐺) − 𝑀)))
94 simpl 471 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝜑)
9556a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))))
9695, 55fvmpt2d 6086 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → (𝐼𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
9794, 89, 96syl2anc 690 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
9897adantlr 746 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
9998oveq1d 6441 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼𝑘) · (𝑧𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧𝑘)))
10093, 99sumeq12rdv 14154 . . . . . . . . . 10 ((𝜑𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧𝑘)))
101100mpteq2dva 4570 . . . . . . . . 9 (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧𝑘))))
1022, 101eqtrd 2548 . . . . . . . 8 (𝜑𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝑧𝑘))))
10360, 45, 92, 102coeeq2 23686 . . . . . . 7 (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ ((deg‘𝐺) − 𝑀), ((coeff‘𝐺)‘(𝑘 + 𝑀)), 0)))
10485, 103, 953eqtr4d 2558 . . . . . 6 (𝜑 → (coeff‘𝐹) = 𝐼)
105104fveq1d 5989 . . . . 5 (𝜑 → ((coeff‘𝐹)‘0) = (𝐼‘0))
106 oveq1 6433 . . . . . . . . 9 (𝑘 = 0 → (𝑘 + 𝑀) = (0 + 𝑀))
107106adantl 480 . . . . . . . 8 ((𝜑𝑘 = 0) → (𝑘 + 𝑀) = (0 + 𝑀))
1083, 33sseldi 3470 . . . . . . . . . 10 (𝜑𝑀 ∈ ℂ)
109108addid2d 9988 . . . . . . . . 9 (𝜑 → (0 + 𝑀) = 𝑀)
110109adantr 479 . . . . . . . 8 ((𝜑𝑘 = 0) → (0 + 𝑀) = 𝑀)
111107, 110eqtrd 2548 . . . . . . 7 ((𝜑𝑘 = 0) → (𝑘 + 𝑀) = 𝑀)
112111fveq2d 5991 . . . . . 6 ((𝜑𝑘 = 0) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘𝑀))
113 0nn0 11062 . . . . . . 7 0 ∈ ℕ0
114113a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℕ0)
11550, 32ffvelrnd 6152 . . . . . 6 (𝜑 → ((coeff‘𝐺)‘𝑀) ∈ ℤ)
11695, 112, 114, 115fvmptd 6081 . . . . 5 (𝜑 → (𝐼‘0) = ((coeff‘𝐺)‘𝑀))
117 eqidd 2515 . . . . 5 (𝜑 → ((coeff‘𝐺)‘𝑀) = ((coeff‘𝐺)‘𝑀))
118105, 116, 1173eqtrd 2552 . . . 4 (𝜑 → ((coeff‘𝐹)‘0) = ((coeff‘𝐺)‘𝑀))
11935, 30eqeltrd 2592 . . . . . 6 (𝜑𝑀 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
120 fveq2 5987 . . . . . . . 8 (𝑛 = 𝑀 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑀))
121120neeq1d 2745 . . . . . . 7 (𝑛 = 𝑀 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑀) ≠ 0))
122121elrab 3235 . . . . . 6 (𝑀 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑀 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑀) ≠ 0))
123119, 122sylib 206 . . . . 5 (𝜑 → (𝑀 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑀) ≠ 0))
124123simprd 477 . . . 4 (𝜑 → ((coeff‘𝐺)‘𝑀) ≠ 0)
125118, 124eqnetrd 2753 . . 3 (𝜑 → ((coeff‘𝐹)‘0) ≠ 0)
1265, 47syl 17 . . . . . . 7 (𝜑 → 0 ∈ ℤ)
127 aasscn 23761 . . . . . . . . . . 11 𝔸 ⊆ ℂ
128 elaa2lem.a . . . . . . . . . . 11 (𝜑𝐴 ∈ 𝔸)
129127, 128sseldi 3470 . . . . . . . . . 10 (𝜑𝐴 ∈ ℂ)
13094, 129syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → 𝐴 ∈ ℂ)
131130, 89expcld 12738 . . . . . . . 8 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐴𝑘) ∈ ℂ)
13292, 131mulcld 9815 . . . . . . 7 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)) ∈ ℂ)
133 oveq1 6433 . . . . . . . . 9 (𝑘 = (𝑗𝑀) → (𝑘 + 𝑀) = ((𝑗𝑀) + 𝑀))
134133fveq2d 5991 . . . . . . . 8 (𝑘 = (𝑗𝑀) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) = ((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)))
135 oveq2 6434 . . . . . . . 8 (𝑘 = (𝑗𝑀) → (𝐴𝑘) = (𝐴↑(𝑗𝑀)))
136134, 135oveq12d 6444 . . . . . . 7 (𝑘 = (𝑗𝑀) → (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)) = (((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))))
13733, 126, 34, 132, 136fsumshft 14223 . . . . . 6 (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)) = Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))))
1383, 8sseldi 3470 . . . . . . . . . 10 (𝜑 → (deg‘𝐺) ∈ ℂ)
139138, 108npcand 10147 . . . . . . . . 9 (𝜑 → (((deg‘𝐺) − 𝑀) + 𝑀) = (deg‘𝐺))
140109, 139oveq12d 6444 . . . . . . . 8 (𝜑 → ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀)) = (𝑀...(deg‘𝐺)))
141140sumeq1d 14148 . . . . . . 7 (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))))
142 elfzelz 12081 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑗 ∈ ℤ)
143142adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ)
1443, 143sseldi 3470 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℂ)
145108adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℂ)
146144, 145npcand 10147 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → ((𝑗𝑀) + 𝑀) = 𝑗)
147146fveq2d 5991 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) = ((coeff‘𝐺)‘𝑗))
148147oveq1d 6441 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗𝑀))))
149129adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝐴 ∈ ℂ)
150 elaa2lem.an0 . . . . . . . . . . . . 13 (𝜑𝐴 ≠ 0)
151150adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝐴 ≠ 0)
15233adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℤ)
153149, 151, 152, 143expsubd 12749 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴↑(𝑗𝑀)) = ((𝐴𝑗) / (𝐴𝑀)))
154153oveq2d 6442 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗𝑀))) = (((coeff‘𝐺)‘𝑗) · ((𝐴𝑗) / (𝐴𝑀))))
15586adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ)
156 0red 9796 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ∈ ℝ)
15740adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀 ∈ ℝ)
158143zred 11222 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ)
15932nn0ge0d 11109 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ 𝑀)
160159adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑀)
161 elfzle1 12083 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...(deg‘𝐺)) → 𝑀𝑗)
162161adantl 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑀𝑗)
163156, 157, 158, 160, 162letrd 9945 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 0 ≤ 𝑗)
164143, 163jca 552 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
165 elnn0z 11131 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
166164, 165sylibr 222 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0)
167155, 166ffvelrnd 6152 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ)
168149, 166expcld 12738 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴𝑗) ∈ ℂ)
169129, 32expcld 12738 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝑀) ∈ ℂ)
170169adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴𝑀) ∈ ℂ)
171149, 151, 152expne0d 12744 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (𝐴𝑀) ≠ 0)
172167, 168, 170, 171divassd 10585 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) = (((coeff‘𝐺)‘𝑗) · ((𝐴𝑗) / (𝐴𝑀))))
173172eqcomd 2520 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · ((𝐴𝑗) / (𝐴𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
174154, 173eqtr2d 2549 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) = (((coeff‘𝐺)‘𝑗) · (𝐴↑(𝑗𝑀))))
175148, 174eqtr4d 2551 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))) = ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
176175sumeq2dv 14150 . . . . . . 7 (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))(((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
177141, 176eqtrd 2548 . . . . . 6 (𝜑 → Σ𝑗 ∈ ((0 + 𝑀)...(((deg‘𝐺) − 𝑀) + 𝑀))(((coeff‘𝐺)‘((𝑗𝑀) + 𝑀)) · (𝐴↑(𝑗𝑀))) = Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
17832, 11syl6eleq 2602 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘0))
179 fzss1 12119 . . . . . . . 8 (𝑀 ∈ (ℤ‘0) → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺)))
180178, 179syl 17 . . . . . . 7 (𝜑 → (𝑀...(deg‘𝐺)) ⊆ (0...(deg‘𝐺)))
181167, 168mulcld 9815 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) ∈ ℂ)
182181, 170, 171divcld 10550 . . . . . . 7 ((𝜑𝑗 ∈ (𝑀...(deg‘𝐺))) → ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) ∈ ℂ)
18333ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℤ)
1848ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (deg‘𝐺) ∈ ℤ)
185 eldifi 3598 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ (0...(deg‘𝐺)))
186 elfznn0 12170 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ∈ ℕ0)
187186nn0zd 11220 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ∈ ℤ)
188185, 187syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℤ)
189188ad2antlr 758 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℤ)
190183, 184, 1893jca 1234 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (𝑀 ∈ ℤ ∧ (deg‘𝐺) ∈ ℤ ∧ 𝑗 ∈ ℤ))
191 simpr 475 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 < 𝑀)
19240ad2antrr 757 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀 ∈ ℝ)
193189zred 11222 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ ℝ)
194192, 193lenltd 9934 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → (𝑀𝑗 ↔ ¬ 𝑗 < 𝑀))
195191, 194mpbird 245 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑀𝑗)
196 elfzle2 12084 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...(deg‘𝐺)) → 𝑗 ≤ (deg‘𝐺))
197185, 196syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ≤ (deg‘𝐺))
198197ad2antlr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ≤ (deg‘𝐺))
199190, 195, 198jca32 555 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ((𝑀 ∈ ℤ ∧ (deg‘𝐺) ∈ ℤ ∧ 𝑗 ∈ ℤ) ∧ (𝑀𝑗𝑗 ≤ (deg‘𝐺))))
200 elfz2 12072 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀...(deg‘𝐺)) ↔ ((𝑀 ∈ ℤ ∧ (deg‘𝐺) ∈ ℤ ∧ 𝑗 ∈ ℤ) ∧ (𝑀𝑗𝑗 ≤ (deg‘𝐺))))
201199, 200sylibr 222 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → 𝑗 ∈ (𝑀...(deg‘𝐺)))
202 eldifn 3599 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺)))
203202ad2antlr 758 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ 𝑗 < 𝑀) → ¬ 𝑗 ∈ (𝑀...(deg‘𝐺)))
204201, 203condan 830 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 < 𝑀)
205204adantr 479 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 < 𝑀)
2069a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ))
20712a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ‘0))
208185, 186syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℕ0)
209208adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℕ0)
210 neqne 2694 . . . . . . . . . . . . . . . . . . 19 (¬ ((coeff‘𝐺)‘𝑗) = 0 → ((coeff‘𝐺)‘𝑗) ≠ 0)
211210adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ((coeff‘𝐺)‘𝑗) ≠ 0)
212209, 211jca 552 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑗 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑗) ≠ 0))
213 fveq2 5987 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑗 → ((coeff‘𝐺)‘𝑛) = ((coeff‘𝐺)‘𝑗))
214213neeq1d 2745 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑗 → (((coeff‘𝐺)‘𝑛) ≠ 0 ↔ ((coeff‘𝐺)‘𝑗) ≠ 0))
215214elrab 3235 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ↔ (𝑗 ∈ ℕ0 ∧ ((coeff‘𝐺)‘𝑗) ≠ 0))
216212, 215sylibr 222 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
217216adantll 745 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0})
218 infssuzle 11511 . . . . . . . . . . . . . . 15 (({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0} ⊆ (ℤ‘0) ∧ 𝑗 ∈ {𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗)
219207, 217, 218syl2anc 690 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑗)
220206, 219eqbrtrd 4503 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀𝑗)
22140ad2antrr 757 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑀 ∈ ℝ)
222188zred 11222 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺))) → 𝑗 ∈ ℝ)
223222ad2antlr 758 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → 𝑗 ∈ ℝ)
224221, 223lenltd 9934 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → (𝑀𝑗 ↔ ¬ 𝑗 < 𝑀))
225220, 224mpbid 220 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) ∧ ¬ ((coeff‘𝐺)‘𝑗) = 0) → ¬ 𝑗 < 𝑀)
226205, 225condan 830 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((coeff‘𝐺)‘𝑗) = 0)
227226oveq1d 6441 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) = (0 · (𝐴𝑗)))
228129adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝐴 ∈ ℂ)
229208adantl 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → 𝑗 ∈ ℕ0)
230228, 229expcld 12738 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (𝐴𝑗) ∈ ℂ)
231230mul02d 9985 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 · (𝐴𝑗)) = 0)
232227, 231eqtrd 2548 . . . . . . . . 9 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) = 0)
233232oveq1d 6441 . . . . . . . 8 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) = (0 / (𝐴𝑀)))
234129, 150, 33expne0d 12744 . . . . . . . . . 10 (𝜑 → (𝐴𝑀) ≠ 0)
235169, 234div0d 10549 . . . . . . . . 9 (𝜑 → (0 / (𝐴𝑀)) = 0)
236235adantr 479 . . . . . . . 8 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → (0 / (𝐴𝑀)) = 0)
237233, 236eqtrd 2548 . . . . . . 7 ((𝜑𝑗 ∈ ((0...(deg‘𝐺)) ∖ (𝑀...(deg‘𝐺)))) → ((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) = 0)
238 fzfid 12502 . . . . . . 7 (𝜑 → (0...(deg‘𝐺)) ∈ Fin)
239180, 182, 237, 238fsumss 14172 . . . . . 6 (𝜑 → Σ𝑗 ∈ (𝑀...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
240137, 177, 2393eqtrd 2552 . . . . 5 (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
24189, 55syldan 485 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ)
24256fvmpt2 6084 . . . . . . . . . 10 ((𝑘 ∈ ℕ0 ∧ ((coeff‘𝐺)‘(𝑘 + 𝑀)) ∈ ℤ) → (𝐼𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
24389, 241, 242syl2anc 690 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
244243adantlr 746 . . . . . . . 8 (((𝜑𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝐼𝑘) = ((coeff‘𝐺)‘(𝑘 + 𝑀)))
245 oveq1 6433 . . . . . . . . 9 (𝑧 = 𝐴 → (𝑧𝑘) = (𝐴𝑘))
246245ad2antlr 758 . . . . . . . 8 (((𝜑𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → (𝑧𝑘) = (𝐴𝑘))
247244, 246oveq12d 6444 . . . . . . 7 (((𝜑𝑧 = 𝐴) ∧ 𝑘 ∈ (0...((deg‘𝐺) − 𝑀))) → ((𝐼𝑘) · (𝑧𝑘)) = (((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)))
248247sumeq2dv 14150 . . . . . 6 ((𝜑𝑧 = 𝐴) → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼𝑘) · (𝑧𝑘)) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)))
249 fzfid 12502 . . . . . . 7 (𝜑 → (0...((deg‘𝐺) − 𝑀)) ∈ Fin)
250249, 132fsumcl 14180 . . . . . 6 (𝜑 → Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)) ∈ ℂ)
2512, 248, 129, 250fvmptd 6081 . . . . 5 (𝜑 → (𝐹𝐴) = Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))(((coeff‘𝐺)‘(𝑘 + 𝑀)) · (𝐴𝑘)))
25217, 16coeid2 23683 . . . . . . . 8 ((𝐺 ∈ (Poly‘ℤ) ∧ 𝐴 ∈ ℂ) → (𝐺𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴𝑗)))
2535, 129, 252syl2anc 690 . . . . . . 7 (𝜑 → (𝐺𝐴) = Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴𝑗)))
254253oveq1d 6441 . . . . . 6 (𝜑 → ((𝐺𝐴) / (𝐴𝑀)) = (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
25586adantr 479 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(deg‘𝐺))) → (coeff‘𝐺):ℕ0⟶ℂ)
256186adantl 480 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(deg‘𝐺))) → 𝑗 ∈ ℕ0)
257255, 256ffvelrnd 6152 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(deg‘𝐺))) → ((coeff‘𝐺)‘𝑗) ∈ ℂ)
258129adantr 479 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(deg‘𝐺))) → 𝐴 ∈ ℂ)
259258, 256expcld 12738 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(deg‘𝐺))) → (𝐴𝑗) ∈ ℂ)
260257, 259mulcld 9815 . . . . . . 7 ((𝜑𝑗 ∈ (0...(deg‘𝐺))) → (((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) ∈ ℂ)
261238, 169, 260, 234fsumdivc 14229 . . . . . 6 (𝜑 → (Σ𝑗 ∈ (0...(deg‘𝐺))(((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
262254, 261eqtrd 2548 . . . . 5 (𝜑 → ((𝐺𝐴) / (𝐴𝑀)) = Σ𝑗 ∈ (0...(deg‘𝐺))((((coeff‘𝐺)‘𝑗) · (𝐴𝑗)) / (𝐴𝑀)))
263240, 251, 2623eqtr4d 2558 . . . 4 (𝜑 → (𝐹𝐴) = ((𝐺𝐴) / (𝐴𝑀)))
264 elaa2lem.ga . . . . 5 (𝜑 → (𝐺𝐴) = 0)
265264oveq1d 6441 . . . 4 (𝜑 → ((𝐺𝐴) / (𝐴𝑀)) = (0 / (𝐴𝑀)))
266263, 265, 2353eqtrd 2552 . . 3 (𝜑 → (𝐹𝐴) = 0)
267125, 266jca 552 . 2 (𝜑 → (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹𝐴) = 0))
268 fveq2 5987 . . . . . 6 (𝑓 = 𝐹 → (coeff‘𝑓) = (coeff‘𝐹))
269268fveq1d 5989 . . . . 5 (𝑓 = 𝐹 → ((coeff‘𝑓)‘0) = ((coeff‘𝐹)‘0))
270269neeq1d 2745 . . . 4 (𝑓 = 𝐹 → (((coeff‘𝑓)‘0) ≠ 0 ↔ ((coeff‘𝐹)‘0) ≠ 0))
271 fveq1 5986 . . . . 5 (𝑓 = 𝐹 → (𝑓𝐴) = (𝐹𝐴))
272271eqeq1d 2516 . . . 4 (𝑓 = 𝐹 → ((𝑓𝐴) = 0 ↔ (𝐹𝐴) = 0))
273270, 272anbi12d 742 . . 3 (𝑓 = 𝐹 → ((((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓𝐴) = 0) ↔ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹𝐴) = 0)))
274273rspcev 3186 . 2 ((𝐹 ∈ (Poly‘ℤ) ∧ (((coeff‘𝐹)‘0) ≠ 0 ∧ (𝐹𝐴) = 0)) → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓𝐴) = 0))
27560, 267, 274syl2anc 690 1 (𝜑 → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓𝐴) = 0))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1938  wne 2684  wrex 2801  {crab 2804  cdif 3441  wss 3444  c0 3777  ifcif 3939   class class class wbr 4481  cmpt 4541  wf 5685  cfv 5689  (class class class)co 6426  infcinf 8106  cc 9689  cr 9690  0cc0 9691   + caddc 9694   · cmul 9696   < clt 9829  cle 9830  cmin 10017   / cdiv 10433  0cn0 11047  cz 11118  cuz 11427  ...cfz 12065  cexp 12590  Σcsu 14133  0𝑝c0p 23117  Polycply 23628  coeffccoe 23630  degcdgr 23631  𝔸caa 23757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-inf2 8297  ax-cnex 9747  ax-resscn 9748  ax-1cn 9749  ax-icn 9750  ax-addcl 9751  ax-addrcl 9752  ax-mulcl 9753  ax-mulrcl 9754  ax-mulcom 9755  ax-addass 9756  ax-mulass 9757  ax-distr 9758  ax-i2m1 9759  ax-1ne0 9760  ax-1rid 9761  ax-rnegex 9762  ax-rrecex 9763  ax-cnre 9764  ax-pre-lttri 9765  ax-pre-lttrn 9766  ax-pre-ltadd 9767  ax-pre-mulgt0 9768  ax-pre-sup 9769  ax-addf 9770
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-se 4892  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-isom 5698  df-riota 6388  df-ov 6429  df-oprab 6430  df-mpt2 6431  df-of 6671  df-om 6834  df-1st 6934  df-2nd 6935  df-wrecs 7169  df-recs 7231  df-rdg 7269  df-1o 7323  df-oadd 7327  df-er 7505  df-map 7622  df-pm 7623  df-en 7718  df-dom 7719  df-sdom 7720  df-fin 7721  df-sup 8107  df-inf 8108  df-oi 8174  df-card 8524  df-pnf 9831  df-mnf 9832  df-xr 9833  df-ltxr 9834  df-le 9835  df-sub 10019  df-neg 10020  df-div 10434  df-nn 10776  df-2 10834  df-3 10835  df-n0 11048  df-z 11119  df-uz 11428  df-rp 11575  df-fz 12066  df-fzo 12203  df-fl 12323  df-seq 12532  df-exp 12591  df-hash 12848  df-cj 13546  df-re 13547  df-im 13548  df-sqrt 13682  df-abs 13683  df-clim 13933  df-rlim 13934  df-sum 14134  df-0p 23118  df-ply 23632  df-coe 23634  df-dgr 23635  df-aa 23758
This theorem is referenced by:  elaa2  39033
  Copyright terms: Public domain W3C validator