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	eqtrid	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝑅 ‘ 𝐴 ) = ( ( 𝐹 ‘ 𝐴 ) − 0 ) )
77	46	ffvelcdmda	⊢ ( ( 𝐹 ∈ ( 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 ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → 𝑅 = ( ℂ × { ( 𝐹 ‘ 𝐴 ) } ) )