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 ⊢ 𝐺 = ( Xp ∘f − ( ℂ × { 𝐴 } ) )
plyrem.2 ⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) )
Assertion plyrem ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝑅 = ( ℂ × { ( 𝐹 ‘ 𝐴 ) } ) )

Proof

Step Hyp Ref Expression
1 plyrem.1 ⊢ 𝐺 = ( Xp ∘f − ( ℂ × { 𝐴 } ) )
2 plyrem.2 ⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) )
3 plyssc ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
4 simpl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
5 3 4 sselid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
6 1 plyremlem ⊢ ( 𝐴 ∈ ℂ → ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝐺 ) = 1 ∧ ( ◡ 𝐺 “ { 0 } ) = { 𝐴 } ) )
7 6 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝐺 ) = 1 ∧ ( ◡ 𝐺 “ { 0 } ) = { 𝐴 } ) )
8 7 simp1d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝐺 ∈ ( Poly ‘ ℂ ) )
9 7 simp2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( deg ‘ 𝐺 ) = 1 )
10 ax-1ne0 ⊢ 1 ≠ 0
11 10 a1i ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 1 ≠ 0 )
12 9 11 eqnetrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( deg ‘ 𝐺 ) ≠ 0 )
13 fveq2 ⊢ ( 𝐺 = 0𝑝 → ( deg ‘ 𝐺 ) = ( deg ‘ 0𝑝 ) )
14 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
15 13 14 eqtrdi ⊢ ( 𝐺 = 0𝑝 → ( deg ‘ 𝐺 ) = 0 )
16 15 necon3i ⊢ ( ( deg ‘ 𝐺 ) ≠ 0 → 𝐺 ≠ 0𝑝 )
17 12 16 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝐺 ≠ 0𝑝 )
18 2 quotdgr ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) )
19 5 8 17 18 syl3anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) )
20 0lt1 ⊢ 0 < 1
21 20 9 breqtrrid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 0 < ( deg ‘ 𝐺 ) )
22 fveq2 ⊢ ( 𝑅 = 0𝑝 → ( deg ‘ 𝑅 ) = ( deg ‘ 0𝑝 ) )
23 22 14 eqtrdi ⊢ ( 𝑅 = 0𝑝 → ( deg ‘ 𝑅 ) = 0 )
24 23 breq1d ⊢ ( 𝑅 = 0𝑝 → ( ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ↔ 0 < ( deg ‘ 𝐺 ) ) )
25 21 24 syl5ibrcom ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝑅 = 0𝑝 → ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) )
26 pm2.62 ⊢ ( ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) → ( ( 𝑅 = 0𝑝 → ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) → ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) )
27 19 25 26 sylc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) )
28 27 9 breqtrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( deg ‘ 𝑅 ) < 1 )
29 quotcl2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 quot 𝐺 ) ∈ ( Poly ‘ ℂ ) )
30 5 8 17 29 syl3anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐹 quot 𝐺 ) ∈ ( Poly ‘ ℂ ) )
31 plymulcl ⊢ ( ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ ( 𝐹 quot 𝐺 ) ∈ ( Poly ‘ ℂ ) ) → ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) )
32 8 30 31 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) )
33 plysubcl ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) ) → ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) ∈ ( Poly ‘ ℂ ) )
34 5 32 33 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) ∈ ( Poly ‘ ℂ ) )
35 2 34 eqeltrid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝑅 ∈ ( Poly ‘ ℂ ) )
36 dgrcl ⊢ ( 𝑅 ∈ ( Poly ‘ ℂ ) → ( deg ‘ 𝑅 ) ∈ ℕ0 )
37 35 36 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( deg ‘ 𝑅 ) ∈ ℕ0 )
38 nn0lt10b ⊢ ( ( deg ‘ 𝑅 ) ∈ ℕ0 → ( ( deg ‘ 𝑅 ) < 1 ↔ ( deg ‘ 𝑅 ) = 0 ) )
39 37 38 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( ( deg ‘ 𝑅 ) < 1 ↔ ( deg ‘ 𝑅 ) = 0 ) )
40 28 39 mpbid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( deg ‘ 𝑅 ) = 0 )
41 0dgrb ⊢ ( 𝑅 ∈ ( Poly ‘ ℂ ) → ( ( deg ‘ 𝑅 ) = 0 ↔ 𝑅 = ( ℂ × { ( 𝑅 ‘ 0 ) } ) ) )
42 35 41 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( ( deg ‘ 𝑅 ) = 0 ↔ 𝑅 = ( ℂ × { ( 𝑅 ‘ 0 ) } ) ) )
43 40 42 mpbid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝑅 = ( ℂ × { ( 𝑅 ‘ 0 ) } ) )
44 43 fveq1d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝑅 ‘ 𝐴 ) = ( ( ℂ × { ( 𝑅 ‘ 0 ) } ) ‘ 𝐴 ) )
45 2 fveq1i ⊢ ( 𝑅 ‘ 𝐴 ) = ( ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) ‘ 𝐴 )
46 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
47 46 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝐹 : ℂ ⟶ ℂ )
48 47 ffnd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝐹 Fn ℂ )
49 plyf ⊢ ( 𝐺 ∈ ( Poly ‘ ℂ ) → 𝐺 : ℂ ⟶ ℂ )
50 8 49 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝐺 : ℂ ⟶ ℂ )
51 50 ffnd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝐺 Fn ℂ )
52 plyf ⊢ ( ( 𝐹 quot 𝐺 ) ∈ ( Poly ‘ ℂ ) → ( 𝐹 quot 𝐺 ) : ℂ ⟶ ℂ )
53 30 52 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐹 quot 𝐺 ) : ℂ ⟶ ℂ )
54 53 ffnd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐹 quot 𝐺 ) Fn ℂ )
55 cnex ⊢ ℂ ∈ V
56 55 a1i ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ℂ ∈ V )
57 inidm ⊢ ( ℂ ∩ ℂ ) = ℂ
58 51 54 56 56 57 offn ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) Fn ℂ )
59 eqidd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) ∧ 𝐴 ∈ ℂ ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
60 7 simp3d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( ◡ 𝐺 “ { 0 } ) = { 𝐴 } )
61 ssun1 ⊢ ( ◡ 𝐺 “ { 0 } ) ⊆ ( ( ◡ 𝐺 “ { 0 } ) ∪ ( ◡ ( 𝐹 quot 𝐺 ) “ { 0 } ) )
62 60 61 eqsstrrdi ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → { 𝐴 } ⊆ ( ( ◡ 𝐺 “ { 0 } ) ∪ ( ◡ ( 𝐹 quot 𝐺 ) “ { 0 } ) ) )
63 snssg ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ( ( ◡ 𝐺 “ { 0 } ) ∪ ( ◡ ( 𝐹 quot 𝐺 ) “ { 0 } ) ) ↔ { 𝐴 } ⊆ ( ( ◡ 𝐺 “ { 0 } ) ∪ ( ◡ ( 𝐹 quot 𝐺 ) “ { 0 } ) ) ) )
64 63 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐴 ∈ ( ( ◡ 𝐺 “ { 0 } ) ∪ ( ◡ ( 𝐹 quot 𝐺 ) “ { 0 } ) ) ↔ { 𝐴 } ⊆ ( ( ◡ 𝐺 “ { 0 } ) ∪ ( ◡ ( 𝐹 quot 𝐺 ) “ { 0 } ) ) ) )
65 62 64 mpbird ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝐴 ∈ ( ( ◡ 𝐺 “ { 0 } ) ∪ ( ◡ ( 𝐹 quot 𝐺 ) “ { 0 } ) ) )
66 ofmulrt ⊢ ( ( ℂ ∈ V ∧ 𝐺 : ℂ ⟶ ℂ ∧ ( 𝐹 quot 𝐺 ) : ℂ ⟶ ℂ ) → ( ◡ ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) “ { 0 } ) = ( ( ◡ 𝐺 “ { 0 } ) ∪ ( ◡ ( 𝐹 quot 𝐺 ) “ { 0 } ) ) )
67 56 50 53 66 syl3anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( ◡ ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) “ { 0 } ) = ( ( ◡ 𝐺 “ { 0 } ) ∪ ( ◡ ( 𝐹 quot 𝐺 ) “ { 0 } ) ) )
68 65 67 eleqtrrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝐴 ∈ ( ◡ ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) “ { 0 } ) )
69 fniniseg ⊢ ( ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) Fn ℂ → ( 𝐴 ∈ ( ◡ ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ‘ 𝐴 ) = 0 ) ) )
70 58 69 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐴 ∈ ( ◡ ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ‘ 𝐴 ) = 0 ) ) )
71 68 70 mpbid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐴 ∈ ℂ ∧ ( ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ‘ 𝐴 ) = 0 ) )
72 71 simprd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ‘ 𝐴 ) = 0 )
73 72 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ‘ 𝐴 ) = 0 )
74 48 58 56 56 57 59 73 ofval ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) ‘ 𝐴 ) = ( ( 𝐹 ‘ 𝐴 ) − 0 ) )
75 74 anabss3 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) ‘ 𝐴 ) = ( ( 𝐹 ‘ 𝐴 ) − 0 ) )
76 45 75 syl5eq ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝑅 ‘ 𝐴 ) = ( ( 𝐹 ‘ 𝐴 ) − 0 ) )
77 46 ffvelrnda ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
78 77 subid1d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝐹 ‘ 𝐴 ) − 0 ) = ( 𝐹 ‘ 𝐴 ) )
79 76 78 eqtrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝑅 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
80 fvex ⊢ ( 𝑅 ‘ 0 ) ∈ V
81 80 fvconst2 ⊢ ( 𝐴 ∈ ℂ → ( ( ℂ × { ( 𝑅 ‘ 0 ) } ) ‘ 𝐴 ) = ( 𝑅 ‘ 0 ) )
82 81 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( ( ℂ × { ( 𝑅 ‘ 0 ) } ) ‘ 𝐴 ) = ( 𝑅 ‘ 0 ) )
83 44 79 82 3eqtr3d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐹 ‘ 𝐴 ) = ( 𝑅 ‘ 0 ) )
84 83 sneqd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → { ( 𝐹 ‘ 𝐴 ) } = { ( 𝑅 ‘ 0 ) } )
85 84 xpeq2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( ℂ × { ( 𝐹 ‘ 𝐴 ) } ) = ( ℂ × { ( 𝑅 ‘ 0 ) } ) )
86 43 85 eqtr4d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝑅 = ( ℂ × { ( 𝐹 ‘ 𝐴 ) } ) )