Metamath Proof Explorer


Theorem elaa2lem

Description: Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 . (Contributed by Glauco Siliprandi, 5-Apr-2020) (Revised by AV, 1-Oct-2020)

Ref Expression
Hypotheses 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 elaa2lem ( 𝜑 → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓𝐴 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 elaa2lem.a ( 𝜑𝐴 ∈ 𝔸 )
2 elaa2lem.an0 ( 𝜑𝐴 ≠ 0 )
3 elaa2lem.g ( 𝜑𝐺 ∈ ( Poly ‘ ℤ ) )
4 elaa2lem.gn0 ( 𝜑𝐺 ≠ 0𝑝 )
5 elaa2lem.ga ( 𝜑 → ( 𝐺𝐴 ) = 0 )
6 elaa2lem.m 𝑀 = inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < )
7 elaa2lem.i 𝐼 = ( 𝑘 ∈ ℕ0 ↦ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) )
8 elaa2lem.f 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼𝑘 ) · ( 𝑧𝑘 ) ) )
9 8 a1i ( 𝜑𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼𝑘 ) · ( 𝑧𝑘 ) ) ) )
10 zsscn ℤ ⊆ ℂ
11 10 a1i ( 𝜑 → ℤ ⊆ ℂ )
12 dgrcl ( 𝐺 ∈ ( Poly ‘ ℤ ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
13 3 12 syl ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℕ0 )
14 13 nn0zd ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℤ )
15 ssrab2 { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ℕ0
16 nn0uz 0 = ( ℤ ‘ 0 )
17 15 16 sseqtri { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ ‘ 0 )
18 17 a1i ( 𝜑 → { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ ‘ 0 ) )
19 4 neneqd ( 𝜑 → ¬ 𝐺 = 0𝑝 )
20 eqid ( deg ‘ 𝐺 ) = ( deg ‘ 𝐺 )
21 eqid ( coeff ‘ 𝐺 ) = ( coeff ‘ 𝐺 )
22 20 21 dgreq0 ( 𝐺 ∈ ( Poly ‘ ℤ ) → ( 𝐺 = 0𝑝 ↔ ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) = 0 ) )
23 3 22 syl ( 𝜑 → ( 𝐺 = 0𝑝 ↔ ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) = 0 ) )
24 19 23 mtbid ( 𝜑 → ¬ ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) = 0 )
25 24 neqned ( 𝜑 → ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ≠ 0 )
26 13 25 jca ( 𝜑 → ( ( deg ‘ 𝐺 ) ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ≠ 0 ) )
27 fveq2 ( 𝑛 = ( deg ‘ 𝐺 ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) = ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) )
28 27 neeq1d ( 𝑛 = ( deg ‘ 𝐺 ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 ↔ ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ≠ 0 ) )
29 28 elrab ( ( deg ‘ 𝐺 ) ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ↔ ( ( deg ‘ 𝐺 ) ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ≠ 0 ) )
30 26 29 sylibr ( 𝜑 → ( deg ‘ 𝐺 ) ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } )
31 30 ne0d ( 𝜑 → { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ≠ ∅ )
32 infssuzcl ( ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ ‘ 0 ) ∧ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ≠ ∅ ) → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } )
33 18 31 32 syl2anc ( 𝜑 → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } )
34 15 33 sseldi ( 𝜑 → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ∈ ℕ0 )
35 6 34 eqeltrid ( 𝜑𝑀 ∈ ℕ0 )
36 35 nn0zd ( 𝜑𝑀 ∈ ℤ )
37 14 36 zsubcld ( 𝜑 → ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℤ )
38 6 a1i ( 𝜑𝑀 = inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) )
39 infssuzle ( ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ ‘ 0 ) ∧ ( deg ‘ 𝐺 ) ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ) → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ≤ ( deg ‘ 𝐺 ) )
40 18 30 39 syl2anc ( 𝜑 → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ≤ ( deg ‘ 𝐺 ) )
41 38 40 eqbrtrd ( 𝜑𝑀 ≤ ( deg ‘ 𝐺 ) )
42 13 nn0red ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℝ )
43 35 nn0red ( 𝜑𝑀 ∈ ℝ )
44 42 43 subge0d ( 𝜑 → ( 0 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ↔ 𝑀 ≤ ( deg ‘ 𝐺 ) ) )
45 41 44 mpbird ( 𝜑 → 0 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) )
46 37 45 jca ( 𝜑 → ( ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℤ ∧ 0 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) )
47 elnn0z ( ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℕ0 ↔ ( ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℤ ∧ 0 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) )
48 46 47 sylibr ( 𝜑 → ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℕ0 )
49 0zd ( 𝐺 ∈ ( Poly ‘ ℤ ) → 0 ∈ ℤ )
50 21 coef2 ( ( 𝐺 ∈ ( Poly ‘ ℤ ) ∧ 0 ∈ ℤ ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℤ )
51 3 49 50 syl2anc2 ( 𝜑 → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℤ )
52 51 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℤ )
53 simpr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
54 35 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
55 53 54 nn0addcld ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑘 + 𝑀 ) ∈ ℕ0 )
56 52 55 ffvelrnd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ∈ ℤ )
57 56 7 fmptd ( 𝜑𝐼 : ℕ0 ⟶ ℤ )
58 elplyr ( ( ℤ ⊆ ℂ ∧ ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℕ0𝐼 : ℕ0 ⟶ ℤ ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼𝑘 ) · ( 𝑧𝑘 ) ) ) ∈ ( Poly ‘ ℤ ) )
59 11 48 57 58 syl3anc ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼𝑘 ) · ( 𝑧𝑘 ) ) ) ∈ ( Poly ‘ ℤ ) )
60 9 59 eqeltrd ( 𝜑𝐹 ∈ ( Poly ‘ ℤ ) )
61 simpr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) )
62 61 iftrued ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) )
63 iffalse ( ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) → if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) = 0 )
64 63 adantl ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) = 0 )
65 simpr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) )
66 42 ad2antrr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( deg ‘ 𝐺 ) ∈ ℝ )
67 43 ad2antrr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → 𝑀 ∈ ℝ )
68 66 67 resubcld ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℝ )
69 nn0re ( 𝑘 ∈ ℕ0𝑘 ∈ ℝ )
70 69 ad2antlr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → 𝑘 ∈ ℝ )
71 68 70 ltnled ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( ( deg ‘ 𝐺 ) − 𝑀 ) < 𝑘 ↔ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) )
72 65 71 mpbird ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( deg ‘ 𝐺 ) − 𝑀 ) < 𝑘 )
73 66 67 70 ltsubaddd ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( ( deg ‘ 𝐺 ) − 𝑀 ) < 𝑘 ↔ ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) ) )
74 72 73 mpbid ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) )
75 olc ( ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) → ( 𝐺 = 0𝑝 ∨ ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) ) )
76 74 75 syl ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( 𝐺 = 0𝑝 ∨ ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) ) )
77 3 ad2antrr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → 𝐺 ∈ ( Poly ‘ ℤ ) )
78 55 adantr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( 𝑘 + 𝑀 ) ∈ ℕ0 )
79 20 21 dgrlt ( ( 𝐺 ∈ ( Poly ‘ ℤ ) ∧ ( 𝑘 + 𝑀 ) ∈ ℕ0 ) → ( ( 𝐺 = 0𝑝 ∨ ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) ) ↔ ( ( deg ‘ 𝐺 ) ≤ ( 𝑘 + 𝑀 ) ∧ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) = 0 ) ) )
80 77 78 79 syl2anc ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( 𝐺 = 0𝑝 ∨ ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) ) ↔ ( ( deg ‘ 𝐺 ) ≤ ( 𝑘 + 𝑀 ) ∧ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) = 0 ) ) )
81 76 80 mpbid ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( deg ‘ 𝐺 ) ≤ ( 𝑘 + 𝑀 ) ∧ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) = 0 ) )
82 81 simprd ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) = 0 )
83 64 82 eqtr4d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) )
84 62 83 pm2.61dan ( ( 𝜑𝑘 ∈ ℕ0 ) → if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) )
85 84 mpteq2dva ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) )
86 51 11 fssd ( 𝜑 → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ )
87 86 adantr ( ( 𝜑𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ )
88 elfznn0 ( 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → 𝑘 ∈ ℕ0 )
89 88 adantl ( ( 𝜑𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → 𝑘 ∈ ℕ0 )
90 35 adantr ( ( 𝜑𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → 𝑀 ∈ ℕ0 )
91 89 90 nn0addcld ( ( 𝜑𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝑘 + 𝑀 ) ∈ ℕ0 )
92 87 91 ffvelrnd ( ( 𝜑𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ∈ ℂ )
93 eqidd ( ( 𝜑𝑧 ∈ ℂ ) → ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) = ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) )
94 simpl ( ( 𝜑𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → 𝜑 )
95 7 a1i ( 𝜑𝐼 = ( 𝑘 ∈ ℕ0 ↦ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) )
96 95 56 fvmpt2d ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐼𝑘 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) )
97 94 89 96 syl2anc ( ( 𝜑𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝐼𝑘 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) )
98 97 adantlr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝐼𝑘 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) )
99 98 oveq1d ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( ( 𝐼𝑘 ) · ( 𝑧𝑘 ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝑧𝑘 ) ) )
100 93 99 sumeq12rdv ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼𝑘 ) · ( 𝑧𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝑧𝑘 ) ) )
101 100 mpteq2dva ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼𝑘 ) · ( 𝑧𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝑧𝑘 ) ) ) )
102 9 101 eqtrd ( 𝜑𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝑧𝑘 ) ) ) )
103 60 48 92 102 coeeq2 ( 𝜑 → ( coeff ‘ 𝐹 ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) ) )
104 85 103 95 3eqtr4d ( 𝜑 → ( coeff ‘ 𝐹 ) = 𝐼 )
105 104 fveq1d ( 𝜑 → ( ( coeff ‘ 𝐹 ) ‘ 0 ) = ( 𝐼 ‘ 0 ) )
106 oveq1 ( 𝑘 = 0 → ( 𝑘 + 𝑀 ) = ( 0 + 𝑀 ) )
107 106 adantl ( ( 𝜑𝑘 = 0 ) → ( 𝑘 + 𝑀 ) = ( 0 + 𝑀 ) )
108 10 36 sseldi ( 𝜑𝑀 ∈ ℂ )
109 108 addid2d ( 𝜑 → ( 0 + 𝑀 ) = 𝑀 )
110 109 adantr ( ( 𝜑𝑘 = 0 ) → ( 0 + 𝑀 ) = 𝑀 )
111 107 110 eqtrd ( ( 𝜑𝑘 = 0 ) → ( 𝑘 + 𝑀 ) = 𝑀 )
112 111 fveq2d ( ( 𝜑𝑘 = 0 ) → ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) )
113 0nn0 0 ∈ ℕ0
114 113 a1i ( 𝜑 → 0 ∈ ℕ0 )
115 51 35 ffvelrnd ( 𝜑 → ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ∈ ℤ )
116 95 112 114 115 fvmptd ( 𝜑 → ( 𝐼 ‘ 0 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) )
117 eqidd ( 𝜑 → ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) )
118 105 116 117 3eqtrd ( 𝜑 → ( ( coeff ‘ 𝐹 ) ‘ 0 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) )
119 38 33 eqeltrd ( 𝜑𝑀 ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } )
120 fveq2 ( 𝑛 = 𝑀 → ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) )
121 120 neeq1d ( 𝑛 = 𝑀 → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 ↔ ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ≠ 0 ) )
122 121 elrab ( 𝑀 ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ↔ ( 𝑀 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ≠ 0 ) )
123 119 122 sylib ( 𝜑 → ( 𝑀 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ≠ 0 ) )
124 123 simprd ( 𝜑 → ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ≠ 0 )
125 118 124 eqnetrd ( 𝜑 → ( ( coeff ‘ 𝐹 ) ‘ 0 ) ≠ 0 )
126 3 49 syl ( 𝜑 → 0 ∈ ℤ )
127 aasscn 𝔸 ⊆ ℂ
128 127 1 sseldi ( 𝜑𝐴 ∈ ℂ )
129 94 128 syl ( ( 𝜑𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → 𝐴 ∈ ℂ )
130 129 89 expcld ( ( 𝜑𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝐴𝑘 ) ∈ ℂ )
131 92 130 mulcld ( ( 𝜑𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴𝑘 ) ) ∈ ℂ )
132 fvoveq1 ( 𝑘 = ( 𝑗𝑀 ) → ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) = ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗𝑀 ) + 𝑀 ) ) )
133 oveq2 ( 𝑘 = ( 𝑗𝑀 ) → ( 𝐴𝑘 ) = ( 𝐴 ↑ ( 𝑗𝑀 ) ) )
134 132 133 oveq12d ( 𝑘 = ( 𝑗𝑀 ) → ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴𝑘 ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗𝑀 ) ) ) )
135 36 126 37 131 134 fsumshft ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴𝑘 ) ) = Σ 𝑗 ∈ ( ( 0 + 𝑀 ) ... ( ( ( deg ‘ 𝐺 ) − 𝑀 ) + 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗𝑀 ) ) ) )
136 10 14 sseldi ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℂ )
137 136 108 npcand ( 𝜑 → ( ( ( deg ‘ 𝐺 ) − 𝑀 ) + 𝑀 ) = ( deg ‘ 𝐺 ) )
138 109 137 oveq12d ( 𝜑 → ( ( 0 + 𝑀 ) ... ( ( ( deg ‘ 𝐺 ) − 𝑀 ) + 𝑀 ) ) = ( 𝑀 ... ( deg ‘ 𝐺 ) ) )
139 138 sumeq1d ( 𝜑 → Σ 𝑗 ∈ ( ( 0 + 𝑀 ) ... ( ( ( deg ‘ 𝐺 ) − 𝑀 ) + 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗𝑀 ) ) ) = Σ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗𝑀 ) ) ) )
140 elfzelz ( 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) → 𝑗 ∈ ℤ )
141 140 adantl ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℤ )
142 10 141 sseldi ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℂ )
143 108 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑀 ∈ ℂ )
144 142 143 npcand ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( 𝑗𝑀 ) + 𝑀 ) = 𝑗 )
145 144 fveq2d ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗𝑀 ) + 𝑀 ) ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) )
146 145 oveq1d ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗𝑀 ) ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ ( 𝑗𝑀 ) ) ) )
147 128 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝐴 ∈ ℂ )
148 2 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝐴 ≠ 0 )
149 36 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑀 ∈ ℤ )
150 147 148 149 141 expsubd ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( 𝐴 ↑ ( 𝑗𝑀 ) ) = ( ( 𝐴𝑗 ) / ( 𝐴𝑀 ) ) )
151 150 oveq2d ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ ( 𝑗𝑀 ) ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( ( 𝐴𝑗 ) / ( 𝐴𝑀 ) ) ) )
152 86 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ )
153 0red ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 0 ∈ ℝ )
154 43 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑀 ∈ ℝ )
155 141 zred ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℝ )
156 35 nn0ge0d ( 𝜑 → 0 ≤ 𝑀 )
157 156 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 0 ≤ 𝑀 )
158 elfzle1 ( 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) → 𝑀𝑗 )
159 158 adantl ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑀𝑗 )
160 153 154 155 157 159 letrd ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 0 ≤ 𝑗 )
161 141 160 jca ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( 𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ) )
162 elnn0z ( 𝑗 ∈ ℕ0 ↔ ( 𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ) )
163 161 162 sylibr ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℕ0 )
164 152 163 ffvelrnd ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ∈ ℂ )
165 147 163 expcld ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( 𝐴𝑗 ) ∈ ℂ )
166 128 35 expcld ( 𝜑 → ( 𝐴𝑀 ) ∈ ℂ )
167 166 adantr ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( 𝐴𝑀 ) ∈ ℂ )
168 147 148 149 expne0d ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( 𝐴𝑀 ) ≠ 0 )
169 164 165 167 168 divassd ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( ( 𝐴𝑗 ) / ( 𝐴𝑀 ) ) ) )
170 169 eqcomd ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( ( 𝐴𝑗 ) / ( 𝐴𝑀 ) ) ) = ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) )
171 151 170 eqtr2d ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ ( 𝑗𝑀 ) ) ) )
172 146 171 eqtr4d ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗𝑀 ) ) ) = ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) )
173 172 sumeq2dv ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗𝑀 ) ) ) = Σ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) )
174 139 173 eqtrd ( 𝜑 → Σ 𝑗 ∈ ( ( 0 + 𝑀 ) ... ( ( ( deg ‘ 𝐺 ) − 𝑀 ) + 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗𝑀 ) ) ) = Σ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) )
175 35 16 eleqtrdi ( 𝜑𝑀 ∈ ( ℤ ‘ 0 ) )
176 fzss1 ( 𝑀 ∈ ( ℤ ‘ 0 ) → ( 𝑀 ... ( deg ‘ 𝐺 ) ) ⊆ ( 0 ... ( deg ‘ 𝐺 ) ) )
177 175 176 syl ( 𝜑 → ( 𝑀 ... ( deg ‘ 𝐺 ) ) ⊆ ( 0 ... ( deg ‘ 𝐺 ) ) )
178 164 165 mulcld ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) ∈ ℂ )
179 178 167 168 divcld ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) ∈ ℂ )
180 36 ad2antrr ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑀 ∈ ℤ )
181 14 ad2antrr ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → ( deg ‘ 𝐺 ) ∈ ℤ )
182 eldifi ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) )
183 182 elfzelzd ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℤ )
184 183 ad2antlr ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑗 ∈ ℤ )
185 simpr ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → ¬ 𝑗 < 𝑀 )
186 43 ad2antrr ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑀 ∈ ℝ )
187 184 zred ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑗 ∈ ℝ )
188 186 187 lenltd ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → ( 𝑀𝑗 ↔ ¬ 𝑗 < 𝑀 ) )
189 185 188 mpbird ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑀𝑗 )
190 elfzle2 ( 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) → 𝑗 ≤ ( deg ‘ 𝐺 ) )
191 182 190 syl ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ≤ ( deg ‘ 𝐺 ) )
192 191 ad2antlr ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑗 ≤ ( deg ‘ 𝐺 ) )
193 180 181 184 189 192 elfzd ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) )
194 eldifn ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ¬ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) )
195 194 ad2antlr ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → ¬ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) )
196 193 195 condan ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → 𝑗 < 𝑀 )
197 196 adantr ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑗 < 𝑀 )
198 6 a1i ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑀 = inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) )
199 17 a1i ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ ‘ 0 ) )
200 elfznn0 ( 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) → 𝑗 ∈ ℕ0 )
201 182 200 syl ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℕ0 )
202 201 adantr ( ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑗 ∈ ℕ0 )
203 neqne ( ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 → ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ≠ 0 )
204 203 adantl ( ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ≠ 0 )
205 202 204 jca ( ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → ( 𝑗 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ≠ 0 ) )
206 fveq2 ( 𝑛 = 𝑗 → ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) )
207 206 neeq1d ( 𝑛 = 𝑗 → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 ↔ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ≠ 0 ) )
208 207 elrab ( 𝑗 ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ↔ ( 𝑗 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ≠ 0 ) )
209 205 208 sylibr ( ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑗 ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } )
210 209 adantll ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑗 ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } )
211 infssuzle ( ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ ‘ 0 ) ∧ 𝑗 ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ) → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ≤ 𝑗 )
212 199 210 211 syl2anc ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ≤ 𝑗 )
213 198 212 eqbrtrd ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑀𝑗 )
214 43 ad2antrr ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑀 ∈ ℝ )
215 183 zred ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℝ )
216 215 ad2antlr ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑗 ∈ ℝ )
217 214 216 lenltd ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → ( 𝑀𝑗 ↔ ¬ 𝑗 < 𝑀 ) )
218 213 217 mpbid ( ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → ¬ 𝑗 < 𝑀 )
219 197 218 condan ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 )
220 219 oveq1d ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) = ( 0 · ( 𝐴𝑗 ) ) )
221 128 adantr ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → 𝐴 ∈ ℂ )
222 201 adantl ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → 𝑗 ∈ ℕ0 )
223 221 222 expcld ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( 𝐴𝑗 ) ∈ ℂ )
224 223 mul02d ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( 0 · ( 𝐴𝑗 ) ) = 0 )
225 220 224 eqtrd ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) = 0 )
226 225 oveq1d ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) = ( 0 / ( 𝐴𝑀 ) ) )
227 128 2 36 expne0d ( 𝜑 → ( 𝐴𝑀 ) ≠ 0 )
228 166 227 div0d ( 𝜑 → ( 0 / ( 𝐴𝑀 ) ) = 0 )
229 228 adantr ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( 0 / ( 𝐴𝑀 ) ) = 0 )
230 226 229 eqtrd ( ( 𝜑𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) = 0 )
231 fzfid ( 𝜑 → ( 0 ... ( deg ‘ 𝐺 ) ) ∈ Fin )
232 177 179 230 231 fsumss ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) = Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) )
233 135 174 232 3eqtrd ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) )
234 89 56 syldan ( ( 𝜑𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ∈ ℤ )
235 7 fvmpt2 ( ( 𝑘 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ∈ ℤ ) → ( 𝐼𝑘 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) )
236 89 234 235 syl2anc ( ( 𝜑𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝐼𝑘 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) )
237 236 adantlr ( ( ( 𝜑𝑧 = 𝐴 ) ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝐼𝑘 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) )
238 oveq1 ( 𝑧 = 𝐴 → ( 𝑧𝑘 ) = ( 𝐴𝑘 ) )
239 238 ad2antlr ( ( ( 𝜑𝑧 = 𝐴 ) ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝑧𝑘 ) = ( 𝐴𝑘 ) )
240 237 239 oveq12d ( ( ( 𝜑𝑧 = 𝐴 ) ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( ( 𝐼𝑘 ) · ( 𝑧𝑘 ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴𝑘 ) ) )
241 240 sumeq2dv ( ( 𝜑𝑧 = 𝐴 ) → Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼𝑘 ) · ( 𝑧𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴𝑘 ) ) )
242 fzfid ( 𝜑 → ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ∈ Fin )
243 242 131 fsumcl ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴𝑘 ) ) ∈ ℂ )
244 9 241 128 243 fvmptd ( 𝜑 → ( 𝐹𝐴 ) = Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴𝑘 ) ) )
245 21 20 coeid2 ( ( 𝐺 ∈ ( Poly ‘ ℤ ) ∧ 𝐴 ∈ ℂ ) → ( 𝐺𝐴 ) = Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) )
246 3 128 245 syl2anc ( 𝜑 → ( 𝐺𝐴 ) = Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) )
247 246 oveq1d ( 𝜑 → ( ( 𝐺𝐴 ) / ( 𝐴𝑀 ) ) = ( Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) )
248 86 adantr ( ( 𝜑𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ )
249 200 adantl ( ( 𝜑𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℕ0 )
250 248 249 ffvelrnd ( ( 𝜑𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ∈ ℂ )
251 128 adantr ( ( 𝜑𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) → 𝐴 ∈ ℂ )
252 251 249 expcld ( ( 𝜑𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) → ( 𝐴𝑗 ) ∈ ℂ )
253 250 252 mulcld ( ( 𝜑𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) ∈ ℂ )
254 231 166 253 227 fsumdivc ( 𝜑 → ( Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) = Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) )
255 247 254 eqtrd ( 𝜑 → ( ( 𝐺𝐴 ) / ( 𝐴𝑀 ) ) = Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴𝑗 ) ) / ( 𝐴𝑀 ) ) )
256 233 244 255 3eqtr4d ( 𝜑 → ( 𝐹𝐴 ) = ( ( 𝐺𝐴 ) / ( 𝐴𝑀 ) ) )
257 5 oveq1d ( 𝜑 → ( ( 𝐺𝐴 ) / ( 𝐴𝑀 ) ) = ( 0 / ( 𝐴𝑀 ) ) )
258 256 257 228 3eqtrd ( 𝜑 → ( 𝐹𝐴 ) = 0 )
259 125 258 jca ( 𝜑 → ( ( ( coeff ‘ 𝐹 ) ‘ 0 ) ≠ 0 ∧ ( 𝐹𝐴 ) = 0 ) )
260 fveq2 ( 𝑓 = 𝐹 → ( coeff ‘ 𝑓 ) = ( coeff ‘ 𝐹 ) )
261 260 fveq1d ( 𝑓 = 𝐹 → ( ( coeff ‘ 𝑓 ) ‘ 0 ) = ( ( coeff ‘ 𝐹 ) ‘ 0 ) )
262 261 neeq1d ( 𝑓 = 𝐹 → ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ↔ ( ( coeff ‘ 𝐹 ) ‘ 0 ) ≠ 0 ) )
263 fveq1 ( 𝑓 = 𝐹 → ( 𝑓𝐴 ) = ( 𝐹𝐴 ) )
264 263 eqeq1d ( 𝑓 = 𝐹 → ( ( 𝑓𝐴 ) = 0 ↔ ( 𝐹𝐴 ) = 0 ) )
265 262 264 anbi12d ( 𝑓 = 𝐹 → ( ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓𝐴 ) = 0 ) ↔ ( ( ( coeff ‘ 𝐹 ) ‘ 0 ) ≠ 0 ∧ ( 𝐹𝐴 ) = 0 ) ) )
266 265 rspcev ( ( 𝐹 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝐹 ) ‘ 0 ) ≠ 0 ∧ ( 𝐹𝐴 ) = 0 ) ) → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓𝐴 ) = 0 ) )
267 60 259 266 syl2anc ( 𝜑 → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓𝐴 ) = 0 ) )