Metamath Proof Explorer

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 biimtrrdi ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑀 ) = 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 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑀 · 𝑁 ) )