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 = X^{p} -_{f} (ℂ \times \{A\})$
	plyrem.2	$⊢ R = F -_{f} (G \times_{f} (F quot G))$
Assertion	plyrem	$⊢ (F \in Poly (S) \land A \in ℂ) \to R = ℂ \times \{F (A)\}$

Proof

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

Metamath Proof Explorer

Theorem plyrem

Proof