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

Theorem vieta1lem1 24110
 Description: Lemma for vieta1 24112. (Contributed by Mario Carneiro, 28-Jul-2014.)
Hypotheses
Ref Expression
vieta1.1 𝐴 = (coeff‘𝐹)
vieta1.2 𝑁 = (deg‘𝐹)
vieta1.3 𝑅 = (𝐹 “ {0})
vieta1.4 (𝜑𝐹 ∈ (Poly‘𝑆))
vieta1.5 (𝜑 → (#‘𝑅) = 𝑁)
vieta1lem.6 (𝜑𝐷 ∈ ℕ)
vieta1lem.7 (𝜑 → (𝐷 + 1) = 𝑁)
vieta1lem.8 (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
vieta1lem.9 𝑄 = (𝐹 quot (Xp𝑓 − (ℂ × {𝑧})))
Assertion
Ref Expression
vieta1lem1 ((𝜑𝑧𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
Distinct variable groups:   𝐷,𝑓   𝑓,𝐹   𝑧,𝑓,𝑁   𝑥,𝑓,𝑄   𝑅,𝑓   𝑥,𝑧,𝑅   𝐴,𝑓,𝑧   𝜑,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑓)   𝐴(𝑥)   𝐷(𝑥,𝑧)   𝑄(𝑧)   𝑆(𝑥,𝑧,𝑓)   𝐹(𝑥,𝑧)   𝑁(𝑥)

Proof of Theorem vieta1lem1
StepHypRef Expression
1 vieta1lem.9 . . 3 𝑄 = (𝐹 quot (Xp𝑓 − (ℂ × {𝑧})))
2 plyssc 24001 . . . . 5 (Poly‘𝑆) ⊆ (Poly‘ℂ)
3 vieta1.4 . . . . . 6 (𝜑𝐹 ∈ (Poly‘𝑆))
43adantr 480 . . . . 5 ((𝜑𝑧𝑅) → 𝐹 ∈ (Poly‘𝑆))
52, 4sseldi 3634 . . . 4 ((𝜑𝑧𝑅) → 𝐹 ∈ (Poly‘ℂ))
6 vieta1.3 . . . . . . . . 9 𝑅 = (𝐹 “ {0})
7 cnvimass 5520 . . . . . . . . 9 (𝐹 “ {0}) ⊆ dom 𝐹
86, 7eqsstri 3668 . . . . . . . 8 𝑅 ⊆ dom 𝐹
9 plyf 23999 . . . . . . . . . 10 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
103, 9syl 17 . . . . . . . . 9 (𝜑𝐹:ℂ⟶ℂ)
11 fdm 6089 . . . . . . . . 9 (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
1210, 11syl 17 . . . . . . . 8 (𝜑 → dom 𝐹 = ℂ)
138, 12syl5sseq 3686 . . . . . . 7 (𝜑𝑅 ⊆ ℂ)
1413sselda 3636 . . . . . 6 ((𝜑𝑧𝑅) → 𝑧 ∈ ℂ)
15 eqid 2651 . . . . . . 7 (Xp𝑓 − (ℂ × {𝑧})) = (Xp𝑓 − (ℂ × {𝑧}))
1615plyremlem 24104 . . . . . 6 (𝑧 ∈ ℂ → ((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = 1 ∧ ((Xp𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧}))
1714, 16syl 17 . . . . 5 ((𝜑𝑧𝑅) → ((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = 1 ∧ ((Xp𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧}))
1817simp1d 1093 . . . 4 ((𝜑𝑧𝑅) → (Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
1917simp2d 1094 . . . . . 6 ((𝜑𝑧𝑅) → (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = 1)
20 ax-1ne0 10043 . . . . . . 7 1 ≠ 0
2120a1i 11 . . . . . 6 ((𝜑𝑧𝑅) → 1 ≠ 0)
2219, 21eqnetrd 2890 . . . . 5 ((𝜑𝑧𝑅) → (deg‘(Xp𝑓 − (ℂ × {𝑧}))) ≠ 0)
23 fveq2 6229 . . . . . . 7 ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = (deg‘0𝑝))
24 dgr0 24063 . . . . . . 7 (deg‘0𝑝) = 0
2523, 24syl6eq 2701 . . . . . 6 ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = 0)
2625necon3i 2855 . . . . 5 ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) ≠ 0 → (Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝)
2722, 26syl 17 . . . 4 ((𝜑𝑧𝑅) → (Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝)
28 quotcl2 24102 . . . 4 ((𝐹 ∈ (Poly‘ℂ) ∧ (Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝) → (𝐹 quot (Xp𝑓 − (ℂ × {𝑧}))) ∈ (Poly‘ℂ))
295, 18, 27, 28syl3anc 1366 . . 3 ((𝜑𝑧𝑅) → (𝐹 quot (Xp𝑓 − (ℂ × {𝑧}))) ∈ (Poly‘ℂ))
301, 29syl5eqel 2734 . 2 ((𝜑𝑧𝑅) → 𝑄 ∈ (Poly‘ℂ))
31 ax-1cn 10032 . . . 4 1 ∈ ℂ
3231a1i 11 . . 3 ((𝜑𝑧𝑅) → 1 ∈ ℂ)
33 vieta1lem.6 . . . . 5 (𝜑𝐷 ∈ ℕ)
3433nncnd 11074 . . . 4 (𝜑𝐷 ∈ ℂ)
3534adantr 480 . . 3 ((𝜑𝑧𝑅) → 𝐷 ∈ ℂ)
36 dgrcl 24034 . . . . 5 (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ0)
3730, 36syl 17 . . . 4 ((𝜑𝑧𝑅) → (deg‘𝑄) ∈ ℕ0)
3837nn0cnd 11391 . . 3 ((𝜑𝑧𝑅) → (deg‘𝑄) ∈ ℂ)
39 addcom 10260 . . . . 5 ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
4031, 35, 39sylancr 696 . . . 4 ((𝜑𝑧𝑅) → (1 + 𝐷) = (𝐷 + 1))
41 vieta1lem.7 . . . . . . 7 (𝜑 → (𝐷 + 1) = 𝑁)
42 vieta1.2 . . . . . . 7 𝑁 = (deg‘𝐹)
4341, 42syl6eq 2701 . . . . . 6 (𝜑 → (𝐷 + 1) = (deg‘𝐹))
4443adantr 480 . . . . 5 ((𝜑𝑧𝑅) → (𝐷 + 1) = (deg‘𝐹))
456eleq2i 2722 . . . . . . . . . 10 (𝑧𝑅𝑧 ∈ (𝐹 “ {0}))
46 ffn 6083 . . . . . . . . . . . 12 (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
4710, 46syl 17 . . . . . . . . . . 11 (𝜑𝐹 Fn ℂ)
48 fniniseg 6378 . . . . . . . . . . 11 (𝐹 Fn ℂ → (𝑧 ∈ (𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
4947, 48syl 17 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ (𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
5045, 49syl5bb 272 . . . . . . . . 9 (𝜑 → (𝑧𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
5150simplbda 653 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐹𝑧) = 0)
5215facth 24106 . . . . . . . 8 ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0) → 𝐹 = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝑧})))))
534, 14, 51, 52syl3anc 1366 . . . . . . 7 ((𝜑𝑧𝑅) → 𝐹 = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝑧})))))
541oveq2i 6701 . . . . . . 7 ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝑧}))))
5553, 54syl6eqr 2703 . . . . . 6 ((𝜑𝑧𝑅) → 𝐹 = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))
5655fveq2d 6233 . . . . 5 ((𝜑𝑧𝑅) → (deg‘𝐹) = (deg‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)))
5733peano2nnd 11075 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 + 1) ∈ ℕ)
5841, 57eqeltrrd 2731 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
5958nnne0d 11103 . . . . . . . . . . . . 13 (𝜑𝑁 ≠ 0)
6042, 59syl5eqner 2898 . . . . . . . . . . . 12 (𝜑 → (deg‘𝐹) ≠ 0)
61 fveq2 6229 . . . . . . . . . . . . . 14 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
6261, 24syl6eq 2701 . . . . . . . . . . . . 13 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
6362necon3i 2855 . . . . . . . . . . . 12 ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0𝑝)
6460, 63syl 17 . . . . . . . . . . 11 (𝜑𝐹 ≠ 0𝑝)
6564adantr 480 . . . . . . . . . 10 ((𝜑𝑧𝑅) → 𝐹 ≠ 0𝑝)
6655, 65eqnetrrd 2891 . . . . . . . . 9 ((𝜑𝑧𝑅) → ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) ≠ 0𝑝)
67 plymul0or 24081 . . . . . . . . . . 11 (((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) = 0𝑝 ↔ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
6818, 30, 67syl2anc 694 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) = 0𝑝 ↔ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
6968necon3abid 2859 . . . . . . . . 9 ((𝜑𝑧𝑅) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) ≠ 0𝑝 ↔ ¬ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
7066, 69mpbid 222 . . . . . . . 8 ((𝜑𝑧𝑅) → ¬ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝))
71 neanior 2915 . . . . . . . 8 (((Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝𝑄 ≠ 0𝑝) ↔ ¬ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝))
7270, 71sylibr 224 . . . . . . 7 ((𝜑𝑧𝑅) → ((Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝𝑄 ≠ 0𝑝))
7372simprd 478 . . . . . 6 ((𝜑𝑧𝑅) → 𝑄 ≠ 0𝑝)
74 eqid 2651 . . . . . . 7 (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = (deg‘(Xp𝑓 − (ℂ × {𝑧})))
75 eqid 2651 . . . . . . 7 (deg‘𝑄) = (deg‘𝑄)
7674, 75dgrmul 24071 . . . . . 6 ((((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝)) → (deg‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)) = ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
7718, 27, 30, 73, 76syl22anc 1367 . . . . 5 ((𝜑𝑧𝑅) → (deg‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)) = ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
7844, 56, 773eqtrd 2689 . . . 4 ((𝜑𝑧𝑅) → (𝐷 + 1) = ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
7919oveq1d 6705 . . . 4 ((𝜑𝑧𝑅) → ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)) = (1 + (deg‘𝑄)))
8040, 78, 793eqtrd 2689 . . 3 ((𝜑𝑧𝑅) → (1 + 𝐷) = (1 + (deg‘𝑄)))
8132, 35, 38, 80addcanad 10279 . 2 ((𝜑𝑧𝑅) → 𝐷 = (deg‘𝑄))
8230, 81jca 553 1 ((𝜑𝑧𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  {csn 4210   × cxp 5141  ◡ccnv 5142  dom cdm 5143   “ cima 5146   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ∘𝑓 cof 6937  ℂcc 9972  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   − cmin 10304  -cneg 10305   / cdiv 10722  ℕcn 11058  ℕ0cn0 11330  #chash 13157  Σcsu 14460  0𝑝c0p 23481  Polycply 23985  Xpcidp 23986  coeffccoe 23987  degcdgr 23988   quot cquot 24090 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-0p 23482  df-ply 23989  df-idp 23990  df-coe 23991  df-dgr 23992  df-quot 24091 This theorem is referenced by:  vieta1lem2  24111
 Copyright terms: Public domain W3C validator