This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem deg1tmle

Description: Limiting degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses deg1tm.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
deg1tm.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
deg1tm.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
deg1tm.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
deg1tm.m ⊢ · = ( ·𝑠 ‘ 𝑃 )
deg1tm.n ⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
deg1tm.e ⊢ ↑ = ( .g ‘ 𝑁 )
Assertion deg1tmle ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ≤ 𝐹 )

Proof

Step Hyp Ref Expression
1 deg1tm.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2 deg1tm.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
3 deg1tm.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 deg1tm.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
5 deg1tm.m ⊢ · = ( ·𝑠 ‘ 𝑃 )
6 deg1tm.n ⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
7 deg1tm.e ⊢ ↑ = ( .g ‘ 𝑁 )
8 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝑅 ∈ Ring )
10 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝐶 ∈ 𝐾 )
11 simpl3 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝐹 ∈ ℕ0 )
12 simprl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝑥 ∈ ℕ0 )
13 11 nn0red ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝐹 ∈ ℝ )
14 simprr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝐹 < 𝑥 )
15 13 14 ltned ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → 𝐹 ≠ 𝑥 )
16 8 2 3 4 5 6 7 9 10 11 12 15 coe1tmfv2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝐹 < 𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) )
17 16 expr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝐹 < 𝑥 → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
18 17 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → ∀ 𝑥 ∈ ℕ0 ( 𝐹 < 𝑥 → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
19 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
20 2 3 4 5 6 7 19 ply1tmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
21 nn0re ⊢ ( 𝐹 ∈ ℕ0 → 𝐹 ∈ ℝ )
22 21 rexrd ⊢ ( 𝐹 ∈ ℕ0 → 𝐹 ∈ ℝ* )
23 22 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → 𝐹 ∈ ℝ* )
24 eqid ⊢ ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) = ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) )
25 1 3 19 8 24 deg1leb ⊢ ( ( ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) ∧ 𝐹 ∈ ℝ* ) → ( ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℕ0 ( 𝐹 < 𝑥 → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
26 20 23 25 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → ( ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℕ0 ( 𝐹 < 𝑥 → ( ( coe1 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
27 18 26 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐶 · ( 𝐹 ↑ 𝑋 ) ) ) ≤ 𝐹 )