Proof of Theorem vieta1lem1
Step | Hyp | Ref
| Expression |
1 | | vieta1lem.9 |
. . 3
⊢ 𝑄 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝑧}))) |
2 | | plyssc 23760 |
. . . . 5
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
3 | | vieta1.4 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ∈ (Poly‘𝑆)) |
5 | 2, 4 | sseldi 3566 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ∈
(Poly‘ℂ)) |
6 | | vieta1.3 |
. . . . . . . . 9
⊢ 𝑅 = (◡𝐹 “ {0}) |
7 | | cnvimass 5404 |
. . . . . . . . 9
⊢ (◡𝐹 “ {0}) ⊆ dom 𝐹 |
8 | 6, 7 | eqsstri 3598 |
. . . . . . . 8
⊢ 𝑅 ⊆ dom 𝐹 |
9 | | plyf 23758 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
10 | 3, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
11 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝐹:ℂ⟶ℂ →
dom 𝐹 =
ℂ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐹 = ℂ) |
13 | 8, 12 | syl5sseq 3616 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ⊆ ℂ) |
14 | 13 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑧 ∈ ℂ) |
15 | | eqid 2610 |
. . . . . . 7
⊢
(Xp ∘𝑓 − (ℂ
× {𝑧})) =
(Xp ∘𝑓 − (ℂ ×
{𝑧})) |
16 | 15 | plyremlem 23863 |
. . . . . 6
⊢ (𝑧 ∈ ℂ →
((Xp ∘𝑓 − (ℂ ×
{𝑧})) ∈
(Poly‘ℂ) ∧ (deg‘(Xp
∘𝑓 − (ℂ × {𝑧}))) = 1 ∧ (◡(Xp
∘𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧})) |
17 | 14, 16 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((Xp
∘𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧
(deg‘(Xp ∘𝑓 − (ℂ
× {𝑧}))) = 1 ∧
(◡(Xp
∘𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧})) |
18 | 17 | simp1d 1066 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp
∘𝑓 − (ℂ × {𝑧})) ∈
(Poly‘ℂ)) |
19 | 17 | simp2d 1067 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(Xp
∘𝑓 − (ℂ × {𝑧}))) = 1) |
20 | | ax-1ne0 9884 |
. . . . . . 7
⊢ 1 ≠
0 |
21 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ≠ 0) |
22 | 19, 21 | eqnetrd 2849 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘(Xp
∘𝑓 − (ℂ × {𝑧}))) ≠ 0) |
23 | | fveq2 6103 |
. . . . . . 7
⊢
((Xp ∘𝑓 − (ℂ
× {𝑧})) =
0𝑝 → (deg‘(Xp
∘𝑓 − (ℂ × {𝑧}))) =
(deg‘0𝑝)) |
24 | | dgr0 23822 |
. . . . . . 7
⊢
(deg‘0𝑝) = 0 |
25 | 23, 24 | syl6eq 2660 |
. . . . . 6
⊢
((Xp ∘𝑓 − (ℂ
× {𝑧})) =
0𝑝 → (deg‘(Xp
∘𝑓 − (ℂ × {𝑧}))) = 0) |
26 | 25 | necon3i 2814 |
. . . . 5
⊢
((deg‘(Xp ∘𝑓 −
(ℂ × {𝑧})))
≠ 0 → (Xp ∘𝑓 −
(ℂ × {𝑧})) ≠
0𝑝) |
27 | 22, 26 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (Xp
∘𝑓 − (ℂ × {𝑧})) ≠
0𝑝) |
28 | | quotcl2 23861 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ (Xp ∘𝑓 − (ℂ
× {𝑧})) ∈
(Poly‘ℂ) ∧ (Xp ∘𝑓
− (ℂ × {𝑧})) ≠ 0𝑝) → (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝑧}))) ∈
(Poly‘ℂ)) |
29 | 5, 18, 27, 28 | syl3anc 1318 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝑧}))) ∈
(Poly‘ℂ)) |
30 | 1, 29 | syl5eqel 2692 |
. 2
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ∈
(Poly‘ℂ)) |
31 | | ax-1cn 9873 |
. . . 4
⊢ 1 ∈
ℂ |
32 | 31 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 1 ∈ ℂ) |
33 | | vieta1lem.6 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ ℕ) |
34 | 33 | nncnd 10913 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ ℂ) |
35 | 34 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 ∈ ℂ) |
36 | | dgrcl 23793 |
. . . . 5
⊢ (𝑄 ∈ (Poly‘ℂ)
→ (deg‘𝑄) ∈
ℕ0) |
37 | 30, 36 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈
ℕ0) |
38 | 37 | nn0cnd 11230 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝑄) ∈ ℂ) |
39 | | addcom 10101 |
. . . . 5
⊢ ((1
∈ ℂ ∧ 𝐷
∈ ℂ) → (1 + 𝐷) = (𝐷 + 1)) |
40 | 31, 35, 39 | sylancr 694 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) = (𝐷 + 1)) |
41 | | vieta1lem.7 |
. . . . . . 7
⊢ (𝜑 → (𝐷 + 1) = 𝑁) |
42 | | vieta1.2 |
. . . . . . 7
⊢ 𝑁 = (deg‘𝐹) |
43 | 41, 42 | syl6eq 2660 |
. . . . . 6
⊢ (𝜑 → (𝐷 + 1) = (deg‘𝐹)) |
44 | 43 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 + 1) = (deg‘𝐹)) |
45 | 6 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑅 ↔ 𝑧 ∈ (◡𝐹 “ {0})) |
46 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐹:ℂ⟶ℂ →
𝐹 Fn
ℂ) |
47 | 10, 46 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 Fn ℂ) |
48 | | fniniseg 6246 |
. . . . . . . . . . 11
⊢ (𝐹 Fn ℂ → (𝑧 ∈ (◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0))) |
49 | 47, 48 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ (◡𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0))) |
50 | 45, 49 | syl5bb 271 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ 𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0))) |
51 | 50 | simplbda 652 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐹‘𝑧) = 0) |
52 | 15 | facth 23865 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹‘𝑧) = 0) → 𝐹 = ((Xp
∘𝑓 − (ℂ × {𝑧})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝑧}))))) |
53 | 4, 14, 51, 52 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((Xp
∘𝑓 − (ℂ × {𝑧})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝑧}))))) |
54 | 1 | oveq2i 6560 |
. . . . . . 7
⊢
((Xp ∘𝑓 − (ℂ
× {𝑧}))
∘𝑓 · 𝑄) = ((Xp
∘𝑓 − (ℂ × {𝑧})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝑧})))) |
55 | 53, 54 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 = ((Xp
∘𝑓 − (ℂ × {𝑧})) ∘𝑓 ·
𝑄)) |
56 | 55 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘𝐹) = (deg‘((Xp
∘𝑓 − (ℂ × {𝑧})) ∘𝑓 ·
𝑄))) |
57 | 33 | peano2nnd 10914 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐷 + 1) ∈ ℕ) |
58 | 41, 57 | eqeltrrd 2689 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℕ) |
59 | 58 | nnne0d 10942 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ≠ 0) |
60 | 42, 59 | syl5eqner 2857 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐹) ≠ 0) |
61 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
(deg‘0𝑝)) |
62 | 61, 24 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
0) |
63 | 62 | necon3i 2814 |
. . . . . . . . . . . 12
⊢
((deg‘𝐹) ≠
0 → 𝐹 ≠
0𝑝) |
64 | 60, 63 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ≠
0𝑝) |
65 | 64 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐹 ≠
0𝑝) |
66 | 55, 65 | eqnetrrd 2850 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((Xp
∘𝑓 − (ℂ × {𝑧})) ∘𝑓 ·
𝑄) ≠
0𝑝) |
67 | | plymul0or 23840 |
. . . . . . . . . . 11
⊢
(((Xp ∘𝑓 − (ℂ
× {𝑧})) ∈
(Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) →
(((Xp ∘𝑓 − (ℂ ×
{𝑧}))
∘𝑓 · 𝑄) = 0𝑝 ↔
((Xp ∘𝑓 − (ℂ ×
{𝑧})) =
0𝑝 ∨ 𝑄 = 0𝑝))) |
68 | 18, 30, 67 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((Xp
∘𝑓 − (ℂ × {𝑧})) ∘𝑓 ·
𝑄) = 0𝑝
↔ ((Xp ∘𝑓 − (ℂ
× {𝑧})) =
0𝑝 ∨ 𝑄 = 0𝑝))) |
69 | 68 | necon3abid 2818 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (((Xp
∘𝑓 − (ℂ × {𝑧})) ∘𝑓 ·
𝑄) ≠
0𝑝 ↔ ¬ ((Xp
∘𝑓 − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 =
0𝑝))) |
70 | 66, 69 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ¬ ((Xp
∘𝑓 − (ℂ × {𝑧})) = 0𝑝 ∨ 𝑄 =
0𝑝)) |
71 | | neanior 2874 |
. . . . . . . 8
⊢
(((Xp ∘𝑓 − (ℂ
× {𝑧})) ≠
0𝑝 ∧ 𝑄 ≠ 0𝑝) ↔ ¬
((Xp ∘𝑓 − (ℂ ×
{𝑧})) =
0𝑝 ∨ 𝑄 = 0𝑝)) |
72 | 70, 71 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((Xp
∘𝑓 − (ℂ × {𝑧})) ≠ 0𝑝 ∧ 𝑄 ≠
0𝑝)) |
73 | 72 | simprd 478 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝑄 ≠
0𝑝) |
74 | | eqid 2610 |
. . . . . . 7
⊢
(deg‘(Xp ∘𝑓 −
(ℂ × {𝑧}))) =
(deg‘(Xp ∘𝑓 − (ℂ
× {𝑧}))) |
75 | | eqid 2610 |
. . . . . . 7
⊢
(deg‘𝑄) =
(deg‘𝑄) |
76 | 74, 75 | dgrmul 23830 |
. . . . . 6
⊢
((((Xp ∘𝑓 − (ℂ
× {𝑧})) ∈
(Poly‘ℂ) ∧ (Xp ∘𝑓
− (ℂ × {𝑧})) ≠ 0𝑝) ∧ (𝑄 ∈ (Poly‘ℂ)
∧ 𝑄 ≠
0𝑝)) → (deg‘((Xp
∘𝑓 − (ℂ × {𝑧})) ∘𝑓 ·
𝑄)) =
((deg‘(Xp ∘𝑓 − (ℂ
× {𝑧}))) +
(deg‘𝑄))) |
77 | 18, 27, 30, 73, 76 | syl22anc 1319 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (deg‘((Xp
∘𝑓 − (ℂ × {𝑧})) ∘𝑓 ·
𝑄)) =
((deg‘(Xp ∘𝑓 − (ℂ
× {𝑧}))) +
(deg‘𝑄))) |
78 | 44, 56, 77 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝐷 + 1) = ((deg‘(Xp
∘𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))) |
79 | 19 | oveq1d 6564 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → ((deg‘(Xp
∘𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)) = (1 + (deg‘𝑄))) |
80 | 40, 78, 79 | 3eqtrd 2648 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (1 + 𝐷) = (1 + (deg‘𝑄))) |
81 | 32, 35, 38, 80 | addcanad 10120 |
. 2
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → 𝐷 = (deg‘𝑄)) |
82 | 30, 81 | jca 553 |
1
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄))) |