# Metamath Proof Explorer

## 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 {ℤ}_{\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.1lem2 ${⊢}{\phi }\to {{K}}^{{N}}<2{A}{K}-{{K}}^{2}-1$

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