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