Metamath Proof Explorer

Theorem quotdgr

Description: Remainder property of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis quotdgr.1 
|- R = ( F oF - ( G oF x. ( F quot G ) ) )
Assertion quotdgr 
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) )

Proof

Step Hyp Ref Expression
1 quotdgr.1 
 |-  R = ( F oF - ( G oF x. ( F quot G ) ) )
2 addcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
3 2 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) /\ ( x e. CC /\ y e. CC ) ) -> ( x + y ) e. CC )
4 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
5 4 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) e. CC )
6 reccl 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( 1 / x ) e. CC )
7 6 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) /\ ( x e. CC /\ x =/= 0 ) ) -> ( 1 / x ) e. CC )
8 neg1cn 
 |-  -u 1 e. CC
9 8 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> -u 1 e. CC )
10 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
11 simp1 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> F e. ( Poly ` S ) )
12 10 11 sselid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> F e. ( Poly ` CC ) )
13 simp2 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> G e. ( Poly ` S ) )
14 10 13 sselid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> G e. ( Poly ` CC ) )
15 simp3 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> G =/= 0p )
16 3 5 7 9 12 14 15 1 quotlem 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( F quot G ) e. ( Poly ` CC ) /\ ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
17 16 simprd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) )