plymulx0

Description: Coefficients of a polynomial multiplied by Xp . (Contributed by Thierry Arnoux, 25-Sep-2018)

		Ref	Expression
	Assertion	plymulx0	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F \times_{f} X^{p}) = (n \in ℕ_{0} ⟼ if (n = 0, 0, coeff (F) (n - 1)))$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to F \in Poly (ℝ)$
2		ax-resscn	$⊢ ℝ \subseteq ℂ$
3		1re	$⊢ 1 \in ℝ$
4		plyid	$⊢ (ℝ \subseteq ℂ \land 1 \in ℝ) \to X^{p} \in Poly (ℝ)$
5	2 3 4	mp2an	$⊢ X^{p} \in Poly (ℝ)$
6	5	a1i	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to X^{p} \in Poly (ℝ)$
7		simprl	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℝ \land y \in ℝ)) \to x \in ℝ$
8		simprr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℝ \land y \in ℝ)) \to y \in ℝ$
9	7 8	readdcld	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℝ \land y \in ℝ)) \to x + y \in ℝ$
10	7 8	remulcld	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℝ \land y \in ℝ)) \to x y \in ℝ$
11	1 6 9 10	plymul	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to F \times_{f} X^{p} \in Poly (ℝ)$
12		0re	$⊢ 0 \in ℝ$
13		eqid	$⊢ coeff (F \times_{f} X^{p}) = coeff (F \times_{f} X^{p})$
14	13	coef2	$⊢ (F \times_{f} X^{p} \in Poly (ℝ) \land 0 \in ℝ) \to coeff (F \times_{f} X^{p}) : ℕ_{0} ⟶ ℝ$
15	11 12 14	sylancl	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F \times_{f} X^{p}) : ℕ_{0} ⟶ ℝ$
16	15	feqmptd	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F \times_{f} X^{p}) = (n \in ℕ_{0} ⟼ coeff (F \times_{f} X^{p}) (n))$
17		cnex	$⊢ ℂ \in V$
18	17	a1i	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to ℂ \in V$
19		plyf	$⊢ F \in Poly (ℝ) \to F : ℂ ⟶ ℂ$
20	1 19	syl	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to F : ℂ ⟶ ℂ$
21		plyf	$⊢ X^{p} \in Poly (ℝ) \to X^{p} : ℂ ⟶ ℂ$
22	5 21	ax-mp	$⊢ X^{p} : ℂ ⟶ ℂ$
23	22	a1i	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to X^{p} : ℂ ⟶ ℂ$
24		simprl	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℂ \land y \in ℂ)) \to x \in ℂ$
25		simprr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℂ \land y \in ℂ)) \to y \in ℂ$
26	24 25	mulcomd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℂ \land y \in ℂ)) \to x y = y x$
27	18 20 23 26	caofcom	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to F \times_{f} X^{p} = X^{p} \times_{f} F$
28	27	fveq2d	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F \times_{f} X^{p}) = coeff (X^{p} \times_{f} F)$
29	28	fveq1d	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F \times_{f} X^{p}) (n) = coeff (X^{p} \times_{f} F) (n)$
30	29	adantr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to coeff (F \times_{f} X^{p}) (n) = coeff (X^{p} \times_{f} F) (n)$
31	5	a1i	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to X^{p} \in Poly (ℝ)$
32	1	adantr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to F \in Poly (ℝ)$
33		simpr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
34		eqid	$⊢ coeff (X^{p}) = coeff (X^{p})$
35		eqid	$⊢ coeff (F) = coeff (F)$
36	34 35	coemul	$⊢ (X^{p} \in Poly (ℝ) \land F \in Poly (ℝ) \land n \in ℕ_{0}) \to coeff (X^{p} \times_{f} F) (n) = \sum_{i = 0}^{n} coeff (X^{p}) (i) coeff (F) (n - i)$
37	31 32 33 36	syl3anc	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to coeff (X^{p} \times_{f} F) (n) = \sum_{i = 0}^{n} coeff (X^{p}) (i) coeff (F) (n - i)$
38		elfznn0	$⊢ i \in (0 \dots n) \to i \in ℕ_{0}$
39		coeidp	$⊢ i \in ℕ_{0} \to coeff (X^{p}) (i) = if (i = 1, 1, 0)$
40	38 39	syl	$⊢ i \in (0 \dots n) \to coeff (X^{p}) (i) = if (i = 1, 1, 0)$
41	40	oveq1d	$⊢ i \in (0 \dots n) \to coeff (X^{p}) (i) coeff (F) (n - i) = if (i = 1, 1, 0) coeff (F) (n - i)$
42		ovif	$⊢ if (i = 1, 1, 0) coeff (F) (n - i) = if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i))$
43	41 42	eqtrdi	$⊢ i \in (0 \dots n) \to coeff (X^{p}) (i) coeff (F) (n - i) = if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i))$
44	43	adantl	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to coeff (X^{p}) (i) coeff (F) (n - i) = if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i))$
45	44	sumeq2dv	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to \sum_{i = 0}^{n} coeff (X^{p}) (i) coeff (F) (n - i) = \sum_{i = 0}^{n} if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i))$
46		velsn	$⊢ i \in \{1\} \leftrightarrow i = 1$
47	46	bicomi	$⊢ i = 1 \leftrightarrow i \in \{1\}$
48	47	a1i	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to (i = 1 \leftrightarrow i \in \{1\})$
49	35	coef2	$⊢ (F \in Poly (ℝ) \land 0 \in ℝ) \to coeff (F) : ℕ_{0} ⟶ ℝ$
50	1 12 49	sylancl	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F) : ℕ_{0} ⟶ ℝ$
51	50	ad2antrr	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to coeff (F) : ℕ_{0} ⟶ ℝ$
52		fznn0sub	$⊢ i \in (0 \dots n) \to n - i \in ℕ_{0}$
53	52	adantl	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to n - i \in ℕ_{0}$
54	51 53	ffvelrnd	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to coeff (F) (n - i) \in ℝ$
55	54	recnd	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to coeff (F) (n - i) \in ℂ$
56	55	mulid2d	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to 1 coeff (F) (n - i) = coeff (F) (n - i)$
57	55	mul02d	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to 0 \cdot coeff (F) (n - i) = 0$
58	48 56 57	ifbieq12d	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i)) = if (i \in \{1\}, coeff (F) (n - i), 0)$
59	58	sumeq2dv	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to \sum_{i = 0}^{n} if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i)) = \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0)$
60		eqeq2	$⊢ 0 = if (n = 0, 0, coeff (F) (n - 1)) \to (\sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = 0 \leftrightarrow \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = if (n = 0, 0, coeff (F) (n - 1)))$
61		eqeq2	$⊢ coeff (F) (n - 1) = if (n = 0, 0, coeff (F) (n - 1)) \to (\sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = coeff (F) (n - 1) \leftrightarrow \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = if (n = 0, 0, coeff (F) (n - 1)))$
62		oveq2	$⊢ n = 0 \to (0 \dots n) = (0 \dots 0)$
63		0z	$⊢ 0 \in ℤ$
64		fzsn	$⊢ 0 \in ℤ \to (0 \dots 0) = \{0\}$
65	63 64	ax-mp	$⊢ (0 \dots 0) = \{0\}$
66	62 65	eqtrdi	$⊢ n = 0 \to (0 \dots n) = \{0\}$
67		elsni	$⊢ i \in \{0\} \to i = 0$
68	67	adantl	$⊢ (n = 0 \land i \in \{0\}) \to i = 0$
69		ax-1ne0	$⊢ 1 \neq 0$
70	69	nesymi	$⊢ \neg 0 = 1$
71		eqeq1	$⊢ i = 0 \to (i = 1 \leftrightarrow 0 = 1)$
72	70 71	mtbiri	$⊢ i = 0 \to \neg i = 1$
73	68 72	syl	$⊢ (n = 0 \land i \in \{0\}) \to \neg i = 1$
74	47	notbii	$⊢ \neg i = 1 \leftrightarrow \neg i \in \{1\}$
75	74	biimpi	$⊢ \neg i = 1 \to \neg i \in \{1\}$
76		iffalse	$⊢ \neg i \in \{1\} \to if (i \in \{1\}, coeff (F) (n - i), 0) = 0$
77	73 75 76	3syl	$⊢ (n = 0 \land i \in \{0\}) \to if (i \in \{1\}, coeff (F) (n - i), 0) = 0$
78	66 77	sumeq12rdv	$⊢ n = 0 \to \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = \sum_{i \in \{0\}} 0$
79		snfi	$⊢ \{0\} \in Fin$
80	79	olci	$⊢ (\{0\} \subseteq ℤ_{\geq 0} \lor \{0\} \in Fin)$
81		sumz	$⊢ (\{0\} \subseteq ℤ_{\geq 0} \lor \{0\} \in Fin) \to \sum_{i \in \{0\}} 0 = 0$
82	80 81	ax-mp	$⊢ \sum_{i \in \{0\}} 0 = 0$
83	78 82	eqtrdi	$⊢ n = 0 \to \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = 0$
84	83	adantl	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land n = 0) \to \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = 0$
85		simpll	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land \neg n = 0) \to F \in (Poly (ℝ) ∖ \{0_{𝑝}\})$
86	33	adantr	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land \neg n = 0) \to n \in ℕ_{0}$
87		simpr	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land \neg n = 0) \to \neg n = 0$
88	87	neqned	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land \neg n = 0) \to n \neq 0$
89		elnnne0	$⊢ n \in ℕ \leftrightarrow (n \in ℕ_{0} \land n \neq 0)$
90	86 88 89	sylanbrc	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land \neg n = 0) \to n \in ℕ$
91		1nn0	$⊢ 1 \in ℕ_{0}$
92	91	a1i	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to 1 \in ℕ_{0}$
93		simpr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to n \in ℕ$
94	93	nnnn0d	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to n \in ℕ_{0}$
95	93	nnge1d	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to 1 \leq n$
96		elfz2nn0	$⊢ 1 \in (0 \dots n) \leftrightarrow (1 \in ℕ_{0} \land n \in ℕ_{0} \land 1 \leq n)$
97	92 94 95 96	syl3anbrc	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to 1 \in (0 \dots n)$
98	97	snssd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to \{1\} \subseteq (0 \dots n)$
99	50	ad2antrr	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \land i \in \{1\}) \to coeff (F) : ℕ_{0} ⟶ ℝ$
100		oveq2	$⊢ i = 1 \to n - i = n - 1$
101	46 100	sylbi	$⊢ i \in \{1\} \to n - i = n - 1$
102	101	adantl	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \land i \in \{1\}) \to n - i = n - 1$
103		nnm1nn0	$⊢ n \in ℕ \to n - 1 \in ℕ_{0}$
104	103	ad2antlr	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \land i \in \{1\}) \to n - 1 \in ℕ_{0}$
105	102 104	eqeltrd	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \land i \in \{1\}) \to n - i \in ℕ_{0}$
106	99 105	ffvelrnd	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \land i \in \{1\}) \to coeff (F) (n - i) \in ℝ$
107	106	recnd	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \land i \in \{1\}) \to coeff (F) (n - i) \in ℂ$
108	107	ralrimiva	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to \forall i \in \{1\} coeff (F) (n - i) \in ℂ$
109		fzfi	$⊢ (0 \dots n) \in Fin$
110	109	olci	$⊢ ((0 \dots n) \subseteq ℤ_{\geq 0} \lor (0 \dots n) \in Fin)$
111	110	a1i	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to ((0 \dots n) \subseteq ℤ_{\geq 0} \lor (0 \dots n) \in Fin)$
112		sumss2	$⊢ ((\{1\} \subseteq (0 \dots n) \land \forall i \in \{1\} coeff (F) (n - i) \in ℂ) \land ((0 \dots n) \subseteq ℤ_{\geq 0} \lor (0 \dots n) \in Fin)) \to \sum_{i \in \{1\}} coeff (F) (n - i) = \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0)$
113	98 108 111 112	syl21anc	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to \sum_{i \in \{1\}} coeff (F) (n - i) = \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0)$
114	50	adantr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to coeff (F) : ℕ_{0} ⟶ ℝ$
115	103	adantl	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to n - 1 \in ℕ_{0}$
116	114 115	ffvelrnd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to coeff (F) (n - 1) \in ℝ$
117	116	recnd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to coeff (F) (n - 1) \in ℂ$
118	100	fveq2d	$⊢ i = 1 \to coeff (F) (n - i) = coeff (F) (n - 1)$
119	118	sumsn	$⊢ (1 \in ℝ \land coeff (F) (n - 1) \in ℂ) \to \sum_{i \in \{1\}} coeff (F) (n - i) = coeff (F) (n - 1)$
120	3 117 119	sylancr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to \sum_{i \in \{1\}} coeff (F) (n - i) = coeff (F) (n - 1)$
121	113 120	eqtr3d	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = coeff (F) (n - 1)$
122	85 90 121	syl2anc	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land \neg n = 0) \to \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = coeff (F) (n - 1)$
123	60 61 84 122	ifbothda	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = if (n = 0, 0, coeff (F) (n - 1))$
124	59 123	eqtrd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to \sum_{i = 0}^{n} if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i)) = if (n = 0, 0, coeff (F) (n - 1))$
125	37 45 124	3eqtrd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to coeff (X^{p} \times_{f} F) (n) = if (n = 0, 0, coeff (F) (n - 1))$
126	30 125	eqtrd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to coeff (F \times_{f} X^{p}) (n) = if (n = 0, 0, coeff (F) (n - 1))$
127	126	mpteq2dva	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to (n \in ℕ_{0} ⟼ coeff (F \times_{f} X^{p}) (n)) = (n \in ℕ_{0} ⟼ if (n = 0, 0, coeff (F) (n - 1)))$
128	16 127	eqtrd	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F \times_{f} X^{p}) = (n \in ℕ_{0} ⟼ if (n = 0, 0, coeff (F) (n - 1)))$

Metamath Proof Explorer

Theorem plymulx0

Proof