Step | Hyp | Ref
| Expression |
1 | | plydiv.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
2 | | dgrcl 23793 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
4 | 3 | nn0red 11229 |
. . . 4
⊢ (𝜑 → (deg‘𝐹) ∈
ℝ) |
5 | | plydiv.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) |
6 | | dgrcl 23793 |
. . . . . 6
⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈
ℕ0) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → (deg‘𝐺) ∈
ℕ0) |
8 | 7 | nn0red 11229 |
. . . 4
⊢ (𝜑 → (deg‘𝐺) ∈
ℝ) |
9 | 4, 8 | resubcld 10337 |
. . 3
⊢ (𝜑 → ((deg‘𝐹) − (deg‘𝐺)) ∈
ℝ) |
10 | | arch 11166 |
. . 3
⊢
(((deg‘𝐹)
− (deg‘𝐺))
∈ ℝ → ∃𝑑 ∈ ℕ ((deg‘𝐹) − (deg‘𝐺)) < 𝑑) |
11 | 9, 10 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑑 ∈ ℕ ((deg‘𝐹) − (deg‘𝐺)) < 𝑑) |
12 | | olc 398 |
. . . 4
⊢
(((deg‘𝐹)
− (deg‘𝐺)) <
𝑑 → (𝐹 = 0𝑝 ∨
((deg‘𝐹) −
(deg‘𝐺)) < 𝑑)) |
13 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → 𝐹 ∈ (Poly‘𝑆)) |
14 | | nnnn0 11176 |
. . . . . . 7
⊢ (𝑑 ∈ ℕ → 𝑑 ∈
ℕ0) |
15 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (((deg‘𝑓) − (deg‘𝐺)) < 𝑥 ↔ ((deg‘𝑓) − (deg‘𝐺)) < 0)) |
16 | 15 | orbi2d 734 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑥) ↔ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) <
0))) |
17 | 16 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑥) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
((𝑓 = 0𝑝
∨ ((deg‘𝑓) −
(deg‘𝐺)) < 0)
→ ∃𝑞 ∈
(Poly‘𝑆)((𝑓 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝑓
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺))))) |
18 | 17 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑥) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)
→ ∃𝑞 ∈
(Poly‘𝑆)((𝑓 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝑓
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺))))) |
19 | 18 | imbi2d 329 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝜑 → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑥) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))) ↔
(𝜑 → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)
→ ∃𝑞 ∈
(Poly‘𝑆)((𝑓 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝑓
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)))))) |
20 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑑 → (((deg‘𝑓) − (deg‘𝐺)) < 𝑥 ↔ ((deg‘𝑓) − (deg‘𝐺)) < 𝑑)) |
21 | 20 | orbi2d 734 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑑 → ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑥) ↔ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑))) |
22 | 21 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑑 → (((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑥) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
((𝑓 = 0𝑝
∨ ((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
23 | 22 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑥 = 𝑑 → (∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑥) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
24 | 23 | imbi2d 329 |
. . . . . . . 8
⊢ (𝑥 = 𝑑 → ((𝜑 → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑥) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))) ↔
(𝜑 → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))))) |
25 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑑 + 1) → (((deg‘𝑓) − (deg‘𝐺)) < 𝑥 ↔ ((deg‘𝑓) − (deg‘𝐺)) < (𝑑 + 1))) |
26 | 25 | orbi2d 734 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑑 + 1) → ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑥) ↔ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)))) |
27 | 26 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑑 + 1) → (((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑥) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
((𝑓 = 0𝑝
∨ ((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
28 | 27 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑥 = (𝑑 + 1) → (∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑥) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
29 | 28 | imbi2d 329 |
. . . . . . . 8
⊢ (𝑥 = (𝑑 + 1) → ((𝜑 → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑥) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))) ↔
(𝜑 → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))))) |
30 | | plydiv.pl |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
31 | 30 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ (Poly‘𝑆) ∧ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)))
∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
32 | | plydiv.tm |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) |
33 | 32 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ (Poly‘𝑆) ∧ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)))
∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) |
34 | | plydiv.rc |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆) |
35 | 34 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ (Poly‘𝑆) ∧ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)))
∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆) |
36 | | plydiv.m1 |
. . . . . . . . . . . 12
⊢ (𝜑 → -1 ∈ 𝑆) |
37 | 36 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘𝑆) ∧ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)))
→ -1 ∈ 𝑆) |
38 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘𝑆) ∧ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)))
→ 𝑓 ∈
(Poly‘𝑆)) |
39 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘𝑆) ∧ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)))
→ 𝐺 ∈
(Poly‘𝑆)) |
40 | | plydiv.z |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ≠
0𝑝) |
41 | 40 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘𝑆) ∧ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)))
→ 𝐺 ≠
0𝑝) |
42 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑓 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = (𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) |
43 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘𝑆) ∧ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)))
→ (𝑓 =
0𝑝 ∨ ((deg‘𝑓) − (deg‘𝐺)) < 0)) |
44 | 31, 33, 35, 37, 38, 39, 41, 42, 43 | plydivlem3 23854 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (Poly‘𝑆) ∧ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)))
→ ∃𝑞 ∈
(Poly‘𝑆)((𝑓 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝑓
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺))) |
45 | 44 | expr 641 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (Poly‘𝑆)) → ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)
→ ∃𝑞 ∈
(Poly‘𝑆)((𝑓 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝑓
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)))) |
46 | 45 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 0)
→ ∃𝑞 ∈
(Poly‘𝑆)((𝑓 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝑓
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)))) |
47 | | eqeq1 2614 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑔 → (𝑓 = 0𝑝 ↔ 𝑔 =
0𝑝)) |
48 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = 𝑔 → (deg‘𝑓) = (deg‘𝑔)) |
49 | 48 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 𝑔 → ((deg‘𝑓) − (deg‘𝐺)) = ((deg‘𝑔) − (deg‘𝐺))) |
50 | 49 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑔 → (((deg‘𝑓) − (deg‘𝐺)) < 𝑑 ↔ ((deg‘𝑔) − (deg‘𝐺)) < 𝑑)) |
51 | 47, 50 | orbi12d 742 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑔 → ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) ↔ (𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑))) |
52 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = 𝑔 → (𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) = (𝑔 ∘𝑓
− (𝐺
∘𝑓 · 𝑞))) |
53 | 52 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 𝑔 → ((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ↔ (𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝)) |
54 | 52 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = 𝑔 → (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) =
(deg‘(𝑔
∘𝑓 − (𝐺 ∘𝑓 · 𝑞)))) |
55 | 54 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 𝑔 → ((deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺) ↔
(deg‘(𝑔
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺))) |
56 | 53, 55 | orbi12d 742 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑔 → (((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)) ↔
((𝑔
∘𝑓 − (𝐺 ∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝑔
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)))) |
57 | 56 | rexbidv 3034 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑔 → (∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)) ↔
∃𝑞 ∈
(Poly‘𝑆)((𝑔 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝑔
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)))) |
58 | 51, 57 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑔 → (((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
((𝑔 = 0𝑝
∨ ((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
59 | 58 | cbvralv 3147 |
. . . . . . . . . . . . 13
⊢
(∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
∀𝑔 ∈
(Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))) |
60 | | simplll 794 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) ∧ (∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) → 𝜑) |
61 | 60, 30 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑑 ∈ ℕ0)
∧ 𝑓 ∈
(Poly‘𝑆)) ∧
(∀𝑔 ∈
(Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
62 | 60, 32 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑑 ∈ ℕ0)
∧ 𝑓 ∈
(Poly‘𝑆)) ∧
(∀𝑔 ∈
(Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) |
63 | 60, 34 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑑 ∈ ℕ0)
∧ 𝑓 ∈
(Poly‘𝑆)) ∧
(∀𝑔 ∈
(Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆) |
64 | 60, 36 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) ∧ (∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) → -1 ∈ 𝑆) |
65 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) ∧ (∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) → 𝑓 ∈ (Poly‘𝑆)) |
66 | 60, 5 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) ∧ (∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) → 𝐺 ∈ (Poly‘𝑆)) |
67 | 60, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) ∧ (∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) → 𝐺 ≠
0𝑝) |
68 | | simpllr 795 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) ∧ (∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) → 𝑑 ∈ ℕ0) |
69 | | simprrr 801 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) ∧ (∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) → ((deg‘𝑓) − (deg‘𝐺)) = 𝑑) |
70 | | simprrl 800 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) ∧ (∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) → 𝑓 ≠ 0𝑝) |
71 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 ∘𝑓
− (𝐺
∘𝑓 · 𝑝)) = (𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑝)) |
72 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → (𝑤↑𝑑) = (𝑧↑𝑑)) |
73 | 72 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑧 → ((((coeff‘𝑓)‘(deg‘𝑓)) / ((coeff‘𝐺)‘(deg‘𝐺))) · (𝑤↑𝑑)) = ((((coeff‘𝑓)‘(deg‘𝑓)) / ((coeff‘𝐺)‘(deg‘𝐺))) · (𝑧↑𝑑))) |
74 | 73 | cbvmptv 4678 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℂ ↦
((((coeff‘𝑓)‘(deg‘𝑓)) / ((coeff‘𝐺)‘(deg‘𝐺))) · (𝑤↑𝑑))) = (𝑧 ∈ ℂ ↦ ((((coeff‘𝑓)‘(deg‘𝑓)) / ((coeff‘𝐺)‘(deg‘𝐺))) · (𝑧↑𝑑))) |
75 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) ∧ (∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) → ∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))) |
76 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 = 𝑝 → (𝐺 ∘𝑓 · 𝑞) = (𝐺 ∘𝑓 · 𝑝)) |
77 | 76 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 = 𝑝 → (𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) = (𝑔 ∘𝑓
− (𝐺
∘𝑓 · 𝑝))) |
78 | 77 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑞 = 𝑝 → ((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ↔ (𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑝)) =
0𝑝)) |
79 | 77 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 = 𝑝 → (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) =
(deg‘(𝑔
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)))) |
80 | 79 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑞 = 𝑝 → ((deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺) ↔
(deg‘(𝑔
∘𝑓 − (𝐺 ∘𝑓 · 𝑝))) < (deg‘𝐺))) |
81 | 78, 80 | orbi12d 742 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 = 𝑝 → (((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)) ↔
((𝑔
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = 0𝑝 ∨
(deg‘(𝑔
∘𝑓 − (𝐺 ∘𝑓 · 𝑝))) < (deg‘𝐺)))) |
82 | 81 | cbvrexv 3148 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑞 ∈
(Poly‘𝑆)((𝑔 ∘𝑓
− (𝐺
∘𝑓 · 𝑞)) = 0𝑝 ∨
(deg‘(𝑔
∘𝑓 − (𝐺 ∘𝑓 · 𝑞))) < (deg‘𝐺)) ↔ ∃𝑝 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑝)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑝))) <
(deg‘𝐺))) |
83 | 82 | imbi2i 325 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
((𝑔 = 0𝑝
∨ ((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑝 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑝)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑝))) <
(deg‘𝐺)))) |
84 | 83 | ralbii 2963 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑔 ∈
(Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
∀𝑔 ∈
(Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑝 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑝)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑝))) <
(deg‘𝐺)))) |
85 | 75, 84 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) ∧ (∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) → ∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑝 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑝)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑝))) <
(deg‘𝐺)))) |
86 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(coeff‘𝑓) =
(coeff‘𝑓) |
87 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(coeff‘𝐺) =
(coeff‘𝐺) |
88 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(deg‘𝑓) =
(deg‘𝑓) |
89 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(deg‘𝐺) =
(deg‘𝐺) |
90 | 61, 62, 63, 64, 65, 66, 67, 42, 68, 69, 70, 71, 74, 85, 86, 87, 88, 89 | plydivlem4 23855 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) ∧ (∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) |
91 | 90 | exp32 629 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → (∀𝑔 ∈ (Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) →
((𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
92 | 91 | ralrimdva 2952 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) →
(∀𝑔 ∈
(Poly‘𝑆)((𝑔 = 0𝑝 ∨
((deg‘𝑔) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑔 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) →
∀𝑓 ∈
(Poly‘𝑆)((𝑓 ≠ 0𝑝
∧ ((deg‘𝑓)
− (deg‘𝐺)) =
𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
93 | 59, 92 | syl5bi 231 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) →
(∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) →
∀𝑓 ∈
(Poly‘𝑆)((𝑓 ≠ 0𝑝
∧ ((deg‘𝑓)
− (deg‘𝐺)) =
𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
94 | 93 | ancld 574 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) →
(∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) →
(∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
∀𝑓 ∈
(Poly‘𝑆)((𝑓 ≠ 0𝑝
∧ ((deg‘𝑓)
− (deg‘𝐺)) =
𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))))) |
95 | | dgrcl 23793 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ (Poly‘𝑆) → (deg‘𝑓) ∈
ℕ0) |
96 | 95 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → (deg‘𝑓) ∈
ℕ0) |
97 | 96 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → (deg‘𝑓) ∈
ℤ) |
98 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → 𝐺 ∈ (Poly‘𝑆)) |
99 | 98, 6 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → (deg‘𝐺) ∈
ℕ0) |
100 | 99 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → (deg‘𝐺) ∈
ℤ) |
101 | 97, 100 | zsubcld 11363 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → ((deg‘𝑓) − (deg‘𝐺)) ∈
ℤ) |
102 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 ∈ ℕ0
→ 𝑑 ∈
ℤ) |
103 | 102 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → 𝑑 ∈ ℤ) |
104 | | zleltp1 11305 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((deg‘𝑓)
− (deg‘𝐺))
∈ ℤ ∧ 𝑑
∈ ℤ) → (((deg‘𝑓) − (deg‘𝐺)) ≤ 𝑑 ↔ ((deg‘𝑓) − (deg‘𝐺)) < (𝑑 + 1))) |
105 | 101, 103,
104 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → (((deg‘𝑓) − (deg‘𝐺)) ≤ 𝑑 ↔ ((deg‘𝑓) − (deg‘𝐺)) < (𝑑 + 1))) |
106 | 101 | zred 11358 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → ((deg‘𝑓) − (deg‘𝐺)) ∈
ℝ) |
107 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 ∈ ℕ0
→ 𝑑 ∈
ℝ) |
108 | 107 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → 𝑑 ∈ ℝ) |
109 | 106, 108 | leloed 10059 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → (((deg‘𝑓) − (deg‘𝐺)) ≤ 𝑑 ↔ (((deg‘𝑓) − (deg‘𝐺)) < 𝑑 ∨ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) |
110 | 105, 109 | bitr3d 269 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → (((deg‘𝑓) − (deg‘𝐺)) < (𝑑 + 1) ↔ (((deg‘𝑓) − (deg‘𝐺)) < 𝑑 ∨ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑))) |
111 | 110 | orbi2d 734 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)) ↔ (𝑓 = 0𝑝 ∨
(((deg‘𝑓) −
(deg‘𝐺)) < 𝑑 ∨ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑)))) |
112 | | pm5.63 961 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑) ↔ (𝑓 = 0𝑝 ∨ (¬ 𝑓 = 0𝑝 ∧
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑))) |
113 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ≠ 0𝑝
↔ ¬ 𝑓 =
0𝑝) |
114 | 113 | anbi1i 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ≠ 0𝑝
∧ ((deg‘𝑓)
− (deg‘𝐺)) =
𝑑) ↔ (¬ 𝑓 = 0𝑝 ∧
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑)) |
115 | 114 | orbi2i 540 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 = 0𝑝 ∨
(𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑)) ↔ (𝑓 = 0𝑝 ∨ (¬ 𝑓 = 0𝑝 ∧
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑))) |
116 | 112, 115 | bitr4i 266 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑) ↔ (𝑓 = 0𝑝 ∨ (𝑓 ≠ 0𝑝
∧ ((deg‘𝑓)
− (deg‘𝐺)) =
𝑑))) |
117 | 116 | orbi2i 540 |
. . . . . . . . . . . . . . . . . 18
⊢
((((deg‘𝑓)
− (deg‘𝐺)) <
𝑑 ∨ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑)) ↔ (((deg‘𝑓) − (deg‘𝐺)) < 𝑑 ∨ (𝑓 = 0𝑝 ∨ (𝑓 ≠ 0𝑝
∧ ((deg‘𝑓)
− (deg‘𝐺)) =
𝑑)))) |
118 | | or12 544 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 = 0𝑝 ∨
(((deg‘𝑓) −
(deg‘𝐺)) < 𝑑 ∨ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑)) ↔ (((deg‘𝑓) − (deg‘𝐺)) < 𝑑 ∨ (𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑))) |
119 | | or12 544 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 = 0𝑝 ∨
(((deg‘𝑓) −
(deg‘𝐺)) < 𝑑 ∨ (𝑓 ≠ 0𝑝 ∧
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑))) ↔ (((deg‘𝑓) − (deg‘𝐺)) < 𝑑 ∨ (𝑓 = 0𝑝 ∨ (𝑓 ≠ 0𝑝
∧ ((deg‘𝑓)
− (deg‘𝐺)) =
𝑑)))) |
120 | 117, 118,
119 | 3bitr4i 291 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 = 0𝑝 ∨
(((deg‘𝑓) −
(deg‘𝐺)) < 𝑑 ∨ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑)) ↔ (𝑓 = 0𝑝 ∨
(((deg‘𝑓) −
(deg‘𝐺)) < 𝑑 ∨ (𝑓 ≠ 0𝑝 ∧
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑)))) |
121 | | orass 545 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) ∨ (𝑓 ≠ 0𝑝 ∧
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑)) ↔ (𝑓 = 0𝑝 ∨
(((deg‘𝑓) −
(deg‘𝐺)) < 𝑑 ∨ (𝑓 ≠ 0𝑝 ∧
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑)))) |
122 | 120, 121 | bitr4i 266 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 = 0𝑝 ∨
(((deg‘𝑓) −
(deg‘𝐺)) < 𝑑 ∨ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑)) ↔ ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) ∨ (𝑓 ≠ 0𝑝 ∧
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑))) |
123 | 111, 122 | syl6bb 275 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)) ↔ ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) ∨ (𝑓 ≠ 0𝑝 ∧
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑)))) |
124 | 123 | imbi1d 330 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → (((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
(((𝑓 =
0𝑝 ∨ ((deg‘𝑓) − (deg‘𝐺)) < 𝑑) ∨ (𝑓 ≠ 0𝑝 ∧
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑)) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
125 | | jaob 818 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) ∨ (𝑓 ≠ 0𝑝 ∧
((deg‘𝑓) −
(deg‘𝐺)) = 𝑑)) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
(((𝑓 =
0𝑝 ∨ ((deg‘𝑓) − (deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
((𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
126 | 124, 125 | syl6bb 275 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑓 ∈ (Poly‘𝑆)) → (((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
(((𝑓 =
0𝑝 ∨ ((deg‘𝑓) − (deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
((𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))))) |
127 | 126 | ralbidva 2968 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) →
(∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
∀𝑓 ∈
(Poly‘𝑆)(((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
((𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))))) |
128 | | r19.26 3046 |
. . . . . . . . . . . 12
⊢
(∀𝑓 ∈
(Poly‘𝑆)(((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
((𝑓 ≠
0𝑝 ∧ ((deg‘𝑓) − (deg‘𝐺)) = 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))) ↔
(∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
∀𝑓 ∈
(Poly‘𝑆)((𝑓 ≠ 0𝑝
∧ ((deg‘𝑓)
− (deg‘𝐺)) =
𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
129 | 127, 128 | syl6bb 275 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) →
(∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
(∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ∧
∀𝑓 ∈
(Poly‘𝑆)((𝑓 ≠ 0𝑝
∧ ((deg‘𝑓)
− (deg‘𝐺)) =
𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))))) |
130 | 94, 129 | sylibrd 248 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) →
(∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) →
∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
131 | 130 | expcom 450 |
. . . . . . . . 9
⊢ (𝑑 ∈ ℕ0
→ (𝜑 →
(∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) →
∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))))) |
132 | 131 | a2d 29 |
. . . . . . . 8
⊢ (𝑑 ∈ ℕ0
→ ((𝜑 →
∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))) →
(𝜑 → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < (𝑑 + 1)) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))))) |
133 | 19, 24, 29, 24, 46, 132 | nn0ind 11348 |
. . . . . . 7
⊢ (𝑑 ∈ ℕ0
→ (𝜑 →
∀𝑓 ∈
(Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
134 | 14, 133 | syl 17 |
. . . . . 6
⊢ (𝑑 ∈ ℕ → (𝜑 → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))))) |
135 | 134 | impcom 445 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)))) |
136 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓 = 0𝑝 ↔ 𝐹 =
0𝑝)) |
137 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → (deg‘𝑓) = (deg‘𝐹)) |
138 | 137 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → ((deg‘𝑓) − (deg‘𝐺)) = ((deg‘𝐹) − (deg‘𝐺))) |
139 | 138 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (((deg‘𝑓) − (deg‘𝐺)) < 𝑑 ↔ ((deg‘𝐹) − (deg‘𝐺)) < 𝑑)) |
140 | 136, 139 | orbi12d 742 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) ↔ (𝐹 = 0𝑝 ∨
((deg‘𝐹) −
(deg‘𝐺)) < 𝑑))) |
141 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → (𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) = (𝐹 ∘𝑓
− (𝐺
∘𝑓 · 𝑞))) |
142 | | plydiv.r |
. . . . . . . . . . 11
⊢ 𝑅 = (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) |
143 | 141, 142 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → (𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) = 𝑅) |
144 | 143 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → ((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ↔ 𝑅 = 0𝑝)) |
145 | 143 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) =
(deg‘𝑅)) |
146 | 145 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → ((deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺) ↔
(deg‘𝑅) <
(deg‘𝐺))) |
147 | 144, 146 | orbi12d 742 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)) ↔
(𝑅 = 0𝑝
∨ (deg‘𝑅) <
(deg‘𝐺)))) |
148 | 147 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺)) ↔
∃𝑞 ∈
(Poly‘𝑆)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
149 | 140, 148 | imbi12d 333 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) ↔
((𝐹 = 0𝑝
∨ ((deg‘𝐹) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺))))) |
150 | 149 | rspcv 3278 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → (∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)((𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) =
0𝑝 ∨ (deg‘(𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞))) <
(deg‘𝐺))) →
((𝐹 = 0𝑝
∨ ((deg‘𝐹) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺))))) |
151 | 13, 135, 150 | sylc 63 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → ((𝐹 = 0𝑝 ∨
((deg‘𝐹) −
(deg‘𝐺)) < 𝑑) → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
152 | 12, 151 | syl5 33 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → (((deg‘𝐹) − (deg‘𝐺)) < 𝑑 → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
153 | 152 | rexlimdva 3013 |
. 2
⊢ (𝜑 → (∃𝑑 ∈ ℕ ((deg‘𝐹) − (deg‘𝐺)) < 𝑑 → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺)))) |
154 | 11, 153 | mpd 15 |
1
⊢ (𝜑 → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨
(deg‘𝑅) <
(deg‘𝐺))) |