Metamath Proof Explorer

Theorem perfect1

Description: Euclid's contribution to the Euclid-Euler theorem. A number of the form 2 ^ ( p - 1 ) x. ( 2 ^ p - 1 ) is a perfect number. (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Assertion perfect1 
|- ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 1 sigma ( ( 2 ^ ( P - 1 ) ) x. ( ( 2 ^ P ) - 1 ) ) ) = ( ( 2 ^ P ) x. ( ( 2 ^ P ) - 1 ) ) )

Proof

Step Hyp Ref Expression
1 mersenne 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> P e. Prime )
2 prmnn 
 |-  ( P e. Prime -> P e. NN )
3 1 2 syl 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> P e. NN )
4 1sgm2ppw 
 |-  ( P e. NN -> ( 1 sigma ( 2 ^ ( P - 1 ) ) ) = ( ( 2 ^ P ) - 1 ) )
5 3 4 syl 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 1 sigma ( 2 ^ ( P - 1 ) ) ) = ( ( 2 ^ P ) - 1 ) )
6 1sgmprm 
 |-  ( ( ( 2 ^ P ) - 1 ) e. Prime -> ( 1 sigma ( ( 2 ^ P ) - 1 ) ) = ( ( ( 2 ^ P ) - 1 ) + 1 ) )
7 6 adantl 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 1 sigma ( ( 2 ^ P ) - 1 ) ) = ( ( ( 2 ^ P ) - 1 ) + 1 ) )
8 2nn 
 |-  2 e. NN
9 3 nnnn0d 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> P e. NN0 )
10 nnexpcl 
 |-  ( ( 2 e. NN /\ P e. NN0 ) -> ( 2 ^ P ) e. NN )
11 8 9 10 sylancr 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 2 ^ P ) e. NN )
12 11 nncnd 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 2 ^ P ) e. CC )
13 ax-1cn 
 |-  1 e. CC
14 npcan 
 |-  ( ( ( 2 ^ P ) e. CC /\ 1 e. CC ) -> ( ( ( 2 ^ P ) - 1 ) + 1 ) = ( 2 ^ P ) )
15 12 13 14 sylancl 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( ( 2 ^ P ) - 1 ) + 1 ) = ( 2 ^ P ) )
16 7 15 eqtrd 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 1 sigma ( ( 2 ^ P ) - 1 ) ) = ( 2 ^ P ) )
17 5 16 oveq12d 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( 1 sigma ( 2 ^ ( P - 1 ) ) ) x. ( 1 sigma ( ( 2 ^ P ) - 1 ) ) ) = ( ( ( 2 ^ P ) - 1 ) x. ( 2 ^ P ) ) )
18 13 a1i 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> 1 e. CC )
19 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
20 3 19 syl 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( P - 1 ) e. NN0 )
21 nnexpcl 
 |-  ( ( 2 e. NN /\ ( P - 1 ) e. NN0 ) -> ( 2 ^ ( P - 1 ) ) e. NN )
22 8 20 21 sylancr 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 2 ^ ( P - 1 ) ) e. NN )
23 prmnn 
 |-  ( ( ( 2 ^ P ) - 1 ) e. Prime -> ( ( 2 ^ P ) - 1 ) e. NN )
24 23 adantl 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( 2 ^ P ) - 1 ) e. NN )
25 22 nnzd 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 2 ^ ( P - 1 ) ) e. ZZ )
26 prmz 
 |-  ( ( ( 2 ^ P ) - 1 ) e. Prime -> ( ( 2 ^ P ) - 1 ) e. ZZ )
27 26 adantl 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( 2 ^ P ) - 1 ) e. ZZ )
28 25 27 gcdcomd 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( 2 ^ ( P - 1 ) ) gcd ( ( 2 ^ P ) - 1 ) ) = ( ( ( 2 ^ P ) - 1 ) gcd ( 2 ^ ( P - 1 ) ) ) )
29 iddvds 
 |-  ( ( ( 2 ^ P ) - 1 ) e. ZZ -> ( ( 2 ^ P ) - 1 ) || ( ( 2 ^ P ) - 1 ) )
30 27 29 syl 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( 2 ^ P ) - 1 ) || ( ( 2 ^ P ) - 1 ) )
31 prmuz2 
 |-  ( ( ( 2 ^ P ) - 1 ) e. Prime -> ( ( 2 ^ P ) - 1 ) e. ( ZZ>= ` 2 ) )
32 31 adantl 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( 2 ^ P ) - 1 ) e. ( ZZ>= ` 2 ) )
33 eluz2gt1 
 |-  ( ( ( 2 ^ P ) - 1 ) e. ( ZZ>= ` 2 ) -> 1 < ( ( 2 ^ P ) - 1 ) )
34 32 33 syl 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> 1 < ( ( 2 ^ P ) - 1 ) )
35 ndvdsp1 
 |-  ( ( ( ( 2 ^ P ) - 1 ) e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. NN /\ 1 < ( ( 2 ^ P ) - 1 ) ) -> ( ( ( 2 ^ P ) - 1 ) || ( ( 2 ^ P ) - 1 ) -> -. ( ( 2 ^ P ) - 1 ) || ( ( ( 2 ^ P ) - 1 ) + 1 ) ) )
36 27 24 34 35 syl3anc 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( ( 2 ^ P ) - 1 ) || ( ( 2 ^ P ) - 1 ) -> -. ( ( 2 ^ P ) - 1 ) || ( ( ( 2 ^ P ) - 1 ) + 1 ) ) )
37 30 36 mpd 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> -. ( ( 2 ^ P ) - 1 ) || ( ( ( 2 ^ P ) - 1 ) + 1 ) )
38 2z 
 |-  2 e. ZZ
39 38 a1i 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> 2 e. ZZ )
40 dvdsmultr1 
 |-  ( ( ( ( 2 ^ P ) - 1 ) e. ZZ /\ ( 2 ^ ( P - 1 ) ) e. ZZ /\ 2 e. ZZ ) -> ( ( ( 2 ^ P ) - 1 ) || ( 2 ^ ( P - 1 ) ) -> ( ( 2 ^ P ) - 1 ) || ( ( 2 ^ ( P - 1 ) ) x. 2 ) ) )
41 27 25 39 40 syl3anc 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( ( 2 ^ P ) - 1 ) || ( 2 ^ ( P - 1 ) ) -> ( ( 2 ^ P ) - 1 ) || ( ( 2 ^ ( P - 1 ) ) x. 2 ) ) )
42 2cn 
 |-  2 e. CC
43 expm1t 
 |-  ( ( 2 e. CC /\ P e. NN ) -> ( 2 ^ P ) = ( ( 2 ^ ( P - 1 ) ) x. 2 ) )
44 42 3 43 sylancr 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 2 ^ P ) = ( ( 2 ^ ( P - 1 ) ) x. 2 ) )
45 15 44 eqtr2d 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( 2 ^ ( P - 1 ) ) x. 2 ) = ( ( ( 2 ^ P ) - 1 ) + 1 ) )
46 45 breq2d 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( ( 2 ^ P ) - 1 ) || ( ( 2 ^ ( P - 1 ) ) x. 2 ) <-> ( ( 2 ^ P ) - 1 ) || ( ( ( 2 ^ P ) - 1 ) + 1 ) ) )
47 41 46 sylibd 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( ( 2 ^ P ) - 1 ) || ( 2 ^ ( P - 1 ) ) -> ( ( 2 ^ P ) - 1 ) || ( ( ( 2 ^ P ) - 1 ) + 1 ) ) )
48 37 47 mtod 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> -. ( ( 2 ^ P ) - 1 ) || ( 2 ^ ( P - 1 ) ) )
49 simpr 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( 2 ^ P ) - 1 ) e. Prime )
50 coprm 
 |-  ( ( ( ( 2 ^ P ) - 1 ) e. Prime /\ ( 2 ^ ( P - 1 ) ) e. ZZ ) -> ( -. ( ( 2 ^ P ) - 1 ) || ( 2 ^ ( P - 1 ) ) <-> ( ( ( 2 ^ P ) - 1 ) gcd ( 2 ^ ( P - 1 ) ) ) = 1 ) )
51 49 25 50 syl2anc 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( -. ( ( 2 ^ P ) - 1 ) || ( 2 ^ ( P - 1 ) ) <-> ( ( ( 2 ^ P ) - 1 ) gcd ( 2 ^ ( P - 1 ) ) ) = 1 ) )
52 48 51 mpbid 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( ( 2 ^ P ) - 1 ) gcd ( 2 ^ ( P - 1 ) ) ) = 1 )
53 28 52 eqtrd 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( 2 ^ ( P - 1 ) ) gcd ( ( 2 ^ P ) - 1 ) ) = 1 )
54 sgmmul 
 |-  ( ( 1 e. CC /\ ( ( 2 ^ ( P - 1 ) ) e. NN /\ ( ( 2 ^ P ) - 1 ) e. NN /\ ( ( 2 ^ ( P - 1 ) ) gcd ( ( 2 ^ P ) - 1 ) ) = 1 ) ) -> ( 1 sigma ( ( 2 ^ ( P - 1 ) ) x. ( ( 2 ^ P ) - 1 ) ) ) = ( ( 1 sigma ( 2 ^ ( P - 1 ) ) ) x. ( 1 sigma ( ( 2 ^ P ) - 1 ) ) ) )
55 18 22 24 53 54 syl13anc 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 1 sigma ( ( 2 ^ ( P - 1 ) ) x. ( ( 2 ^ P ) - 1 ) ) ) = ( ( 1 sigma ( 2 ^ ( P - 1 ) ) ) x. ( 1 sigma ( ( 2 ^ P ) - 1 ) ) ) )
56 subcl 
 |-  ( ( ( 2 ^ P ) e. CC /\ 1 e. CC ) -> ( ( 2 ^ P ) - 1 ) e. CC )
57 12 13 56 sylancl 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( 2 ^ P ) - 1 ) e. CC )
58 12 57 mulcomd 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( ( 2 ^ P ) x. ( ( 2 ^ P ) - 1 ) ) = ( ( ( 2 ^ P ) - 1 ) x. ( 2 ^ P ) ) )
59 17 55 58 3eqtr4d 
 |-  ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 1 sigma ( ( 2 ^ ( P - 1 ) ) x. ( ( 2 ^ P ) - 1 ) ) ) = ( ( 2 ^ P ) x. ( ( 2 ^ P ) - 1 ) ) )