Theorem dgrcolem2

Description: Lemma for dgrco . (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Hypotheses	dgrco.1	⊢ 𝑀 = ( deg ‘ 𝐹 )
	dgrco.2	⊢ 𝑁 = ( deg ‘ 𝐺 )
	dgrco.3	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
	dgrco.4	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
	dgrco.5	⊢ 𝐴 = ( coeff ‘ 𝐹 )
	dgrco.6	⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
	dgrco.7	⊢ ( 𝜑 → 𝑀 = ( 𝐷 + 1 ) )
	dgrco.8	⊢ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝐷 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
Assertion	dgrcolem2	⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑀 · 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		dgrco.1	⊢ 𝑀 = ( deg ‘ 𝐹 )
2		dgrco.2	⊢ 𝑁 = ( deg ‘ 𝐺 )
3		dgrco.3	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4		dgrco.4	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
5		dgrco.5	⊢ 𝐴 = ( coeff ‘ 𝐹 )
6		dgrco.6	⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
7		dgrco.7	⊢ ( 𝜑 → 𝑀 = ( 𝐷 + 1 ) )
8		dgrco.8	⊢ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( deg ‘ 𝑓 ) ≤ 𝐷 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) )
9		plyf	⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 : ℂ ⟶ ℂ )
10	4 9	syl	⊢ ( 𝜑 → 𝐺 : ℂ ⟶ ℂ )
11	10	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
12		plyf	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
13	3 12	syl	⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
14	13	ffvelcdmda	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℂ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
15	11 14	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
16	5	coef3	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
17	3 16	syl	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
18		dgrcl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
19	3 18	syl	⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 )
20	1 19	eqeltrid	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
21	17 20	ffvelcdmd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) ∈ ℂ )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐴 ‘ 𝑀 ) ∈ ℂ )
23	20	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑀 ∈ ℕ0 )
24	11 23	expcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ∈ ℂ )
25	22 24	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ∈ ℂ )
26	15 25	npcand	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) + ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
27	26	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) + ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
28		cnex	⊢ ℂ ∈ V
29	28	a1i	⊢ ( 𝜑 → ℂ ∈ V )
30	15 25	subcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ∈ ℂ )
31		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) )
32		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) )
33	29 30 25 31 32	offval2	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ∘f + ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) + ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) )
34	10	feqmptd	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝐺 ‘ 𝑥 ) ) )
35	13	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℂ ↦ ( 𝐹 ‘ 𝑦 ) ) )
36		fveq2	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
37	11 34 35 36	fmptco	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) = ( 𝑥 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
38	27 33 37	3eqtr4rd	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) = ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ∘f + ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) )
39	38	fveq2d	⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) = ( deg ‘ ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ∘f + ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ) )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) = ( deg ‘ ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ∘f + ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ) )
41	29 15 25 37 32	offval2	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) ∘f − ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) )
42		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
43	42 3	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℂ ) )
44	42 4	sselid	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ ℂ ) )
45		addcl	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝑧 + 𝑤 ) ∈ ℂ )
46	45	adantl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ) → ( 𝑧 + 𝑤 ) ∈ ℂ )
47		mulcl	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝑧 · 𝑤 ) ∈ ℂ )
48	47	adantl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ) → ( 𝑧 · 𝑤 ) ∈ ℂ )
49	43 44 46 48	plyco	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ∈ ( Poly ‘ ℂ ) )
50		eqidd	⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) )
51		oveq1	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( 𝑦 ↑ 𝑀 ) = ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) )
52	51	oveq2d	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) = ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) )
53	11 34 50 52	fmptco	⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ∘ 𝐺 ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) )
54		ssidd	⊢ ( 𝜑 → ℂ ⊆ ℂ )
55		eqid	⊢ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) )
56	55	ply1term	⊢ ( ( ℂ ⊆ ℂ ∧ ( 𝐴 ‘ 𝑀 ) ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ∈ ( Poly ‘ ℂ ) )
57	54 21 20 56	syl3anc	⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ∈ ( Poly ‘ ℂ ) )
58	57 44 46 48	plyco	⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ∘ 𝐺 ) ∈ ( Poly ‘ ℂ ) )
59	53 58	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ∈ ( Poly ‘ ℂ ) )
60		plysubcl	⊢ ( ( ( 𝐹 ∘ 𝐺 ) ∈ ( Poly ‘ ℂ ) ∧ ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ∈ ( Poly ‘ ℂ ) ) → ( ( 𝐹 ∘ 𝐺 ) ∘f − ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ∈ ( Poly ‘ ℂ ) )
61	49 59 60	syl2anc	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) ∘f − ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ∈ ( Poly ‘ ℂ ) )
62	41 61	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ∈ ( Poly ‘ ℂ ) )
63	62	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ∈ ( Poly ‘ ℂ ) )
64	59	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ∈ ( Poly ‘ ℂ ) )
65		nn0p1nn	⊢ ( 𝐷 ∈ ℕ0 → ( 𝐷 + 1 ) ∈ ℕ )
66	6 65	syl	⊢ ( 𝜑 → ( 𝐷 + 1 ) ∈ ℕ )
67	7 66	eqeltrd	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
68	67	nngt0d	⊢ ( 𝜑 → 0 < 𝑀 )
69		fveq2	⊢ ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) = 0𝑝 → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) = ( deg ‘ 0𝑝 ) )
70		dgr0	⊢ ( deg ‘ 0𝑝 ) = 0
71	69 70	eqtrdi	⊢ ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) = 0𝑝 → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) = 0 )
72	71	breq1d	⊢ ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) = 0𝑝 → ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < 𝑀 ↔ 0 < 𝑀 ) )
73	68 72	syl5ibrcom	⊢ ( 𝜑 → ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) = 0𝑝 → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < 𝑀 ) )
74		idd	⊢ ( 𝜑 → ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < 𝑀 → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < 𝑀 ) )
75		eqid	⊢ ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) = ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) )
76	1 75	dgrsub	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ∈ ( Poly ‘ ℂ ) ) → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ≤ if ( 𝑀 ≤ ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) , ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) , 𝑀 ) )
77	43 57 76	syl2anc	⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ≤ if ( 𝑀 ≤ ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) , ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) , 𝑀 ) )
78	67	nnne0d	⊢ ( 𝜑 → 𝑀 ≠ 0 )
79	1 5	dgreq0	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑀 ) = 0 ) )
80	3 79	syl	⊢ ( 𝜑 → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑀 ) = 0 ) )
81		fveq2	⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = ( deg ‘ 0𝑝 ) )
82	81 70	eqtrdi	⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = 0 )
83	1 82	eqtrid	⊢ ( 𝐹 = 0𝑝 → 𝑀 = 0 )
84	80 83	syl6bir	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑀 ) = 0 → 𝑀 = 0 ) )
85	84	necon3d	⊢ ( 𝜑 → ( 𝑀 ≠ 0 → ( 𝐴 ‘ 𝑀 ) ≠ 0 ) )
86	78 85	mpd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) ≠ 0 )
87	55	dgr1term	⊢ ( ( ( 𝐴 ‘ 𝑀 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ∧ 𝑀 ∈ ℕ0 ) → ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) = 𝑀 )
88	21 86 20 87	syl3anc	⊢ ( 𝜑 → ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) = 𝑀 )
89	88	ifeq1d	⊢ ( 𝜑 → if ( 𝑀 ≤ ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) , ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) , 𝑀 ) = if ( 𝑀 ≤ ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) , 𝑀 , 𝑀 ) )
90		ifid	⊢ if ( 𝑀 ≤ ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) , 𝑀 , 𝑀 ) = 𝑀
91	89 90	eqtrdi	⊢ ( 𝜑 → if ( 𝑀 ≤ ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) , ( deg ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) , 𝑀 ) = 𝑀 )
92	77 91	breqtrd	⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ≤ 𝑀 )
93		eqid	⊢ ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) = ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) )
94	5 93	coesub	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ∈ ( Poly ‘ ℂ ) ) → ( coeff ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) = ( 𝐴 ∘f − ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) )
95	43 57 94	syl2anc	⊢ ( 𝜑 → ( coeff ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) = ( 𝐴 ∘f − ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) )
96	95	fveq1d	⊢ ( 𝜑 → ( ( coeff ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ‘ 𝑀 ) = ( ( 𝐴 ∘f − ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ‘ 𝑀 ) )
97	17	ffnd	⊢ ( 𝜑 → 𝐴 Fn ℕ0 )
98	93	coef3	⊢ ( ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ∈ ( Poly ‘ ℂ ) → ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) : ℕ0 ⟶ ℂ )
99	57 98	syl	⊢ ( 𝜑 → ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) : ℕ0 ⟶ ℂ )
100	99	ffnd	⊢ ( 𝜑 → ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) Fn ℕ0 )
101		nn0ex	⊢ ℕ0 ∈ V
102	101	a1i	⊢ ( 𝜑 → ℕ0 ∈ V )
103		inidm	⊢ ( ℕ0 ∩ ℕ0 ) = ℕ0
104		eqidd	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑀 ) = ( 𝐴 ‘ 𝑀 ) )
105	55	coe1term	⊢ ( ( ( 𝐴 ‘ 𝑀 ) ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ‘ 𝑀 ) = if ( 𝑀 = 𝑀 , ( 𝐴 ‘ 𝑀 ) , 0 ) )
106	21 20 20 105	syl3anc	⊢ ( 𝜑 → ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ‘ 𝑀 ) = if ( 𝑀 = 𝑀 , ( 𝐴 ‘ 𝑀 ) , 0 ) )
107		eqid	⊢ 𝑀 = 𝑀
108	107	iftruei	⊢ if ( 𝑀 = 𝑀 , ( 𝐴 ‘ 𝑀 ) , 0 ) = ( 𝐴 ‘ 𝑀 )
109	106 108	eqtrdi	⊢ ( 𝜑 → ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ‘ 𝑀 ) = ( 𝐴 ‘ 𝑀 ) )
110	109	adantr	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ0 ) → ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ‘ 𝑀 ) = ( 𝐴 ‘ 𝑀 ) )
111	97 100 102 102 103 104 110	ofval	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴 ∘f − ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ‘ 𝑀 ) = ( ( 𝐴 ‘ 𝑀 ) − ( 𝐴 ‘ 𝑀 ) ) )
112	20 111	mpdan	⊢ ( 𝜑 → ( ( 𝐴 ∘f − ( coeff ‘ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ‘ 𝑀 ) = ( ( 𝐴 ‘ 𝑀 ) − ( 𝐴 ‘ 𝑀 ) ) )
113	21	subidd	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑀 ) − ( 𝐴 ‘ 𝑀 ) ) = 0 )
114	96 112 113	3eqtrd	⊢ ( 𝜑 → ( ( coeff ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ‘ 𝑀 ) = 0 )
115		plysubcl	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ∈ ( Poly ‘ ℂ ) ) → ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ∈ ( Poly ‘ ℂ ) )
116	43 57 115	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ∈ ( Poly ‘ ℂ ) )
117		eqid	⊢ ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) = ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) )
118		eqid	⊢ ( coeff ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) = ( coeff ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) )
119	117 118	dgrlt	⊢ ( ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ∈ ( Poly ‘ ℂ ) ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < 𝑀 ) ↔ ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ≤ 𝑀 ∧ ( ( coeff ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ‘ 𝑀 ) = 0 ) ) )
120	116 20 119	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < 𝑀 ) ↔ ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ≤ 𝑀 ∧ ( ( coeff ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ‘ 𝑀 ) = 0 ) ) )
121	92 114 120	mpbir2and	⊢ ( 𝜑 → ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < 𝑀 ) )
122	73 74 121	mpjaod	⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < 𝑀 )
123	122	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < 𝑀 )
124		dgrcl	⊢ ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ∈ ℕ0 )
125	116 124	syl	⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ∈ ℕ0 )
126	125	nn0red	⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ∈ ℝ )
127	126	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ∈ ℝ )
128	20	nn0red	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
129	128	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℝ )
130		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
131	130	adantl	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
132		nngt0	⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
133	132	adantl	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 0 < 𝑁 )
134		ltmul1	⊢ ( ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < 𝑀 ↔ ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) · 𝑁 ) < ( 𝑀 · 𝑁 ) ) )
135	127 129 131 133 134	syl112anc	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < 𝑀 ↔ ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) · 𝑁 ) < ( 𝑀 · 𝑁 ) ) )
136	123 135	mpbid	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) · 𝑁 ) < ( 𝑀 · 𝑁 ) )
137	13	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
138	21	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐴 ‘ 𝑀 ) ∈ ℂ )
139		id	⊢ ( 𝑦 ∈ ℂ → 𝑦 ∈ ℂ )
140		expcl	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑦 ↑ 𝑀 ) ∈ ℂ )
141	139 20 140	syl2anr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ 𝑀 ) ∈ ℂ )
142	138 141	mulcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ∈ ℂ )
143	29 137 142 35 50	offval2	⊢ ( 𝜑 → ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝐹 ‘ 𝑦 ) − ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) )
144	36 52	oveq12d	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) − ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) )
145	11 34 143 144	fmptco	⊢ ( 𝜑 → ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ∘ 𝐺 ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) )
146	145	fveq2d	⊢ ( 𝜑 → ( deg ‘ ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ∘ 𝐺 ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ) )
147	122 7	breqtrd	⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < ( 𝐷 + 1 ) )
148		nn0leltp1	⊢ ( ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) → ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ≤ 𝐷 ↔ ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < ( 𝐷 + 1 ) ) )
149	125 6 148	syl2anc	⊢ ( 𝜑 → ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ≤ 𝐷 ↔ ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) < ( 𝐷 + 1 ) ) )
150	147 149	mpbird	⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ≤ 𝐷 )
151		fveq2	⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) → ( deg ‘ 𝑓 ) = ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) )
152	151	breq1d	⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) → ( ( deg ‘ 𝑓 ) ≤ 𝐷 ↔ ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ≤ 𝐷 ) )
153		coeq1	⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) → ( 𝑓 ∘ 𝐺 ) = ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ∘ 𝐺 ) )
154	153	fveq2d	⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( deg ‘ ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ∘ 𝐺 ) ) )
155	151	oveq1d	⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) → ( ( deg ‘ 𝑓 ) · 𝑁 ) = ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) · 𝑁 ) )
156	154 155	eqeq12d	⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) → ( ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ↔ ( deg ‘ ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ∘ 𝐺 ) ) = ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) · 𝑁 ) ) )
157	152 156	imbi12d	⊢ ( 𝑓 = ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) → ( ( ( deg ‘ 𝑓 ) ≤ 𝐷 → ( deg ‘ ( 𝑓 ∘ 𝐺 ) ) = ( ( deg ‘ 𝑓 ) · 𝑁 ) ) ↔ ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ≤ 𝐷 → ( deg ‘ ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ∘ 𝐺 ) ) = ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) · 𝑁 ) ) ) )
158	157 8 116	rspcdva	⊢ ( 𝜑 → ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) ≤ 𝐷 → ( deg ‘ ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ∘ 𝐺 ) ) = ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) · 𝑁 ) ) )
159	150 158	mpd	⊢ ( 𝜑 → ( deg ‘ ( ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ∘ 𝐺 ) ) = ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) · 𝑁 ) )
160	146 159	eqtr3d	⊢ ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ) = ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) · 𝑁 ) )
161	160	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ) = ( ( deg ‘ ( 𝐹 ∘f − ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( 𝑦 ↑ 𝑀 ) ) ) ) ) · 𝑁 ) )
162		fconstmpt	⊢ ( ℂ × { ( 𝐴 ‘ 𝑀 ) } ) = ( 𝑥 ∈ ℂ ↦ ( 𝐴 ‘ 𝑀 ) )
163	162	a1i	⊢ ( 𝜑 → ( ℂ × { ( 𝐴 ‘ 𝑀 ) } ) = ( 𝑥 ∈ ℂ ↦ ( 𝐴 ‘ 𝑀 ) ) )
164		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) )
165	29 22 24 163 164	offval2	⊢ ( 𝜑 → ( ( ℂ × { ( 𝐴 ‘ 𝑀 ) } ) ∘f · ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) )
166	165	fveq2d	⊢ ( 𝜑 → ( deg ‘ ( ( ℂ × { ( 𝐴 ‘ 𝑀 ) } ) ∘f · ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) )
167		eqidd	⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑀 ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑀 ) ) )
168	11 34 167 51	fmptco	⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑀 ) ) ∘ 𝐺 ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) )
169		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
170		plypow	⊢ ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑀 ) ) ∈ ( Poly ‘ ℂ ) )
171	54 169 20 170	syl3anc	⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑀 ) ) ∈ ( Poly ‘ ℂ ) )
172	171 44 46 48	plyco	⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑀 ) ) ∘ 𝐺 ) ∈ ( Poly ‘ ℂ ) )
173	168 172	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ∈ ( Poly ‘ ℂ ) )
174		dgrmulc	⊢ ( ( ( 𝐴 ‘ 𝑀 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ∧ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ∈ ( Poly ‘ ℂ ) ) → ( deg ‘ ( ( ℂ × { ( 𝐴 ‘ 𝑀 ) } ) ∘f · ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) )
175	21 86 173 174	syl3anc	⊢ ( 𝜑 → ( deg ‘ ( ( ℂ × { ( 𝐴 ‘ 𝑀 ) } ) ∘f · ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) )
176	166 175	eqtr3d	⊢ ( 𝜑 → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) )
177	176	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) )
178	67	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℕ )
179		simpr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
180	4	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
181	2 178 179 180	dgrcolem1	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) = ( 𝑀 · 𝑁 ) )
182	177 181	eqtrd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) = ( 𝑀 · 𝑁 ) )
183	136 161 182	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ) < ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) )
184		eqid	⊢ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) )
185		eqid	⊢ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) )
186	184 185	dgradd2	⊢ ( ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ∈ ( Poly ‘ ℂ ) ∧ ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ) < ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ) → ( deg ‘ ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ∘f + ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) )
187	63 64 183 186	syl3anc	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( deg ‘ ( ( 𝑥 ∈ ℂ ↦ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) − ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ∘f + ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) ) = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑀 ) · ( ( 𝐺 ‘ 𝑥 ) ↑ 𝑀 ) ) ) ) )
188	40 187 182	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑀 · 𝑁 ) )
189		0cn	⊢ 0 ∈ ℂ
190		ffvelcdm	⊢ ( ( 𝐺 : ℂ ⟶ ℂ ∧ 0 ∈ ℂ ) → ( 𝐺 ‘ 0 ) ∈ ℂ )
191	10 189 190	sylancl	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) ∈ ℂ )
192	13 191	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 0 ) ) ∈ ℂ )
193		0dgr	⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 0 ) ) ∈ ℂ → ( deg ‘ ( ℂ × { ( 𝐹 ‘ ( 𝐺 ‘ 0 ) ) } ) ) = 0 )
194	192 193	syl	⊢ ( 𝜑 → ( deg ‘ ( ℂ × { ( 𝐹 ‘ ( 𝐺 ‘ 0 ) ) } ) ) = 0 )
195	20	nn0cnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
196	195	mul01d	⊢ ( 𝜑 → ( 𝑀 · 0 ) = 0 )
197	194 196	eqtr4d	⊢ ( 𝜑 → ( deg ‘ ( ℂ × { ( 𝐹 ‘ ( 𝐺 ‘ 0 ) ) } ) ) = ( 𝑀 · 0 ) )
198	197	adantr	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( deg ‘ ( ℂ × { ( 𝐹 ‘ ( 𝐺 ‘ 0 ) ) } ) ) = ( 𝑀 · 0 ) )
199	191	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ) ∧ 𝑥 ∈ ℂ ) → ( 𝐺 ‘ 0 ) ∈ ℂ )
200		simpr	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
201	2 200	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( deg ‘ 𝐺 ) = 0 )
202		0dgrb	⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( ( deg ‘ 𝐺 ) = 0 ↔ 𝐺 = ( ℂ × { ( 𝐺 ‘ 0 ) } ) ) )
203	4 202	syl	⊢ ( 𝜑 → ( ( deg ‘ 𝐺 ) = 0 ↔ 𝐺 = ( ℂ × { ( 𝐺 ‘ 0 ) } ) ) )
204	203	adantr	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( ( deg ‘ 𝐺 ) = 0 ↔ 𝐺 = ( ℂ × { ( 𝐺 ‘ 0 ) } ) ) )
205	201 204	mpbid	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝐺 = ( ℂ × { ( 𝐺 ‘ 0 ) } ) )
206		fconstmpt	⊢ ( ℂ × { ( 𝐺 ‘ 0 ) } ) = ( 𝑥 ∈ ℂ ↦ ( 𝐺 ‘ 0 ) )
207	205 206	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝐺 ‘ 0 ) ) )
208	35	adantr	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝐹 = ( 𝑦 ∈ ℂ ↦ ( 𝐹 ‘ 𝑦 ) ) )
209		fveq2	⊢ ( 𝑦 = ( 𝐺 ‘ 0 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 0 ) ) )
210	199 207 208 209	fmptco	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 𝐹 ∘ 𝐺 ) = ( 𝑥 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝐺 ‘ 0 ) ) ) )
211		fconstmpt	⊢ ( ℂ × { ( 𝐹 ‘ ( 𝐺 ‘ 0 ) ) } ) = ( 𝑥 ∈ ℂ ↦ ( 𝐹 ‘ ( 𝐺 ‘ 0 ) ) )
212	210 211	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 𝐹 ∘ 𝐺 ) = ( ℂ × { ( 𝐹 ‘ ( 𝐺 ‘ 0 ) ) } ) )
213	212	fveq2d	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) = ( deg ‘ ( ℂ × { ( 𝐹 ‘ ( 𝐺 ‘ 0 ) ) } ) ) )
214	200	oveq2d	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 𝑀 · 𝑁 ) = ( 𝑀 · 0 ) )
215	198 213 214	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑀 · 𝑁 ) )
216		dgrcl	⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
217	4 216	syl	⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℕ0 )
218	2 217	eqeltrid	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
219		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
220	218 219	sylib	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
221	188 215 220	mpjaodan	⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑀 · 𝑁 ) )