mersenne - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > mersenne		GIF version

Theorem mersenne 15317

Description: A Mersenne prime is a prime number of the form 2↑𝑃 − 1. This theorem shows that the 𝑃 in this expression is necessarily also prime. (Contributed by Mario Carneiro, 17-May-2016.)

**Assertion**
Ref	Expression
mersenne	⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 𝑃 ∈ ℙ)

Proof of Theorem mersenne Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 109	. . 3 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 𝑃 ∈ ℤ)
2		2nn0 9283	. . . . . . 7 ⊢ 2 ∈ ℕ₀
3	2	numexp1 12617	. . . . . 6 ⊢ (2↑1) = 2
4		df-2 9066	. . . . . 6 ⊢ 2 = (1 + 1)
5	3, 4	eqtri 2217	. . . . 5 ⊢ (2↑1) = (1 + 1)
6		prmuz2 12324	. . . . . . . 8 ⊢ (((2↑𝑃) − 1) ∈ ℙ → ((2↑𝑃) − 1) ∈ (ℤ_≥‘2))
7	6	adantl 277	. . . . . . 7 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → ((2↑𝑃) − 1) ∈ (ℤ_≥‘2))
8		eluz2gt1 9693	. . . . . . 7 ⊢ (((2↑𝑃) − 1) ∈ (ℤ_≥‘2) → 1 < ((2↑𝑃) − 1))
9	7, 8	syl 14	. . . . . 6 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 1 < ((2↑𝑃) − 1))
10		1red 8058	. . . . . . 7 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 1 ∈ ℝ)
11		2re 9077	. . . . . . . . 9 ⊢ 2 ∈ ℝ
12	11	a1i 9	. . . . . . . 8 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 2 ∈ ℝ)
13		2ap0 9100	. . . . . . . . 9 ⊢ 2 # 0
14	13	a1i 9	. . . . . . . 8 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 2 # 0)
15	12, 14, 1	reexpclzapd 10807	. . . . . . 7 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → (2↑𝑃) ∈ ℝ)
16	10, 10, 15	ltaddsubd 8589	. . . . . 6 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → ((1 + 1) < (2↑𝑃) ↔ 1 < ((2↑𝑃) − 1)))
17	9, 16	mpbird 167	. . . . 5 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → (1 + 1) < (2↑𝑃))
18	5, 17	eqbrtrid 4069	. . . 4 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → (2↑1) < (2↑𝑃))
19		1zzd 9370	. . . . 5 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 1 ∈ ℤ)
20		1lt2 9177	. . . . . 6 ⊢ 1 < 2
21	20	a1i 9	. . . . 5 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 1 < 2)
22	12, 19, 1, 21	ltexp2d 15262	. . . 4 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → (1 < 𝑃 ↔ (2↑1) < (2↑𝑃)))
23	18, 22	mpbird 167	. . 3 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 1 < 𝑃)
24		eluz2b1 9692	. . 3 ⊢ (𝑃 ∈ (ℤ_≥‘2) ↔ (𝑃 ∈ ℤ ∧ 1 < 𝑃))
25	1, 23, 24	sylanbrc 417	. 2 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 𝑃 ∈ (ℤ_≥‘2))
26		simpllr 534	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((2↑𝑃) − 1) ∈ ℙ)
27		prmnn 12303	. . . . . . . 8 ⊢ (((2↑𝑃) − 1) ∈ ℙ → ((2↑𝑃) − 1) ∈ ℕ)
28	26, 27	syl 14	. . . . . . 7 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((2↑𝑃) − 1) ∈ ℕ)
29	28	nncnd 9021	. . . . . 6 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((2↑𝑃) − 1) ∈ ℂ)
30		2nn 9169	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
31		elfzuz 10113	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (2...(𝑃 − 1)) → 𝑘 ∈ (ℤ_≥‘2))
32	31	ad2antlr 489	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ (ℤ_≥‘2))
33		eluz2nn 9657	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℕ)
34	32, 33	syl 14	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ ℕ)
35	34	nnnn0d 9319	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ ℕ₀)
36		nnexpcl 10661	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ₀) → (2↑𝑘) ∈ ℕ)
37	30, 35, 36	sylancr 414	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ∈ ℕ)
38	37	nnzd 9464	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ∈ ℤ)
39		peano2zm 9381	. . . . . . . . 9 ⊢ ((2↑𝑘) ∈ ℤ → ((2↑𝑘) − 1) ∈ ℤ)
40	38, 39	syl 14	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈ ℤ)
41	40	zred 9465	. . . . . . 7 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈ ℝ)
42	41	recnd 8072	. . . . . 6 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈ ℂ)
43		0red 8044	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 0 ∈ ℝ)
44		1red 8058	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 1 ∈ ℝ)
45		0lt1 8170	. . . . . . . . 9 ⊢ 0 < 1
46	45	a1i 9	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 0 < 1)
47		eluz2gt1 9693	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 1 < 𝑘)
48	32, 47	syl 14	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 1 < 𝑘)
49	11	a1i 9	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 2 ∈ ℝ)
50		1zzd 9370	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 1 ∈ ℤ)
51		elfzelz 10117	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (2...(𝑃 − 1)) → 𝑘 ∈ ℤ)
52	51	ad2antlr 489	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ ℤ)
53	20	a1i 9	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 1 < 2)
54	49, 50, 52, 53	ltexp2d 15262	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (1 < 𝑘 ↔ (2↑1) < (2↑𝑘)))
55	48, 54	mpbid 147	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (2↑1) < (2↑𝑘))
56	5, 55	eqbrtrrid 4070	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (1 + 1) < (2↑𝑘))
57	37	nnred 9020	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ∈ ℝ)
58	44, 44, 57	ltaddsubd 8589	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((1 + 1) < (2↑𝑘) ↔ 1 < ((2↑𝑘) − 1)))
59	56, 58	mpbid 147	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 1 < ((2↑𝑘) − 1))
60	43, 44, 41, 46, 59	lttrd 8169	. . . . . . 7 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 0 < ((2↑𝑘) − 1))
61	41, 60	gt0ap0d 8673	. . . . . 6 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) # 0)
62	29, 42, 61	divcanap2d 8836	. . . . 5 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (((2↑𝑘) − 1) · (((2↑𝑃) − 1) / ((2↑𝑘) − 1))) = ((2↑𝑃) − 1))
63	62, 26	eqeltrd 2273	. . . 4 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (((2↑𝑘) − 1) · (((2↑𝑃) − 1) / ((2↑𝑘) − 1))) ∈ ℙ)
64		elnnz 9353	. . . . . . 7 ⊢ (((2↑𝑘) − 1) ∈ ℕ ↔ (((2↑𝑘) − 1) ∈ ℤ ∧ 0 < ((2↑𝑘) − 1)))
65	40, 60, 64	sylanbrc 417	. . . . . 6 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈ ℕ)
66		eluz2b2 9694	. . . . . 6 ⊢ (((2↑𝑘) − 1) ∈ (ℤ_≥‘2) ↔ (((2↑𝑘) − 1) ∈ ℕ ∧ 1 < ((2↑𝑘) − 1)))
67	65, 59, 66	sylanbrc 417	. . . . 5 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) ∈ (ℤ_≥‘2))
68	37	nncnd 9021	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (2↑𝑘) ∈ ℂ)
69		ax-1cn 7989	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
70		subap0 8687	. . . . . . . . . . 11 ⊢ (((2↑𝑘) ∈ ℂ ∧ 1 ∈ ℂ) → (((2↑𝑘) − 1) # 0 ↔ (2↑𝑘) # 1))
71	68, 69, 70	sylancl 413	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (((2↑𝑘) − 1) # 0 ↔ (2↑𝑘) # 1))
72	61, 71	mpbid 147	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (2↑𝑘) # 1)
73		simpr 110	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 𝑘 ∥ 𝑃)
74		eluz2nn 9657	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ (ℤ_≥‘2) → 𝑃 ∈ ℕ)
75	25, 74	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 𝑃 ∈ ℕ)
76	75	ad2antrr 488	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 𝑃 ∈ ℕ)
77		nndivdvds 11978	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑘 ∥ 𝑃 ↔ (𝑃 / 𝑘) ∈ ℕ))
78	76, 34, 77	syl2anc 411	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (𝑘 ∥ 𝑃 ↔ (𝑃 / 𝑘) ∈ ℕ))
79	73, 78	mpbid 147	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (𝑃 / 𝑘) ∈ ℕ)
80	79	nnnn0d 9319	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (𝑃 / 𝑘) ∈ ℕ₀)
81	68, 72, 80	geoserap 11689	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → Σ𝑛 ∈ (0...((𝑃 / 𝑘) − 1))((2↑𝑘)↑𝑛) = ((1 − ((2↑𝑘)↑(𝑃 / 𝑘))) / (1 − (2↑𝑘))))
82	15	ad2antrr 488	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (2↑𝑃) ∈ ℝ)
83	82	recnd 8072	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (2↑𝑃) ∈ ℂ)
84		negsubdi2 8302	. . . . . . . . . . 11 ⊢ (((2↑𝑃) ∈ ℂ ∧ 1 ∈ ℂ) → -((2↑𝑃) − 1) = (1 − (2↑𝑃)))
85	83, 69, 84	sylancl 413	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → -((2↑𝑃) − 1) = (1 − (2↑𝑃)))
86	76	nncnd 9021	. . . . . . . . . . . . . 14 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 𝑃 ∈ ℂ)
87	34	nncnd 9021	. . . . . . . . . . . . . 14 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 𝑘 ∈ ℂ)
88	34	nnap0d 9053	. . . . . . . . . . . . . 14 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 𝑘 # 0)
89	86, 87, 88	divcanap2d 8836	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (𝑘 · (𝑃 / 𝑘)) = 𝑃)
90	89	oveq2d 5941	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (2↑(𝑘 · (𝑃 / 𝑘))) = (2↑𝑃))
91	49	recnd 8072	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 2 ∈ ℂ)
92	91, 80, 35	expmuld 10785	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (2↑(𝑘 · (𝑃 / 𝑘))) = ((2↑𝑘)↑(𝑃 / 𝑘)))
93	90, 92	eqtr3d 2231	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (2↑𝑃) = ((2↑𝑘)↑(𝑃 / 𝑘)))
94	93	oveq2d 5941	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (1 − (2↑𝑃)) = (1 − ((2↑𝑘)↑(𝑃 / 𝑘))))
95	85, 94	eqtrd 2229	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → -((2↑𝑃) − 1) = (1 − ((2↑𝑘)↑(𝑃 / 𝑘))))
96		negsubdi2 8302	. . . . . . . . . 10 ⊢ (((2↑𝑘) ∈ ℂ ∧ 1 ∈ ℂ) → -((2↑𝑘) − 1) = (1 − (2↑𝑘)))
97	68, 69, 96	sylancl 413	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → -((2↑𝑘) − 1) = (1 − (2↑𝑘)))
98	95, 97	oveq12d 5943	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (-((2↑𝑃) − 1) / -((2↑𝑘) − 1)) = ((1 − ((2↑𝑘)↑(𝑃 / 𝑘))) / (1 − (2↑𝑘))))
99	29, 42, 61	div2negapd 8849	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (-((2↑𝑃) − 1) / -((2↑𝑘) − 1)) = (((2↑𝑃) − 1) / ((2↑𝑘) − 1)))
100	81, 98, 99	3eqtr2d 2235	. . . . . . 7 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → Σ𝑛 ∈ (0...((𝑃 / 𝑘) − 1))((2↑𝑘)↑𝑛) = (((2↑𝑃) − 1) / ((2↑𝑘) − 1)))
101		0zd 9355	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 0 ∈ ℤ)
102	79	nnzd 9464	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (𝑃 / 𝑘) ∈ ℤ)
103	102, 50	zsubcld 9470	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((𝑃 / 𝑘) − 1) ∈ ℤ)
104	101, 103	fzfigd 10540	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (0...((𝑃 / 𝑘) − 1)) ∈ Fin)
105		elfznn0 10206	. . . . . . . . 9 ⊢ (𝑛 ∈ (0...((𝑃 / 𝑘) − 1)) → 𝑛 ∈ ℕ₀)
106		zexpcl 10663	. . . . . . . . 9 ⊢ (((2↑𝑘) ∈ ℤ ∧ 𝑛 ∈ ℕ₀) → ((2↑𝑘)↑𝑛) ∈ ℤ)
107	38, 105, 106	syl2an 289	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) ∧ 𝑛 ∈ (0...((𝑃 / 𝑘) − 1))) → ((2↑𝑘)↑𝑛) ∈ ℤ)
108	104, 107	fsumzcl 11584	. . . . . . 7 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → Σ𝑛 ∈ (0...((𝑃 / 𝑘) − 1))((2↑𝑘)↑𝑛) ∈ ℤ)
109	100, 108	eqeltrrd 2274	. . . . . 6 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈ ℤ)
110	42	mullidd 8061	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (1 · ((2↑𝑘) − 1)) = ((2↑𝑘) − 1))
111		2z 9371	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℤ
112		elfzm11 10183	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑘 ∈ (2...(𝑃 − 1)) ↔ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ∧ 𝑘 < 𝑃)))
113	111, 1, 112	sylancr 414	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → (𝑘 ∈ (2...(𝑃 − 1)) ↔ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ∧ 𝑘 < 𝑃)))
114	113	biimpa 296	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) → (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ∧ 𝑘 < 𝑃))
115	114	simp3d 1013	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) → 𝑘 < 𝑃)
116	115	adantr 276	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 𝑘 < 𝑃)
117	1	ad2antrr 488	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 𝑃 ∈ ℤ)
118	49, 52, 117, 53	ltexp2d 15262	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (𝑘 < 𝑃 ↔ (2↑𝑘) < (2↑𝑃)))
119	116, 118	mpbid 147	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (2↑𝑘) < (2↑𝑃))
120	57, 82, 44, 119	ltsub1dd 8601	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((2↑𝑘) − 1) < ((2↑𝑃) − 1))
121	110, 120	eqbrtrd 4056	. . . . . . 7 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (1 · ((2↑𝑘) − 1)) < ((2↑𝑃) − 1))
122	28	nnred 9020	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((2↑𝑃) − 1) ∈ ℝ)
123		ltmuldiv 8918	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ ((2↑𝑃) − 1) ∈ ℝ ∧ (((2↑𝑘) − 1) ∈ ℝ ∧ 0 < ((2↑𝑘) − 1))) → ((1 · ((2↑𝑘) − 1)) < ((2↑𝑃) − 1) ↔ 1 < (((2↑𝑃) − 1) / ((2↑𝑘) − 1))))
124	44, 122, 41, 60, 123	syl112anc 1253	. . . . . . 7 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ((1 · ((2↑𝑘) − 1)) < ((2↑𝑃) − 1) ↔ 1 < (((2↑𝑃) − 1) / ((2↑𝑘) − 1))))
125	121, 124	mpbid 147	. . . . . 6 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → 1 < (((2↑𝑃) − 1) / ((2↑𝑘) − 1)))
126		eluz2b1 9692	. . . . . 6 ⊢ ((((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈ (ℤ_≥‘2) ↔ ((((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈ ℤ ∧ 1 < (((2↑𝑃) − 1) / ((2↑𝑘) − 1))))
127	109, 125, 126	sylanbrc 417	. . . . 5 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → (((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈ (ℤ_≥‘2))
128		nprm 12316	. . . . 5 ⊢ ((((2↑𝑘) − 1) ∈ (ℤ_≥‘2) ∧ (((2↑𝑃) − 1) / ((2↑𝑘) − 1)) ∈ (ℤ_≥‘2)) → ¬ (((2↑𝑘) − 1) · (((2↑𝑃) − 1) / ((2↑𝑘) − 1))) ∈ ℙ)
129	67, 127, 128	syl2anc 411	. . . 4 ⊢ ((((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) ∧ 𝑘 ∥ 𝑃) → ¬ (((2↑𝑘) − 1) · (((2↑𝑃) − 1) / ((2↑𝑘) − 1))) ∈ ℙ)
130	63, 129	pm2.65da 662	. . 3 ⊢ (((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) ∧ 𝑘 ∈ (2...(𝑃 − 1))) → ¬ 𝑘 ∥ 𝑃)
131	130	ralrimiva 2570	. 2 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → ∀𝑘 ∈ (2...(𝑃 − 1)) ¬ 𝑘 ∥ 𝑃)
132		isprm3 12311	. 2 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ_≥‘2) ∧ ∀𝑘 ∈ (2...(𝑃 − 1)) ¬ 𝑘 ∥ 𝑃))
133	25, 131, 132	sylanbrc 417	1 ⊢ ((𝑃 ∈ ℤ ∧ ((2↑𝑃) − 1) ∈ ℙ) → 𝑃 ∈ ℙ)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 980 = wceq 1364 ∈ wcel 2167 ∀wral 2475 class class class wbr 4034 ‘cfv 5259 (class class class)co 5925 ℂcc 7894 ℝcr 7895 0cc0 7896 1c1 7897 + caddc 7899 · cmul 7901 < clt 8078 ≤ cle 8079 − cmin 8214 -cneg 8215 # cap 8625 / cdiv 8716 ℕcn 9007 2c2 9058 ℕ₀cn0 9266 ℤcz 9343 ℤ_≥cuz 9618 ...cfz 10100 ↑cexp 10647 Σcsu 11535 ∥ cdvds 11969 ℙcprime 12300

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7987 ax-resscn 7988 ax-1cn 7989 ax-1re 7990 ax-icn 7991 ax-addcl 7992 ax-addrcl 7993 ax-mulcl 7994 ax-mulrcl 7995 ax-addcom 7996 ax-mulcom 7997 ax-addass 7998 ax-mulass 7999 ax-distr 8000 ax-i2m1 8001 ax-0lt1 8002 ax-1rid 8003 ax-0id 8004 ax-rnegex 8005 ax-precex 8006 ax-cnre 8007 ax-pre-ltirr 8008 ax-pre-ltwlin 8009 ax-pre-lttrn 8010 ax-pre-apti 8011 ax-pre-ltadd 8012 ax-pre-mulgt0 8013 ax-pre-mulext 8014 ax-arch 8015 ax-caucvg 8016 ax-pre-suploc 8017 ax-addf 8018 ax-mulf 8019

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-disj 4012 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-isom 5268 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-of 6139 df-1st 6207 df-2nd 6208 df-recs 6372 df-irdg 6437 df-frec 6458 df-1o 6483 df-2o 6484 df-oadd 6487 df-er 6601 df-map 6718 df-pm 6719 df-en 6809 df-dom 6810 df-fin 6811 df-sup 7059 df-inf 7060 df-pnf 8080 df-mnf 8081 df-xr 8082 df-ltxr 8083 df-le 8084 df-sub 8216 df-neg 8217 df-reap 8619 df-ap 8626 df-div 8717 df-inn 9008 df-2 9066 df-3 9067 df-4 9068 df-n0 9267 df-z 9344 df-uz 9619 df-q 9711 df-rp 9746 df-xneg 9864 df-xadd 9865 df-ioo 9984 df-ico 9986 df-icc 9987 df-fz 10101 df-fzo 10235 df-seqfrec 10557 df-exp 10648 df-fac 10835 df-bc 10857 df-ihash 10885 df-shft 10997 df-cj 11024 df-re 11025 df-im 11026 df-rsqrt 11180 df-abs 11181 df-clim 11461 df-sumdc 11536 df-ef 11830 df-e 11831 df-dvds 11970 df-prm 12301 df-rest 12943 df-topgen 12962 df-psmet 14175 df-xmet 14176 df-met 14177 df-bl 14178 df-mopn 14179 df-top 14318 df-topon 14331 df-bases 14363 df-ntr 14416 df-cn 14508 df-cnp 14509 df-tx 14573 df-cncf 14891 df-limced 14976 df-dvap 14977 df-relog 15178 df-rpcxp 15179

This theorem is referenced by: perfect1 15318 perfect 15321

W3C validator