Metamath Proof Explorer

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 ) ∈ ℕ ) )