Theorem jm3.1lem1

Description: Lemma for jm3.1 . (Contributed by Stefan O'Rear, 16-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.1lem1	$$⊢\phi \to K^N<A$$

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		eluzelre	$$⊢K\in {\mathbb{Z}}_{\ge 2}\to K\in ℝ$$
6	2 5	syl	$$⊢\phi \to K\in ℝ$$
7	3	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
8	6 7	reexpcld	$$⊢\phi \to K^N\in ℝ$$
9		2z	$$⊢2\in \mathbb{Z}$$
10		uzid	$$⊢2\in \mathbb{Z}\to 2\in {\mathbb{Z}}_{\ge 2}$$
11	9 10	ax-mp	$$⊢2\in {\mathbb{Z}}_{\ge 2}$$
12		uz2mulcl	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge K\in {\mathbb{Z}}_{\ge 2}\right)\to 2K\in {\mathbb{Z}}_{\ge 2}$$
13	11 2 12	sylancr	$$⊢\phi \to 2K\in {\mathbb{Z}}_{\ge 2}$$
14		uz2m1nn	$$⊢2K\in {\mathbb{Z}}_{\ge 2}\to 2K-1\in \mathbb{N}$$
15	13 14	syl	$$⊢\phi \to 2K-1\in \mathbb{N}$$
16	15	nnred	$$⊢\phi \to 2K-1\in ℝ$$
17	16 7	reexpcld	$$⊢\phi \to {\left(2K-1\right)}^N\in ℝ$$
18		eluzelre	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in ℝ$$
19	1 18	syl	$$⊢\phi \to A\in ℝ$$
20		uz2m1nn	$$⊢K\in {\mathbb{Z}}_{\ge 2}\to K-1\in \mathbb{N}$$
21	2 20	syl	$$⊢\phi \to K-1\in \mathbb{N}$$
22	21	nngt0d	$$⊢\phi \to 0<K-1$$
23		2cn	$$⊢2\in ℂ$$
24	6	recnd	$$⊢\phi \to K\in ℂ$$
25		mulcl	$$⊢\left(2\in ℂ\wedge K\in ℂ\right)\to 2K\in ℂ$$
26	23 24 25	sylancr	$$⊢\phi \to 2K\in ℂ$$
27		1cnd	$$⊢\phi \to 1\in ℂ$$
28	26 27 24	sub32d	$$⊢\phi \to 2K-1-K=2K-K-1$$
29	24	2timesd	$$⊢\phi \to 2K=K+K$$
30	24 24 29	mvrladdd	$$⊢\phi \to 2K-K=K$$
31	30	oveq1d	$$⊢\phi \to 2K-K-1=K-1$$
32	28 31	eqtrd	$$⊢\phi \to 2K-1-K=K-1$$
33	22 32	breqtrrd	$$⊢\phi \to 0<2K-1-K$$
34	6 16	posdifd	$$⊢\phi \to \left(K<2K-1\leftrightarrow 0<2K-1-K\right)$$
35	33 34	mpbird	$$⊢\phi \to K<2K-1$$
36		eluz2nn	$$⊢K\in {\mathbb{Z}}_{\ge 2}\to K\in \mathbb{N}$$
37	2 36	syl	$$⊢\phi \to K\in \mathbb{N}$$
38	37	nnrpd	$$⊢\phi \to K\in {ℝ}^{+}$$
39	15	nnrpd	$$⊢\phi \to 2K-1\in {ℝ}^{+}$$
40		rpexpmord	$$⊢\left(N\in \mathbb{N}\wedge K\in {ℝ}^{+}\wedge 2K-1\in {ℝ}^{+}\right)\to \left(K<2K-1\leftrightarrow K^N<{\left(2K-1\right)}^N\right)$$
41	3 38 39 40	syl3anc	$$⊢\phi \to \left(K<2K-1\leftrightarrow K^N<{\left(2K-1\right)}^N\right)$$
42	35 41	mpbid	$$⊢\phi \to K^N<{\left(2K-1\right)}^N$$
43	3	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
44	43	peano2zd	$$⊢\phi \to N+1\in \mathbb{Z}$$
45		frmy	$$⊢Y_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶\mathbb{Z}$$
46	45	fovcl	$$⊢\left(K\in {\mathbb{Z}}_{\ge 2}\wedge N+1\in \mathbb{Z}\right)\to K{Y}_{\mathrm{rm}}\left(N+1\right)\in \mathbb{Z}$$
47	2 44 46	syl2anc	$$⊢\phi \to K{Y}_{\mathrm{rm}}\left(N+1\right)\in \mathbb{Z}$$
48	47	zred	$$⊢\phi \to K{Y}_{\mathrm{rm}}\left(N+1\right)\in ℝ$$
49		jm2.17a	$$⊢\left(K\in {\mathbb{Z}}_{\ge 2}\wedge N\in {\mathbb{N}}_0\right)\to {\left(2K-1\right)}^N\le K{Y}_{\mathrm{rm}}\left(N+1\right)$$
50	2 7 49	syl2anc	$$⊢\phi \to {\left(2K-1\right)}^N\le K{Y}_{\mathrm{rm}}\left(N+1\right)$$
51	17 48 19 50 4	letrd	$$⊢\phi \to {\left(2K-1\right)}^N\le A$$
52	8 17 19 42 51	ltletrd	$$⊢\phi \to K^N<A$$