Step | Hyp | Ref
| Expression |
1 | | fta1.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℂ) ∖
{0𝑝})) |
2 | | eldifsn 4317 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ((Poly‘ℂ)
∖ {0𝑝}) ↔ (𝐹 ∈ (Poly‘ℂ) ∧ 𝐹 ≠
0𝑝)) |
3 | 1, 2 | sylib 208 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∈ (Poly‘ℂ) ∧ 𝐹 ≠
0𝑝)) |
4 | 3 | simpld 475 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℂ)) |
5 | | fta1.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (◡𝐹 “ {0})) |
6 | | plyf 23954 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘ℂ)
→ 𝐹:ℂ⟶ℂ) |
7 | | ffn 6045 |
. . . . . . . . . . 11
⊢ (𝐹:ℂ⟶ℂ →
𝐹 Fn
ℂ) |
8 | | fniniseg 6338 |
. . . . . . . . . . 11
⊢ (𝐹 Fn ℂ → (𝐴 ∈ (◡𝐹 “ {0}) ↔ (𝐴 ∈ ℂ ∧ (𝐹‘𝐴) = 0))) |
9 | 4, 6, 7, 8 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ (◡𝐹 “ {0}) ↔ (𝐴 ∈ ℂ ∧ (𝐹‘𝐴) = 0))) |
10 | 5, 9 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ ℂ ∧ (𝐹‘𝐴) = 0)) |
11 | 10 | simpld 475 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
12 | 10 | simprd 479 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝐴) = 0) |
13 | | eqid 2622 |
. . . . . . . . 9
⊢
(Xp ∘𝑓 − (ℂ
× {𝐴})) =
(Xp ∘𝑓 − (ℂ ×
{𝐴})) |
14 | 13 | facth 24061 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐴 ∈ ℂ
∧ (𝐹‘𝐴) = 0) → 𝐹 = ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))))) |
15 | 4, 11, 12, 14 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))))) |
16 | 15 | cnveqd 5298 |
. . . . . 6
⊢ (𝜑 → ◡𝐹 = ◡((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))))) |
17 | 16 | imaeq1d 5465 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ {0}) = (◡((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) “
{0})) |
18 | | cnex 10017 |
. . . . . . 7
⊢ ℂ
∈ V |
19 | 18 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂ ∈
V) |
20 | | ssid 3624 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
21 | | ax-1cn 9994 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
22 | | plyid 23965 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈
(Poly‘ℂ)) |
23 | 20, 21, 22 | mp2an 708 |
. . . . . . . 8
⊢
Xp ∈ (Poly‘ℂ) |
24 | | plyconst 23962 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 𝐴
∈ ℂ) → (ℂ × {𝐴}) ∈
(Poly‘ℂ)) |
25 | 20, 11, 24 | sylancr 695 |
. . . . . . . 8
⊢ (𝜑 → (ℂ × {𝐴}) ∈
(Poly‘ℂ)) |
26 | | plysubcl 23978 |
. . . . . . . 8
⊢
((Xp ∈ (Poly‘ℂ) ∧ (ℂ
× {𝐴}) ∈
(Poly‘ℂ)) → (Xp ∘𝑓
− (ℂ × {𝐴})) ∈
(Poly‘ℂ)) |
27 | 23, 25, 26 | sylancr 695 |
. . . . . . 7
⊢ (𝜑 → (Xp
∘𝑓 − (ℂ × {𝐴})) ∈
(Poly‘ℂ)) |
28 | | plyf 23954 |
. . . . . . 7
⊢
((Xp ∘𝑓 − (ℂ
× {𝐴})) ∈
(Poly‘ℂ) → (Xp ∘𝑓
− (ℂ × {𝐴})):ℂ⟶ℂ) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → (Xp
∘𝑓 − (ℂ × {𝐴})):ℂ⟶ℂ) |
30 | 13 | plyremlem 24059 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((Xp ∘𝑓 − (ℂ ×
{𝐴})) ∈
(Poly‘ℂ) ∧ (deg‘(Xp
∘𝑓 − (ℂ × {𝐴}))) = 1 ∧ (◡(Xp
∘𝑓 − (ℂ × {𝐴})) “ {0}) = {𝐴})) |
31 | 11, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((Xp
∘𝑓 − (ℂ × {𝐴})) ∈ (Poly‘ℂ) ∧
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐴}))) = 1 ∧
(◡(Xp
∘𝑓 − (ℂ × {𝐴})) “ {0}) = {𝐴})) |
32 | 31 | simp2d 1074 |
. . . . . . . . . 10
⊢ (𝜑 →
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐴}))) =
1) |
33 | | ax-1ne0 10005 |
. . . . . . . . . . 11
⊢ 1 ≠
0 |
34 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≠ 0) |
35 | 32, 34 | eqnetrd 2861 |
. . . . . . . . 9
⊢ (𝜑 →
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐴}))) ≠
0) |
36 | | fveq2 6191 |
. . . . . . . . . . 11
⊢
((Xp ∘𝑓 − (ℂ
× {𝐴})) =
0𝑝 → (deg‘(Xp
∘𝑓 − (ℂ × {𝐴}))) =
(deg‘0𝑝)) |
37 | | dgr0 24018 |
. . . . . . . . . . 11
⊢
(deg‘0𝑝) = 0 |
38 | 36, 37 | syl6eq 2672 |
. . . . . . . . . 10
⊢
((Xp ∘𝑓 − (ℂ
× {𝐴})) =
0𝑝 → (deg‘(Xp
∘𝑓 − (ℂ × {𝐴}))) = 0) |
39 | 38 | necon3i 2826 |
. . . . . . . . 9
⊢
((deg‘(Xp ∘𝑓 −
(ℂ × {𝐴})))
≠ 0 → (Xp ∘𝑓 −
(ℂ × {𝐴})) ≠
0𝑝) |
40 | 35, 39 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (Xp
∘𝑓 − (ℂ × {𝐴})) ≠
0𝑝) |
41 | | quotcl2 24057 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ (Xp ∘𝑓 − (ℂ
× {𝐴})) ∈
(Poly‘ℂ) ∧ (Xp ∘𝑓
− (ℂ × {𝐴})) ≠ 0𝑝) →
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))) ∈
(Poly‘ℂ)) |
42 | 4, 27, 40, 41 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈
(Poly‘ℂ)) |
43 | | plyf 23954 |
. . . . . . 7
⊢ ((𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈ (Poly‘ℂ) →
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))):ℂ⟶ℂ) |
44 | 42, 43 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))):ℂ⟶ℂ) |
45 | | ofmulrt 24037 |
. . . . . 6
⊢ ((ℂ
∈ V ∧ (Xp ∘𝑓 −
(ℂ × {𝐴})):ℂ⟶ℂ ∧ (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))):ℂ⟶ℂ) → (◡((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) “ {0}) =
((◡(Xp
∘𝑓 − (ℂ × {𝐴})) “ {0}) ∪ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}))) |
46 | 19, 29, 44, 45 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (◡((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) “ {0}) =
((◡(Xp
∘𝑓 − (ℂ × {𝐴})) “ {0}) ∪ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}))) |
47 | 31 | simp3d 1075 |
. . . . . 6
⊢ (𝜑 → (◡(Xp
∘𝑓 − (ℂ × {𝐴})) “ {0}) = {𝐴}) |
48 | 47 | uneq1d 3766 |
. . . . 5
⊢ (𝜑 → ((◡(Xp
∘𝑓 − (ℂ × {𝐴})) “ {0}) ∪ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) = ({𝐴} ∪ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}))) |
49 | 17, 46, 48 | 3eqtrd 2660 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ {0}) = ({𝐴} ∪ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}))) |
50 | | fta1.1 |
. . . 4
⊢ 𝑅 = (◡𝐹 “ {0}) |
51 | | uncom 3757 |
. . . 4
⊢ ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}) = ({𝐴} ∪ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) |
52 | 49, 50, 51 | 3eqtr4g 2681 |
. . 3
⊢ (𝜑 → 𝑅 = ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) |
53 | 3 | simprd 479 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ≠
0𝑝) |
54 | 15 | eqcomd 2628 |
. . . . . . . . 9
⊢ (𝜑 → ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) = 𝐹) |
55 | | 0cnd 10033 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℂ) |
56 | | mul01 10215 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (𝑥 · 0) =
0) |
57 | 56 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑥 · 0) = 0) |
58 | 19, 29, 55, 55, 57 | caofid1 6927 |
. . . . . . . . . 10
⊢ (𝜑 → ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(ℂ × {0})) = (ℂ × {0})) |
59 | | df-0p 23437 |
. . . . . . . . . . 11
⊢
0𝑝 = (ℂ × {0}) |
60 | 59 | oveq2i 6661 |
. . . . . . . . . 10
⊢
((Xp ∘𝑓 − (ℂ
× {𝐴}))
∘𝑓 · 0𝑝) =
((Xp ∘𝑓 − (ℂ ×
{𝐴}))
∘𝑓 · (ℂ × {0})) |
61 | 58, 60, 59 | 3eqtr4g 2681 |
. . . . . . . . 9
⊢ (𝜑 → ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
0𝑝) = 0𝑝) |
62 | 53, 54, 61 | 3netr4d 2871 |
. . . . . . . 8
⊢ (𝜑 → ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) ≠
((Xp ∘𝑓 − (ℂ ×
{𝐴}))
∘𝑓 · 0𝑝)) |
63 | | oveq2 6658 |
. . . . . . . . 9
⊢ ((𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) = 0𝑝 →
((Xp ∘𝑓 − (ℂ ×
{𝐴}))
∘𝑓 · (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) = ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
0𝑝)) |
64 | 63 | necon3i 2826 |
. . . . . . . 8
⊢
(((Xp ∘𝑓 − (ℂ
× {𝐴}))
∘𝑓 · (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) ≠ ((Xp
∘𝑓 − (ℂ × {𝐴})) ∘𝑓 ·
0𝑝) → (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ≠
0𝑝) |
65 | 62, 64 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ≠
0𝑝) |
66 | | eldifsn 4317 |
. . . . . . 7
⊢ ((𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈ ((Poly‘ℂ) ∖
{0𝑝}) ↔ ((𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈ (Poly‘ℂ) ∧
(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))) ≠
0𝑝)) |
67 | 42, 65, 66 | sylanbrc 698 |
. . . . . 6
⊢ (𝜑 → (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈ ((Poly‘ℂ) ∖
{0𝑝})) |
68 | | fta1.6 |
. . . . . 6
⊢ (𝜑 → ∀𝑔 ∈ ((Poly‘ℂ) ∖
{0𝑝})((deg‘𝑔) = 𝐷 → ((◡𝑔 “ {0}) ∈ Fin ∧
(#‘(◡𝑔 “ {0})) ≤ (deg‘𝑔)))) |
69 | 21 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
70 | | dgrcl 23989 |
. . . . . . . . 9
⊢ ((𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) ∈ (Poly‘ℂ) →
(deg‘(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) ∈
ℕ0) |
71 | 42, 70 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) ∈
ℕ0) |
72 | 71 | nn0cnd 11353 |
. . . . . . 7
⊢ (𝜑 → (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) ∈ ℂ) |
73 | | fta1.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
74 | 73 | nn0cnd 11353 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℂ) |
75 | | addcom 10222 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ 𝐷
∈ ℂ) → (1 + 𝐷) = (𝐷 + 1)) |
76 | 21, 74, 75 | sylancr 695 |
. . . . . . . 8
⊢ (𝜑 → (1 + 𝐷) = (𝐷 + 1)) |
77 | 15 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝜑 → (deg‘𝐹) =
(deg‘((Xp ∘𝑓 − (ℂ
× {𝐴}))
∘𝑓 · (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))) |
78 | | fta1.4 |
. . . . . . . . 9
⊢ (𝜑 → (deg‘𝐹) = (𝐷 + 1)) |
79 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(deg‘(Xp ∘𝑓 −
(ℂ × {𝐴}))) =
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐴}))) |
80 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(deg‘(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))) = (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) |
81 | 79, 80 | dgrmul 24026 |
. . . . . . . . . 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 1327 |
. . . . . . . . 9
⊢ (𝜑 →
(deg‘((Xp ∘𝑓 − (ℂ
× {𝐴}))
∘𝑓 · (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))))) = ((deg‘(Xp
∘𝑓 − (ℂ × {𝐴}))) + (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))) |
83 | 77, 78, 82 | 3eqtr3d 2664 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 + 1) = ((deg‘(Xp
∘𝑓 − (ℂ × {𝐴}))) + (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))) |
84 | 32 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝜑 →
((deg‘(Xp ∘𝑓 − (ℂ
× {𝐴}))) +
(deg‘(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴}))))) = (1 +
(deg‘(𝐹 quot
(Xp ∘𝑓 − (ℂ ×
{𝐴})))))) |
85 | 76, 83, 84 | 3eqtrrd 2661 |
. . . . . . 7
⊢ (𝜑 → (1 + (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))))) = (1 + 𝐷)) |
86 | 69, 72, 74, 85 | addcanad 10241 |
. . . . . 6
⊢ (𝜑 → (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) = 𝐷) |
87 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → (deg‘𝑔) = (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))))) |
88 | 87 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → ((deg‘𝑔) = 𝐷 ↔ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) = 𝐷)) |
89 | | cnveq 5296 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → ◡𝑔 = ◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) |
90 | 89 | imaeq1d 5465 |
. . . . . . . . . 10
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → (◡𝑔 “ {0}) = (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) |
91 | 90 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → ((◡𝑔 “ {0}) ∈ Fin ↔ (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈
Fin)) |
92 | 90 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → (#‘(◡𝑔 “ {0})) = (#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}))) |
93 | 92, 87 | breq12d 4666 |
. . . . . . . . 9
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → ((#‘(◡𝑔 “ {0})) ≤ (deg‘𝑔) ↔ (#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))) |
94 | 91, 93 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → (((◡𝑔 “ {0}) ∈ Fin ∧
(#‘(◡𝑔 “ {0})) ≤ (deg‘𝑔)) ↔ ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧
(#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))))))) |
95 | 88, 94 | imbi12d 334 |
. . . . . . 7
⊢ (𝑔 = (𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) → (((deg‘𝑔) = 𝐷 → ((◡𝑔 “ {0}) ∈ Fin ∧
(#‘(◡𝑔 “ {0})) ≤ (deg‘𝑔))) ↔ ((deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))) = 𝐷 → ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧
(#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))))) |
96 | 95 | rspcv 3305 |
. . . . . 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 66 |
. . . . 5
⊢ (𝜑 → ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧
(#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴})))))) |
98 | 97 | simpld 475 |
. . . 4
⊢ (𝜑 → (◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈
Fin) |
99 | | snfi 8038 |
. . . 4
⊢ {𝐴} ∈ Fin |
100 | | unfi 8227 |
. . . 4
⊢ (((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧ {𝐴} ∈ Fin) → ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}) ∈ Fin) |
101 | 98, 99, 100 | sylancl 694 |
. . 3
⊢ (𝜑 → ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}) ∈ Fin) |
102 | 52, 101 | eqeltrd 2701 |
. 2
⊢ (𝜑 → 𝑅 ∈ Fin) |
103 | 52 | fveq2d 6195 |
. . 3
⊢ (𝜑 → (#‘𝑅) = (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}))) |
104 | | hashcl 13147 |
. . . . . 6
⊢ (((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}) ∈ Fin → (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ∈
ℕ0) |
105 | 101, 104 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ∈
ℕ0) |
106 | 105 | nn0red 11352 |
. . . 4
⊢ (𝜑 → (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ∈ ℝ) |
107 | | hashcl 13147 |
. . . . . . 7
⊢ ((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin →
(#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ∈
ℕ0) |
108 | 98, 107 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ∈
ℕ0) |
109 | 108 | nn0red 11352 |
. . . . 5
⊢ (𝜑 → (#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ∈
ℝ) |
110 | | peano2re 10209 |
. . . . 5
⊢
((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ∈ ℝ →
((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + 1) ∈
ℝ) |
111 | 109, 110 | syl 17 |
. . . 4
⊢ (𝜑 → ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + 1) ∈
ℝ) |
112 | | dgrcl 23989 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℂ)
→ (deg‘𝐹) ∈
ℕ0) |
113 | 4, 112 | syl 17 |
. . . . 5
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
114 | 113 | nn0red 11352 |
. . . 4
⊢ (𝜑 → (deg‘𝐹) ∈
ℝ) |
115 | | hashun2 13172 |
. . . . . 6
⊢ (((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧ {𝐴} ∈ Fin) →
(#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ≤ ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + (#‘{𝐴}))) |
116 | 98, 99, 115 | sylancl 694 |
. . . . 5
⊢ (𝜑 → (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ≤ ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + (#‘{𝐴}))) |
117 | | hashsng 13159 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(#‘{𝐴}) =
1) |
118 | 11, 117 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘{𝐴}) = 1) |
119 | 118 | oveq2d 6666 |
. . . . 5
⊢ (𝜑 → ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + (#‘{𝐴})) = ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + 1)) |
120 | 116, 119 | breqtrd 4679 |
. . . 4
⊢ (𝜑 → (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ≤ ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + 1)) |
121 | 73 | nn0red 11352 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ℝ) |
122 | | 1red 10055 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
123 | 97 | simprd 479 |
. . . . . . 7
⊢ (𝜑 → (#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))))) |
124 | 123, 86 | breqtrd 4679 |
. . . . . 6
⊢ (𝜑 → (#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ 𝐷) |
125 | 109, 121,
122, 124 | leadd1dd 10641 |
. . . . 5
⊢ (𝜑 → ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + 1) ≤ (𝐷 + 1)) |
126 | 125, 78 | breqtrrd 4681 |
. . . 4
⊢ (𝜑 → ((#‘(◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0})) + 1) ≤
(deg‘𝐹)) |
127 | 106, 111,
114, 120, 126 | letrd 10194 |
. . 3
⊢ (𝜑 → (#‘((◡(𝐹 quot (Xp
∘𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ≤ (deg‘𝐹)) |
128 | 103, 127 | eqbrtrd 4675 |
. 2
⊢ (𝜑 → (#‘𝑅) ≤ (deg‘𝐹)) |
129 | 102, 128 | jca 554 |
1
⊢ (𝜑 → (𝑅 ∈ Fin ∧ (#‘𝑅) ≤ (deg‘𝐹))) |