Theorem jm3.1lem3

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

	Ref	Expression
Hypotheses	jm3.1.a	|- ( ph -> A e. ( ZZ>= ` 2 ) )
	jm3.1.b	|- ( ph -> K e. ( ZZ>= ` 2 ) )
	jm3.1.c	|- ( ph -> N e. NN )
	jm3.1.d	|- ( ph -> ( K rmY ( N + 1 ) ) <_ A )
Assertion	jm3.1lem3	|- ( ph -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		jm3.1.a	|- ( ph -> A e. ( ZZ>= ` 2 ) )
2		jm3.1.b	|- ( ph -> K e. ( ZZ>= ` 2 ) )
3		jm3.1.c	|- ( ph -> N e. NN )
4		jm3.1.d	|- ( ph -> ( K rmY ( N + 1 ) ) <_ A )
5		2z	|- 2 e. ZZ
6		eluzelz	|- ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )
7	1 6	syl	|- ( ph -> A e. ZZ )
8		zmulcl	|- ( ( 2 e. ZZ /\ A e. ZZ ) -> ( 2 x. A ) e. ZZ )
9	5 7 8	sylancr	|- ( ph -> ( 2 x. A ) e. ZZ )
10		eluz2nn	|- ( K e. ( ZZ>= ` 2 ) -> K e. NN )
11	2 10	syl	|- ( ph -> K e. NN )
12	11	nnzd	|- ( ph -> K e. ZZ )
13	9 12	zmulcld	|- ( ph -> ( ( 2 x. A ) x. K ) e. ZZ )
14		zsqcl	|- ( K e. ZZ -> ( K ^ 2 ) e. ZZ )
15	12 14	syl	|- ( ph -> ( K ^ 2 ) e. ZZ )
16	13 15	zsubcld	|- ( ph -> ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) e. ZZ )
17		peano2zm	|- ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) e. ZZ -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ )
18	16 17	syl	|- ( ph -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ )
19		0red	|- ( ph -> 0 e. RR )
20	3	nnnn0d	|- ( ph -> N e. NN0 )
21	11 20	nnexpcld	|- ( ph -> ( K ^ N ) e. NN )
22	21	nnred	|- ( ph -> ( K ^ N ) e. RR )
23	18	zred	|- ( ph -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. RR )
24	21	nngt0d	|- ( ph -> 0 < ( K ^ N ) )
25	1 2 3 4	jm3.1lem2	|- ( ph -> ( K ^ N ) < ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) )
26	19 22 23 24 25	lttrd	|- ( ph -> 0 < ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) )
27		elnnz	|- ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. NN <-> ( ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. ZZ /\ 0 < ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) ) )
28	18 26 27	sylanbrc	|- ( ph -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. NN )