# Metamath Proof Explorer

## 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 {ℤ}_{\ge 2}$
jm3.1.b ${⊢}{\phi }\to {K}\in {ℤ}_{\ge 2}$
jm3.1.c ${⊢}{\phi }\to {N}\in ℕ$
jm3.1.d ${⊢}{\phi }\to {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}$
Assertion jm3.1lem3 ${⊢}{\phi }\to 2{A}{K}-{{K}}^{2}-1\in ℕ$

### Proof

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