perfectALTV

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). (It follows from this that p is also prime.) This is Metamath 100 proof #70. (Contributed by Mario Carneiro, 17-May-2016) (Revised by AV, 1-Jul-2020) (Proof modification is discouraged.)

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

Proof