Step | Hyp | Ref
| Expression |
1 | | fta1.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℂ) ∖
{0𝑝})) |
2 | | eldifsn 4260 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ((Poly‘ℂ)
∖ {0𝑝}) ↔ (𝐹 ∈ (Poly‘ℂ) ∧ 𝐹 ≠
0𝑝)) |
3 | 1, 2 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∈ (Poly‘ℂ) ∧ 𝐹 ≠
0𝑝)) |
4 | 3 | simpld 474 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℂ)) |
5 | | fta1.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (◡𝐹 “ {0})) |
6 | | plyf 23758 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘ℂ)
→ 𝐹:ℂ⟶ℂ) |
7 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝐹:ℂ⟶ℂ →
𝐹 Fn
ℂ) |
8 | | fniniseg 6246 |
. . . . . . . . . . 11
⊢ (𝐹 Fn ℂ → (𝐴 ∈ (◡𝐹 “ {0}) ↔ (𝐴 ∈ ℂ ∧ (𝐹‘𝐴) = 0))) |
9 | 4, 6, 7, 8 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ (◡𝐹 “ {0}) ↔ (𝐴 ∈ ℂ ∧ (𝐹‘𝐴) = 0))) |
10 | 5, 9 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ ℂ ∧ (𝐹‘𝐴) = 0)) |
11 | 10 | simpld 474 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
12 | 10 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝐴) = 0) |
13 | | eqid 2610 |
. . . . . . . . 9
⊢
(Xp ∘𝑓 − (ℂ
× {𝐴})) =
(Xp ∘𝑓 − (ℂ ×
{𝐴})) |
14 | 13 | facth 23865 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐴 ∈ ℂ
∧ (𝐹‘𝐴) = 0) → 𝐹 = ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))))) |
15 | 4, 11, 12, 14 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))))) |
16 | 15 | cnveqd 5220 |
. . . . . 6
⊢ (𝜑 → ◡𝐹 = ◡((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))))) |
17 | 16 | imaeq1d 5384 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ {0}) = (◡((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) “
{0})) |
18 | | cnex 9896 |
. . . . . . 7
⊢ ℂ
∈ V |
19 | 18 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂ ∈
V) |
20 | | ssid 3587 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
21 | | ax-1cn 9873 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
22 | | plyid 23769 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈
(Poly‘ℂ)) |
23 | 20, 21, 22 | mp2an 704 |
. . . . . . . 8
⊢
Xp ∈ (Poly‘ℂ) |
24 | | plyconst 23766 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 𝐴
∈ ℂ) → (ℂ × {𝐴}) ∈
(Poly‘ℂ)) |
25 | 20, 11, 24 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → (ℂ × {𝐴}) ∈
(Poly‘ℂ)) |
26 | | plysubcl 23782 |
. . . . . . . 8
⊢
((Xp ∈ (Poly‘ℂ) ∧ (ℂ
× {𝐴}) ∈
(Poly‘ℂ)) → (Xp ∘𝑓
− (ℂ × {𝐴})) ∈
(Poly‘ℂ)) |
27 | 23, 25, 26 | sylancr 694 |
. . . . . . 7
⊢ (𝜑 → (Xp
∘𝑓 − (ℂ × {𝐴})) ∈
(Poly‘ℂ)) |
28 | | plyf 23758 |
. . . . . . 7
⊢
((Xp ∘𝑓 − (ℂ
× {𝐴})) ∈
(Poly‘ℂ) → (Xp ∘𝑓
− (ℂ × {𝐴})):ℂ⟶ℂ) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → (Xp
∘𝑓 − (ℂ × {𝐴})):ℂ⟶ℂ) |
30 | 13 | plyremlem 23863 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((Xp ∘𝑓 − (ℂ ×
{𝐴})) ∈
(Poly‘ℂ) ∧ (deg‘(Xp
∘𝑓 − (ℂ × {𝐴}))) = 1 ∧ (◡(Xp
∘𝑓 − (ℂ × {𝐴})) “ {0}) = {𝐴})) |
31 | 11, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((Xp
∘𝑓 − (ℂ × {𝐴})) ∈ (Poly‘ℂ) ∧
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐴}))) = 1 ∧
(◡(Xp
∘𝑓 − (ℂ × {𝐴})) “ {0}) = {𝐴})) |
32 | 31 | simp2d 1067 |
. . . . . . . . . 10
⊢ (𝜑 →
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐴}))) =
1) |
33 | | ax-1ne0 9884 |
. . . . . . . . . . 11
⊢ 1 ≠
0 |
34 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≠ 0) |
35 | 32, 34 | eqnetrd 2849 |
. . . . . . . . 9
⊢ (𝜑 →
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐴}))) ≠
0) |
36 | | fveq2 6103 |
. . . . . . . . . . 11
⊢
((Xp ∘𝑓 − (ℂ
× {𝐴})) =
0𝑝 → (deg‘(Xp
∘𝑓 − (ℂ × {𝐴}))) =
(deg‘0𝑝)) |
37 | | dgr0 23822 |
. . . . . . . . . . 11
⊢
(deg‘0𝑝) = 0 |
38 | 36, 37 | syl6eq 2660 |
. . . . . . . . . 10
⊢
((Xp ∘𝑓 − (ℂ
× {𝐴})) =
0𝑝 → (deg‘(Xp
∘𝑓 − (ℂ × {𝐴}))) = 0) |
39 | 38 | necon3i 2814 |
. . . . . . . . 9
⊢
((deg‘(Xp ∘𝑓 −
(ℂ × {𝐴})))
≠ 0 → (Xp ∘𝑓 −
(ℂ × {𝐴})) ≠
0𝑝) |
40 | 35, 39 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (Xp
∘𝑓 − (ℂ × {𝐴})) ≠
0𝑝) |
41 | | quotcl2 23861 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ (Xp ∘𝑓 − (ℂ
× {𝐴})) ∈
(Poly‘ℂ) ∧ (Xp ∘𝑓
− (ℂ × {𝐴})) ≠ 0𝑝) →
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))) ∈
(Poly‘ℂ)) |
42 | 4, 27, 40, 41 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈
(Poly‘ℂ)) |
43 | | plyf 23758 |
. . . . . . 7
⊢ ((𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈ (Poly‘ℂ) →
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))):ℂ⟶ℂ) |
44 | 42, 43 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))):ℂ⟶ℂ) |
45 | | ofmulrt 23841 |
. . . . . 6
⊢ ((ℂ
∈ V ∧ (Xp ∘𝑓 −
(ℂ × {𝐴})):ℂ⟶ℂ ∧ (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))):ℂ⟶ℂ) → (◡((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) “ {0}) =
((◡(Xp
∘𝑓 − (ℂ × {𝐴})) “ {0}) ∪ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}))) |
46 | 19, 29, 44, 45 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (◡((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) “ {0}) =
((◡(Xp
∘𝑓 − (ℂ × {𝐴})) “ {0}) ∪ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}))) |
47 | 31 | simp3d 1068 |
. . . . . 6
⊢ (𝜑 → (◡(Xp
∘𝑓 − (ℂ × {𝐴})) “ {0}) = {𝐴}) |
48 | 47 | uneq1d 3728 |
. . . . 5
⊢ (𝜑 → ((◡(Xp
∘𝑓 − (ℂ × {𝐴})) “ {0}) ∪ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) = ({𝐴} ∪ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}))) |
49 | 17, 46, 48 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ {0}) = ({𝐴} ∪ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}))) |
50 | | fta1.1 |
. . . 4
⊢ 𝑅 = (◡𝐹 “ {0}) |
51 | | uncom 3719 |
. . . 4
⊢ ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}) = ({𝐴} ∪ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) |
52 | 49, 50, 51 | 3eqtr4g 2669 |
. . 3
⊢ (𝜑 → 𝑅 = ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) |
53 | 3 | simprd 478 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ≠
0𝑝) |
54 | 15 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝜑 → ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) = 𝐹) |
55 | | 0cnd 9912 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℂ) |
56 | | mul01 10094 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (𝑥 · 0) =
0) |
57 | 56 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑥 · 0) = 0) |
58 | 19, 29, 55, 55, 57 | caofid1 6825 |
. . . . . . . . . 10
⊢ (𝜑 → ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(ℂ × {0})) = (ℂ × {0})) |
59 | | df-0p 23243 |
. . . . . . . . . . 11
⊢
0𝑝 = (ℂ × {0}) |
60 | 59 | oveq2i 6560 |
. . . . . . . . . 10
⊢
((Xp ∘𝑓 − (ℂ
× {𝐴}))
∘𝑓 · 0𝑝) =
((Xp ∘𝑓 − (ℂ ×
{𝐴}))
∘𝑓 · (ℂ × {0})) |
61 | 58, 60, 59 | 3eqtr4g 2669 |
. . . . . . . . 9
⊢ (𝜑 → ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
0𝑝) = 0𝑝) |
62 | 53, 54, 61 | 3netr4d 2859 |
. . . . . . . 8
⊢ (𝜑 → ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) ≠
((Xp ∘𝑓 − (ℂ ×
{𝐴}))
∘𝑓 · 0𝑝)) |
63 | | oveq2 6557 |
. . . . . . . . 9
⊢ ((𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) = 0𝑝 →
((Xp ∘𝑓 − (ℂ ×
{𝐴}))
∘𝑓 · (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) = ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
0𝑝)) |
64 | 63 | necon3i 2814 |
. . . . . . . 8
⊢
(((Xp ∘𝑓 − (ℂ
× {𝐴}))
∘𝑓 · (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) ≠ ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
0𝑝) → (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ≠
0𝑝) |
65 | 62, 64 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ≠
0𝑝) |
66 | | eldifsn 4260 |
. . . . . . 7
⊢ ((𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈ ((Poly‘ℂ) ∖
{0𝑝}) ↔ ((𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈ (Poly‘ℂ) ∧
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))) ≠
0𝑝)) |
67 | 42, 65, 66 | sylanbrc 695 |
. . . . . 6
⊢ (𝜑 → (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈ ((Poly‘ℂ) ∖
{0𝑝})) |
68 | | fta1.6 |
. . . . . 6
⊢ (𝜑 → ∀𝑔 ∈ ((Poly‘ℂ) ∖
{0𝑝})((deg‘𝑔) = 𝐷 → ((◡𝑔 “ {0}) ∈ Fin ∧
(#‘(◡𝑔 “ {0})) ≤ (deg‘𝑔)))) |
69 | 21 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
70 | | dgrcl 23793 |
. . . . . . . . 9
⊢ ((𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈ (Poly‘ℂ) →
(deg‘(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) ∈
ℕ0) |
71 | 42, 70 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) ∈
ℕ0) |
72 | 71 | nn0cnd 11230 |
. . . . . . 7
⊢ (𝜑 → (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) ∈ ℂ) |
73 | | fta1.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
74 | 73 | nn0cnd 11230 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℂ) |
75 | | addcom 10101 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ 𝐷
∈ ℂ) → (1 + 𝐷) = (𝐷 + 1)) |
76 | 21, 74, 75 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → (1 + 𝐷) = (𝐷 + 1)) |
77 | 15 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝜑 → (deg‘𝐹) =
(deg‘((Xp ∘𝑓 − (ℂ
× {𝐴}))
∘𝑓 · (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))) |
78 | | fta1.4 |
. . . . . . . . 9
⊢ (𝜑 → (deg‘𝐹) = (𝐷 + 1)) |
79 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(deg‘(Xp ∘𝑓 −
(ℂ × {𝐴}))) =
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐴}))) |
80 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(deg‘(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) = (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) |
81 | 79, 80 | dgrmul 23830 |
. . . . . . . . . 10
⊢
((((Xp ∘𝑓 − (ℂ
× {𝐴})) ∈
(Poly‘ℂ) ∧ (Xp ∘𝑓
− (ℂ × {𝐴})) ≠ 0𝑝) ∧
((𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))) ∈
(Poly‘ℂ) ∧ (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ≠ 0𝑝)) →
(deg‘((Xp ∘𝑓 − (ℂ
× {𝐴}))
∘𝑓 · (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))))) = ((deg‘(Xp
∘𝑓 − (ℂ × {𝐴}))) + (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))) |
82 | 27, 40, 42, 65, 81 | syl22anc 1319 |
. . . . . . . . 9
⊢ (𝜑 →
(deg‘((Xp ∘𝑓 − (ℂ
× {𝐴}))
∘𝑓 · (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))))) = ((deg‘(Xp
∘𝑓 − (ℂ × {𝐴}))) + (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))) |
83 | 77, 78, 82 | 3eqtr3d 2652 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 + 1) = ((deg‘(Xp
∘𝑓 − (ℂ × {𝐴}))) + (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))) |
84 | 32 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝜑 →
((deg‘(Xp ∘𝑓 − (ℂ
× {𝐴}))) +
(deg‘(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))))) = (1 +
(deg‘(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))))) |
85 | 76, 83, 84 | 3eqtrrd 2649 |
. . . . . . 7
⊢ (𝜑 → (1 + (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))))) = (1 + 𝐷)) |
86 | 69, 72, 74, 85 | addcanad 10120 |
. . . . . 6
⊢ (𝜑 → (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) = 𝐷) |
87 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → (deg‘𝑔) = (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))))) |
88 | 87 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → ((deg‘𝑔) = 𝐷 ↔ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) = 𝐷)) |
89 | | cnveq 5218 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → ◡𝑔 = ◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) |
90 | 89 | imaeq1d 5384 |
. . . . . . . . . 10
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → (◡𝑔 “ {0}) = (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) |
91 | 90 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → ((◡𝑔 “ {0}) ∈ Fin ↔ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈
Fin)) |
92 | 90 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → (#‘(◡𝑔 “ {0})) = (#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}))) |
93 | 92, 87 | breq12d 4596 |
. . . . . . . . 9
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → ((#‘(◡𝑔 “ {0})) ≤ (deg‘𝑔) ↔ (#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))) |
94 | 91, 93 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → (((◡𝑔 “ {0}) ∈ Fin ∧
(#‘(◡𝑔 “ {0})) ≤ (deg‘𝑔)) ↔ ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧
(#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))))))) |
95 | 88, 94 | imbi12d 333 |
. . . . . . 7
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → (((deg‘𝑔) = 𝐷 → ((◡𝑔 “ {0}) ∈ Fin ∧
(#‘(◡𝑔 “ {0})) ≤ (deg‘𝑔))) ↔ ((deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) = 𝐷 → ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧
(#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))))) |
96 | 95 | rspcv 3278 |
. . . . . 6
⊢ ((𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈ ((Poly‘ℂ) ∖
{0𝑝}) → (∀𝑔 ∈ ((Poly‘ℂ) ∖
{0𝑝})((deg‘𝑔) = 𝐷 → ((◡𝑔 “ {0}) ∈ Fin ∧
(#‘(◡𝑔 “ {0})) ≤ (deg‘𝑔))) → ((deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) = 𝐷 → ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧
(#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))))) |
97 | 67, 68, 86, 96 | syl3c 64 |
. . . . 5
⊢ (𝜑 → ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧
(#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))) |
98 | 97 | simpld 474 |
. . . 4
⊢ (𝜑 → (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈
Fin) |
99 | | snfi 7923 |
. . . 4
⊢ {𝐴} ∈ Fin |
100 | | unfi 8112 |
. . . 4
⊢ (((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧ {𝐴} ∈ Fin) → ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}) ∈ Fin) |
101 | 98, 99, 100 | sylancl 693 |
. . 3
⊢ (𝜑 → ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}) ∈ Fin) |
102 | 52, 101 | eqeltrd 2688 |
. 2
⊢ (𝜑 → 𝑅 ∈ Fin) |
103 | 52 | fveq2d 6107 |
. . 3
⊢ (𝜑 → (#‘𝑅) = (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}))) |
104 | | hashcl 13009 |
. . . . . 6
⊢ (((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}) ∈ Fin → (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ∈
ℕ0) |
105 | 101, 104 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ∈
ℕ0) |
106 | 105 | nn0red 11229 |
. . . 4
⊢ (𝜑 → (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ∈ ℝ) |
107 | | hashcl 13009 |
. . . . . . 7
⊢ ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin →
(#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ∈
ℕ0) |
108 | 98, 107 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ∈
ℕ0) |
109 | 108 | nn0red 11229 |
. . . . 5
⊢ (𝜑 → (#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ∈
ℝ) |
110 | | peano2re 10088 |
. . . . 5
⊢
((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ∈ ℝ →
((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + 1) ∈
ℝ) |
111 | 109, 110 | syl 17 |
. . . 4
⊢ (𝜑 → ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + 1) ∈
ℝ) |
112 | | dgrcl 23793 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℂ)
→ (deg‘𝐹) ∈
ℕ0) |
113 | 4, 112 | syl 17 |
. . . . 5
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
114 | 113 | nn0red 11229 |
. . . 4
⊢ (𝜑 → (deg‘𝐹) ∈
ℝ) |
115 | | hashun2 13033 |
. . . . . 6
⊢ (((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧ {𝐴} ∈ Fin) →
(#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ≤ ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + (#‘{𝐴}))) |
116 | 98, 99, 115 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ≤ ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + (#‘{𝐴}))) |
117 | | hashsng 13020 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(#‘{𝐴}) =
1) |
118 | 11, 117 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘{𝐴}) = 1) |
119 | 118 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + (#‘{𝐴})) = ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + 1)) |
120 | 116, 119 | breqtrd 4609 |
. . . 4
⊢ (𝜑 → (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ≤ ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + 1)) |
121 | 73 | nn0red 11229 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ℝ) |
122 | | 1red 9934 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
123 | 97 | simprd 478 |
. . . . . . 7
⊢ (𝜑 → (#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))))) |
124 | 123, 86 | breqtrd 4609 |
. . . . . 6
⊢ (𝜑 → (#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ 𝐷) |
125 | 109, 121,
122, 124 | leadd1dd 10520 |
. . . . 5
⊢ (𝜑 → ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + 1) ≤ (𝐷 + 1)) |
126 | 125, 78 | breqtrrd 4611 |
. . . 4
⊢ (𝜑 → ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + 1) ≤
(deg‘𝐹)) |
127 | 106, 111,
114, 120, 126 | letrd 10073 |
. . 3
⊢ (𝜑 → (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ≤ (deg‘𝐹)) |
128 | 103, 127 | eqbrtrd 4605 |
. 2
⊢ (𝜑 → (#‘𝑅) ≤ (deg‘𝐹)) |
129 | 102, 128 | jca 553 |
1
⊢ (𝜑 → (𝑅 ∈ Fin ∧ (#‘𝑅) ≤ (deg‘𝐹))) |