perfect

Description: The Euclid-Euler theorem, or Perfect Number theorem. A positive even integer N is a perfect number (that is, its divisor sum is 2 N ) if and only if it is of the form 2 ^ ( p - 1 ) x. ( 2 ^ p - 1 ) , where 2 ^ p - 1 is prime (a Mersenne prime), and therefore p is also prime, see mersenne . This is Metamath 100 proof #70. (Contributed by Mario Carneiro, 17-May-2016)

		Ref	Expression
	Assertion	perfect	$⊢ (N \in ℕ \land 2 ∥ N) \to (1 σ N = 2 \cdot N \leftrightarrow \exists p \in ℤ (2^{p} - 1 \in ℙ \land N = 2^{p - 1} (2^{p} - 1)))$

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2 ∥ N$
2		2prm	$⊢ 2 \in ℙ$
3		simpll	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to N \in ℕ$
4		pcelnn	$⊢ (2 \in ℙ \land N \in ℕ) \to (2 pCnt N \in ℕ \leftrightarrow 2 ∥ N)$
5	2 3 4	sylancr	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to (2 pCnt N \in ℕ \leftrightarrow 2 ∥ N)$
6	1 5	mpbird	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2 pCnt N \in ℕ$
7	6	nnzd	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2 pCnt N \in ℤ$
8	7	peano2zd	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to (2 pCnt N) + 1 \in ℤ$
9		pcdvds	$⊢ (2 \in ℙ \land N \in ℕ) \to 2^{2 pCnt N} ∥ N$
10	2 3 9	sylancr	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2^{2 pCnt N} ∥ N$
11		2nn	$⊢ 2 \in ℕ$
12	6	nnnn0d	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2 pCnt N \in ℕ_{0}$
13		nnexpcl	$⊢ (2 \in ℕ \land 2 pCnt N \in ℕ_{0}) \to 2^{2 pCnt N} \in ℕ$
14	11 12 13	sylancr	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2^{2 pCnt N} \in ℕ$
15		nndivdvds	$⊢ (N \in ℕ \land 2^{2 pCnt N} \in ℕ) \to (2^{2 pCnt N} ∥ N \leftrightarrow \frac{N}{2^{2 pCnt N}} \in ℕ)$
16	3 14 15	syl2anc	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to (2^{2 pCnt N} ∥ N \leftrightarrow \frac{N}{2^{2 pCnt N}} \in ℕ)$
17	10 16	mpbid	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to \frac{N}{2^{2 pCnt N}} \in ℕ$
18		pcndvds2	$⊢ (2 \in ℙ \land N \in ℕ) \to \neg 2 ∥ (\frac{N}{2^{2 pCnt N}})$
19	2 3 18	sylancr	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to \neg 2 ∥ (\frac{N}{2^{2 pCnt N}})$
20		simpr	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 1 σ N = 2 \cdot N$
21		nncn	$⊢ N \in ℕ \to N \in ℂ$
22	21	ad2antrr	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to N \in ℂ$
23	14	nncnd	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2^{2 pCnt N} \in ℂ$
24	14	nnne0d	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2^{2 pCnt N} \neq 0$
25	22 23 24	divcan2d	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2^{2 pCnt N} (\frac{N}{2^{2 pCnt N}}) = N$
26	25	oveq2d	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 1 σ 2^{2 pCnt N} (\frac{N}{2^{2 pCnt N}}) = 1 σ N$
27	25	oveq2d	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2 2^{2 pCnt N} (\frac{N}{2^{2 pCnt N}}) = 2 \cdot N$
28	20 26 27	3eqtr4d	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 1 σ 2^{2 pCnt N} (\frac{N}{2^{2 pCnt N}}) = 2 2^{2 pCnt N} (\frac{N}{2^{2 pCnt N}})$
29	6 17 19 28	perfectlem2	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to (\frac{N}{2^{2 pCnt N}} \in ℙ \land \frac{N}{2^{2 pCnt N}} = 2^{(2 pCnt N) + 1} - 1)$
30	29	simprd	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to \frac{N}{2^{2 pCnt N}} = 2^{(2 pCnt N) + 1} - 1$
31	29	simpld	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to \frac{N}{2^{2 pCnt N}} \in ℙ$
32	30 31	eqeltrrd	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2^{(2 pCnt N) + 1} - 1 \in ℙ$
33	6	nncnd	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2 pCnt N \in ℂ$
34		ax-1cn	$⊢ 1 \in ℂ$
35		pncan	$⊢ (2 pCnt N \in ℂ \land 1 \in ℂ) \to (2 pCnt N) + 1 - 1 = 2 pCnt N$
36	33 34 35	sylancl	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to (2 pCnt N) + 1 - 1 = 2 pCnt N$
37	36	eqcomd	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2 pCnt N = (2 pCnt N) + 1 - 1$
38	37	oveq2d	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2^{2 pCnt N} = 2^{(2 pCnt N) + 1 - 1}$
39	38 30	oveq12d	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to 2^{2 pCnt N} (\frac{N}{2^{2 pCnt N}}) = 2^{(2 pCnt N) + 1 - 1} (2^{(2 pCnt N) + 1} - 1)$
40	25 39	eqtr3d	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to N = 2^{(2 pCnt N) + 1 - 1} (2^{(2 pCnt N) + 1} - 1)$
41		oveq2	$⊢ p = (2 pCnt N) + 1 \to 2^{p} = 2^{(2 pCnt N) + 1}$
42	41	oveq1d	$⊢ p = (2 pCnt N) + 1 \to 2^{p} - 1 = 2^{(2 pCnt N) + 1} - 1$
43	42	eleq1d	$⊢ p = (2 pCnt N) + 1 \to (2^{p} - 1 \in ℙ \leftrightarrow 2^{(2 pCnt N) + 1} - 1 \in ℙ)$
44		oveq1	$⊢ p = (2 pCnt N) + 1 \to p - 1 = (2 pCnt N) + 1 - 1$
45	44	oveq2d	$⊢ p = (2 pCnt N) + 1 \to 2^{p - 1} = 2^{(2 pCnt N) + 1 - 1}$
46	45 42	oveq12d	$⊢ p = (2 pCnt N) + 1 \to 2^{p - 1} (2^{p} - 1) = 2^{(2 pCnt N) + 1 - 1} (2^{(2 pCnt N) + 1} - 1)$
47	46	eqeq2d	$⊢ p = (2 pCnt N) + 1 \to (N = 2^{p - 1} (2^{p} - 1) \leftrightarrow N = 2^{(2 pCnt N) + 1 - 1} (2^{(2 pCnt N) + 1} - 1))$
48	43 47	anbi12d	$⊢ p = (2 pCnt N) + 1 \to ((2^{p} - 1 \in ℙ \land N = 2^{p - 1} (2^{p} - 1)) \leftrightarrow (2^{(2 pCnt N) + 1} - 1 \in ℙ \land N = 2^{(2 pCnt N) + 1 - 1} (2^{(2 pCnt N) + 1} - 1)))$
49	48	rspcev	$⊢ ((2 pCnt N) + 1 \in ℤ \land (2^{(2 pCnt N) + 1} - 1 \in ℙ \land N = 2^{(2 pCnt N) + 1 - 1} (2^{(2 pCnt N) + 1} - 1))) \to \exists p \in ℤ (2^{p} - 1 \in ℙ \land N = 2^{p - 1} (2^{p} - 1))$
50	8 32 40 49	syl12anc	$⊢ ((N \in ℕ \land 2 ∥ N) \land 1 σ N = 2 \cdot N) \to \exists p \in ℤ (2^{p} - 1 \in ℙ \land N = 2^{p - 1} (2^{p} - 1))$
51	50	ex	$⊢ (N \in ℕ \land 2 ∥ N) \to (1 σ N = 2 \cdot N \to \exists p \in ℤ (2^{p} - 1 \in ℙ \land N = 2^{p - 1} (2^{p} - 1)))$
52		perfect1	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to 1 σ 2^{p - 1} (2^{p} - 1) = 2^{p} (2^{p} - 1)$
53		2cn	$⊢ 2 \in ℂ$
54		mersenne	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to p \in ℙ$
55		prmnn	$⊢ p \in ℙ \to p \in ℕ$
56	54 55	syl	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to p \in ℕ$
57		expm1t	$⊢ (2 \in ℂ \land p \in ℕ) \to 2^{p} = 2^{p - 1} \cdot 2$
58	53 56 57	sylancr	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to 2^{p} = 2^{p - 1} \cdot 2$
59		nnm1nn0	$⊢ p \in ℕ \to p - 1 \in ℕ_{0}$
60	56 59	syl	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to p - 1 \in ℕ_{0}$
61		expcl	$⊢ (2 \in ℂ \land p - 1 \in ℕ_{0}) \to 2^{p - 1} \in ℂ$
62	53 60 61	sylancr	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to 2^{p - 1} \in ℂ$
63		mulcom	$⊢ (2^{p - 1} \in ℂ \land 2 \in ℂ) \to 2^{p - 1} \cdot 2 = 2 2^{p - 1}$
64	62 53 63	sylancl	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to 2^{p - 1} \cdot 2 = 2 2^{p - 1}$
65	58 64	eqtrd	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to 2^{p} = 2 2^{p - 1}$
66	65	oveq1d	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to 2^{p} (2^{p} - 1) = 2 2^{p - 1} (2^{p} - 1)$
67		2cnd	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to 2 \in ℂ$
68		prmnn	$⊢ 2^{p} - 1 \in ℙ \to 2^{p} - 1 \in ℕ$
69	68	adantl	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to 2^{p} - 1 \in ℕ$
70	69	nncnd	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to 2^{p} - 1 \in ℂ$
71	67 62 70	mulassd	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to 2 2^{p - 1} (2^{p} - 1) = 2 2^{p - 1} (2^{p} - 1)$
72	52 66 71	3eqtrd	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to 1 σ 2^{p - 1} (2^{p} - 1) = 2 2^{p - 1} (2^{p} - 1)$
73		oveq2	$⊢ N = 2^{p - 1} (2^{p} - 1) \to 1 σ N = 1 σ 2^{p - 1} (2^{p} - 1)$
74		oveq2	$⊢ N = 2^{p - 1} (2^{p} - 1) \to 2 \cdot N = 2 2^{p - 1} (2^{p} - 1)$
75	73 74	eqeq12d	$⊢ N = 2^{p - 1} (2^{p} - 1) \to (1 σ N = 2 \cdot N \leftrightarrow 1 σ 2^{p - 1} (2^{p} - 1) = 2 2^{p - 1} (2^{p} - 1))$
76	72 75	syl5ibrcom	$⊢ (p \in ℤ \land 2^{p} - 1 \in ℙ) \to (N = 2^{p - 1} (2^{p} - 1) \to 1 σ N = 2 \cdot N)$
77	76	impr	$⊢ (p \in ℤ \land (2^{p} - 1 \in ℙ \land N = 2^{p - 1} (2^{p} - 1))) \to 1 σ N = 2 \cdot N$
78	77	rexlimiva	$⊢ \exists p \in ℤ (2^{p} - 1 \in ℙ \land N = 2^{p - 1} (2^{p} - 1)) \to 1 σ N = 2 \cdot N$
79	51 78	impbid1	$⊢ (N \in ℕ \land 2 ∥ N) \to (1 σ N = 2 \cdot N \leftrightarrow \exists p \in ℤ (2^{p} - 1 \in ℙ \land N = 2^{p - 1} (2^{p} - 1)))$

Metamath Proof Explorer

Theorem perfect

Proof