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 ) )