Theorem jm3.1lem2

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.1lem2	$$⊢\phi \to K^N<2AK-K^2-1$$

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		eluzelre	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in ℝ$$
10	1 9	syl	$$⊢\phi \to A\in ℝ$$
11		2re	$$⊢2\in ℝ$$
12		remulcl	$$⊢\left(2\in ℝ\wedge A\in ℝ\right)\to 2A\in ℝ$$
13	11 10 12	sylancr	$$⊢\phi \to 2A\in ℝ$$
14	13 6	remulcld	$$⊢\phi \to 2AK\in ℝ$$
15	6	resqcld	$$⊢\phi \to K^2\in ℝ$$
16	14 15	resubcld	$$⊢\phi \to 2AK-K^2\in ℝ$$
17		1re	$$⊢1\in ℝ$$
18		resubcl	$$⊢\left(2AK-K^2\in ℝ\wedge 1\in ℝ\right)\to 2AK-K^2-1\in ℝ$$
19	16 17 18	sylancl	$$⊢\phi \to 2AK-K^2-1\in ℝ$$
20	1 2 3 4	jm3.1lem1	$$⊢\phi \to K^N<A$$
21	10 6	remulcld	$$⊢\phi \to AK\in ℝ$$
22		resubcl	$$⊢\left(K\in ℝ\wedge 1\in ℝ\right)\to K-1\in ℝ$$
23	6 17 22	sylancl	$$⊢\phi \to K-1\in ℝ$$
24	21 23	readdcld	$$⊢\phi \to AK+K-1\in ℝ$$
25		eluz2b1	$$⊢K\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(K\in \mathbb{Z}\wedge 1<K\right)$$
26	25	simprbi	$$⊢K\in {\mathbb{Z}}_{\ge 2}\to 1<K$$
27	2 26	syl	$$⊢\phi \to 1<K$$
28		eluz2nn	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{N}$$
29	1 28	syl	$$⊢\phi \to A\in \mathbb{N}$$
30	29	nngt0d	$$⊢\phi \to 0<A$$
31		ltmulgt11	$$⊢\left(A\in ℝ\wedge K\in ℝ\wedge 0<A\right)\to \left(1<K\leftrightarrow A<AK\right)$$
32	10 6 30 31	syl3anc	$$⊢\phi \to \left(1<K\leftrightarrow A<AK\right)$$
33	27 32	mpbid	$$⊢\phi \to A<AK$$
34		uz2m1nn	$$⊢K\in {\mathbb{Z}}_{\ge 2}\to K-1\in \mathbb{N}$$
35	2 34	syl	$$⊢\phi \to K-1\in \mathbb{N}$$
36	35	nnrpd	$$⊢\phi \to K-1\in {ℝ}^{+}$$
37	21 36	ltaddrpd	$$⊢\phi \to AK<AK+K-1$$
38	10 21 24 33 37	lttrd	$$⊢\phi \to A<AK+K-1$$
39		peano2re	$$⊢K\in ℝ\to K+1\in ℝ$$
40	6 39	syl	$$⊢\phi \to K+1\in ℝ$$
41	40 6	remulcld	$$⊢\phi \to \left(K+1\right)K\in ℝ$$
42		resubcl	$$⊢\left(AK\in ℝ\wedge 1\in ℝ\right)\to AK-1\in ℝ$$
43	21 17 42	sylancl	$$⊢\phi \to AK-1\in ℝ$$
44	43 15	resubcld	$$⊢\phi \to AK-1-K^2\in ℝ$$
45	6	recnd	$$⊢\phi \to K\in ℂ$$
46	45	exp1d	$$⊢\phi \to K^1=K$$
47		eluz2nn	$$⊢K\in {\mathbb{Z}}_{\ge 2}\to K\in \mathbb{N}$$
48	2 47	syl	$$⊢\phi \to K\in \mathbb{N}$$
49	48	nnge1d	$$⊢\phi \to 1\le K$$
50		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
51	3 50	eleqtrdi	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 1}$$
52	6 49 51	leexp2ad	$$⊢\phi \to K^1\le K^N$$
53	46 52	eqbrtrrd	$$⊢\phi \to K\le K^N$$
54	6 8 10 53 20	lelttrd	$$⊢\phi \to K<A$$
55		eluzelz	$$⊢K\in {\mathbb{Z}}_{\ge 2}\to K\in \mathbb{Z}$$
56	2 55	syl	$$⊢\phi \to K\in \mathbb{Z}$$
57		eluzelz	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{Z}$$
58	1 57	syl	$$⊢\phi \to A\in \mathbb{Z}$$
59		zltp1le	$$⊢\left(K\in \mathbb{Z}\wedge A\in \mathbb{Z}\right)\to \left(K<A\leftrightarrow K+1\le A\right)$$
60	56 58 59	syl2anc	$$⊢\phi \to \left(K<A\leftrightarrow K+1\le A\right)$$
61	54 60	mpbid	$$⊢\phi \to K+1\le A$$
62	48	nngt0d	$$⊢\phi \to 0<K$$
63		lemul1	$$⊢\left(K+1\in ℝ\wedge A\in ℝ\wedge \left(K\in ℝ\wedge 0<K\right)\right)\to \left(K+1\le A\leftrightarrow \left(K+1\right)K\le AK\right)$$
64	40 10 6 62 63	syl112anc	$$⊢\phi \to \left(K+1\le A\leftrightarrow \left(K+1\right)K\le AK\right)$$
65	61 64	mpbid	$$⊢\phi \to \left(K+1\right)K\le AK$$
66	41 21 44 65	leadd1dd	$$⊢\phi \to \left(K+1\right)K+\left(AK-1\right)-K^2\le AK+\left(AK-1\right)-K^2$$
67	21	recnd	$$⊢\phi \to AK\in ℂ$$
68	41 15	resubcld	$$⊢\phi \to \left(K+1\right)K-K^2\in ℝ$$
69	68	recnd	$$⊢\phi \to \left(K+1\right)K-K^2\in ℂ$$
70		1cnd	$$⊢\phi \to 1\in ℂ$$
71	67 69 70	addsub12d	$$⊢\phi \to AK+\left(\left(K+1\right)K-K^2\right)-1=\left(\left(K+1\right)K-K^2\right)+AK-1$$
72	45 70 45	adddird	$$⊢\phi \to \left(K+1\right)K=KK+1K$$
73	45	sqvald	$$⊢\phi \to K^2=KK$$
74	72 73	oveq12d	$$⊢\phi \to \left(K+1\right)K-K^2=KK+1K-KK$$
75	45 45	mulcld	$$⊢\phi \to KK\in ℂ$$
76		ax-1cn	$$⊢1\in ℂ$$
77		mulcl	$$⊢\left(1\in ℂ\wedge K\in ℂ\right)\to 1K\in ℂ$$
78	76 45 77	sylancr	$$⊢\phi \to 1K\in ℂ$$
79	75 78	pncan2d	$$⊢\phi \to KK+1K-KK=1K$$
80	45	mullidd	$$⊢\phi \to 1K=K$$
81	74 79 80	3eqtrd	$$⊢\phi \to \left(K+1\right)K-K^2=K$$
82	81	oveq1d	$$⊢\phi \to \left(K+1\right)K-K^2-1=K-1$$
83	82	oveq2d	$$⊢\phi \to AK+\left(\left(K+1\right)K-K^2\right)-1=AK+K-1$$
84	41	recnd	$$⊢\phi \to \left(K+1\right)K\in ℂ$$
85	15	recnd	$$⊢\phi \to K^2\in ℂ$$
86	43	recnd	$$⊢\phi \to AK-1\in ℂ$$
87	84 85 86	subadd23d	$$⊢\phi \to \left(\left(K+1\right)K-K^2\right)+AK-1=\left(K+1\right)K+\left(AK-1\right)-K^2$$
88	71 83 87	3eqtr3d	$$⊢\phi \to AK+K-1=\left(K+1\right)K+\left(AK-1\right)-K^2$$
89		2cnd	$$⊢\phi \to 2\in ℂ$$
90	10	recnd	$$⊢\phi \to A\in ℂ$$
91	89 90 45	mulassd	$$⊢\phi \to 2AK=2AK$$
92	67	2timesd	$$⊢\phi \to 2AK=AK+AK$$
93	91 92	eqtrd	$$⊢\phi \to 2AK=AK+AK$$
94	93	oveq1d	$$⊢\phi \to 2AK-K^2=AK+AK-K^2$$
95	94	oveq1d	$$⊢\phi \to 2AK-K^2-1=\left(AK+AK\right)-K^2-1$$
96	21 21	readdcld	$$⊢\phi \to AK+AK\in ℝ$$
97	96	recnd	$$⊢\phi \to AK+AK\in ℂ$$
98	97 85 70	sub32d	$$⊢\phi \to \left(AK+AK\right)-K^2-1=\left(AK+AK\right)-1-K^2$$
99	67 67 70	addsubassd	$$⊢\phi \to AK+AK-1=AK+AK-1$$
100	99	oveq1d	$$⊢\phi \to \left(AK+AK\right)-1-K^2=AK+\left(AK-1\right)-K^2$$
101	67 86 85	addsubassd	$$⊢\phi \to AK+\left(AK-1\right)-K^2=AK+\left(AK-1\right)-K^2$$
102	100 101	eqtrd	$$⊢\phi \to \left(AK+AK\right)-1-K^2=AK+\left(AK-1\right)-K^2$$
103	95 98 102	3eqtrd	$$⊢\phi \to 2AK-K^2-1=AK+\left(AK-1\right)-K^2$$
104	66 88 103	3brtr4d	$$⊢\phi \to AK+K-1\le 2AK-K^2-1$$
105	10 24 19 38 104	ltletrd	$$⊢\phi \to A<2AK-K^2-1$$
106	8 10 19 20 105	lttrd	$$⊢\phi \to K^N<2AK-K^2-1$$