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	⊢ ( ( 𝑁 ∈ ℕ ∧ 2 ∥ 𝑁 ) → ( ( 1 σ 𝑁 ) = ( 2 · 𝑁 ) ↔ ∃ 𝑝 ∈ ℤ ( ( ( 2 ↑ 𝑝 ) − 1 ) ∈ ℙ ∧ 𝑁 = ( ( 2 ↑ ( 𝑝 − 1 ) ) · ( ( 2 ↑ 𝑝 ) − 1 ) ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem perfect

Proof