Metamath Proof Explorer


Theorem 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 N Even 1 σ N = 2 N p 2 p 1 N = 2 p 1 2 p 1

Proof

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