Theorem jm3.1lem3

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

	Ref	Expression
Hypotheses	jm3.1.a	$$⊢\phi \to A\in {\mathbb{Z}}_{\ge 2}$$
	jm3.1.b	$$⊢\phi \to K\in {\mathbb{Z}}_{\ge 2}$$
	jm3.1.c	$$⊢\phi \to N\in \mathbb{N}$$
	jm3.1.d	$$⊢\phi \to K{Y}_{\mathrm{rm}}\left(N+1\right)\le A$$
Assertion	jm3.1lem3	$$⊢\phi \to 2AK-K^2-1\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		jm3.1.a	$$⊢\phi \to A\in {\mathbb{Z}}_{\ge 2}$$
2		jm3.1.b	$$⊢\phi \to K\in {\mathbb{Z}}_{\ge 2}$$
3		jm3.1.c	$$⊢\phi \to N\in \mathbb{N}$$
4		jm3.1.d	$$⊢\phi \to K{Y}_{\mathrm{rm}}\left(N+1\right)\le A$$
5		2z	$$⊢2\in \mathbb{Z}$$
6		eluzelz	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{Z}$$
7	1 6	syl	$$⊢\phi \to A\in \mathbb{Z}$$
8		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge A\in \mathbb{Z}\right)\to 2A\in \mathbb{Z}$$
9	5 7 8	sylancr	$$⊢\phi \to 2A\in \mathbb{Z}$$
10		eluz2nn	$$⊢K\in {\mathbb{Z}}_{\ge 2}\to K\in \mathbb{N}$$
11	2 10	syl	$$⊢\phi \to K\in \mathbb{N}$$
12	11	nnzd	$$⊢\phi \to K\in \mathbb{Z}$$
13	9 12	zmulcld	$$⊢\phi \to 2AK\in \mathbb{Z}$$
14		zsqcl	$$⊢K\in \mathbb{Z}\to K^2\in \mathbb{Z}$$
15	12 14	syl	$$⊢\phi \to K^2\in \mathbb{Z}$$
16	13 15	zsubcld	$$⊢\phi \to 2AK-K^2\in \mathbb{Z}$$
17		peano2zm	$$⊢2AK-K^2\in \mathbb{Z}\to 2AK-K^2-1\in \mathbb{Z}$$
18	16 17	syl	$$⊢\phi \to 2AK-K^2-1\in \mathbb{Z}$$
19		0red	$$⊢\phi \to 0\in ℝ$$
20	3	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
21	11 20	nnexpcld	$$⊢\phi \to K^N\in \mathbb{N}$$
22	21	nnred	$$⊢\phi \to K^N\in ℝ$$
23	18	zred	$$⊢\phi \to 2AK-K^2-1\in ℝ$$
24	21	nngt0d	$$⊢\phi \to 0<K^N$$
25	1 2 3 4	jm3.1lem2	$$⊢\phi \to K^N<2AK-K^2-1$$
26	19 22 23 24 25	lttrd	$$⊢\phi \to 0<2AK-K^2-1$$
27		elnnz	$$⊢2AK-K^2-1\in \mathbb{N}\leftrightarrow \left(2AK-K^2-1\in \mathbb{Z}\wedge 0<2AK-K^2-1\right)$$
28	18 26 27	sylanbrc	$$⊢\phi \to 2AK-K^2-1\in \mathbb{N}$$