pwp1fsum - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pwp1fsum		Structured version Visualization version GIF version

Theorem pwp1fsum 16567

Description: The n-th power of a number increased by 1 expressed by a product with a finite sum. (Contributed by AV, 15-Aug-2021.)

**Hypotheses**
Ref	Expression
pwp1fsum.a	⊢ (𝜑 → 𝐴 ∈ ℂ)
pwp1fsum.n	⊢ (𝜑 → 𝑁 ∈ ℕ)

**Assertion**
Ref	Expression
pwp1fsum	⊢ (𝜑 → ((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 1) = ((𝐴 + 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))))

Distinct variable groups: 𝐴,𝑘 𝑘,𝑁 𝜑,𝑘

Proof of Theorem pwp1fsum Dummy variable 𝑙 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pwp1fsum.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		1cnd 11306	. . . 4 ⊢ (𝜑 → 1 ∈ ℂ)
3		fzfid 14120	. . . . 5 ⊢ (𝜑 → (0...(𝑁 − 1)) ∈ Fin)
4		neg1cn 12309	. . . . . . . 8 ⊢ -1 ∈ ℂ
5	4	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → -1 ∈ ℂ)
6		elfznn0 13758	. . . . . . . 8 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ₀)
7	6	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ₀)
8	5, 7	expcld 14293	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ( -1↑𝑘) ∈ ℂ)
9	1	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐴 ∈ ℂ)
10	9, 7	expcld 14293	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ)
11	8, 10	mulcld 11333	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (( -1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ)
12	3, 11	fsumcl 15905	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ)
13	1, 2, 12	adddird 11338	. . 3 ⊢ (𝜑 → ((𝐴 + 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = ((𝐴 · Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) + (1 · Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)))))
14	3, 1, 11	fsummulc2 15956	. . . . 5 ⊢ (𝜑 → (𝐴 · Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴 · (( -1↑𝑘) · (𝐴↑𝑘))))
15	9, 11	mulcomd 11334	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴 · (( -1↑𝑘) · (𝐴↑𝑘))) = ((( -1↑𝑘) · (𝐴↑𝑘)) · 𝐴))
16	8, 10, 9	mulassd 11336	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((( -1↑𝑘) · (𝐴↑𝑘)) · 𝐴) = (( -1↑𝑘) · ((𝐴↑𝑘) · 𝐴)))
17		expp1 14215	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
18	1, 6, 17	syl2an 608	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴))
19	18	eqcomd 2766	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴↑𝑘) · 𝐴) = (𝐴↑(𝑘 + 1)))
20	19	oveq2d 7437	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (( -1↑𝑘) · ((𝐴↑𝑘) · 𝐴)) = (( -1↑𝑘) · (𝐴↑(𝑘 + 1))))
21	15, 16, 20	3eqtrd 2799	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴 · (( -1↑𝑘) · (𝐴↑𝑘))) = (( -1↑𝑘) · (𝐴↑(𝑘 + 1))))
22	21	sumeq2dv 15875	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴 · (( -1↑𝑘) · (𝐴↑𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑(𝑘 + 1))))
23	14, 22	eqtrd 2795	. . . 4 ⊢ (𝜑 → (𝐴 · Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑(𝑘 + 1))))
24	12	mullidd 11331	. . . 4 ⊢ (𝜑 → (1 · Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)))
25	23, 24	oveq12d 7439	. . 3 ⊢ (𝜑 → ((𝐴 · Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) + (1 · Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)))) = (Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑(𝑘 + 1))) + Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))))
26		1zzd 12731	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
27		0zd 12709	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
28		pwp1fsum.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
29		nnz 12718	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
30		peano2zm 12743	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
31	29, 30	syl 18	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℤ)
32	28, 31	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
33		peano2nn0 12650	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
34	6, 33	syl 18	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → (𝑘 + 1) ∈ ℕ₀)
35	34	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 + 1) ∈ ℕ₀)
36	9, 35	expcld 14293	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑(𝑘 + 1)) ∈ ℂ)
37	8, 36	mulcld 11333	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (( -1↑𝑘) · (𝐴↑(𝑘 + 1))) ∈ ℂ)
38		oveq2 7429	. . . . . . . 8 ⊢ (𝑘 = (𝑙 − 1) → ( -1↑𝑘) = ( -1↑(𝑙 − 1)))
39		oveq1 7428	. . . . . . . . 9 ⊢ (𝑘 = (𝑙 − 1) → (𝑘 + 1) = ((𝑙 − 1) + 1))
40	39	oveq2d 7437	. . . . . . . 8 ⊢ (𝑘 = (𝑙 − 1) → (𝐴↑(𝑘 + 1)) = (𝐴↑((𝑙 − 1) + 1)))
41	38, 40	oveq12d 7439	. . . . . . 7 ⊢ (𝑘 = (𝑙 − 1) → (( -1↑𝑘) · (𝐴↑(𝑘 + 1))) = (( -1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1))))
42	26, 27, 32, 37, 41	fsumshft 15952	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑(𝑘 + 1))) = Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))(( -1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1))))
43		elfzelz 13660	. . . . . . . . . . . 12 ⊢ (𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1)) → 𝑙 ∈ ℤ)
44	43	zcnd 12808	. . . . . . . . . . 11 ⊢ (𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1)) → 𝑙 ∈ ℂ)
45	44	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → 𝑙 ∈ ℂ)
46		npcan1 11745	. . . . . . . . . 10 ⊢ (𝑙 ∈ ℂ → ((𝑙 − 1) + 1) = 𝑙)
47	45, 46	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → ((𝑙 − 1) + 1) = 𝑙)
48	47	oveq2d 7437	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → (𝐴↑((𝑙 − 1) + 1)) = (𝐴↑𝑙))
49	48	oveq2d 7437	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → (( -1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1))) = (( -1↑(𝑙 − 1)) · (𝐴↑𝑙)))
50	49	sumeq2dv 15875	. . . . . 6 ⊢ (𝜑 → Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))(( -1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1))) = Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))(( -1↑(𝑙 − 1)) · (𝐴↑𝑙)))
51	28	nncnd 12355	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℂ)
52		npcan1 11745	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
53	51, 52	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
54		0p1e1 12467	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
55	54	fveq2i 6889	. . . . . . . . . . 11 ⊢ (ℤ_≥‘(0 + 1)) = (ℤ_≥‘1)
56		nnuz 13008	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
57	55, 56	eqtr4i 2786	. . . . . . . . . 10 ⊢ (ℤ_≥‘(0 + 1)) = ℕ
58	57	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (ℤ_≥‘(0 + 1)) = ℕ)
59	28, 53, 58	3eltr4d 2875	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(0 + 1)))
60	54	oveq1i 7431	. . . . . . . . . . 11 ⊢ ((0 + 1)...((𝑁 − 1) + 1)) = (1...((𝑁 − 1) + 1))
61	60	eleq2i 2852	. . . . . . . . . 10 ⊢ (𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1)) ↔ 𝑙 ∈ (1...((𝑁 − 1) + 1)))
62	4	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → -1 ∈ ℂ)
63		nnm1nn0 12651	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ ℕ → (𝑙 − 1) ∈ ℕ₀)
64	63	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝑙 − 1) ∈ ℕ₀)
65	62, 64	expcld 14293	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ( -1↑(𝑙 − 1)) ∈ ℂ)
66	1	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝐴 ∈ ℂ)
67		nnnn0 12617	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ ℕ → 𝑙 ∈ ℕ₀)
68	67	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝑙 ∈ ℕ₀)
69	66, 68	expcld 14293	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐴↑𝑙) ∈ ℂ)
70	65, 69	mulcld 11333	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) ∈ ℂ)
71	70	expcom 419	. . . . . . . . . . 11 ⊢ (𝑙 ∈ ℕ → (𝜑 → (( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) ∈ ℂ))
72		elfznn 13691	. . . . . . . . . . 11 ⊢ (𝑙 ∈ (1...((𝑁 − 1) + 1)) → 𝑙 ∈ ℕ)
73	71, 72	syl11 34	. . . . . . . . . 10 ⊢ (𝜑 → (𝑙 ∈ (1...((𝑁 − 1) + 1)) → (( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) ∈ ℂ))
74	61, 73	biimtrid 245	. . . . . . . . 9 ⊢ (𝜑 → (𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1)) → (( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) ∈ ℂ))
75	74	imp 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → (( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) ∈ ℂ)
76		oveq1 7428	. . . . . . . . . 10 ⊢ (𝑙 = ((𝑁 − 1) + 1) → (𝑙 − 1) = (((𝑁 − 1) + 1) − 1))
77	76	oveq2d 7437	. . . . . . . . 9 ⊢ (𝑙 = ((𝑁 − 1) + 1) → ( -1↑(𝑙 − 1)) = ( -1↑(((𝑁 − 1) + 1) − 1)))
78		oveq2 7429	. . . . . . . . 9 ⊢ (𝑙 = ((𝑁 − 1) + 1) → (𝐴↑𝑙) = (𝐴↑((𝑁 − 1) + 1)))
79	77, 78	oveq12d 7439	. . . . . . . 8 ⊢ (𝑙 = ((𝑁 − 1) + 1) → (( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) = (( -1↑(((𝑁 − 1) + 1) − 1)) · (𝐴↑((𝑁 − 1) + 1))))
80	59, 75, 79	fsumm1 15923	. . . . . . 7 ⊢ (𝜑 → Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))(( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) = (Σ𝑙 ∈ ((0 + 1)...(((𝑁 − 1) + 1) − 1))(( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) + (( -1↑(((𝑁 − 1) + 1) − 1)) · (𝐴↑((𝑁 − 1) + 1)))))
81	32	zcnd 12808	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − 1) ∈ ℂ)
82		pncan1 11744	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1) ∈ ℂ → (((𝑁 − 1) + 1) − 1) = (𝑁 − 1))
83	81, 82	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑁 − 1) + 1) − 1) = (𝑁 − 1))
84	83	oveq2d 7437	. . . . . . . . . 10 ⊢ (𝜑 → ((0 + 1)...(((𝑁 − 1) + 1) − 1)) = ((0 + 1)...(𝑁 − 1)))
85	84	sumeq1d 15873	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑙 ∈ ((0 + 1)...(((𝑁 − 1) + 1) − 1))(( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) = Σ𝑙 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑙 − 1)) · (𝐴↑𝑙)))
86		oveq1 7428	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑘 → (𝑙 − 1) = (𝑘 − 1))
87	86	oveq2d 7437	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑘 → ( -1↑(𝑙 − 1)) = ( -1↑(𝑘 − 1)))
88		oveq2 7429	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑘 → (𝐴↑𝑙) = (𝐴↑𝑘))
89	87, 88	oveq12d 7439	. . . . . . . . . 10 ⊢ (𝑙 = 𝑘 → (( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) = (( -1↑(𝑘 − 1)) · (𝐴↑𝑘)))
90	89	cbvsumv 15869	. . . . . . . . 9 ⊢ Σ𝑙 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘))
91	85, 90	eqtrdi 2811	. . . . . . . 8 ⊢ (𝜑 → Σ𝑙 ∈ ((0 + 1)...(((𝑁 − 1) + 1) − 1))(( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)))
92	83	oveq2d 7437	. . . . . . . . 9 ⊢ (𝜑 → ( -1↑(((𝑁 − 1) + 1) − 1)) = ( -1↑(𝑁 − 1)))
93	53	oveq2d 7437	. . . . . . . . 9 ⊢ (𝜑 → (𝐴↑((𝑁 − 1) + 1)) = (𝐴↑𝑁))
94	92, 93	oveq12d 7439	. . . . . . . 8 ⊢ (𝜑 → (( -1↑(((𝑁 − 1) + 1) − 1)) · (𝐴↑((𝑁 − 1) + 1))) = (( -1↑(𝑁 − 1)) · (𝐴↑𝑁)))
95	91, 94	oveq12d 7439	. . . . . . 7 ⊢ (𝜑 → (Σ𝑙 ∈ ((0 + 1)...(((𝑁 − 1) + 1) − 1))(( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) + (( -1↑(((𝑁 − 1) + 1) − 1)) · (𝐴↑((𝑁 − 1) + 1)))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑(𝑁 − 1)) · (𝐴↑𝑁))))
96	80, 95	eqtrd 2795	. . . . . 6 ⊢ (𝜑 → Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))(( -1↑(𝑙 − 1)) · (𝐴↑𝑙)) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑(𝑁 − 1)) · (𝐴↑𝑁))))
97	42, 50, 96	3eqtrd 2799	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑(𝑘 + 1))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑(𝑁 − 1)) · (𝐴↑𝑁))))
98		nnm1nn0 12651	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
99		elnn0uz 13010	. . . . . . . . 9 ⊢ ((𝑁 − 1) ∈ ℕ₀ ↔ (𝑁 − 1) ∈ (ℤ_≥‘0))
100	98, 99	sylib 221	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ_≥‘0))
101	28, 100	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ_≥‘0))
102		oveq2 7429	. . . . . . . . 9 ⊢ (𝑘 = 0 → ( -1↑𝑘) = ( -1↑0))
103		exp0 14212	. . . . . . . . . 10 ⊢ ( -1 ∈ ℂ → ( -1↑0) = 1)
104	4, 103	ax-mp 5	. . . . . . . . 9 ⊢ ( -1↑0) = 1
105	102, 104	eqtrdi 2811	. . . . . . . 8 ⊢ (𝑘 = 0 → ( -1↑𝑘) = 1)
106		oveq2 7429	. . . . . . . 8 ⊢ (𝑘 = 0 → (𝐴↑𝑘) = (𝐴↑0))
107	105, 106	oveq12d 7439	. . . . . . 7 ⊢ (𝑘 = 0 → (( -1↑𝑘) · (𝐴↑𝑘)) = (1 · (𝐴↑0)))
108	101, 11, 107	fsum1p 15925	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)) = ((1 · (𝐴↑0)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))))
109	1	exp0d 14287	. . . . . . . . 9 ⊢ (𝜑 → (𝐴↑0) = 1)
110	109	oveq2d 7437	. . . . . . . 8 ⊢ (𝜑 → (1 · (𝐴↑0)) = (1 · 1))
111		1t1e1 12508	. . . . . . . 8 ⊢ (1 · 1) = 1
112	110, 111	eqtrdi 2811	. . . . . . 7 ⊢ (𝜑 → (1 · (𝐴↑0)) = 1)
113	112	oveq1d 7436	. . . . . 6 ⊢ (𝜑 → ((1 · (𝐴↑0)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = (1 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))))
114		fzfid 14120	. . . . . . . 8 ⊢ (𝜑 → ((0 + 1)...(𝑁 − 1)) ∈ Fin)
115		elfznn 13691	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ)
116	4	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → -1 ∈ ℂ)
117		nnnn0 12617	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
118	117	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ₀)
119	116, 118	expcld 14293	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ( -1↑𝑘) ∈ ℂ)
120	1	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
121	120, 118	expcld 14293	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) ∈ ℂ)
122	119, 121	mulcld 11333	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (( -1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ)
123	122	expcom 419	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (𝜑 → (( -1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ))
124	115, 123	syl 18	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → (𝜑 → (( -1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ))
125	54	oveq1i 7431	. . . . . . . . . 10 ⊢ ((0 + 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
126	124, 125	eleq2s 2878	. . . . . . . . 9 ⊢ (𝑘 ∈ ((0 + 1)...(𝑁 − 1)) → (𝜑 → (( -1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ))
127	126	impcom 413	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 − 1))) → (( -1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ)
128	114, 127	fsumcl 15905	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ)
129	2, 128	addcomd 11516	. . . . . 6 ⊢ (𝜑 → (1 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)) + 1))
130	108, 113, 129	3eqtrd 2799	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)) + 1))
131	97, 130	oveq12d 7439	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑(𝑘 + 1))) + Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = ((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑(𝑁 − 1)) · (𝐴↑𝑁))) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)) + 1)))
132		nnm1nn0 12651	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ₀)
133	132	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 − 1) ∈ ℕ₀)
134	116, 133	expcld 14293	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ( -1↑(𝑘 − 1)) ∈ ℂ)
135	134, 121	mulcld 11333	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) ∈ ℂ)
136	135	expcom 419	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝜑 → (( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) ∈ ℂ))
137	115, 136	syl 18	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → (𝜑 → (( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) ∈ ℂ))
138	137, 125	eleq2s 2878	. . . . . . . 8 ⊢ (𝑘 ∈ ((0 + 1)...(𝑁 − 1)) → (𝜑 → (( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) ∈ ℂ))
139	138	impcom 413	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 − 1))) → (( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) ∈ ℂ)
140	114, 139	fsumcl 15905	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) ∈ ℂ)
141	4	a1i 11	. . . . . . . 8 ⊢ (𝜑 → -1 ∈ ℂ)
142	28, 98	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
143	141, 142	expcld 14293	. . . . . . 7 ⊢ (𝜑 → ( -1↑(𝑁 − 1)) ∈ ℂ)
144	28	nnnn0d 12671	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
145	1, 144	expcld 14293	. . . . . . 7 ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ)
146	143, 145	mulcld 11333	. . . . . 6 ⊢ (𝜑 → (( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) ∈ ℂ)
147	140, 146	addcld 11332	. . . . 5 ⊢ (𝜑 → (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑(𝑁 − 1)) · (𝐴↑𝑁))) ∈ ℂ)
148	147, 128, 2	addassd 11335	. . . 4 ⊢ (𝜑 → (((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑(𝑁 − 1)) · (𝐴↑𝑁))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) + 1) = ((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑(𝑁 − 1)) · (𝐴↑𝑁))) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)) + 1)))
149	140, 146	addcomd 11516	. . . . . . 7 ⊢ (𝜑 → (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑(𝑁 − 1)) · (𝐴↑𝑁))) = ((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘))))
150	149	oveq1d 7436	. . . . . 6 ⊢ (𝜑 → ((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑(𝑁 − 1)) · (𝐴↑𝑁))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = (((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))))
151	146, 140, 128	addassd 11335	. . . . . 6 ⊢ (𝜑 → (((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = ((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)))))
152		nncn 12347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
153		npcan1 11745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ ℂ → ((𝑘 − 1) + 1) = 𝑘)
154	152, 153	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℕ → ((𝑘 − 1) + 1) = 𝑘)
155	154	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℕ → 𝑘 = ((𝑘 − 1) + 1))
156	155	oveq2d 7437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ → ( -1↑𝑘) = ( -1↑((𝑘 − 1) + 1)))
157	4	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℕ → -1 ∈ ℂ)
158	157, 132	expp1d 14294	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ → ( -1↑((𝑘 − 1) + 1)) = (( -1↑(𝑘 − 1)) · -1))
159	157, 132	expcld 14293	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℕ → ( -1↑(𝑘 − 1)) ∈ ℂ)
160	159, 157	mulcomd 11334	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ → (( -1↑(𝑘 − 1)) · -1) = ( -1 · ( -1↑(𝑘 − 1))))
161	156, 158, 160	3eqtrd 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ → ( -1↑𝑘) = ( -1 · ( -1↑(𝑘 − 1))))
162	161	oveq2d 7437	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (( -1↑(𝑘 − 1)) + ( -1↑𝑘)) = (( -1↑(𝑘 − 1)) + ( -1 · ( -1↑(𝑘 − 1)))))
163	159	mulm1d 11772	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ → ( -1 · ( -1↑(𝑘 − 1))) = -( -1↑(𝑘 − 1)))
164	163	oveq2d 7437	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (( -1↑(𝑘 − 1)) + ( -1 · ( -1↑(𝑘 − 1)))) = (( -1↑(𝑘 − 1)) + -( -1↑(𝑘 − 1))))
165	159	negidd 11663	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (( -1↑(𝑘 − 1)) + -( -1↑(𝑘 − 1))) = 0)
166	162, 164, 165	3eqtrd 2799	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → (( -1↑(𝑘 − 1)) + ( -1↑𝑘)) = 0)
167	166	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (( -1↑(𝑘 − 1)) + ( -1↑𝑘)) = 0)
168	167	oveq1d 7436	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((( -1↑(𝑘 − 1)) + ( -1↑𝑘)) · (𝐴↑𝑘)) = (0 · (𝐴↑𝑘)))
169	134, 119, 121	adddird 11338	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((( -1↑(𝑘 − 1)) + ( -1↑𝑘)) · (𝐴↑𝑘)) = ((( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑𝑘) · (𝐴↑𝑘))))
170	121	mul02d 11512	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (0 · (𝐴↑𝑘)) = 0)
171	168, 169, 170	3eqtr3d 2803	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑𝑘) · (𝐴↑𝑘))) = 0)
172	171	expcom 419	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝜑 → ((( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑𝑘) · (𝐴↑𝑘))) = 0))
173	115, 172	syl 18	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → (𝜑 → ((( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑𝑘) · (𝐴↑𝑘))) = 0))
174	173, 125	eleq2s 2878	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ((0 + 1)...(𝑁 − 1)) → (𝜑 → ((( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑𝑘) · (𝐴↑𝑘))) = 0))
175	174	impcom 413	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 − 1))) → ((( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑𝑘) · (𝐴↑𝑘))) = 0)
176	175	sumeq2dv 15875	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑𝑘) · (𝐴↑𝑘))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))0)
177	114, 139, 127	fsumadd 15912	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑𝑘) · (𝐴↑𝑘))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))))
178	114	olcd 888	. . . . . . . . . 10 ⊢ (𝜑 → (((0 + 1)...(𝑁 − 1)) ⊆ (ℤ_≥‘1) ∨ ((0 + 1)...(𝑁 − 1)) ∈ Fin))
179		sumz 15894	. . . . . . . . . 10 ⊢ ((((0 + 1)...(𝑁 − 1)) ⊆ (ℤ_≥‘1) ∨ ((0 + 1)...(𝑁 − 1)) ∈ Fin) → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))0 = 0)
180	178, 179	syl 18	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))0 = 0)
181	176, 177, 180	3eqtr3d 2803	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = 0)
182	181	oveq2d 7437	. . . . . . 7 ⊢ (𝜑 → ((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)))) = ((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 0))
183	146	addridd 11514	. . . . . . 7 ⊢ (𝜑 → ((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 0) = (( -1↑(𝑁 − 1)) · (𝐴↑𝑁)))
184	182, 183	eqtrd 2795	. . . . . 6 ⊢ (𝜑 → ((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘)))) = (( -1↑(𝑁 − 1)) · (𝐴↑𝑁)))
185	150, 151, 184	3eqtrd 2799	. . . . 5 ⊢ (𝜑 → ((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑(𝑁 − 1)) · (𝐴↑𝑁))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = (( -1↑(𝑁 − 1)) · (𝐴↑𝑁)))
186	185	oveq1d 7436	. . . 4 ⊢ (𝜑 → (((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑(𝑘 − 1)) · (𝐴↑𝑘)) + (( -1↑(𝑁 − 1)) · (𝐴↑𝑁))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) + 1) = ((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 1))
187	131, 148, 186	3eqtr2d 2801	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑(𝑘 + 1))) + Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = ((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 1))
188	13, 25, 187	3eqtrd 2799	. 2 ⊢ (𝜑 → ((𝐴 + 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))) = ((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 1))
189	188	eqcomd 2766	1 ⊢ (𝜑 → ((( -1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 1) = ((𝐴 + 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(( -1↑𝑘) · (𝐴↑𝑘))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∨ wo 861 = wceq 1569 ∈ wcel 2144 ⊆ wss 3895 ‘cfv 6539 (class class class)co 7421 Fincfn 8977 ℂcc 11202 0cc0 11204 1c1 11205 + caddc 11207 · cmul 11209 − cmin 11545 -cneg 11546 ℕcn 12339 ℕ₀cn0 12610 ℤcz 12697 ℤ_≥cuz 12969 ...cfz 13643 ↑cexp 14208 Σcsu 15859

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-inf2 9646 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-pre-sup 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-er 8721 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-sup 9438 df-oi 9508 df-card 10024 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-div 11978 df-nn 12340 df-2 12409 df-3 12410 df-n0 12611 df-z 12698 df-uz 12970 df-rp 13125 df-fz 13644 df-fzo 13793 df-seq 14149 df-exp 14209 df-hash 14479 df-cj 15272 df-re 15273 df-im 15274 df-sqrt 15408 df-abs 15409 df-clim 15661 df-sum 15860

This theorem is used by: oddpwp1fsum 16568

W3C validator