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

Theorem dgrcolem2 23748
Description: Lemma for dgrco 23749. (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 23672 . . . . . . . . . . 11 (𝐺 ∈ (Poly‘𝑆) → 𝐺:ℂ⟶ℂ)
31, 2syl 17 . . . . . . . . . 10 (𝜑𝐺:ℂ⟶ℂ)
43ffvelrnda 6249 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → (𝐺𝑥) ∈ ℂ)
5 dgrco.3 . . . . . . . . . . 11 (𝜑𝐹 ∈ (Poly‘𝑆))
6 plyf 23672 . . . . . . . . . . 11 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
75, 6syl 17 . . . . . . . . . 10 (𝜑𝐹:ℂ⟶ℂ)
87ffvelrnda 6249 . . . . . . . . 9 ((𝜑 ∧ (𝐺𝑥) ∈ ℂ) → (𝐹‘(𝐺𝑥)) ∈ ℂ)
94, 8syldan 485 . . . . . . . 8 ((𝜑𝑥 ∈ ℂ) → (𝐹‘(𝐺𝑥)) ∈ ℂ)
10 dgrco.5 . . . . . . . . . . . . 13 𝐴 = (coeff‘𝐹)
1110coef3 23706 . . . . . . . . . . . 12 (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
125, 11syl 17 . . . . . . . . . . 11 (𝜑𝐴:ℕ0⟶ℂ)
13 dgrco.1 . . . . . . . . . . . 12 𝑀 = (deg‘𝐹)
14 dgrcl 23707 . . . . . . . . . . . . 13 (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈ ℕ0)
155, 14syl 17 . . . . . . . . . . . 12 (𝜑 → (deg‘𝐹) ∈ ℕ0)
1613, 15syl5eqel 2688 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ0)
1712, 16ffvelrnd 6250 . . . . . . . . . 10 (𝜑 → (𝐴𝑀) ∈ ℂ)
1817adantr 479 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → (𝐴𝑀) ∈ ℂ)
1916adantr 479 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → 𝑀 ∈ ℕ0)
204, 19expcld 12822 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → ((𝐺𝑥)↑𝑀) ∈ ℂ)
2118, 20mulcld 9913 . . . . . . . 8 ((𝜑𝑥 ∈ ℂ) → ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)) ∈ ℂ)
229, 21npcand 10244 . . . . . . 7 ((𝜑𝑥 ∈ ℂ) → (((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) + ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) = (𝐹‘(𝐺𝑥)))
2322mpteq2dva 4663 . . . . . 6 (𝜑 → (𝑥 ∈ ℂ ↦ (((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) + ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (𝑥 ∈ ℂ ↦ (𝐹‘(𝐺𝑥))))
24 cnex 9870 . . . . . . . 8 ℂ ∈ V
2524a1i 11 . . . . . . 7 (𝜑 → ℂ ∈ V)
269, 21subcld 10240 . . . . . . 7 ((𝜑𝑥 ∈ ℂ) → ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) ∈ ℂ)
27 eqidd 2607 . . . . . . 7 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
28 eqidd 2607 . . . . . . 7 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) = (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))
2925, 26, 21, 27, 28offval2 6786 . . . . . 6 (𝜑 → ((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (𝑥 ∈ ℂ ↦ (((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) + ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
303feqmptd 6141 . . . . . . 7 (𝜑𝐺 = (𝑥 ∈ ℂ ↦ (𝐺𝑥)))
317feqmptd 6141 . . . . . . 7 (𝜑𝐹 = (𝑦 ∈ ℂ ↦ (𝐹𝑦)))
32 fveq2 6085 . . . . . . 7 (𝑦 = (𝐺𝑥) → (𝐹𝑦) = (𝐹‘(𝐺𝑥)))
334, 30, 31, 32fmptco 6285 . . . . . 6 (𝜑 → (𝐹𝐺) = (𝑥 ∈ ℂ ↦ (𝐹‘(𝐺𝑥))))
3423, 29, 333eqtr4rd 2651 . . . . 5 (𝜑 → (𝐹𝐺) = ((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
3534fveq2d 6089 . . . 4 (𝜑 → (deg‘(𝐹𝐺)) = (deg‘((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))))
3635adantr 479 . . 3 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝐹𝐺)) = (deg‘((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))))
3725, 9, 21, 33, 28offval2 6786 . . . . . 6 (𝜑 → ((𝐹𝐺) ∘𝑓 − (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
38 plyssc 23674 . . . . . . . . 9 (Poly‘𝑆) ⊆ (Poly‘ℂ)
3938, 5sseldi 3562 . . . . . . . 8 (𝜑𝐹 ∈ (Poly‘ℂ))
4038, 1sseldi 3562 . . . . . . . 8 (𝜑𝐺 ∈ (Poly‘ℂ))
41 addcl 9871 . . . . . . . . 9 ((𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑧 + 𝑤) ∈ ℂ)
4241adantl 480 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 + 𝑤) ∈ ℂ)
43 mulcl 9873 . . . . . . . . 9 ((𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑧 · 𝑤) ∈ ℂ)
4443adantl 480 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 · 𝑤) ∈ ℂ)
4539, 40, 42, 44plyco 23715 . . . . . . 7 (𝜑 → (𝐹𝐺) ∈ (Poly‘ℂ))
46 eqidd 2607 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) = (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))
47 oveq1 6531 . . . . . . . . . 10 (𝑦 = (𝐺𝑥) → (𝑦𝑀) = ((𝐺𝑥)↑𝑀))
4847oveq2d 6540 . . . . . . . . 9 (𝑦 = (𝐺𝑥) → ((𝐴𝑀) · (𝑦𝑀)) = ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))
494, 30, 46, 48fmptco 6285 . . . . . . . 8 (𝜑 → ((𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∘ 𝐺) = (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))
50 ssid 3583 . . . . . . . . . . 11 ℂ ⊆ ℂ
5150a1i 11 . . . . . . . . . 10 (𝜑 → ℂ ⊆ ℂ)
52 eqid 2606 . . . . . . . . . . 11 (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) = (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))
5352ply1term 23678 . . . . . . . . . 10 ((ℂ ⊆ ℂ ∧ (𝐴𝑀) ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∈ (Poly‘ℂ))
5451, 17, 16, 53syl3anc 1317 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∈ (Poly‘ℂ))
5554, 40, 42, 44plyco 23715 . . . . . . . 8 (𝜑 → ((𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∘ 𝐺) ∈ (Poly‘ℂ))
5649, 55eqeltrrd 2685 . . . . . . 7 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) ∈ (Poly‘ℂ))
57 plysubcl 23696 . . . . . . 7 (((𝐹𝐺) ∈ (Poly‘ℂ) ∧ (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) ∈ (Poly‘ℂ)) → ((𝐹𝐺) ∘𝑓 − (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∈ (Poly‘ℂ))
5845, 56, 57syl2anc 690 . . . . . 6 (𝜑 → ((𝐹𝐺) ∘𝑓 − (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∈ (Poly‘ℂ))
5937, 58eqeltrrd 2685 . . . . 5 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∈ (Poly‘ℂ))
6059adantr 479 . . . 4 ((𝜑𝑁 ∈ ℕ) → (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∈ (Poly‘ℂ))
6156adantr 479 . . . 4 ((𝜑𝑁 ∈ ℕ) → (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) ∈ (Poly‘ℂ))
62 dgrco.7 . . . . . . . . . . 11 (𝜑𝑀 = (𝐷 + 1))
63 dgrco.6 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℕ0)
64 nn0p1nn 11176 . . . . . . . . . . . 12 (𝐷 ∈ ℕ0 → (𝐷 + 1) ∈ ℕ)
6563, 64syl 17 . . . . . . . . . . 11 (𝜑 → (𝐷 + 1) ∈ ℕ)
6662, 65eqeltrd 2684 . . . . . . . . . 10 (𝜑𝑀 ∈ ℕ)
6766nngt0d 10908 . . . . . . . . 9 (𝜑 → 0 < 𝑀)
68 fveq2 6085 . . . . . . . . . . 11 ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) = (deg‘0𝑝))
69 dgr0 23736 . . . . . . . . . . 11 (deg‘0𝑝) = 0
7068, 69syl6eq 2656 . . . . . . . . . 10 ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) = 0)
7170breq1d 4584 . . . . . . . . 9 ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀 ↔ 0 < 𝑀))
7267, 71syl5ibrcom 235 . . . . . . . 8 (𝜑 → ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀))
73 idd 24 . . . . . . . 8 (𝜑 → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀))
74 eqid 2606 . . . . . . . . . . . 12 (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))
7513, 74dgrsub 23746 . . . . . . . . . . 11 ((𝐹 ∈ (Poly‘ℂ) ∧ (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∈ (Poly‘ℂ)) → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), 𝑀))
7639, 54, 75syl2anc 690 . . . . . . . . . 10 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), 𝑀))
7766nnne0d 10909 . . . . . . . . . . . . . 14 (𝜑𝑀 ≠ 0)
7813, 10dgreq0 23739 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴𝑀) = 0))
795, 78syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴𝑀) = 0))
80 fveq2 6085 . . . . . . . . . . . . . . . . . 18 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
8180, 69syl6eq 2656 . . . . . . . . . . . . . . . . 17 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
8213, 81syl5eq 2652 . . . . . . . . . . . . . . . 16 (𝐹 = 0𝑝𝑀 = 0)
8379, 82syl6bir 242 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴𝑀) = 0 → 𝑀 = 0))
8483necon3d 2799 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 ≠ 0 → (𝐴𝑀) ≠ 0))
8577, 84mpd 15 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝑀) ≠ 0)
8652dgr1term 23734 . . . . . . . . . . . . 13 (((𝐴𝑀) ∈ ℂ ∧ (𝐴𝑀) ≠ 0 ∧ 𝑀 ∈ ℕ0) → (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 𝑀)
8717, 85, 16, 86syl3anc 1317 . . . . . . . . . . . 12 (𝜑 → (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 𝑀)
8887ifeq1d 4050 . . . . . . . . . . 11 (𝜑 → if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), 𝑀) = if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), 𝑀, 𝑀))
89 ifid 4071 . . . . . . . . . . 11 if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), 𝑀, 𝑀) = 𝑀
9088, 89syl6eq 2656 . . . . . . . . . 10 (𝜑 → if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), (deg‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))), 𝑀) = 𝑀)
9176, 90breqtrd 4600 . . . . . . . . 9 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝑀)
92 eqid 2606 . . . . . . . . . . . . 13 (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))
9310, 92coesub 23731 . . . . . . . . . . . 12 ((𝐹 ∈ (Poly‘ℂ) ∧ (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∈ (Poly‘ℂ)) → (coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) = (𝐴𝑓 − (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))))
9439, 54, 93syl2anc 690 . . . . . . . . . . 11 (𝜑 → (coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) = (𝐴𝑓 − (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))))
9594fveq1d 6087 . . . . . . . . . 10 (𝜑 → ((coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀) = ((𝐴𝑓 − (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀))
96 ffn 5941 . . . . . . . . . . . . 13 (𝐴:ℕ0⟶ℂ → 𝐴 Fn ℕ0)
9712, 96syl 17 . . . . . . . . . . . 12 (𝜑𝐴 Fn ℕ0)
9892coef3 23706 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∈ (Poly‘ℂ) → (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))):ℕ0⟶ℂ)
9954, 98syl 17 . . . . . . . . . . . . 13 (𝜑 → (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))):ℕ0⟶ℂ)
100 ffn 5941 . . . . . . . . . . . . 13 ((coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))):ℕ0⟶ℂ → (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) Fn ℕ0)
10199, 100syl 17 . . . . . . . . . . . 12 (𝜑 → (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) Fn ℕ0)
102 nn0ex 11142 . . . . . . . . . . . . 13 0 ∈ V
103102a1i 11 . . . . . . . . . . . 12 (𝜑 → ℕ0 ∈ V)
104 inidm 3780 . . . . . . . . . . . 12 (ℕ0 ∩ ℕ0) = ℕ0
105 eqidd 2607 . . . . . . . . . . . 12 ((𝜑𝑀 ∈ ℕ0) → (𝐴𝑀) = (𝐴𝑀))
10652coe1term 23733 . . . . . . . . . . . . . . 15 (((𝐴𝑀) ∈ ℂ ∧ 𝑀 ∈ ℕ0𝑀 ∈ ℕ0) → ((coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))‘𝑀) = if(𝑀 = 𝑀, (𝐴𝑀), 0))
10717, 16, 16, 106syl3anc 1317 . . . . . . . . . . . . . 14 (𝜑 → ((coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))‘𝑀) = if(𝑀 = 𝑀, (𝐴𝑀), 0))
108 eqid 2606 . . . . . . . . . . . . . . 15 𝑀 = 𝑀
109108iftruei 4039 . . . . . . . . . . . . . 14 if(𝑀 = 𝑀, (𝐴𝑀), 0) = (𝐴𝑀)
110107, 109syl6eq 2656 . . . . . . . . . . . . 13 (𝜑 → ((coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))‘𝑀) = (𝐴𝑀))
111110adantr 479 . . . . . . . . . . . 12 ((𝜑𝑀 ∈ ℕ0) → ((coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))‘𝑀) = (𝐴𝑀))
11297, 101, 103, 103, 104, 105, 111ofval 6778 . . . . . . . . . . 11 ((𝜑𝑀 ∈ ℕ0) → ((𝐴𝑓 − (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀) = ((𝐴𝑀) − (𝐴𝑀)))
11316, 112mpdan 698 . . . . . . . . . 10 (𝜑 → ((𝐴𝑓 − (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀) = ((𝐴𝑀) − (𝐴𝑀)))
11417subidd 10228 . . . . . . . . . 10 (𝜑 → ((𝐴𝑀) − (𝐴𝑀)) = 0)
11595, 113, 1143eqtrd 2644 . . . . . . . . 9 (𝜑 → ((coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀) = 0)
116 plysubcl 23696 . . . . . . . . . . 11 ((𝐹 ∈ (Poly‘ℂ) ∧ (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))) ∈ (Poly‘ℂ)) → (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∈ (Poly‘ℂ))
11739, 54, 116syl2anc 690 . . . . . . . . . 10 (𝜑 → (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∈ (Poly‘ℂ))
118 eqid 2606 . . . . . . . . . . 11 (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) = (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))
119 eqid 2606 . . . . . . . . . . 11 (coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) = (coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))
120118, 119dgrlt 23740 . . . . . . . . . 10 (((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∈ (Poly‘ℂ) ∧ 𝑀 ∈ ℕ0) → (((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 ∨ (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀) ↔ ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝑀 ∧ ((coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀) = 0)))
121117, 16, 120syl2anc 690 . . . . . . . . 9 (𝜑 → (((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 ∨ (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀) ↔ ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝑀 ∧ ((coeff‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))))‘𝑀) = 0)))
12291, 115, 121mpbir2and 958 . . . . . . . 8 (𝜑 → ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = 0𝑝 ∨ (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀))
12372, 73, 122mpjaod 394 . . . . . . 7 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀)
124123adantr 479 . . . . . 6 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀)
125 dgrcl 23707 . . . . . . . . . 10 ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∈ (Poly‘ℂ) → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ∈ ℕ0)
126117, 125syl 17 . . . . . . . . 9 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ∈ ℕ0)
127126nn0red 11196 . . . . . . . 8 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ∈ ℝ)
128127adantr 479 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ∈ ℝ)
12916nn0red 11196 . . . . . . . 8 (𝜑𝑀 ∈ ℝ)
130129adantr 479 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → 𝑀 ∈ ℝ)
131 nnre 10871 . . . . . . . 8 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
132131adantl 480 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → 𝑁 ∈ ℝ)
133 nngt0 10893 . . . . . . . 8 (𝑁 ∈ ℕ → 0 < 𝑁)
134133adantl 480 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → 0 < 𝑁)
135 ltmul1 10719 . . . . . . 7 (((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀 ↔ ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁) < (𝑀 · 𝑁)))
136128, 130, 132, 134, 135syl112anc 1321 . . . . . 6 ((𝜑𝑁 ∈ ℕ) → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < 𝑀 ↔ ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁) < (𝑀 · 𝑁)))
137124, 136mpbid 220 . . . . 5 ((𝜑𝑁 ∈ ℕ) → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁) < (𝑀 · 𝑁))
1387ffvelrnda 6249 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → (𝐹𝑦) ∈ ℂ)
13917adantr 479 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℂ) → (𝐴𝑀) ∈ ℂ)
140 id 22 . . . . . . . . . . . 12 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
141 expcl 12692 . . . . . . . . . . . 12 ((𝑦 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑦𝑀) ∈ ℂ)
142140, 16, 141syl2anr 493 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℂ) → (𝑦𝑀) ∈ ℂ)
143139, 142mulcld 9913 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → ((𝐴𝑀) · (𝑦𝑀)) ∈ ℂ)
14425, 138, 143, 31, 46offval2 6786 . . . . . . . . 9 (𝜑 → (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) = (𝑦 ∈ ℂ ↦ ((𝐹𝑦) − ((𝐴𝑀) · (𝑦𝑀)))))
14532, 48oveq12d 6542 . . . . . . . . 9 (𝑦 = (𝐺𝑥) → ((𝐹𝑦) − ((𝐴𝑀) · (𝑦𝑀))) = ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))
1464, 30, 144, 145fmptco 6285 . . . . . . . 8 (𝜑 → ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺) = (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
147146fveq2d 6089 . . . . . . 7 (𝜑 → (deg‘((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺)) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))))
148 dgrco.8 . . . . . . . 8 (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝐷 → (deg‘(𝑓𝐺)) = ((deg‘𝑓) · 𝑁)))
149123, 62breqtrd 4600 . . . . . . . . 9 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < (𝐷 + 1))
150 nn0leltp1 11266 . . . . . . . . . 10 (((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ∈ ℕ0𝐷 ∈ ℕ0) → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝐷 ↔ (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < (𝐷 + 1)))
151126, 63, 150syl2anc 690 . . . . . . . . 9 (𝜑 → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝐷 ↔ (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) < (𝐷 + 1)))
152149, 151mpbird 245 . . . . . . . 8 (𝜑 → (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝐷)
153 fveq2 6085 . . . . . . . . . . 11 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → (deg‘𝑓) = (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))))
154153breq1d 4584 . . . . . . . . . 10 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → ((deg‘𝑓) ≤ 𝐷 ↔ (deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝐷))
155 coeq1 5186 . . . . . . . . . . . 12 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → (𝑓𝐺) = ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺))
156155fveq2d 6089 . . . . . . . . . . 11 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → (deg‘(𝑓𝐺)) = (deg‘((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺)))
157153oveq1d 6539 . . . . . . . . . . 11 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → ((deg‘𝑓) · 𝑁) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁))
158156, 157eqeq12d 2621 . . . . . . . . . 10 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → ((deg‘(𝑓𝐺)) = ((deg‘𝑓) · 𝑁) ↔ (deg‘((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺)) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁)))
159154, 158imbi12d 332 . . . . . . . . 9 (𝑓 = (𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) → (((deg‘𝑓) ≤ 𝐷 → (deg‘(𝑓𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝐷 → (deg‘((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺)) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁))))
160159rspcv 3274 . . . . . . . 8 ((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∈ (Poly‘ℂ) → (∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝐷 → (deg‘(𝑓𝐺)) = ((deg‘𝑓) · 𝑁)) → ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) ≤ 𝐷 → (deg‘((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺)) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁))))
161117, 148, 152, 160syl3c 63 . . . . . . 7 (𝜑 → (deg‘((𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀)))) ∘ 𝐺)) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁))
162147, 161eqtr3d 2642 . . . . . 6 (𝜑 → (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁))
163162adantr 479 . . . . 5 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) = ((deg‘(𝐹𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴𝑀) · (𝑦𝑀))))) · 𝑁))
164 fconstmpt 5072 . . . . . . . . . . 11 (ℂ × {(𝐴𝑀)}) = (𝑥 ∈ ℂ ↦ (𝐴𝑀))
165164a1i 11 . . . . . . . . . 10 (𝜑 → (ℂ × {(𝐴𝑀)}) = (𝑥 ∈ ℂ ↦ (𝐴𝑀)))
166 eqidd 2607 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)) = (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)))
16725, 18, 20, 165, 166offval2 6786 . . . . . . . . 9 (𝜑 → ((ℂ × {(𝐴𝑀)}) ∘𝑓 · (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀))) = (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))
168167fveq2d 6089 . . . . . . . 8 (𝜑 → (deg‘((ℂ × {(𝐴𝑀)}) ∘𝑓 · (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
169 eqidd 2607 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦𝑀)) = (𝑦 ∈ ℂ ↦ (𝑦𝑀)))
1704, 30, 169, 47fmptco 6285 . . . . . . . . . 10 (𝜑 → ((𝑦 ∈ ℂ ↦ (𝑦𝑀)) ∘ 𝐺) = (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)))
171 1cnd 9909 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
172 plypow 23679 . . . . . . . . . . . 12 ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑦 ∈ ℂ ↦ (𝑦𝑀)) ∈ (Poly‘ℂ))
17351, 171, 16, 172syl3anc 1317 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦𝑀)) ∈ (Poly‘ℂ))
174173, 40, 42, 44plyco 23715 . . . . . . . . . 10 (𝜑 → ((𝑦 ∈ ℂ ↦ (𝑦𝑀)) ∘ 𝐺) ∈ (Poly‘ℂ))
175170, 174eqeltrrd 2685 . . . . . . . . 9 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)) ∈ (Poly‘ℂ))
176 dgrmulc 23745 . . . . . . . . 9 (((𝐴𝑀) ∈ ℂ ∧ (𝐴𝑀) ≠ 0 ∧ (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)) ∈ (Poly‘ℂ)) → (deg‘((ℂ × {(𝐴𝑀)}) ∘𝑓 · (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀))))
17717, 85, 175, 176syl3anc 1317 . . . . . . . 8 (𝜑 → (deg‘((ℂ × {(𝐴𝑀)}) ∘𝑓 · (𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀))))
178168, 177eqtr3d 2642 . . . . . . 7 (𝜑 → (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀))))
179178adantr 479 . . . . . 6 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀))))
180 dgrco.2 . . . . . . 7 𝑁 = (deg‘𝐺)
18166adantr 479 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → 𝑀 ∈ ℕ)
182 simpr 475 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → 𝑁 ∈ ℕ)
1831adantr 479 . . . . . . 7 ((𝜑𝑁 ∈ ℕ) → 𝐺 ∈ (Poly‘𝑆))
184180, 181, 182, 183dgrcolem1 23747 . . . . . 6 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐺𝑥)↑𝑀))) = (𝑀 · 𝑁))
185179, 184eqtrd 2640 . . . . 5 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (𝑀 · 𝑁))
186137, 163, 1853brtr4d 4606 . . . 4 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) < (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
187 eqid 2606 . . . . 5 (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
188 eqid 2606 . . . . 5 (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))
189187, 188dgradd2 23742 . . . 4 (((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∈ (Poly‘ℂ) ∧ (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))) ∈ (Poly‘ℂ) ∧ (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) < (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) → (deg‘((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
19060, 61, 186, 189syl3anc 1317 . . 3 ((𝜑𝑁 ∈ ℕ) → (deg‘((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺𝑥)) − ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀))))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐴𝑀) · ((𝐺𝑥)↑𝑀)))))
19136, 190, 1853eqtrd 2644 . 2 ((𝜑𝑁 ∈ ℕ) → (deg‘(𝐹𝐺)) = (𝑀 · 𝑁))
192 0cn 9885 . . . . . . . 8 0 ∈ ℂ
193 ffvelrn 6247 . . . . . . . 8 ((𝐺:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐺‘0) ∈ ℂ)
1943, 192, 193sylancl 692 . . . . . . 7 (𝜑 → (𝐺‘0) ∈ ℂ)
1957, 194ffvelrnd 6250 . . . . . 6 (𝜑 → (𝐹‘(𝐺‘0)) ∈ ℂ)
196 0dgr 23719 . . . . . 6 ((𝐹‘(𝐺‘0)) ∈ ℂ → (deg‘(ℂ × {(𝐹‘(𝐺‘0))})) = 0)
197195, 196syl 17 . . . . 5 (𝜑 → (deg‘(ℂ × {(𝐹‘(𝐺‘0))})) = 0)
19816nn0cnd 11197 . . . . . 6 (𝜑𝑀 ∈ ℂ)
199198mul01d 10083 . . . . 5 (𝜑 → (𝑀 · 0) = 0)
200197, 199eqtr4d 2643 . . . 4 (𝜑 → (deg‘(ℂ × {(𝐹‘(𝐺‘0))})) = (𝑀 · 0))
201200adantr 479 . . 3 ((𝜑𝑁 = 0) → (deg‘(ℂ × {(𝐹‘(𝐺‘0))})) = (𝑀 · 0))
202194ad2antrr 757 . . . . . 6 (((𝜑𝑁 = 0) ∧ 𝑥 ∈ ℂ) → (𝐺‘0) ∈ ℂ)
203 simpr 475 . . . . . . . . 9 ((𝜑𝑁 = 0) → 𝑁 = 0)
204180, 203syl5eqr 2654 . . . . . . . 8 ((𝜑𝑁 = 0) → (deg‘𝐺) = 0)
205 0dgrb 23720 . . . . . . . . . 10 (𝐺 ∈ (Poly‘𝑆) → ((deg‘𝐺) = 0 ↔ 𝐺 = (ℂ × {(𝐺‘0)})))
2061, 205syl 17 . . . . . . . . 9 (𝜑 → ((deg‘𝐺) = 0 ↔ 𝐺 = (ℂ × {(𝐺‘0)})))
207206adantr 479 . . . . . . . 8 ((𝜑𝑁 = 0) → ((deg‘𝐺) = 0 ↔ 𝐺 = (ℂ × {(𝐺‘0)})))
208204, 207mpbid 220 . . . . . . 7 ((𝜑𝑁 = 0) → 𝐺 = (ℂ × {(𝐺‘0)}))
209 fconstmpt 5072 . . . . . . 7 (ℂ × {(𝐺‘0)}) = (𝑥 ∈ ℂ ↦ (𝐺‘0))
210208, 209syl6eq 2656 . . . . . 6 ((𝜑𝑁 = 0) → 𝐺 = (𝑥 ∈ ℂ ↦ (𝐺‘0)))
21131adantr 479 . . . . . 6 ((𝜑𝑁 = 0) → 𝐹 = (𝑦 ∈ ℂ ↦ (𝐹𝑦)))
212 fveq2 6085 . . . . . 6 (𝑦 = (𝐺‘0) → (𝐹𝑦) = (𝐹‘(𝐺‘0)))
213202, 210, 211, 212fmptco 6285 . . . . 5 ((𝜑𝑁 = 0) → (𝐹𝐺) = (𝑥 ∈ ℂ ↦ (𝐹‘(𝐺‘0))))
214 fconstmpt 5072 . . . . 5 (ℂ × {(𝐹‘(𝐺‘0))}) = (𝑥 ∈ ℂ ↦ (𝐹‘(𝐺‘0)))
215213, 214syl6eqr 2658 . . . 4 ((𝜑𝑁 = 0) → (𝐹𝐺) = (ℂ × {(𝐹‘(𝐺‘0))}))
216215fveq2d 6089 . . 3 ((𝜑𝑁 = 0) → (deg‘(𝐹𝐺)) = (deg‘(ℂ × {(𝐹‘(𝐺‘0))})))
217203oveq2d 6540 . . 3 ((𝜑𝑁 = 0) → (𝑀 · 𝑁) = (𝑀 · 0))
218201, 216, 2173eqtr4d 2650 . 2 ((𝜑𝑁 = 0) → (deg‘(𝐹𝐺)) = (𝑀 · 𝑁))
219 dgrcl 23707 . . . . 5 (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈ ℕ0)
2201, 219syl 17 . . . 4 (𝜑 → (deg‘𝐺) ∈ ℕ0)
221180, 220syl5eqel 2688 . . 3 (𝜑𝑁 ∈ ℕ0)
222 elnn0 11138 . . 3 (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
223221, 222sylib 206 . 2 (𝜑 → (𝑁 ∈ ℕ ∨ 𝑁 = 0))
224191, 218, 223mpjaodan 822 1 (𝜑 → (deg‘(𝐹𝐺)) = (𝑀 · 𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381  wa 382   = wceq 1474  wcel 1976  wne 2776  wral 2892  Vcvv 3169  wss 3536  ifcif 4032  {csn 4121   class class class wbr 4574  cmpt 4634   × cxp 5023  ccom 5029   Fn wfn 5782  wf 5783  cfv 5787  (class class class)co 6524  𝑓 cof 6767  cc 9787  cr 9788  0cc0 9789  1c1 9790   + caddc 9792   · cmul 9794   < clt 9927  cle 9928  cmin 10114  cn 10864  0cn0 11136  cexp 12674  0𝑝c0p 23156  Polycply 23658  coeffccoe 23660  degcdgr 23661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867  ax-addf 9868
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-of 6769  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-oadd 7425  df-er 7603  df-map 7720  df-pm 7721  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-sup 8205  df-inf 8206  df-oi 8272  df-card 8622  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-n0 11137  df-z 11208  df-uz 11517  df-rp 11662  df-fz 12150  df-fzo 12287  df-fl 12407  df-seq 12616  df-exp 12675  df-hash 12932  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-clim 14010  df-rlim 14011  df-sum 14208  df-0p 23157  df-ply 23662  df-coe 23664  df-dgr 23665
This theorem is referenced by:  dgrco  23749
  Copyright terms: Public domain W3C validator