Metamath Proof Explorer

Theorem dgrsub2

Description: Subtracting two polynomials with the same degree and top coefficient gives a polynomial of strictly lower degree. (Contributed by Stefan O'Rear, 25-Nov-2014)

Ref Expression
Hypothesis dgrsub2.a ⊢ 𝑁 = ( deg ‘ 𝐹 )
Assertion dgrsub2 ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) < 𝑁 )

Proof

Step Hyp Ref Expression
1 dgrsub2.a ⊢ 𝑁 = ( deg ‘ 𝐹 )
2 simpr2 ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
3 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
4 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
5 3 4 eqbrtrid ⊢ ( 𝑁 ∈ ℕ → ( deg ‘ 0𝑝 ) < 𝑁 )
6 fveq2 ⊢ ( ( 𝐹 ∘f − 𝐺 ) = 0𝑝 → ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) = ( deg ‘ 0𝑝 ) )
7 6 breq1d ⊢ ( ( 𝐹 ∘f − 𝐺 ) = 0𝑝 → ( ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) < 𝑁 ↔ ( deg ‘ 0𝑝 ) < 𝑁 ) )
8 5 7 syl5ibrcom ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐹 ∘f − 𝐺 ) = 0𝑝 → ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) < 𝑁 ) )
9 2 8 syl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( ( 𝐹 ∘f − 𝐺 ) = 0𝑝 → ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) < 𝑁 ) )
10 plyssc ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
11 10 sseli ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
12 plyssc ⊢ ( Poly ‘ 𝑇 ) ⊆ ( Poly ‘ ℂ )
13 12 sseli ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑇 ) → 𝐺 ∈ ( Poly ‘ ℂ ) )
14 eqid ⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
15 eqid ⊢ ( deg ‘ 𝐺 ) = ( deg ‘ 𝐺 )
16 14 15 dgrsub ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ) → ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) ≤ if ( ( deg ‘ 𝐹 ) ≤ ( deg ‘ 𝐺 ) , ( deg ‘ 𝐺 ) , ( deg ‘ 𝐹 ) ) )
17 11 13 16 syl2an ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) → ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) ≤ if ( ( deg ‘ 𝐹 ) ≤ ( deg ‘ 𝐺 ) , ( deg ‘ 𝐺 ) , ( deg ‘ 𝐹 ) ) )
18 17 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) ≤ if ( ( deg ‘ 𝐹 ) ≤ ( deg ‘ 𝐺 ) , ( deg ‘ 𝐺 ) , ( deg ‘ 𝐹 ) ) )
19 simpr1 ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( deg ‘ 𝐺 ) = 𝑁 )
20 1 eqcomi ⊢ ( deg ‘ 𝐹 ) = 𝑁
21 20 a1i ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( deg ‘ 𝐹 ) = 𝑁 )
22 19 21 ifeq12d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → if ( ( deg ‘ 𝐹 ) ≤ ( deg ‘ 𝐺 ) , ( deg ‘ 𝐺 ) , ( deg ‘ 𝐹 ) ) = if ( ( deg ‘ 𝐹 ) ≤ ( deg ‘ 𝐺 ) , 𝑁 , 𝑁 ) )
23 ifid ⊢ if ( ( deg ‘ 𝐹 ) ≤ ( deg ‘ 𝐺 ) , 𝑁 , 𝑁 ) = 𝑁
24 22 23 eqtrdi ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → if ( ( deg ‘ 𝐹 ) ≤ ( deg ‘ 𝐺 ) , ( deg ‘ 𝐺 ) , ( deg ‘ 𝐹 ) ) = 𝑁 )
25 18 24 breqtrd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) ≤ 𝑁 )
26 eqid ⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
27 eqid ⊢ ( coeff ‘ 𝐺 ) = ( coeff ‘ 𝐺 )
28 26 27 coesub ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ) → ( coeff ‘ ( 𝐹 ∘f − 𝐺 ) ) = ( ( coeff ‘ 𝐹 ) ∘f − ( coeff ‘ 𝐺 ) ) )
29 11 13 28 syl2an ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) → ( coeff ‘ ( 𝐹 ∘f − 𝐺 ) ) = ( ( coeff ‘ 𝐹 ) ∘f − ( coeff ‘ 𝐺 ) ) )
30 29 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( coeff ‘ ( 𝐹 ∘f − 𝐺 ) ) = ( ( coeff ‘ 𝐹 ) ∘f − ( coeff ‘ 𝐺 ) ) )
31 30 fveq1d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( ( coeff ‘ ( 𝐹 ∘f − 𝐺 ) ) ‘ 𝑁 ) = ( ( ( coeff ‘ 𝐹 ) ∘f − ( coeff ‘ 𝐺 ) ) ‘ 𝑁 ) )
32 2 nnnn0d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
33 26 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
34 33 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
35 34 ffnd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( coeff ‘ 𝐹 ) Fn ℕ0 )
36 27 coef3 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑇 ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ )
37 36 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ )
38 37 ffnd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( coeff ‘ 𝐺 ) Fn ℕ0 )
39 nn0ex ⊢ ℕ0 ∈ V
40 39 a1i ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ℕ0 ∈ V )
41 inidm ⊢ ( ℕ0 ∩ ℕ0 ) = ℕ0
42 simplr3 ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) )
43 eqidd ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) )
44 35 38 40 40 41 42 43 ofval ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( coeff ‘ 𝐹 ) ∘f − ( coeff ‘ 𝐺 ) ) ‘ 𝑁 ) = ( ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) − ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) )
45 32 44 mpdan ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( ( ( coeff ‘ 𝐹 ) ∘f − ( coeff ‘ 𝐺 ) ) ‘ 𝑁 ) = ( ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) − ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) )
46 37 32 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ∈ ℂ )
47 46 subidd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) − ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) = 0 )
48 31 45 47 3eqtrd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( ( coeff ‘ ( 𝐹 ∘f − 𝐺 ) ) ‘ 𝑁 ) = 0 )
49 plysubcl ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ) → ( 𝐹 ∘f − 𝐺 ) ∈ ( Poly ‘ ℂ ) )
50 11 13 49 syl2an ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) → ( 𝐹 ∘f − 𝐺 ) ∈ ( Poly ‘ ℂ ) )
51 50 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( 𝐹 ∘f − 𝐺 ) ∈ ( Poly ‘ ℂ ) )
52 eqid ⊢ ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) = ( deg ‘ ( 𝐹 ∘f − 𝐺 ) )
53 eqid ⊢ ( coeff ‘ ( 𝐹 ∘f − 𝐺 ) ) = ( coeff ‘ ( 𝐹 ∘f − 𝐺 ) )
54 52 53 dgrlt ⊢ ( ( ( 𝐹 ∘f − 𝐺 ) ∈ ( Poly ‘ ℂ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐹 ∘f − 𝐺 ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) < 𝑁 ) ↔ ( ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) ≤ 𝑁 ∧ ( ( coeff ‘ ( 𝐹 ∘f − 𝐺 ) ) ‘ 𝑁 ) = 0 ) ) )
55 51 32 54 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( ( ( 𝐹 ∘f − 𝐺 ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) < 𝑁 ) ↔ ( ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) ≤ 𝑁 ∧ ( ( coeff ‘ ( 𝐹 ∘f − 𝐺 ) ) ‘ 𝑁 ) = 0 ) ) )
56 25 48 55 mpbir2and ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( ( 𝐹 ∘f − 𝐺 ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) < 𝑁 ) )
57 56 ord ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( ¬ ( 𝐹 ∘f − 𝐺 ) = 0𝑝 → ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) < 𝑁 ) )
58 9 57 pm2.61d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑇 ) ) ∧ ( ( deg ‘ 𝐺 ) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑁 ) ) ) → ( deg ‘ ( 𝐹 ∘f − 𝐺 ) ) < 𝑁 )