Theorem proththdlem

Description: Lemma for proththd . (Contributed by AV, 4-Jul-2020)

	Ref	Expression
Hypotheses	proththd.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	proththd.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
	proththd.p	⊢ ( 𝜑 → 𝑃 = ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) )
Assertion	proththdlem	⊢ ( 𝜑 → ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		proththd.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		proththd.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3		proththd.p	⊢ ( 𝜑 → 𝑃 = ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) )
4		2nn	⊢ 2 ∈ ℕ
5	4	a1i	⊢ ( 𝜑 → 2 ∈ ℕ )
6	1	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7	5 6	nnexpcld	⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℕ )
8	2 7	nnmulcld	⊢ ( 𝜑 → ( 𝐾 · ( 2 ↑ 𝑁 ) ) ∈ ℕ )
9	8	peano2nnd	⊢ ( 𝜑 → ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) ∈ ℕ )
10		1m1e0	⊢ ( 1 − 1 ) = 0
11	8	nngt0d	⊢ ( 𝜑 → 0 < ( 𝐾 · ( 2 ↑ 𝑁 ) ) )
12	10 11	eqbrtrid	⊢ ( 𝜑 → ( 1 − 1 ) < ( 𝐾 · ( 2 ↑ 𝑁 ) ) )
13		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
14	8	nnred	⊢ ( 𝜑 → ( 𝐾 · ( 2 ↑ 𝑁 ) ) ∈ ℝ )
15	13 13 14	ltsubaddd	⊢ ( 𝜑 → ( ( 1 − 1 ) < ( 𝐾 · ( 2 ↑ 𝑁 ) ) ↔ 1 < ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) ) )
16	12 15	mpbid	⊢ ( 𝜑 → 1 < ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) )
17	8	nncnd	⊢ ( 𝜑 → ( 𝐾 · ( 2 ↑ 𝑁 ) ) ∈ ℂ )
18		pncan1	⊢ ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) ∈ ℂ → ( ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) = ( 𝐾 · ( 2 ↑ 𝑁 ) ) )
19	17 18	syl	⊢ ( 𝜑 → ( ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) = ( 𝐾 · ( 2 ↑ 𝑁 ) ) )
20	19	oveq1d	⊢ ( 𝜑 → ( ( ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) / 2 ) = ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) / 2 ) )
21		2z	⊢ 2 ∈ ℤ
22	21	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
23	2	nnzd	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
24	7	nnzd	⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℤ )
25	22 23 24	3jca	⊢ ( 𝜑 → ( 2 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 2 ↑ 𝑁 ) ∈ ℤ ) )
26		iddvdsexp	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 2 ∥ ( 2 ↑ 𝑁 ) )
27	22 1 26	syl2anc	⊢ ( 𝜑 → 2 ∥ ( 2 ↑ 𝑁 ) )
28		dvdsmultr2	⊢ ( ( 2 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 2 ↑ 𝑁 ) ∈ ℤ ) → ( 2 ∥ ( 2 ↑ 𝑁 ) → 2 ∥ ( 𝐾 · ( 2 ↑ 𝑁 ) ) ) )
29	25 27 28	sylc	⊢ ( 𝜑 → 2 ∥ ( 𝐾 · ( 2 ↑ 𝑁 ) ) )
30		nndivdvds	⊢ ( ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) ∈ ℕ ∧ 2 ∈ ℕ ) → ( 2 ∥ ( 𝐾 · ( 2 ↑ 𝑁 ) ) ↔ ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) / 2 ) ∈ ℕ ) )
31	8 5 30	syl2anc	⊢ ( 𝜑 → ( 2 ∥ ( 𝐾 · ( 2 ↑ 𝑁 ) ) ↔ ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) / 2 ) ∈ ℕ ) )
32	29 31	mpbid	⊢ ( 𝜑 → ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) / 2 ) ∈ ℕ )
33	20 32	eqeltrd	⊢ ( 𝜑 → ( ( ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) / 2 ) ∈ ℕ )
34	9 16 33	3jca	⊢ ( 𝜑 → ( ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) ∈ ℕ ∧ 1 < ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) ∧ ( ( ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) / 2 ) ∈ ℕ ) )
35		eleq1	⊢ ( 𝑃 = ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) → ( 𝑃 ∈ ℕ ↔ ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) ∈ ℕ ) )
36		breq2	⊢ ( 𝑃 = ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) → ( 1 < 𝑃 ↔ 1 < ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) ) )
37		oveq1	⊢ ( 𝑃 = ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) → ( 𝑃 − 1 ) = ( ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) )
38	37	oveq1d	⊢ ( 𝑃 = ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) → ( ( 𝑃 − 1 ) / 2 ) = ( ( ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) / 2 ) )
39	38	eleq1d	⊢ ( 𝑃 = ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) → ( ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ↔ ( ( ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) / 2 ) ∈ ℕ ) )
40	35 36 39	3anbi123d	⊢ ( 𝑃 = ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) → ( ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ) ↔ ( ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) ∈ ℕ ∧ 1 < ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) ∧ ( ( ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) / 2 ) ∈ ℕ ) ) )
41	34 40	syl5ibrcom	⊢ ( 𝜑 → ( 𝑃 = ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) → ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ) ) )
42	3 41	mpd	⊢ ( 𝜑 → ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ) )