ply1termlem

		Ref	Expression
	Hypothesis	ply1term.1	$⊢ F = (z \in ℂ ⟼ A z^{N})$
	Assertion	ply1termlem	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} if (k = N, A, 0) z^{k})$

Proof

Step	Hyp	Ref	Expression
1		ply1term.1	$⊢ F = (z \in ℂ ⟼ A z^{N})$
2		simplr	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \to N \in ℕ_{0}$
3		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
4	2 3	eleqtrdi	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \to N \in ℤ_{\geq 0}$
5		fzss1	$⊢ N \in ℤ_{\geq 0} \to (N \dots N) \subseteq (0 \dots N)$
6	4 5	syl	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \to (N \dots N) \subseteq (0 \dots N)$
7		elfz1eq	$⊢ k \in (N \dots N) \to k = N$
8	7	adantl	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in (N \dots N)) \to k = N$
9		iftrue	$⊢ k = N \to if (k = N, A, 0) = A$
10	8 9	syl	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in (N \dots N)) \to if (k = N, A, 0) = A$
11		simpll	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \to A \in ℂ$
12	11	adantr	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in (N \dots N)) \to A \in ℂ$
13	10 12	eqeltrd	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in (N \dots N)) \to if (k = N, A, 0) \in ℂ$
14		simplr	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in (N \dots N)) \to z \in ℂ$
15	2	adantr	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in (N \dots N)) \to N \in ℕ_{0}$
16	8 15	eqeltrd	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in (N \dots N)) \to k \in ℕ_{0}$
17	14 16	expcld	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in (N \dots N)) \to z^{k} \in ℂ$
18	13 17	mulcld	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in (N \dots N)) \to if (k = N, A, 0) z^{k} \in ℂ$
19		eldifn	$⊢ k \in ((0 \dots N) ∖ (N \dots N)) \to \neg k \in (N \dots N)$
20	19	adantl	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in ((0 \dots N) ∖ (N \dots N))) \to \neg k \in (N \dots N)$
21	2	adantr	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in ((0 \dots N) ∖ (N \dots N))) \to N \in ℕ_{0}$
22	21	nn0zd	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in ((0 \dots N) ∖ (N \dots N))) \to N \in ℤ$
23		fzsn	$⊢ N \in ℤ \to (N \dots N) = \{N\}$
24	23	eleq2d	$⊢ N \in ℤ \to (k \in (N \dots N) \leftrightarrow k \in \{N\})$
25		elsn2g	$⊢ N \in ℤ \to (k \in \{N\} \leftrightarrow k = N)$
26	24 25	bitrd	$⊢ N \in ℤ \to (k \in (N \dots N) \leftrightarrow k = N)$
27	22 26	syl	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in ((0 \dots N) ∖ (N \dots N))) \to (k \in (N \dots N) \leftrightarrow k = N)$
28	20 27	mtbid	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in ((0 \dots N) ∖ (N \dots N))) \to \neg k = N$
29	28	iffalsed	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in ((0 \dots N) ∖ (N \dots N))) \to if (k = N, A, 0) = 0$
30	29	oveq1d	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in ((0 \dots N) ∖ (N \dots N))) \to if (k = N, A, 0) z^{k} = 0 \cdot z^{k}$
31		simpr	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \to z \in ℂ$
32		eldifi	$⊢ k \in ((0 \dots N) ∖ (N \dots N)) \to k \in (0 \dots N)$
33		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
34	32 33	syl	$⊢ k \in ((0 \dots N) ∖ (N \dots N)) \to k \in ℕ_{0}$
35		expcl	$⊢ (z \in ℂ \land k \in ℕ_{0}) \to z^{k} \in ℂ$
36	31 34 35	syl2an	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in ((0 \dots N) ∖ (N \dots N))) \to z^{k} \in ℂ$
37	36	mul02d	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in ((0 \dots N) ∖ (N \dots N))) \to 0 \cdot z^{k} = 0$
38	30 37	eqtrd	$⊢ (((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \land k \in ((0 \dots N) ∖ (N \dots N))) \to if (k = N, A, 0) z^{k} = 0$
39		fzfid	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \to (0 \dots N) \in Fin$
40	6 18 38 39	fsumss	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \to \sum_{k = N}^{N} if (k = N, A, 0) z^{k} = \sum_{k = 0}^{N} if (k = N, A, 0) z^{k}$
41	2	nn0zd	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \to N \in ℤ$
42	31 2	expcld	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \to z^{N} \in ℂ$
43	11 42	mulcld	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \to A z^{N} \in ℂ$
44		oveq2	$⊢ k = N \to z^{k} = z^{N}$
45	9 44	oveq12d	$⊢ k = N \to if (k = N, A, 0) z^{k} = A z^{N}$
46	45	fsum1	$⊢ (N \in ℤ \land A z^{N} \in ℂ) \to \sum_{k = N}^{N} if (k = N, A, 0) z^{k} = A z^{N}$
47	41 43 46	syl2anc	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \to \sum_{k = N}^{N} if (k = N, A, 0) z^{k} = A z^{N}$
48	40 47	eqtr3d	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land z \in ℂ) \to \sum_{k = 0}^{N} if (k = N, A, 0) z^{k} = A z^{N}$
49	48	mpteq2dva	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (z \in ℂ ⟼ \sum_{k = 0}^{N} if (k = N, A, 0) z^{k}) = (z \in ℂ ⟼ A z^{N})$
50	1 49	eqtr4id	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} if (k = N, A, 0) z^{k})$

Metamath Proof Explorer

Theorem ply1termlem

Proof