Metamath Proof Explorer


Theorem 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). (It follows from this that p is also prime.) This is Metamath 100 proof #70. (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Assertion perfect
|- ( ( N e. NN /\ 2 || N ) -> ( ( 1 sigma N ) = ( 2 x. N ) <-> E. p e. ZZ ( ( ( 2 ^ p ) - 1 ) e. Prime /\ N = ( ( 2 ^ ( p - 1 ) ) x. ( ( 2 ^ p ) - 1 ) ) ) ) )

Proof

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