bpolycl

Description: Closure law for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014) (Proof shortened by Mario Carneiro, 22-May-2014)

		Ref	Expression
	Assertion	bpolycl	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N BernPoly X \in ℂ$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ n = k \to n BernPoly X = k BernPoly X$
2	1	eleq1d	$⊢ n = k \to (n BernPoly X \in ℂ \leftrightarrow k BernPoly X \in ℂ)$
3	2	imbi2d	$⊢ n = k \to ((X \in ℂ \to n BernPoly X \in ℂ) \leftrightarrow (X \in ℂ \to k BernPoly X \in ℂ))$
4		oveq1	$⊢ n = N \to n BernPoly X = N BernPoly X$
5	4	eleq1d	$⊢ n = N \to (n BernPoly X \in ℂ \leftrightarrow N BernPoly X \in ℂ)$
6	5	imbi2d	$⊢ n = N \to ((X \in ℂ \to n BernPoly X \in ℂ) \leftrightarrow (X \in ℂ \to N BernPoly X \in ℂ))$
7		r19.21v	$⊢ \forall k \in (0 \dots n - 1) (X \in ℂ \to k BernPoly X \in ℂ) \leftrightarrow (X \in ℂ \to \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ)$
8		bpolyval	$⊢ (n \in ℕ_{0} \land X \in ℂ) \to n BernPoly X = X^{n} - \sum_{m = 0}^{n - 1} (\binom{n}{m}) (\frac{m BernPoly X}{n - m + 1})$
9	8	3adant3	$⊢ (n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to n BernPoly X = X^{n} - \sum_{m = 0}^{n - 1} (\binom{n}{m}) (\frac{m BernPoly X}{n - m + 1})$
10		simp2	$⊢ (n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to X \in ℂ$
11		simp1	$⊢ (n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to n \in ℕ_{0}$
12	10 11	expcld	$⊢ (n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to X^{n} \in ℂ$
13		fzfid	$⊢ (n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to (0 \dots n - 1) \in Fin$
14		elfzelz	$⊢ m \in (0 \dots n - 1) \to m \in ℤ$
15		bccl	$⊢ (n \in ℕ_{0} \land m \in ℤ) \to (\binom{n}{m}) \in ℕ_{0}$
16	11 14 15	syl2an	$⊢ ((n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \land m \in (0 \dots n - 1)) \to (\binom{n}{m}) \in ℕ_{0}$
17	16	nn0cnd	$⊢ ((n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \land m \in (0 \dots n - 1)) \to (\binom{n}{m}) \in ℂ$
18		oveq1	$⊢ k = m \to k BernPoly X = m BernPoly X$
19	18	eleq1d	$⊢ k = m \to (k BernPoly X \in ℂ \leftrightarrow m BernPoly X \in ℂ)$
20	19	rspccva	$⊢ (\forall k \in (0 \dots n - 1) k BernPoly X \in ℂ \land m \in (0 \dots n - 1)) \to m BernPoly X \in ℂ$
21	20	3ad2antl3	$⊢ ((n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \land m \in (0 \dots n - 1)) \to m BernPoly X \in ℂ$
22		fzssp1	$⊢ (0 \dots n - 1) \subseteq (0 \dots n - 1 + 1)$
23	11	nn0cnd	$⊢ (n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to n \in ℂ$
24		ax-1cn	$⊢ 1 \in ℂ$
25		npcan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n - 1 + 1 = n$
26	23 24 25	sylancl	$⊢ (n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to n - 1 + 1 = n$
27	26	oveq2d	$⊢ (n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to (0 \dots n - 1 + 1) = (0 \dots n)$
28	22 27	sseqtrid	$⊢ (n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to (0 \dots n - 1) \subseteq (0 \dots n)$
29	28	sselda	$⊢ ((n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \land m \in (0 \dots n - 1)) \to m \in (0 \dots n)$
30		fznn0sub	$⊢ m \in (0 \dots n) \to n - m \in ℕ_{0}$
31		nn0p1nn	$⊢ n - m \in ℕ_{0} \to n - m + 1 \in ℕ$
32	29 30 31	3syl	$⊢ ((n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \land m \in (0 \dots n - 1)) \to n - m + 1 \in ℕ$
33	32	nncnd	$⊢ ((n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \land m \in (0 \dots n - 1)) \to n - m + 1 \in ℂ$
34	32	nnne0d	$⊢ ((n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \land m \in (0 \dots n - 1)) \to n - m + 1 \neq 0$
35	21 33 34	divcld	$⊢ ((n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \land m \in (0 \dots n - 1)) \to \frac{m BernPoly X}{n - m + 1} \in ℂ$
36	17 35	mulcld	$⊢ ((n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \land m \in (0 \dots n - 1)) \to (\binom{n}{m}) (\frac{m BernPoly X}{n - m + 1}) \in ℂ$
37	13 36	fsumcl	$⊢ (n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to \sum_{m = 0}^{n - 1} (\binom{n}{m}) (\frac{m BernPoly X}{n - m + 1}) \in ℂ$
38	12 37	subcld	$⊢ (n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to X^{n} - \sum_{m = 0}^{n - 1} (\binom{n}{m}) (\frac{m BernPoly X}{n - m + 1}) \in ℂ$
39	9 38	eqeltrd	$⊢ (n \in ℕ_{0} \land X \in ℂ \land \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to n BernPoly X \in ℂ$
40	39	3exp	$⊢ n \in ℕ_{0} \to (X \in ℂ \to (\forall k \in (0 \dots n - 1) k BernPoly X \in ℂ \to n BernPoly X \in ℂ))$
41	40	a2d	$⊢ n \in ℕ_{0} \to ((X \in ℂ \to \forall k \in (0 \dots n - 1) k BernPoly X \in ℂ) \to (X \in ℂ \to n BernPoly X \in ℂ))$
42	7 41	biimtrid	$⊢ n \in ℕ_{0} \to (\forall k \in (0 \dots n - 1) (X \in ℂ \to k BernPoly X \in ℂ) \to (X \in ℂ \to n BernPoly X \in ℂ))$
43	3 6 42	nn0sinds	$⊢ N \in ℕ_{0} \to (X \in ℂ \to N BernPoly X \in ℂ)$
44	43	imp	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N BernPoly X \in ℂ$

Metamath Proof Explorer

Theorem bpolycl

Proof