jm3.1lem3

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

Metamath Proof Explorer