Step |
Hyp |
Ref |
Expression |
1 |
|
deg1leb.d |
⊢ 𝐷 = ( deg1 ‘ 𝑅 ) |
2 |
|
deg1leb.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
3 |
|
deg1leb.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
4 |
|
deg1leb.y |
⊢ 0 = ( 0g ‘ 𝑅 ) |
5 |
|
deg1leb.a |
⊢ 𝐴 = ( coe1 ‘ 𝐹 ) |
6 |
|
simp3 |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐹 ) < 𝐺 ) → ( 𝐷 ‘ 𝐹 ) < 𝐺 ) |
7 |
|
breq2 |
⊢ ( 𝑥 = 𝐺 → ( ( 𝐷 ‘ 𝐹 ) < 𝑥 ↔ ( 𝐷 ‘ 𝐹 ) < 𝐺 ) ) |
8 |
|
fveqeq2 |
⊢ ( 𝑥 = 𝐺 → ( ( 𝐴 ‘ 𝑥 ) = 0 ↔ ( 𝐴 ‘ 𝐺 ) = 0 ) ) |
9 |
7 8
|
imbi12d |
⊢ ( 𝑥 = 𝐺 → ( ( ( 𝐷 ‘ 𝐹 ) < 𝑥 → ( 𝐴 ‘ 𝑥 ) = 0 ) ↔ ( ( 𝐷 ‘ 𝐹 ) < 𝐺 → ( 𝐴 ‘ 𝐺 ) = 0 ) ) ) |
10 |
1 2 3
|
deg1xrcl |
⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ) |
11 |
10
|
3ad2ant1 |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐹 ) < 𝐺 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ) |
12 |
11
|
xrleidd |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐹 ) < 𝐺 ) → ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐹 ) ) |
13 |
|
simp1 |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐹 ) < 𝐺 ) → 𝐹 ∈ 𝐵 ) |
14 |
1 2 3 4 5
|
deg1leb |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ ℕ0 ( ( 𝐷 ‘ 𝐹 ) < 𝑥 → ( 𝐴 ‘ 𝑥 ) = 0 ) ) ) |
15 |
13 10 14
|
syl2anc2 |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐹 ) < 𝐺 ) → ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ ℕ0 ( ( 𝐷 ‘ 𝐹 ) < 𝑥 → ( 𝐴 ‘ 𝑥 ) = 0 ) ) ) |
16 |
12 15
|
mpbid |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐹 ) < 𝐺 ) → ∀ 𝑥 ∈ ℕ0 ( ( 𝐷 ‘ 𝐹 ) < 𝑥 → ( 𝐴 ‘ 𝑥 ) = 0 ) ) |
17 |
|
simp2 |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐹 ) < 𝐺 ) → 𝐺 ∈ ℕ0 ) |
18 |
9 16 17
|
rspcdva |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐹 ) < 𝐺 ) → ( ( 𝐷 ‘ 𝐹 ) < 𝐺 → ( 𝐴 ‘ 𝐺 ) = 0 ) ) |
19 |
6 18
|
mpd |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐹 ) < 𝐺 ) → ( 𝐴 ‘ 𝐺 ) = 0 ) |