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 
|- ( 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.1lem2 
|- ( ph -> ( K ^ N ) < ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) )

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