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 2 P 1 1 σ 2 P 1 2 P 1 = 2 P 2 P 1

Proof

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