MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dgrcolem2 Structured version   Visualization version   GIF version

Theorem dgrcolem2 23968
Description: Lemma for dgrco 23969. (Contributed by Mario Carneiro, 15-Sep-2014.)
Hypotheses
Ref Expression
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
Ref Expression
dgrcolem2 (𝜑 → (deg‘(𝐹𝐺)) = (𝑀 · 𝑁))
Distinct variable groups:   𝐴,𝑓   𝑓,𝐹   𝑓,𝑀   𝑓,𝑁   𝐷,𝑓   𝑓,𝐺   𝜑,𝑓
Allowed substitution hint:   𝑆(𝑓)

Proof of Theorem dgrcolem2
Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dgrco.4 . . . . . . . . . . 11 (𝜑𝐺 ∈ (Poly‘𝑆))
2 plyf 23892 . . . . . . . . . . 11 (𝐺 ∈ (Poly‘𝑆) → 𝐺:ℂ⟶ℂ)
31, 2syl 17 . . . . . . . . . 10 (𝜑𝐺:ℂ⟶ℂ)
43ffvelrnda 6325 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → (𝐺𝑥) ∈ ℂ)
5 dgrco.3 . . . . . . . . . . 11 (𝜑𝐹 ∈ (Poly‘𝑆))
6 plyf 23892 . . . . . . . . . . 11 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
75, 6syl 17 . . . . . . . . . 10 (𝜑𝐹:ℂ⟶ℂ)
87ffvelrnda 6325 . . . . . . . . 9 ((𝜑 ∧ (𝐺𝑥) ∈ ℂ) → (𝐹‘(𝐺𝑥)) ∈ ℂ)
94, 8syldan 487 . . . . . . . 8 ((𝜑𝑥 ∈ ℂ) → (𝐹‘(𝐺𝑥)) ∈ ℂ)
10 dgrco.5 . . . . . . . . . . . . 13 𝐴 = (coeff‘𝐹)
1110coef3 23926 . . . . . . . . . . . 12 (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
125, 11syl 17 . . . . . . . . . . 11 (𝜑𝐴:ℕ0⟶ℂ)
13 dgrco.1 . . . . . . . . . . . 12 𝑀 = (deg‘𝐹)
14 dgrcl 23927 . . . . . . . . . . . . 13 (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈ ℕ0)
155, 14syl 17 . . . . . . . . . . . 12 (𝜑 → (deg‘𝐹) ∈ ℕ0)
1613, 15syl5eqel 2702 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ0)
1712, 16ffvelrnd 6326 . . . . . . . . . 10 (𝜑 → (𝐴𝑀) ∈ ℂ)
1817adantr 481 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → (𝐴𝑀) ∈ ℂ)
1916adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → 𝑀 ∈ ℕ0)
204, 19expcld 12964 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → ((𝐺𝑥)↑𝑀) ∈ ℂ)
2118, 20mulcld 10020 . . . . . . . 8 ((𝜑𝑥 ∈ ℂ) → ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)) ∈ ℂ)
229, 21npcand 10356 . . . . . . 7 ((𝜑𝑥 ∈ ℂ) → (((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) + ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) = (𝐹‘(𝐺𝑥)))
2322mpteq2dva 4714 . . . . . 6 (𝜑 → (𝑥 ∈ ℂ ↦ (((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) + ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (𝑥 ∈ ℂ ↦ (𝐹‘(𝐺𝑥))))
24 cnex 9977 . . . . . . . 8 ℂ ∈ V
2524a1i 11 . . . . . . 7 (𝜑 → ℂ ∈ V)
269, 21subcld 10352 . . . . . . 7 ((𝜑𝑥 ∈ ℂ) → ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) ∈ ℂ)
27 eqidd 2622 . . . . . . 7 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
28 eqidd 2622 . . . . . . 7 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) = (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))
2925, 26, 21, 27, 28offval2 6879 . . . . . 6 (𝜑 → ((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (𝑥 ∈ ℂ ↦ (((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) + ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
303feqmptd 6216 . . . . . . 7 (𝜑𝐺 = (𝑥 ∈ ℂ ↦ (𝐺𝑥)))
317feqmptd 6216 . . . . . . 7 (𝜑𝐹 = (𝑦 ∈ ℂ ↦ (𝐹𝑦)))
32 fveq2 6158 . . . . . . 7 (𝑦 = (𝐺𝑥) → (𝐹𝑦) = (𝐹‘(𝐺𝑥)))
334, 30, 31, 32fmptco 6362 . . . . . 6 (𝜑 → (𝐹𝐺) = (𝑥 ∈ ℂ ↦ (𝐹‘(𝐺𝑥))))
3423, 29, 333eqtr4rd 2666 . . . . 5 (𝜑 → (𝐹𝐺) = ((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
3534fveq2d 6162 . . . 4 (𝜑 → (deg‘(𝐹𝐺)) = (deg‘((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))))
3635adantr 481 . . 3 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝐹𝐺)) = (deg‘((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))))
3725, 9, 21, 33, 28offval2 6879 . . . . . 6 (𝜑 → ((𝐹𝐺) ∘𝑓 − (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
38 plyssc 23894 . . . . . . . . 9 (Poly‘𝑆) ⊆ (Poly‘ℂ)
3938, 5sseldi 3586 . . . . . . . 8 (𝜑𝐹 ∈ (Poly‘ℂ))
4038, 1sseldi 3586 . . . . . . . 8 (𝜑𝐺 ∈ (Poly‘ℂ))
41 addcl 9978 . . . . . . . . 9 ((𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑧 + 𝑤) ∈ ℂ)
4241adantl 482 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 + 𝑤) ∈ ℂ)
43 mulcl 9980 . . . . . . . . 9 ((𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑧 · 𝑤) ∈ ℂ)
4443adantl 482 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 · 𝑤) ∈ ℂ)
4539, 40, 42, 44plyco 23935 . . . . . . 7 (𝜑 → (𝐹𝐺) ∈ (Poly‘ℂ))
46 eqidd 2622 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) = (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))
47 oveq1 6622 . . . . . . . . . 10 (𝑦 = (𝐺𝑥) → (𝑦𝑀) = ((𝐺𝑥)↑𝑀))
4847oveq2d 6631 . . . . . . . . 9 (𝑦 = (𝐺𝑥) → ((𝐴𝑀) · (𝑦𝑀)) = ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))
494, 30, 46, 48fmptco 6362 . . . . . . . 8 (𝜑 → ((𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∘ 𝐺) = (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))
50 ssid 3609 . . . . . . . . . . 11 ℂ ⊆ ℂ
5150a1i 11 . . . . . . . . . 10 (𝜑 → ℂ ⊆ ℂ)
52 eqid 2621 . . . . . . . . . . 11 (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) = (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))
5352ply1term 23898 . . . . . . . . . 10 ((ℂ ⊆ ℂ ∧ (𝐴𝑀) ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∈ (Poly‘ℂ))
5451, 17, 16, 53syl3anc 1323 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∈ (Poly‘ℂ))
5554, 40, 42, 44plyco 23935 . . . . . . . 8 (𝜑 → ((𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∘ 𝐺) ∈ (Poly‘ℂ))
5649, 55eqeltrrd 2699 . . . . . . 7 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) ∈ (Poly‘ℂ))
57 plysubcl 23916 . . . . . . 7 (((𝐹𝐺) ∈ (Poly‘ℂ) ∧ (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) ∈ (Poly‘ℂ)) → ((𝐹𝐺) ∘𝑓 − (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∈ (Poly‘ℂ))
5845, 56, 57syl2anc 692 . . . . . 6 (𝜑 → ((𝐹𝐺) ∘𝑓 − (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∈ (Poly‘ℂ))
5937, 58eqeltrrd 2699 . . . . 5 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∈ (Poly‘ℂ))
6059adantr 481 . . . 4 ((𝜑𝑁 ∈ ℕ) → (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∈ (Poly‘ℂ))
6156adantr 481 . . . 4 ((𝜑𝑁 ∈ ℕ) → (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) ∈ (Poly‘ℂ))
62 dgrco.7 . . . . . . . . . . 11 (𝜑𝑀 = (𝐷 + 1))
63 dgrco.6 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℕ0)
64 nn0p1nn 11292 . . . . . . . . . . . 12 (𝐷 ∈ ℕ0 → (𝐷 + 1) ∈ ℕ)
6563, 64syl 17 . . . . . . . . . . 11 (𝜑 → (𝐷 + 1) ∈ ℕ)
6662, 65eqeltrd 2698 . . . . . . . . . 10 (𝜑𝑀 ∈ ℕ)
6766nngt0d 11024 . . . . . . . . 9 (𝜑 → 0 < 𝑀)
68 fveq2 6158 . . . . . . . . . . 11 ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) = (deg‘0𝑝))
69 dgr0 23956 . . . . . . . . . . 11 (deg‘0𝑝) = 0
7068, 69syl6eq 2671 . . . . . . . . . 10 ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) = 0)
7170breq1d 4633 . . . . . . . . 9 ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀 ↔ 0 < 𝑀))
7267, 71syl5ibrcom 237 . . . . . . . 8 (𝜑 → ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀))
73 idd 24 . . . . . . . 8 (𝜑 → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀))
74 eqid 2621 . . . . . . . . . . . 12 (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))
7513, 74dgrsub 23966 . . . . . . . . . . 11 ((𝐹 ∈ (Poly‘ℂ) ∧ (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∈ (Poly‘ℂ)) → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), 𝑀))
7639, 54, 75syl2anc 692 . . . . . . . . . 10 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), 𝑀))
7766nnne0d 11025 . . . . . . . . . . . . . 14 (𝜑𝑀 ≠ 0)
7813, 10dgreq0 23959 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴𝑀) = 0))
795, 78syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴𝑀) = 0))
80 fveq2 6158 . . . . . . . . . . . . . . . . . 18 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
8180, 69syl6eq 2671 . . . . . . . . . . . . . . . . 17 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
8213, 81syl5eq 2667 . . . . . . . . . . . . . . . 16 (𝐹 = 0𝑝𝑀 = 0)
8379, 82syl6bir 244 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴𝑀) = 0 → 𝑀 = 0))
8483necon3d 2811 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 ≠ 0 → (𝐴𝑀) ≠ 0))
8577, 84mpd 15 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝑀) ≠ 0)
8652dgr1term 23954 . . . . . . . . . . . . 13 (((𝐴𝑀) ∈ ℂ ∧ (𝐴𝑀) ≠ 0 ∧ 𝑀 ∈ ℕ0) → (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 𝑀)
8717, 85, 16, 86syl3anc 1323 . . . . . . . . . . . 12 (𝜑 → (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 𝑀)
8887ifeq1d 4082 . . . . . . . . . . 11 (𝜑 → if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), 𝑀) = if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), 𝑀, 𝑀))
89 ifid 4103 . . . . . . . . . . 11 if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), 𝑀, 𝑀) = 𝑀
9088, 89syl6eq 2671 . . . . . . . . . 10 (𝜑 → if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), 𝑀) = 𝑀)
9176, 90breqtrd 4649 . . . . . . . . 9 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝑀)
92 eqid 2621 . . . . . . . . . . . . 13 (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))
9310, 92coesub 23951 . . . . . . . . . . . 12 ((𝐹 ∈ (Poly‘ℂ) ∧ (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∈ (Poly‘ℂ)) → (coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) = (𝐴𝑓 − (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))))
9439, 54, 93syl2anc 692 . . . . . . . . . . 11 (𝜑 → (coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) = (𝐴𝑓 − (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))))
9594fveq1d 6160 . . . . . . . . . 10 (𝜑 → ((coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀) = ((𝐴𝑓 − (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀))
96 ffn 6012 . . . . . . . . . . . . 13 (𝐴:ℕ0⟶ℂ → 𝐴 Fn ℕ0)
9712, 96syl 17 . . . . . . . . . . . 12 (𝜑𝐴 Fn ℕ0)
9892coef3 23926 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∈ (Poly‘ℂ) → (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))):ℕ0⟶ℂ)
9954, 98syl 17 . . . . . . . . . . . . 13 (𝜑 → (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))):ℕ0⟶ℂ)
100 ffn 6012 . . . . . . . . . . . . 13 ((coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))):ℕ0⟶ℂ → (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) Fn ℕ0)
10199, 100syl 17 . . . . . . . . . . . 12 (𝜑 → (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) Fn ℕ0)
102 nn0ex 11258 . . . . . . . . . . . . 13 0 ∈ V
103102a1i 11 . . . . . . . . . . . 12 (𝜑 → ℕ0 ∈ V)
104 inidm 3806 . . . . . . . . . . . 12 (ℕ0 ∩ ℕ0) = ℕ0
105 eqidd 2622 . . . . . . . . . . . 12 ((𝜑𝑀 ∈ ℕ0) → (𝐴𝑀) = (𝐴𝑀))
10652coe1term 23953 . . . . . . . . . . . . . . 15 (((𝐴𝑀) ∈ ℂ ∧ 𝑀 ∈ ℕ0𝑀 ∈ ℕ0) → ((coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))‘𝑀) = if(𝑀 = 𝑀, (𝐴𝑀), 0))
10717, 16, 16, 106syl3anc 1323 . . . . . . . . . . . . . 14 (𝜑 → ((coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))‘𝑀) = if(𝑀 = 𝑀, (𝐴𝑀), 0))
108 eqid 2621 . . . . . . . . . . . . . . 15 𝑀 = 𝑀
109108iftruei 4071 . . . . . . . . . . . . . 14 if(𝑀 = 𝑀, (𝐴𝑀), 0) = (𝐴𝑀)
110107, 109syl6eq 2671 . . . . . . . . . . . . 13 (𝜑 → ((coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))‘𝑀) = (𝐴𝑀))
111110adantr 481 . . . . . . . . . . . 12 ((𝜑𝑀 ∈ ℕ0) → ((coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))‘𝑀) = (𝐴𝑀))
11297, 101, 103, 103, 104, 105, 111ofval 6871 . . . . . . . . . . 11 ((𝜑𝑀 ∈ ℕ0) → ((𝐴𝑓 − (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀) = ((𝐴𝑀) − (𝐴𝑀)))
11316, 112mpdan 701 . . . . . . . . . 10 (𝜑 → ((𝐴𝑓 − (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀) = ((𝐴𝑀) − (𝐴𝑀)))
11417subidd 10340 . . . . . . . . . 10 (𝜑 → ((𝐴𝑀) − (𝐴𝑀)) = 0)
11595, 113, 1143eqtrd 2659 . . . . . . . . 9 (𝜑 → ((coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀) = 0)
116 plysubcl 23916 . . . . . . . . . . 11 ((𝐹 ∈ (Poly‘ℂ) ∧ (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∈ (Poly‘ℂ)) → (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∈ (Poly‘ℂ))
11739, 54, 116syl2anc 692 . . . . . . . . . 10 (𝜑 → (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∈ (Poly‘ℂ))
118 eqid 2621 . . . . . . . . . . 11 (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) = (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))
119 eqid 2621 . . . . . . . . . . 11 (coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) = (coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))
120118, 119dgrlt 23960 . . . . . . . . . 10 (((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∈ (Poly‘ℂ) ∧ 𝑀 ∈ ℕ0) → (((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 ∨ (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀) ↔ ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝑀 ∧ ((coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀) = 0)))
121117, 16, 120syl2anc 692 . . . . . . . . 9 (𝜑 → (((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 ∨ (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀) ↔ ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝑀 ∧ ((coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀) = 0)))
12291, 115, 121mpbir2and 956 . . . . . . . 8 (𝜑 → ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 ∨ (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀))
12372, 73, 122mpjaod 396 . . . . . . 7 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀)
124123adantr 481 . . . . . 6 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀)
125 dgrcl 23927 . . . . . . . . . 10 ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∈ (Poly‘ℂ) → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ∈ ℕ0)
126117, 125syl 17 . . . . . . . . 9 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ∈ ℕ0)
127126nn0red 11312 . . . . . . . 8 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ∈ ℝ)
128127adantr 481 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ∈ ℝ)
12916nn0red 11312 . . . . . . . 8 (𝜑𝑀 ∈ ℝ)
130129adantr 481 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → 𝑀 ∈ ℝ)
131 nnre 10987 . . . . . . . 8 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
132131adantl 482 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → 𝑁 ∈ ℝ)
133 nngt0 11009 . . . . . . . 8 (𝑁 ∈ ℕ → 0 < 𝑁)
134133adantl 482 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → 0 < 𝑁)
135 ltmul1 10833 . . . . . . 7 (((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀 ↔ ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁) < (𝑀 · 𝑁)))
136128, 130, 132, 134, 135syl112anc 1327 . . . . . 6 ((𝜑𝑁 ∈ ℕ) → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀 ↔ ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁) < (𝑀 · 𝑁)))
137124, 136mpbid 222 . . . . 5 ((𝜑𝑁 ∈ ℕ) → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁) < (𝑀 · 𝑁))
1387ffvelrnda 6325 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → (𝐹𝑦) ∈ ℂ)
13917adantr 481 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℂ) → (𝐴𝑀) ∈ ℂ)
140 id 22 . . . . . . . . . . . 12 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
141 expcl 12834 . . . . . . . . . . . 12 ((𝑦 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑦𝑀) ∈ ℂ)
142140, 16, 141syl2anr 495 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℂ) → (𝑦𝑀) ∈ ℂ)
143139, 142mulcld 10020 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → ((𝐴𝑀) · (𝑦𝑀)) ∈ ℂ)
14425, 138, 143, 31, 46offval2 6879 . . . . . . . . 9 (𝜑 → (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = (𝑦 ∈ ℂ ↦ ((𝐹𝑦) − ((𝐴𝑀) · (𝑦𝑀)))))
14532, 48oveq12d 6633 . . . . . . . . 9 (𝑦 = (𝐺𝑥) → ((𝐹𝑦) − ((𝐴𝑀) · (𝑦𝑀))) = ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))
1464, 30, 144, 145fmptco 6362 . . . . . . . 8 (𝜑 → ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺) = (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
147146fveq2d 6162 . . . . . . 7 (𝜑 → (deg‘((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺)) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))))
148 dgrco.8 . . . . . . . 8 (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝐷 → (deg‘(𝑓𝐺)) = ((deg‘𝑓) · 𝑁)))
149123, 62breqtrd 4649 . . . . . . . . 9 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < (𝐷 + 1))
150 nn0leltp1 11396 . . . . . . . . . 10 (((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ∈ ℕ0𝐷 ∈ ℕ0) → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝐷 ↔ (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < (𝐷 + 1)))
151126, 63, 150syl2anc 692 . . . . . . . . 9 (𝜑 → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝐷 ↔ (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < (𝐷 + 1)))
152149, 151mpbird 247 . . . . . . . 8 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝐷)
153 fveq2 6158 . . . . . . . . . . 11 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → (deg‘𝑓) = (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))))
154153breq1d 4633 . . . . . . . . . 10 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → ((deg‘𝑓) ≤ 𝐷 ↔ (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝐷))
155 coeq1 5249 . . . . . . . . . . . 12 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → (𝑓𝐺) = ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺))
156155fveq2d 6162 . . . . . . . . . . 11 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → (deg‘(𝑓𝐺)) = (deg‘((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺)))
157153oveq1d 6630 . . . . . . . . . . 11 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → ((deg‘𝑓) · 𝑁) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁))
158156, 157eqeq12d 2636 . . . . . . . . . 10 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → ((deg‘(𝑓𝐺)) = ((deg‘𝑓) · 𝑁) ↔ (deg‘((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺)) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁)))
159154, 158imbi12d 334 . . . . . . . . 9 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → (((deg‘𝑓) ≤ 𝐷 → (deg‘(𝑓𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝐷 → (deg‘((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺)) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁))))
160159rspcv 3295 . . . . . . . 8 ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∈ (Poly‘ℂ) → (∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝐷 → (deg‘(𝑓𝐺)) = ((deg‘𝑓) · 𝑁)) → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝐷 → (deg‘((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺)) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁))))
161117, 148, 152, 160syl3c 66 . . . . . . 7 (𝜑 → (deg‘((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺)) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁))
162147, 161eqtr3d 2657 . . . . . 6 (𝜑 → (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁))
163162adantr 481 . . . . 5 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁))
164 fconstmpt 5133 . . . . . . . . . . 11 (ℂ × {(𝐴𝑀)}) = (𝑥 ∈ ℂ ↦ (𝐴𝑀))
165164a1i 11 . . . . . . . . . 10 (𝜑 → (ℂ × {(𝐴𝑀)}) = (𝑥 ∈ ℂ ↦ (𝐴𝑀)))
166 eqidd 2622 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)) = (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)))
16725, 18, 20, 165, 166offval2 6879 . . . . . . . . 9 (𝜑 → ((ℂ × {(𝐴𝑀)}) ∘𝑓 · (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀))) = (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))
168167fveq2d 6162 . . . . . . . 8 (𝜑 → (deg‘((ℂ × {(𝐴𝑀)}) ∘𝑓 · (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
169 eqidd 2622 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦𝑀)) = (𝑦 ∈ ℂ ↦ (𝑦𝑀)))
1704, 30, 169, 47fmptco 6362 . . . . . . . . . 10 (𝜑 → ((𝑦 ∈ ℂ ↦ (𝑦𝑀)) ∘ 𝐺) = (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)))
171 1cnd 10016 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
172 plypow 23899 . . . . . . . . . . . 12 ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑦 ∈ ℂ ↦ (𝑦𝑀)) ∈ (Poly‘ℂ))
17351, 171, 16, 172syl3anc 1323 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦𝑀)) ∈ (Poly‘ℂ))
174173, 40, 42, 44plyco 23935 . . . . . . . . . 10 (𝜑 → ((𝑦 ∈ ℂ ↦ (𝑦𝑀)) ∘ 𝐺) ∈ (Poly‘ℂ))
175170, 174eqeltrrd 2699 . . . . . . . . 9 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)) ∈ (Poly‘ℂ))
176 dgrmulc 23965 . . . . . . . . 9 (((𝐴𝑀) ∈ ℂ ∧ (𝐴𝑀) ≠ 0 ∧ (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)) ∈ (Poly‘ℂ)) → (deg‘((ℂ × {(𝐴𝑀)}) ∘𝑓 · (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀))))
17717, 85, 175, 176syl3anc 1323 . . . . . . . 8 (𝜑 → (deg‘((ℂ × {(𝐴𝑀)}) ∘𝑓 · (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀))))
178168, 177eqtr3d 2657 . . . . . . 7 (𝜑 → (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀))))
179178adantr 481 . . . . . 6 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀))))
180 dgrco.2 . . . . . . 7 𝑁 = (deg‘𝐺)
18166adantr 481 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → 𝑀 ∈ ℕ)
182 simpr 477 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → 𝑁 ∈ ℕ)
1831adantr 481 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → 𝐺 ∈ (Poly‘𝑆))
184180, 181, 182, 183dgrcolem1 23967 . . . . . 6 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀))) = (𝑀 · 𝑁))
185179, 184eqtrd 2655 . . . . 5 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (𝑀 · 𝑁))
186137, 163, 1853brtr4d 4655 . . . 4 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) < (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
187 eqid 2621 . . . . 5 (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
188 eqid 2621 . . . . 5 (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))
189187, 188dgradd2 23962 . . . 4 (((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∈ (Poly‘ℂ) ∧ (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) ∈ (Poly‘ℂ) ∧ (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) < (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) → (deg‘((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
19060, 61, 186, 189syl3anc 1323 . . 3 ((𝜑𝑁 ∈ ℕ) → (deg‘((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
19136, 190, 1853eqtrd 2659 . 2 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝐹𝐺)) = (𝑀 · 𝑁))
192 0cn 9992 . . . . . . . 8 0 ∈ ℂ
193 ffvelrn 6323 . . . . . . . 8 ((𝐺:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐺‘0) ∈ ℂ)
1943, 192, 193sylancl 693 . . . . . . 7 (𝜑 → (𝐺‘0) ∈ ℂ)
1957, 194ffvelrnd 6326 . . . . . 6 (𝜑 → (𝐹‘(𝐺‘0)) ∈ ℂ)
196 0dgr 23939 . . . . . 6 ((𝐹‘(𝐺‘0)) ∈ ℂ → (deg‘(ℂ × {(𝐹‘(𝐺‘0))})) = 0)
197195, 196syl 17 . . . . 5 (𝜑 → (deg‘(ℂ × {(𝐹‘(𝐺‘0))})) = 0)
19816nn0cnd 11313 . . . . . 6 (𝜑𝑀 ∈ ℂ)
199198mul01d 10195 . . . . 5 (𝜑 → (𝑀 · 0) = 0)
200197, 199eqtr4d 2658 . . . 4 (𝜑 → (deg‘(ℂ × {(𝐹‘(𝐺‘0))})) = (𝑀 · 0))
201200adantr 481 . . 3 ((𝜑𝑁 = 0) → (deg‘(ℂ × {(𝐹‘(𝐺‘0))})) = (𝑀 · 0))
202194ad2antrr 761 . . . . . 6 (((𝜑𝑁 = 0) ∧ 𝑥 ∈ ℂ) → (𝐺‘0) ∈ ℂ)
203 simpr 477 . . . . . . . . 9 ((𝜑𝑁 = 0) → 𝑁 = 0)
204180, 203syl5eqr 2669 . . . . . . . 8 ((𝜑𝑁 = 0) → (deg‘𝐺) = 0)
205 0dgrb 23940 . . . . . . . . . 10 (𝐺 ∈ (Poly‘𝑆) → ((deg‘𝐺) = 0 ↔ 𝐺 = (ℂ × {(𝐺‘0)})))
2061, 205syl 17 . . . . . . . . 9 (𝜑 → ((deg‘𝐺) = 0 ↔ 𝐺 = (ℂ × {(𝐺‘0)})))
207206adantr 481 . . . . . . . 8 ((𝜑𝑁 = 0) → ((deg‘𝐺) = 0 ↔ 𝐺 = (ℂ × {(𝐺‘0)})))
208204, 207mpbid 222 . . . . . . 7 ((𝜑𝑁 = 0) → 𝐺 = (ℂ × {(𝐺‘0)}))
209 fconstmpt 5133 . . . . . . 7 (ℂ × {(𝐺‘0)}) = (𝑥 ∈ ℂ ↦ (𝐺‘0))
210208, 209syl6eq 2671 . . . . . 6 ((𝜑𝑁 = 0) → 𝐺 = (𝑥 ∈ ℂ ↦ (𝐺‘0)))
21131adantr 481 . . . . . 6 ((𝜑𝑁 = 0) → 𝐹 = (𝑦 ∈ ℂ ↦ (𝐹𝑦)))
212 fveq2 6158 . . . . . 6 (𝑦 = (𝐺‘0) → (𝐹𝑦) = (𝐹‘(𝐺‘0)))
213202, 210, 211, 212fmptco 6362 . . . . 5 ((𝜑𝑁 = 0) → (𝐹𝐺) = (𝑥 ∈ ℂ ↦ (𝐹‘(𝐺‘0))))
214 fconstmpt 5133 . . . . 5 (ℂ × {(𝐹‘(𝐺‘0))}) = (𝑥 ∈ ℂ ↦ (𝐹‘(𝐺‘0)))
215213, 214syl6eqr 2673 . . . 4 ((𝜑𝑁 = 0) → (𝐹𝐺) = (ℂ × {(𝐹‘(𝐺‘0))}))
216215fveq2d 6162 . . 3 ((𝜑𝑁 = 0) → (deg‘(𝐹𝐺)) = (deg‘(ℂ × {(𝐹‘(𝐺‘0))})))
217203oveq2d 6631 . . 3 ((𝜑𝑁 = 0) → (𝑀 · 𝑁) = (𝑀 · 0))
218201, 216, 2173eqtr4d 2665 . 2 ((𝜑𝑁 = 0) → (deg‘(𝐹𝐺)) = (𝑀 · 𝑁))
219 dgrcl 23927 . . . . 5 (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈ ℕ0)
2201, 219syl 17 . . . 4 (𝜑 → (deg‘𝐺) ∈ ℕ0)
221180, 220syl5eqel 2702 . . 3 (𝜑𝑁 ∈ ℕ0)
222 elnn0 11254 . . 3 (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
223221, 222sylib 208 . 2 (𝜑 → (𝑁 ∈ ℕ ∨ 𝑁 = 0))
224191, 218, 223mpjaodan 826 1 (𝜑 → (deg‘(𝐹𝐺)) = (𝑀 · 𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2908  Vcvv 3190  wss 3560  ifcif 4064  {csn 4155   class class class wbr 4623  cmpt 4683   × cxp 5082  ccom 5088   Fn wfn 5852  wf 5853  cfv 5857  (class class class)co 6615  𝑓 cof 6860  cc 9894  cr 9895  0cc0 9896  1c1 9897   + caddc 9899   · cmul 9901   < clt 10034  cle 10035  cmin 10226  cn 10980  0cn0 11252  cexp 12816  0𝑝c0p 23376  Polycply 23878  coeffccoe 23880  degcdgr 23881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974  ax-addf 9975
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-n0 11253  df-z 11338  df-uz 11648  df-rp 11793  df-fz 12285  df-fzo 12423  df-fl 12549  df-seq 12758  df-exp 12817  df-hash 13074  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-clim 14169  df-rlim 14170  df-sum 14367  df-0p 23377  df-ply 23882  df-coe 23884  df-dgr 23885
This theorem is referenced by:  dgrco  23969
  Copyright terms: Public domain W3C validator