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

Proof

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