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
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ ) |
12 |
|
plyf |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ ) |
13 |
3 12
|
syl |
⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ ) |
14 |
13
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℂ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ ) |
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
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) ∈ ℂ ) |
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
|
syl5eq |
⊢ ( 𝐹 = 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
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ ) |
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 |
|
ffvelrn |
⊢ ( ( 𝐺 : ℂ ⟶ ℂ ∧ 0 ∈ ℂ ) → ( 𝐺 ‘ 0 ) ∈ ℂ ) |
191 |
10 189 190
|
sylancl |
⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) ∈ ℂ ) |
192 |
13 191
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 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 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑀 · 𝑁 ) ) |