Theorem jm3.1lem3

Description: Lemma for jm3.1 . (Contributed by Stefan O'Rear, 17-Oct-2014)

	Ref	Expression
Hypotheses	jm3.1.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
	jm3.1.b	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
	jm3.1.c	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	jm3.1.d	⊢ ( 𝜑 → ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 )
Assertion	jm3.1lem3	⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		jm3.1.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
2		jm3.1.b	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
3		jm3.1.c	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		jm3.1.d	⊢ ( 𝜑 → ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 )
5		2z	⊢ 2 ∈ ℤ
6		eluzelz	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℤ )
7	1 6	syl	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
8		zmulcl	⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 2 · 𝐴 ) ∈ ℤ )
9	5 7 8	sylancr	⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℤ )
10		eluz2nn	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℕ )
11	2 10	syl	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
12	11	nnzd	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
13	9 12	zmulcld	⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · 𝐾 ) ∈ ℤ )
14		zsqcl	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 ↑ 2 ) ∈ ℤ )
15	12 14	syl	⊢ ( 𝜑 → ( 𝐾 ↑ 2 ) ∈ ℤ )
16	13 15	zsubcld	⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) ∈ ℤ )
17		peano2zm	⊢ ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) ∈ ℤ → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∈ ℤ )
18	16 17	syl	⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∈ ℤ )
19		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
20	3	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
21	11 20	nnexpcld	⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) ∈ ℕ )
22	21	nnred	⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) ∈ ℝ )
23	18	zred	⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∈ ℝ )
24	21	nngt0d	⊢ ( 𝜑 → 0 < ( 𝐾 ↑ 𝑁 ) )
25	1 2 3 4	jm3.1lem2	⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) < ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) )
26	19 22 23 24 25	lttrd	⊢ ( 𝜑 → 0 < ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) )
27		elnnz	⊢ ( ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∈ ℕ ↔ ( ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∈ ℤ ∧ 0 < ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ) )
28	18 26 27	sylanbrc	⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∈ ℕ )