proththdlem

	Ref	Expression
Hypotheses	proththd.n	$⊢ φ \to N \in ℕ$
	proththd.k	$⊢ φ \to K \in ℕ$
	proththd.p	$⊢ φ \to P = K 2^{N} + 1$
Assertion	proththdlem	$⊢ φ \to (P \in ℕ \land 1 < P \land \frac{P - 1}{2} \in ℕ)$

Proof

Step	Hyp	Ref	Expression
1		proththd.n	$⊢ φ \to N \in ℕ$
2		proththd.k	$⊢ φ \to K \in ℕ$
3		proththd.p	$⊢ φ \to P = K 2^{N} + 1$
4		2nn	$⊢ 2 \in ℕ$
5	4	a1i	$⊢ φ \to 2 \in ℕ$
6	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
7	5 6	nnexpcld	$⊢ φ \to 2^{N} \in ℕ$
8	2 7	nnmulcld	$⊢ φ \to K 2^{N} \in ℕ$
9	8	peano2nnd	$⊢ φ \to K 2^{N} + 1 \in ℕ$
10		1m1e0	$⊢ 1 - 1 = 0$
11	8	nngt0d	$⊢ φ \to 0 < K 2^{N}$
12	10 11	eqbrtrid	$⊢ φ \to 1 - 1 < K 2^{N}$
13		1red	$⊢ φ \to 1 \in ℝ$
14	8	nnred	$⊢ φ \to K 2^{N} \in ℝ$
15	13 13 14	ltsubaddd	$⊢ φ \to (1 - 1 < K 2^{N} \leftrightarrow 1 < K 2^{N} + 1)$
16	12 15	mpbid	$⊢ φ \to 1 < K 2^{N} + 1$
17	8	nncnd	$⊢ φ \to K 2^{N} \in ℂ$
18		pncan1	$⊢ K 2^{N} \in ℂ \to K 2^{N} + 1 - 1 = K 2^{N}$
19	17 18	syl	$⊢ φ \to K 2^{N} + 1 - 1 = K 2^{N}$
20	19	oveq1d	$⊢ φ \to \frac{K 2^{N} + 1 - 1}{2} = \frac{K 2^{N}}{2}$
21		2z	$⊢ 2 \in ℤ$
22	21	a1i	$⊢ φ \to 2 \in ℤ$
23	2	nnzd	$⊢ φ \to K \in ℤ$
24	7	nnzd	$⊢ φ \to 2^{N} \in ℤ$
25	22 23 24	3jca	$⊢ φ \to (2 \in ℤ \land K \in ℤ \land 2^{N} \in ℤ)$
26		iddvdsexp	$⊢ (2 \in ℤ \land N \in ℕ) \to 2 ∥ 2^{N}$
27	22 1 26	syl2anc	$⊢ φ \to 2 ∥ 2^{N}$
28		dvdsmultr2	$⊢ (2 \in ℤ \land K \in ℤ \land 2^{N} \in ℤ) \to (2 ∥ 2^{N} \to 2 ∥ K 2^{N})$
29	25 27 28	sylc	$⊢ φ \to 2 ∥ K 2^{N}$
30		nndivdvds	$⊢ (K 2^{N} \in ℕ \land 2 \in ℕ) \to (2 ∥ K 2^{N} \leftrightarrow \frac{K 2^{N}}{2} \in ℕ)$
31	8 5 30	syl2anc	$⊢ φ \to (2 ∥ K 2^{N} \leftrightarrow \frac{K 2^{N}}{2} \in ℕ)$
32	29 31	mpbid	$⊢ φ \to \frac{K 2^{N}}{2} \in ℕ$
33	20 32	eqeltrd	$⊢ φ \to \frac{K 2^{N} + 1 - 1}{2} \in ℕ$
34	9 16 33	3jca	$⊢ φ \to (K 2^{N} + 1 \in ℕ \land 1 < K 2^{N} + 1 \land \frac{K 2^{N} + 1 - 1}{2} \in ℕ)$
35		eleq1	$⊢ P = K 2^{N} + 1 \to (P \in ℕ \leftrightarrow K 2^{N} + 1 \in ℕ)$
36		breq2	$⊢ P = K 2^{N} + 1 \to (1 < P \leftrightarrow 1 < K 2^{N} + 1)$
37		oveq1	$⊢ P = K 2^{N} + 1 \to P - 1 = K 2^{N} + 1 - 1$
38	37	oveq1d	$⊢ P = K 2^{N} + 1 \to \frac{P - 1}{2} = \frac{K 2^{N} + 1 - 1}{2}$
39	38	eleq1d	$⊢ P = K 2^{N} + 1 \to (\frac{P - 1}{2} \in ℕ \leftrightarrow \frac{K 2^{N} + 1 - 1}{2} \in ℕ)$
40	35 36 39	3anbi123d	$⊢ P = K 2^{N} + 1 \to ((P \in ℕ \land 1 < P \land \frac{P - 1}{2} \in ℕ) \leftrightarrow (K 2^{N} + 1 \in ℕ \land 1 < K 2^{N} + 1 \land \frac{K 2^{N} + 1 - 1}{2} \in ℕ))$
41	34 40	syl5ibrcom	$⊢ φ \to (P = K 2^{N} + 1 \to (P \in ℕ \land 1 < P \land \frac{P - 1}{2} \in ℕ))$
42	3 41	mpd	$⊢ φ \to (P \in ℕ \land 1 < P \land \frac{P - 1}{2} \in ℕ)$

Metamath Proof Explorer

Theorem proththdlem

Proof