Theorem 1sgmprm

Description: The sum of divisors for a prime is P + 1 because the only divisors are 1 and P . (Contributed by Mario Carneiro, 17-May-2016)

	Ref	Expression
Assertion	1sgmprm	$$⊢P\in \mathbb{P}\to 1\sigma P=P+1$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3		sgmppw	$$⊢\left(1\in ℂ\wedge P\in \mathbb{P}\wedge 1\in {\mathbb{N}}_0\right)\to 1\sigma P^1=\sum _{k=0}^1{\left(P^1\right)}^k$$
4	1 2 3	mp3an13	$$⊢P\in \mathbb{P}\to 1\sigma P^1=\sum _{k=0}^1{\left(P^1\right)}^k$$
5		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
6	5	nncnd	$$⊢P\in \mathbb{P}\to P\in ℂ$$
7	6	exp1d	$$⊢P\in \mathbb{P}\to P^1=P$$
8	7	oveq2d	$$⊢P\in \mathbb{P}\to 1\sigma P^1=1\sigma P$$
9	6	adantr	$$⊢\left(P\in \mathbb{P}\wedge k\in \left(0\dots 1\right)\right)\to P\in ℂ$$
10	9	cxp1d	$$⊢\left(P\in \mathbb{P}\wedge k\in \left(0\dots 1\right)\right)\to P^1=P$$
11	10	oveq1d	$$⊢\left(P\in \mathbb{P}\wedge k\in \left(0\dots 1\right)\right)\to {\left(P^1\right)}^k=P^k$$
12	11	sumeq2dv	$$⊢P\in \mathbb{P}\to \sum _{k=0}^1{\left(P^1\right)}^k=\sum _{k=0}^1{P}^k$$
13		1m1e0	$$⊢1-1=0$$
14	13	oveq2i	$$⊢\left(0\dots 1-1\right)=\left(0\dots 0\right)$$
15	14	sumeq1i	$$⊢\sum _{k=0}^{1-1}{P}^k=\sum _{k=0}^0{P}^k$$
16		0z	$$⊢0\in \mathbb{Z}$$
17	6	exp0d	$$⊢P\in \mathbb{P}\to P^0=1$$
18	17 1	eqeltrdi	$$⊢P\in \mathbb{P}\to P^0\in ℂ$$
19		oveq2	$$⊢k=0\to P^k=P^0$$
20	19	fsum1	$$⊢\left(0\in \mathbb{Z}\wedge P^0\in ℂ\right)\to \sum _{k=0}^0{P}^k=P^0$$
21	16 18 20	sylancr	$$⊢P\in \mathbb{P}\to \sum _{k=0}^0{P}^k=P^0$$
22	21 17	eqtrd	$$⊢P\in \mathbb{P}\to \sum _{k=0}^0{P}^k=1$$
23	15 22	eqtrid	$$⊢P\in \mathbb{P}\to \sum _{k=0}^{1-1}{P}^k=1$$
24	23 7	oveq12d	$$⊢P\in \mathbb{P}\to \sum _{k=0}^{1-1}{P}^k+P^1=1+P$$
25	2	a1i	$$⊢P\in \mathbb{P}\to 1\in {\mathbb{N}}_0$$
26		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
27	25 26	eleqtrdi	$$⊢P\in \mathbb{P}\to 1\in {\mathbb{Z}}_{\ge 0}$$
28		elfznn0	$$⊢k\in \left(0\dots 1\right)\to k\in {\mathbb{N}}_0$$
29		expcl	$$⊢\left(P\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to P^k\in ℂ$$
30	6 28 29	syl2an	$$⊢\left(P\in \mathbb{P}\wedge k\in \left(0\dots 1\right)\right)\to P^k\in ℂ$$
31		oveq2	$$⊢k=1\to P^k=P^1$$
32	27 30 31	fsumm1	$$⊢P\in \mathbb{P}\to \sum _{k=0}^1{P}^k=\sum _{k=0}^{1-1}{P}^k+P^1$$
33		addcom	$$⊢\left(P\in ℂ\wedge 1\in ℂ\right)\to P+1=1+P$$
34	6 1 33	sylancl	$$⊢P\in \mathbb{P}\to P+1=1+P$$
35	24 32 34	3eqtr4d	$$⊢P\in \mathbb{P}\to \sum _{k=0}^1{P}^k=P+1$$
36	12 35	eqtrd	$$⊢P\in \mathbb{P}\to \sum _{k=0}^1{\left(P^1\right)}^k=P+1$$
37	4 8 36	3eqtr3d	$$⊢P\in \mathbb{P}\to 1\sigma P=P+1$$