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 \in ℤ \land 2^{P} - 1 \in ℙ) \to 1 σ 2^{P - 1} (2^{P} - 1) = 2^{P} (2^{P} - 1)$

Proof

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

Metamath Proof Explorer

Theorem perfect1

Proof