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 ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → ( 1 σ ( ( 2 ↑ ( 𝑃 − 1 ) ) · ( ( 2 ↑ 𝑃 ) − 1 ) ) ) = ( ( 2 ↑ 𝑃 ) · ( ( 2 ↑ 𝑃 ) − 1 ) ) )

Proof

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