Metamath Proof Explorer

Theorem plyrem

Description: The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout ). If a polynomial F is divided by the linear factor x - A , the remainder is equal to F ( A ) , the evaluation of the polynomial at A (interpreted as a constant polynomial). This is part of Metamath 100 proof #89. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypotheses plyrem.1 
|- G = ( Xp oF - ( CC X. { A } ) )
plyrem.2 
|- R = ( F oF - ( G oF x. ( F quot G ) ) )
Assertion plyrem 
|- ( ( F e. ( Poly ` S ) /\ A e. CC ) -> R = ( CC X. { ( F ` A ) } ) )

Proof

Step Hyp Ref Expression
1 plyrem.1 
 |-  G = ( Xp oF - ( CC X. { A } ) )
2 plyrem.2 
 |-  R = ( F oF - ( G oF x. ( F quot G ) ) )
3 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
4 simpl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> F e. ( Poly ` S ) )
5 3 4 sseldi 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> F e. ( Poly ` CC ) )
6 1 plyremlem 
 |-  ( A e. CC -> ( G e. ( Poly ` CC ) /\ ( deg ` G ) = 1 /\ ( `' G " { 0 } ) = { A } ) )
7 6 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( G e. ( Poly ` CC ) /\ ( deg ` G ) = 1 /\ ( `' G " { 0 } ) = { A } ) )
8 7 simp1d 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> G e. ( Poly ` CC ) )
9 7 simp2d 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( deg ` G ) = 1 )
10 ax-1ne0 
 |-  1 =/= 0
11 10 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> 1 =/= 0 )
12 9 11 eqnetrd 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( deg ` G ) =/= 0 )
13 fveq2 
 |-  ( G = 0p -> ( deg ` G ) = ( deg ` 0p ) )
14 dgr0 
 |-  ( deg ` 0p ) = 0
15 13 14 eqtrdi 
 |-  ( G = 0p -> ( deg ` G ) = 0 )
16 15 necon3i 
 |-  ( ( deg ` G ) =/= 0 -> G =/= 0p )
17 12 16 syl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> G =/= 0p )
18 2 quotdgr 
 |-  ( ( F e. ( Poly ` CC ) /\ G e. ( Poly ` CC ) /\ G =/= 0p ) -> ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) )
19 5 8 17 18 syl3anc 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) )
20 0lt1 
 |-  0 < 1
21 20 9 breqtrrid 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> 0 < ( deg ` G ) )
22 fveq2 
 |-  ( R = 0p -> ( deg ` R ) = ( deg ` 0p ) )
23 22 14 eqtrdi 
 |-  ( R = 0p -> ( deg ` R ) = 0 )
24 23 breq1d 
 |-  ( R = 0p -> ( ( deg ` R ) < ( deg ` G ) <-> 0 < ( deg ` G ) ) )
25 21 24 syl5ibrcom 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( R = 0p -> ( deg ` R ) < ( deg ` G ) ) )
26 pm2.62 
 |-  ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) -> ( ( R = 0p -> ( deg ` R ) < ( deg ` G ) ) -> ( deg ` R ) < ( deg ` G ) ) )
27 19 25 26 sylc 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( deg ` R ) < ( deg ` G ) )
28 27 9 breqtrd 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( deg ` R ) < 1 )
29 quotcl2 
 |-  ( ( F e. ( Poly ` CC ) /\ G e. ( Poly ` CC ) /\ G =/= 0p ) -> ( F quot G ) e. ( Poly ` CC ) )
30 5 8 17 29 syl3anc 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( F quot G ) e. ( Poly ` CC ) )
31 plymulcl 
 |-  ( ( G e. ( Poly ` CC ) /\ ( F quot G ) e. ( Poly ` CC ) ) -> ( G oF x. ( F quot G ) ) e. ( Poly ` CC ) )
32 8 30 31 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( G oF x. ( F quot G ) ) e. ( Poly ` CC ) )
33 plysubcl 
 |-  ( ( F e. ( Poly ` CC ) /\ ( G oF x. ( F quot G ) ) e. ( Poly ` CC ) ) -> ( F oF - ( G oF x. ( F quot G ) ) ) e. ( Poly ` CC ) )
34 5 32 33 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( F oF - ( G oF x. ( F quot G ) ) ) e. ( Poly ` CC ) )
35 2 34 eqeltrid 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> R e. ( Poly ` CC ) )
36 dgrcl 
 |-  ( R e. ( Poly ` CC ) -> ( deg ` R ) e. NN0 )
37 35 36 syl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( deg ` R ) e. NN0 )
38 nn0lt10b 
 |-  ( ( deg ` R ) e. NN0 -> ( ( deg ` R ) < 1 <-> ( deg ` R ) = 0 ) )
39 37 38 syl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( ( deg ` R ) < 1 <-> ( deg ` R ) = 0 ) )
40 28 39 mpbid 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( deg ` R ) = 0 )
41 0dgrb 
 |-  ( R e. ( Poly ` CC ) -> ( ( deg ` R ) = 0 <-> R = ( CC X. { ( R ` 0 ) } ) ) )
42 35 41 syl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( ( deg ` R ) = 0 <-> R = ( CC X. { ( R ` 0 ) } ) ) )
43 40 42 mpbid 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> R = ( CC X. { ( R ` 0 ) } ) )
44 43 fveq1d 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( R ` A ) = ( ( CC X. { ( R ` 0 ) } ) ` A ) )
45 2 fveq1i 
 |-  ( R ` A ) = ( ( F oF - ( G oF x. ( F quot G ) ) ) ` A )
46 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
47 46 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> F : CC --> CC )
48 47 ffnd 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> F Fn CC )
49 plyf 
 |-  ( G e. ( Poly ` CC ) -> G : CC --> CC )
50 8 49 syl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> G : CC --> CC )
51 50 ffnd 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> G Fn CC )
52 plyf 
 |-  ( ( F quot G ) e. ( Poly ` CC ) -> ( F quot G ) : CC --> CC )
53 30 52 syl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( F quot G ) : CC --> CC )
54 53 ffnd 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( F quot G ) Fn CC )
55 cnex 
 |-  CC e. _V
56 55 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> CC e. _V )
57 inidm 
 |-  ( CC i^i CC ) = CC
58 51 54 56 56 57 offn 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( G oF x. ( F quot G ) ) Fn CC )
59 eqidd 
 |-  ( ( ( F e. ( Poly ` S ) /\ A e. CC ) /\ A e. CC ) -> ( F ` A ) = ( F ` A ) )
60 7 simp3d 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( `' G " { 0 } ) = { A } )
61 ssun1 
 |-  ( `' G " { 0 } ) C_ ( ( `' G " { 0 } ) u. ( `' ( F quot G ) " { 0 } ) )
62 60 61 eqsstrrdi 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> { A } C_ ( ( `' G " { 0 } ) u. ( `' ( F quot G ) " { 0 } ) ) )
63 snssg 
 |-  ( A e. CC -> ( A e. ( ( `' G " { 0 } ) u. ( `' ( F quot G ) " { 0 } ) ) <-> { A } C_ ( ( `' G " { 0 } ) u. ( `' ( F quot G ) " { 0 } ) ) ) )
64 63 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( A e. ( ( `' G " { 0 } ) u. ( `' ( F quot G ) " { 0 } ) ) <-> { A } C_ ( ( `' G " { 0 } ) u. ( `' ( F quot G ) " { 0 } ) ) ) )
65 62 64 mpbird 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> A e. ( ( `' G " { 0 } ) u. ( `' ( F quot G ) " { 0 } ) ) )
66 ofmulrt 
 |-  ( ( CC e. _V /\ G : CC --> CC /\ ( F quot G ) : CC --> CC ) -> ( `' ( G oF x. ( F quot G ) ) " { 0 } ) = ( ( `' G " { 0 } ) u. ( `' ( F quot G ) " { 0 } ) ) )
67 56 50 53 66 syl3anc 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( `' ( G oF x. ( F quot G ) ) " { 0 } ) = ( ( `' G " { 0 } ) u. ( `' ( F quot G ) " { 0 } ) ) )
68 65 67 eleqtrrd 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> A e. ( `' ( G oF x. ( F quot G ) ) " { 0 } ) )
69 fniniseg 
 |-  ( ( G oF x. ( F quot G ) ) Fn CC -> ( A e. ( `' ( G oF x. ( F quot G ) ) " { 0 } ) <-> ( A e. CC /\ ( ( G oF x. ( F quot G ) ) ` A ) = 0 ) ) )
70 58 69 syl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( A e. ( `' ( G oF x. ( F quot G ) ) " { 0 } ) <-> ( A e. CC /\ ( ( G oF x. ( F quot G ) ) ` A ) = 0 ) ) )
71 68 70 mpbid 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( A e. CC /\ ( ( G oF x. ( F quot G ) ) ` A ) = 0 ) )
72 71 simprd 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( ( G oF x. ( F quot G ) ) ` A ) = 0 )
73 72 adantr 
 |-  ( ( ( F e. ( Poly ` S ) /\ A e. CC ) /\ A e. CC ) -> ( ( G oF x. ( F quot G ) ) ` A ) = 0 )
74 48 58 56 56 57 59 73 ofval 
 |-  ( ( ( F e. ( Poly ` S ) /\ A e. CC ) /\ A e. CC ) -> ( ( F oF - ( G oF x. ( F quot G ) ) ) ` A ) = ( ( F ` A ) - 0 ) )
75 74 anabss3 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( ( F oF - ( G oF x. ( F quot G ) ) ) ` A ) = ( ( F ` A ) - 0 ) )
76 45 75 syl5eq 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( R ` A ) = ( ( F ` A ) - 0 ) )
77 46 ffvelrnda 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( F ` A ) e. CC )
78 77 subid1d 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( ( F ` A ) - 0 ) = ( F ` A ) )
79 76 78 eqtrd 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( R ` A ) = ( F ` A ) )
80 fvex 
 |-  ( R ` 0 ) e. _V
81 80 fvconst2 
 |-  ( A e. CC -> ( ( CC X. { ( R ` 0 ) } ) ` A ) = ( R ` 0 ) )
82 81 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( ( CC X. { ( R ` 0 ) } ) ` A ) = ( R ` 0 ) )
83 44 79 82 3eqtr3d 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( F ` A ) = ( R ` 0 ) )
84 83 sneqd 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> { ( F ` A ) } = { ( R ` 0 ) } )
85 84 xpeq2d 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( CC X. { ( F ` A ) } ) = ( CC X. { ( R ` 0 ) } ) )
86 43 85 eqtr4d 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> R = ( CC X. { ( F ` A ) } ) )