Theorem 1sgm2ppw

Description: The sum of the divisors of 2 ^ ( N - 1 ) . (Contributed by Mario Carneiro, 17-May-2016)

	Ref	Expression
Assertion	1sgm2ppw	$$⊢N\in \mathbb{N}\to 1\sigma 2^{N-1}=2^N-1$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		2prm	$$⊢2\in \mathbb{P}$$
3		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
4		sgmppw	$$⊢\left(1\in ℂ\wedge 2\in \mathbb{P}\wedge N-1\in {\mathbb{N}}_0\right)\to 1\sigma 2^{N-1}=\sum _{k=0}^{N-1}{\left(2^1\right)}^k$$
5	1 2 3 4	mp3an12i	$$⊢N\in \mathbb{N}\to 1\sigma 2^{N-1}=\sum _{k=0}^{N-1}{\left(2^1\right)}^k$$
6		2cn	$$⊢2\in ℂ$$
7		cxp1	$$⊢2\in ℂ\to 2^1=2$$
8	6 7	mp1i	$$⊢k\in \left(0\dots N-1\right)\to 2^1=2$$
9	8	oveq1d	$$⊢k\in \left(0\dots N-1\right)\to {\left(2^1\right)}^k=2^k$$
10	9	sumeq2i	$$⊢\sum _{k=0}^{N-1}{\left(2^1\right)}^k=\sum _{k=0}^{N-1}{2}^k$$
11	6	a1i	$$⊢N\in \mathbb{N}\to 2\in ℂ$$
12		1ne2	$$⊢1\ne 2$$
13	12	necomi	$$⊢2\ne 1$$
14	13	a1i	$$⊢N\in \mathbb{N}\to 2\ne 1$$
15		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
16	11 14 15	geoser	$$⊢N\in \mathbb{N}\to \sum _{k=0}^{N-1}{2}^k=\frac{1-2^N}{1-2}$$
17	10 16	syl5eq	$$⊢N\in \mathbb{N}\to \sum _{k=0}^{N-1}{\left(2^1\right)}^k=\frac{1-2^N}{1-2}$$
18		2nn	$$⊢2\in \mathbb{N}$$
19		nnexpcl	$$⊢\left(2\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to 2^N\in \mathbb{N}$$
20	18 15 19	sylancr	$$⊢N\in \mathbb{N}\to 2^N\in \mathbb{N}$$
21	20	nncnd	$$⊢N\in \mathbb{N}\to 2^N\in ℂ$$
22		subcl	$$⊢\left(2^N\in ℂ\wedge 1\in ℂ\right)\to 2^N-1\in ℂ$$
23	21 1 22	sylancl	$$⊢N\in \mathbb{N}\to 2^N-1\in ℂ$$
24	1	a1i	$$⊢N\in \mathbb{N}\to 1\in ℂ$$
25		ax-1ne0	$$⊢1\ne 0$$
26	25	a1i	$$⊢N\in \mathbb{N}\to 1\ne 0$$
27	23 24 26	div2negd	$$⊢N\in \mathbb{N}\to \frac{-\left(2^N-1\right)}{-1}=\frac{2^N-1}{1}$$
28		negsubdi2	$$⊢\left(2^N\in ℂ\wedge 1\in ℂ\right)\to -\left(2^N-1\right)=1-2^N$$
29	21 1 28	sylancl	$$⊢N\in \mathbb{N}\to -\left(2^N-1\right)=1-2^N$$
30		df-neg	$$⊢-1=0-1$$
31		0cn	$$⊢0\in ℂ$$
32		pnpcan	$$⊢\left(1\in ℂ\wedge 0\in ℂ\wedge 1\in ℂ\right)\to 1+0-\left(1+1\right)=0-1$$
33	1 31 1 32	mp3an	$$⊢1+0-\left(1+1\right)=0-1$$
34		1p0e1	$$⊢1+0=1$$
35		1p1e2	$$⊢1+1=2$$
36	34 35	oveq12i	$$⊢1+0-\left(1+1\right)=1-2$$
37	30 33 36	3eqtr2i	$$⊢-1=1-2$$
38	37	a1i	$$⊢N\in \mathbb{N}\to -1=1-2$$
39	29 38	oveq12d	$$⊢N\in \mathbb{N}\to \frac{-\left(2^N-1\right)}{-1}=\frac{1-2^N}{1-2}$$
40	23	div1d	$$⊢N\in \mathbb{N}\to \frac{2^N-1}{1}=2^N-1$$
41	27 39 40	3eqtr3d	$$⊢N\in \mathbb{N}\to \frac{1-2^N}{1-2}=2^N-1$$
42	5 17 41	3eqtrd	$$⊢N\in \mathbb{N}\to 1\sigma 2^{N-1}=2^N-1$$