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 sselid ⊢ ( 𝜑 → 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 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 sselid ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
109 108 addlidd ⊢ ( 𝜑 → ( 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 ffvelcdmd ⊢ ( 𝜑 → ( ( 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 sselid ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
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 sselid ⊢ ( 𝜑 → ( 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 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ) )