Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem1 Unicode version

Theorem stoweidlem1 27750
Description: Lemma for stoweid 27812. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 11227. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem1.1  |-  ( ph  ->  N  e.  NN )
stoweidlem1.2  |-  ( ph  ->  K  e.  NN )
stoweidlem1.3  |-  ( ph  ->  D  e.  RR+ )
stoweidlem1.5  |-  ( ph  ->  A  e.  RR+ )
stoweidlem1.6  |-  ( ph  ->  0  <_  A )
stoweidlem1.7  |-  ( ph  ->  A  <_  1 )
stoweidlem1.8  |-  ( ph  ->  D  <_  A )
Assertion
Ref Expression
stoweidlem1  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  <_  ( 1  / 
( ( K  x.  D ) ^ N
) ) )

Proof of Theorem stoweidlem1
StepHypRef Expression
1 1re 8837 . . . . . . . 8  |-  1  e.  RR
21a1i 10 . . . . . . 7  |-  ( ph  ->  1  e.  RR )
3 stoweidlem1.5 . . . . . . . . . 10  |-  ( ph  ->  A  e.  RR+ )
4 rpre 10360 . . . . . . . . . 10  |-  ( A  e.  RR+  ->  A  e.  RR )
53, 4syl 15 . . . . . . . . 9  |-  ( ph  ->  A  e.  RR )
6 stoweidlem1.1 . . . . . . . . . 10  |-  ( ph  ->  N  e.  NN )
7 nnnn0 9972 . . . . . . . . . 10  |-  ( N  e.  NN  ->  N  e.  NN0 )
86, 7syl 15 . . . . . . . . 9  |-  ( ph  ->  N  e.  NN0 )
95, 8jca 518 . . . . . . . 8  |-  ( ph  ->  ( A  e.  RR  /\  N  e.  NN0 )
)
10 reexpcl 11120 . . . . . . . 8  |-  ( ( A  e.  RR  /\  N  e.  NN0 )  -> 
( A ^ N
)  e.  RR )
119, 10syl 15 . . . . . . 7  |-  ( ph  ->  ( A ^ N
)  e.  RR )
122, 11jca 518 . . . . . 6  |-  ( ph  ->  ( 1  e.  RR  /\  ( A ^ N
)  e.  RR ) )
13 resubcl 9111 . . . . . 6  |-  ( ( 1  e.  RR  /\  ( A ^ N )  e.  RR )  -> 
( 1  -  ( A ^ N ) )  e.  RR )
1412, 13syl 15 . . . . 5  |-  ( ph  ->  ( 1  -  ( A ^ N ) )  e.  RR )
15 stoweidlem1.2 . . . . . . . 8  |-  ( ph  ->  K  e.  NN )
16 nnnn0 9972 . . . . . . . 8  |-  ( K  e.  NN  ->  K  e.  NN0 )
1715, 16syl 15 . . . . . . 7  |-  ( ph  ->  K  e.  NN0 )
1817, 8jca 518 . . . . . 6  |-  ( ph  ->  ( K  e.  NN0  /\  N  e.  NN0 )
)
19 nn0expcl 11117 . . . . . 6  |-  ( ( K  e.  NN0  /\  N  e.  NN0 )  -> 
( K ^ N
)  e.  NN0 )
2018, 19syl 15 . . . . 5  |-  ( ph  ->  ( K ^ N
)  e.  NN0 )
2114, 20jca 518 . . . 4  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) )  e.  RR  /\  ( K ^ N
)  e.  NN0 )
)
22 reexpcl 11120 . . . 4  |-  ( ( ( 1  -  ( A ^ N ) )  e.  RR  /\  ( K ^ N )  e. 
NN0 )  ->  (
( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  e.  RR )
2321, 22syl 15 . . 3  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  e.  RR )
24 2nn0 9982 . . . . . . . . . . . . . 14  |-  2  e.  NN0
2524a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  2  e.  NN0 )
2625, 8jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  e.  NN0  /\  N  e.  NN0 )
)
27 nn0mulcl 10000 . . . . . . . . . . . 12  |-  ( ( 2  e.  NN0  /\  N  e.  NN0 )  -> 
( 2  x.  N
)  e.  NN0 )
2826, 27syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( 2  x.  N
)  e.  NN0 )
295, 28jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( A  e.  RR  /\  ( 2  x.  N
)  e.  NN0 )
)
30 reexpcl 11120 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( 2  x.  N
)  e.  NN0 )  ->  ( A ^ (
2  x.  N ) )  e.  RR )
3129, 30syl 15 . . . . . . . . 9  |-  ( ph  ->  ( A ^ (
2  x.  N ) )  e.  RR )
322, 31jca 518 . . . . . . . 8  |-  ( ph  ->  ( 1  e.  RR  /\  ( A ^ (
2  x.  N ) )  e.  RR ) )
33 resubcl 9111 . . . . . . . 8  |-  ( ( 1  e.  RR  /\  ( A ^ ( 2  x.  N ) )  e.  RR )  -> 
( 1  -  ( A ^ ( 2  x.  N ) ) )  e.  RR )
3432, 33syl 15 . . . . . . 7  |-  ( ph  ->  ( 1  -  ( A ^ ( 2  x.  N ) ) )  e.  RR )
3534, 20jca 518 . . . . . 6  |-  ( ph  ->  ( ( 1  -  ( A ^ (
2  x.  N ) ) )  e.  RR  /\  ( K ^ N
)  e.  NN0 )
)
36 reexpcl 11120 . . . . . 6  |-  ( ( ( 1  -  ( A ^ ( 2  x.  N ) ) )  e.  RR  /\  ( K ^ N )  e. 
NN0 )  ->  (
( 1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) )  e.  RR )
3735, 36syl 15 . . . . 5  |-  ( ph  ->  ( ( 1  -  ( A ^ (
2  x.  N ) ) ) ^ ( K ^ N ) )  e.  RR )
38 nnre 9753 . . . . . . . . . 10  |-  ( K  e.  NN  ->  K  e.  RR )
3915, 38syl 15 . . . . . . . . 9  |-  ( ph  ->  K  e.  RR )
4039, 5jca 518 . . . . . . . 8  |-  ( ph  ->  ( K  e.  RR  /\  A  e.  RR ) )
41 remulcl 8822 . . . . . . . 8  |-  ( ( K  e.  RR  /\  A  e.  RR )  ->  ( K  x.  A
)  e.  RR )
4240, 41syl 15 . . . . . . 7  |-  ( ph  ->  ( K  x.  A
)  e.  RR )
4342, 8jca 518 . . . . . 6  |-  ( ph  ->  ( ( K  x.  A )  e.  RR  /\  N  e.  NN0 )
)
44 reexpcl 11120 . . . . . 6  |-  ( ( ( K  x.  A
)  e.  RR  /\  N  e.  NN0 )  -> 
( ( K  x.  A ) ^ N
)  e.  RR )
4543, 44syl 15 . . . . 5  |-  ( ph  ->  ( ( K  x.  A ) ^ N
)  e.  RR )
46 nn0cn 9975 . . . . . . . . . 10  |-  ( K  e.  NN0  ->  K  e.  CC )
4717, 46syl 15 . . . . . . . . 9  |-  ( ph  ->  K  e.  CC )
48 nnne0 9778 . . . . . . . . . 10  |-  ( K  e.  NN  ->  K  =/=  0 )
4915, 48syl 15 . . . . . . . . 9  |-  ( ph  ->  K  =/=  0 )
5047, 49jca 518 . . . . . . . 8  |-  ( ph  ->  ( K  e.  CC  /\  K  =/=  0 ) )
51 rpcn 10362 . . . . . . . . . 10  |-  ( A  e.  RR+  ->  A  e.  CC )
523, 51syl 15 . . . . . . . . 9  |-  ( ph  ->  A  e.  CC )
53 rpgt0 10365 . . . . . . . . . . . 12  |-  ( A  e.  RR+  ->  0  < 
A )
543, 53syl 15 . . . . . . . . . . 11  |-  ( ph  ->  0  <  A )
5554olcd 382 . . . . . . . . . 10  |-  ( ph  ->  ( A  <  0  \/  0  <  A ) )
56 0re 8838 . . . . . . . . . . . . 13  |-  0  e.  RR
5756a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  0  e.  RR )
585, 57jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( A  e.  RR  /\  0  e.  RR ) )
59 lttri2 8904 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  0  e.  RR )  ->  ( A  =/=  0  <->  ( A  <  0  \/  0  <  A ) ) )
6058, 59syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( A  =/=  0  <->  ( A  <  0  \/  0  <  A ) ) )
6155, 60mpbird 223 . . . . . . . . 9  |-  ( ph  ->  A  =/=  0 )
6252, 61jca 518 . . . . . . . 8  |-  ( ph  ->  ( A  e.  CC  /\  A  =/=  0 ) )
6350, 62jca 518 . . . . . . 7  |-  ( ph  ->  ( ( K  e.  CC  /\  K  =/=  0 )  /\  ( A  e.  CC  /\  A  =/=  0 ) ) )
64 mulne0 9410 . . . . . . 7  |-  ( ( ( K  e.  CC  /\  K  =/=  0 )  /\  ( A  e.  CC  /\  A  =/=  0 ) )  -> 
( K  x.  A
)  =/=  0 )
6563, 64syl 15 . . . . . 6  |-  ( ph  ->  ( K  x.  A
)  =/=  0 )
6647, 52jca 518 . . . . . . . . 9  |-  ( ph  ->  ( K  e.  CC  /\  A  e.  CC ) )
67 mulcl 8821 . . . . . . . . 9  |-  ( ( K  e.  CC  /\  A  e.  CC )  ->  ( K  x.  A
)  e.  CC )
6866, 67syl 15 . . . . . . . 8  |-  ( ph  ->  ( K  x.  A
)  e.  CC )
6968, 6jca 518 . . . . . . 7  |-  ( ph  ->  ( ( K  x.  A )  e.  CC  /\  N  e.  NN ) )
70 expne0 11133 . . . . . . 7  |-  ( ( ( K  x.  A
)  e.  CC  /\  N  e.  NN )  ->  ( ( ( K  x.  A ) ^ N )  =/=  0  <->  ( K  x.  A )  =/=  0 ) )
7169, 70syl 15 . . . . . 6  |-  ( ph  ->  ( ( ( K  x.  A ) ^ N )  =/=  0  <->  ( K  x.  A )  =/=  0 ) )
7265, 71mpbird 223 . . . . 5  |-  ( ph  ->  ( ( K  x.  A ) ^ N
)  =/=  0 )
7337, 45, 723jca 1132 . . . 4  |-  ( ph  ->  ( ( ( 1  -  ( A ^
( 2  x.  N
) ) ) ^
( K ^ N
) )  e.  RR  /\  ( ( K  x.  A ) ^ N
)  e.  RR  /\  ( ( K  x.  A ) ^ N
)  =/=  0 ) )
74 redivcl 9479 . . . 4  |-  ( ( ( ( 1  -  ( A ^ (
2  x.  N ) ) ) ^ ( K ^ N ) )  e.  RR  /\  (
( K  x.  A
) ^ N )  e.  RR  /\  (
( K  x.  A
) ^ N )  =/=  0 )  -> 
( ( ( 1  -  ( A ^
( 2  x.  N
) ) ) ^
( K ^ N
) )  /  (
( K  x.  A
) ^ N ) )  e.  RR )
7573, 74syl 15 . . 3  |-  ( ph  ->  ( ( ( 1  -  ( A ^
( 2  x.  N
) ) ) ^
( K ^ N
) )  /  (
( K  x.  A
) ^ N ) )  e.  RR )
76 stoweidlem1.3 . . . . . . . . . 10  |-  ( ph  ->  D  e.  RR+ )
77 rpre 10360 . . . . . . . . . 10  |-  ( D  e.  RR+  ->  D  e.  RR )
7876, 77syl 15 . . . . . . . . 9  |-  ( ph  ->  D  e.  RR )
7939, 78jca 518 . . . . . . . 8  |-  ( ph  ->  ( K  e.  RR  /\  D  e.  RR ) )
80 remulcl 8822 . . . . . . . 8  |-  ( ( K  e.  RR  /\  D  e.  RR )  ->  ( K  x.  D
)  e.  RR )
8179, 80syl 15 . . . . . . 7  |-  ( ph  ->  ( K  x.  D
)  e.  RR )
8281, 8jca 518 . . . . . 6  |-  ( ph  ->  ( ( K  x.  D )  e.  RR  /\  N  e.  NN0 )
)
83 reexpcl 11120 . . . . . 6  |-  ( ( ( K  x.  D
)  e.  RR  /\  N  e.  NN0 )  -> 
( ( K  x.  D ) ^ N
)  e.  RR )
8482, 83syl 15 . . . . 5  |-  ( ph  ->  ( ( K  x.  D ) ^ N
)  e.  RR )
85 rpcn 10362 . . . . . . . . . 10  |-  ( D  e.  RR+  ->  D  e.  CC )
8676, 85syl 15 . . . . . . . . 9  |-  ( ph  ->  D  e.  CC )
87 rpne0 10369 . . . . . . . . . 10  |-  ( D  e.  RR+  ->  D  =/=  0 )
8876, 87syl 15 . . . . . . . . 9  |-  ( ph  ->  D  =/=  0 )
8986, 88jca 518 . . . . . . . 8  |-  ( ph  ->  ( D  e.  CC  /\  D  =/=  0 ) )
9050, 89jca 518 . . . . . . 7  |-  ( ph  ->  ( ( K  e.  CC  /\  K  =/=  0 )  /\  ( D  e.  CC  /\  D  =/=  0 ) ) )
91 mulne0 9410 . . . . . . 7  |-  ( ( ( K  e.  CC  /\  K  =/=  0 )  /\  ( D  e.  CC  /\  D  =/=  0 ) )  -> 
( K  x.  D
)  =/=  0 )
9290, 91syl 15 . . . . . 6  |-  ( ph  ->  ( K  x.  D
)  =/=  0 )
9347, 86jca 518 . . . . . . . . 9  |-  ( ph  ->  ( K  e.  CC  /\  D  e.  CC ) )
94 mulcl 8821 . . . . . . . . 9  |-  ( ( K  e.  CC  /\  D  e.  CC )  ->  ( K  x.  D
)  e.  CC )
9593, 94syl 15 . . . . . . . 8  |-  ( ph  ->  ( K  x.  D
)  e.  CC )
9695, 6jca 518 . . . . . . 7  |-  ( ph  ->  ( ( K  x.  D )  e.  CC  /\  N  e.  NN ) )
97 expne0 11133 . . . . . . 7  |-  ( ( ( K  x.  D
)  e.  CC  /\  N  e.  NN )  ->  ( ( ( K  x.  D ) ^ N )  =/=  0  <->  ( K  x.  D )  =/=  0 ) )
9896, 97syl 15 . . . . . 6  |-  ( ph  ->  ( ( ( K  x.  D ) ^ N )  =/=  0  <->  ( K  x.  D )  =/=  0 ) )
9992, 98mpbird 223 . . . . 5  |-  ( ph  ->  ( ( K  x.  D ) ^ N
)  =/=  0 )
1002, 84, 993jca 1132 . . . 4  |-  ( ph  ->  ( 1  e.  RR  /\  ( ( K  x.  D ) ^ N
)  e.  RR  /\  ( ( K  x.  D ) ^ N
)  =/=  0 ) )
101 redivcl 9479 . . . 4  |-  ( ( 1  e.  RR  /\  ( ( K  x.  D ) ^ N
)  e.  RR  /\  ( ( K  x.  D ) ^ N
)  =/=  0 )  ->  ( 1  / 
( ( K  x.  D ) ^ N
) )  e.  RR )
102100, 101syl 15 . . 3  |-  ( ph  ->  ( 1  /  (
( K  x.  D
) ^ N ) )  e.  RR )
10323, 75, 1023jca 1132 . 2  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  e.  RR  /\  ( ( ( 1  -  ( A ^
( 2  x.  N
) ) ) ^
( K ^ N
) )  /  (
( K  x.  A
) ^ N ) )  e.  RR  /\  ( 1  /  (
( K  x.  D
) ^ N ) )  e.  RR ) )
10439, 8jca 518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( K  e.  RR  /\  N  e.  NN0 )
)
105 reexpcl 11120 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  RR  /\  N  e.  NN0 )  -> 
( K ^ N
)  e.  RR )
106104, 105syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( K ^ N
)  e.  RR )
107106, 11jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( K ^ N )  e.  RR  /\  ( A ^ N
)  e.  RR ) )
108 remulcl 8822 . . . . . . . . . . . . 13  |-  ( ( ( K ^ N
)  e.  RR  /\  ( A ^ N )  e.  RR )  -> 
( ( K ^ N )  x.  ( A ^ N ) )  e.  RR )
109107, 108syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( K ^ N )  x.  ( A ^ N ) )  e.  RR )
1102, 109jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  e.  RR  /\  ( ( K ^ N )  x.  ( A ^ N ) )  e.  RR ) )
111 readdcl 8820 . . . . . . . . . . 11  |-  ( ( 1  e.  RR  /\  ( ( K ^ N )  x.  ( A ^ N ) )  e.  RR )  -> 
( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) )  e.  RR )
112110, 111syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) )  e.  RR )
11323, 112jca 518 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  e.  RR  /\  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) )  e.  RR ) )
114 remulcl 8822 . . . . . . . . 9  |-  ( ( ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  e.  RR  /\  (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  e.  RR )  -> 
( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  e.  RR )
115113, 114syl 15 . . . . . . . 8  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  e.  RR )
116115, 45, 723jca 1132 . . . . . . 7  |-  ( ph  ->  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) ) )  e.  RR  /\  ( ( K  x.  A ) ^ N
)  e.  RR  /\  ( ( K  x.  A ) ^ N
)  =/=  0 ) )
117 redivcl 9479 . . . . . . 7  |-  ( ( ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  e.  RR  /\  ( ( K  x.  A ) ^ N
)  e.  RR  /\  ( ( K  x.  A ) ^ N
)  =/=  0 )  ->  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) ) )  /  (
( K  x.  A
) ^ N ) )  e.  RR )
118116, 117syl 15 . . . . . 6  |-  ( ph  ->  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) ) )  /  (
( K  x.  A
) ^ N ) )  e.  RR )
119 readdcl 8820 . . . . . . . . . . . . 13  |-  ( ( 1  e.  RR  /\  ( A ^ N )  e.  RR )  -> 
( 1  +  ( A ^ N ) )  e.  RR )
12012, 119syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  +  ( A ^ N ) )  e.  RR )
121120, 20jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  +  ( A ^ N
) )  e.  RR  /\  ( K ^ N
)  e.  NN0 )
)
122 reexpcl 11120 . . . . . . . . . . 11  |-  ( ( ( 1  +  ( A ^ N ) )  e.  RR  /\  ( K ^ N )  e.  NN0 )  -> 
( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) )  e.  RR )
123121, 122syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) )  e.  RR )
12423, 123jca 518 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  e.  RR  /\  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) )  e.  RR ) )
125 remulcl 8822 . . . . . . . . 9  |-  ( ( ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  e.  RR  /\  (
( 1  +  ( A ^ N ) ) ^ ( K ^ N ) )  e.  RR )  -> 
( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
( 1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )  e.  RR )
126124, 125syl 15 . . . . . . . 8  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
( 1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )  e.  RR )
127126, 45, 723jca 1132 . . . . . . 7  |-  ( ph  ->  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) ) )  e.  RR  /\  ( ( K  x.  A ) ^ N
)  e.  RR  /\  ( ( K  x.  A ) ^ N
)  =/=  0 ) )
128 redivcl 9479 . . . . . . 7  |-  ( ( ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
( 1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )  e.  RR  /\  ( ( K  x.  A ) ^ N
)  e.  RR  /\  ( ( K  x.  A ) ^ N
)  =/=  0 )  ->  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) )  e.  RR )
129127, 128syl 15 . . . . . 6  |-  ( ph  ->  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) )  e.  RR )
13023, 118, 1293jca 1132 . . . . 5  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  e.  RR  /\  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) ) )  /  (
( K  x.  A
) ^ N ) )  e.  RR  /\  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) )  e.  RR ) )
131112, 45, 723jca 1132 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  e.  RR  /\  ( ( K  x.  A ) ^ N
)  e.  RR  /\  ( ( K  x.  A ) ^ N
)  =/=  0 ) )
132 redivcl 9479 . . . . . . . . . . 11  |-  ( ( ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) )  e.  RR  /\  ( ( K  x.  A ) ^ N
)  e.  RR  /\  ( ( K  x.  A ) ^ N
)  =/=  0 )  ->  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N
) ) )  / 
( ( K  x.  A ) ^ N
) )  e.  RR )
133131, 132syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) )  e.  RR )
13423, 133jca 518 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  e.  RR  /\  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) )  e.  RR ) )
135 stoweidlem1.6 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <_  A )
136 stoweidlem1.7 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A  <_  1 )
1375, 135, 1363jca 1132 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A  e.  RR  /\  0  <_  A  /\  A  <_  1 ) )
138137, 8jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A  e.  RR  /\  0  <_  A  /\  A  <_  1
)  /\  N  e.  NN0 ) )
139 exple1 11161 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  RR  /\  0  <_  A  /\  A  <_  1 )  /\  N  e.  NN0 )  -> 
( A ^ N
)  <_  1 )
140138, 139syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A ^ N
)  <_  1 )
141 subge0 9287 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  RR  /\  ( A ^ N )  e.  RR )  -> 
( 0  <_  (
1  -  ( A ^ N ) )  <-> 
( A ^ N
)  <_  1 ) )
14212, 141syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  <_  (
1  -  ( A ^ N ) )  <-> 
( A ^ N
)  <_  1 ) )
143140, 142mpbird 223 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( 1  -  ( A ^ N ) ) )
14414, 20, 1433jca 1132 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) )  e.  RR  /\  ( K ^ N
)  e.  NN0  /\  0  <_  ( 1  -  ( A ^ N
) ) ) )
145 expge0 11138 . . . . . . . . . . 11  |-  ( ( ( 1  -  ( A ^ N ) )  e.  RR  /\  ( K ^ N )  e. 
NN0  /\  0  <_  ( 1  -  ( A ^ N ) ) )  ->  0  <_  ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) ) )
146144, 145syl 15 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( (
1  -  ( A ^ N ) ) ^ ( K ^ N ) ) )
14768, 8jca 518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( K  x.  A )  e.  CC  /\  N  e.  NN0 )
)
148 expcl 11121 . . . . . . . . . . . . . . 15  |-  ( ( ( K  x.  A
)  e.  CC  /\  N  e.  NN0 )  -> 
( ( K  x.  A ) ^ N
)  e.  CC )
149147, 148syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( K  x.  A ) ^ N
)  e.  CC )
150149, 72jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( K  x.  A ) ^ N )  e.  CC  /\  ( ( K  x.  A ) ^ N
)  =/=  0 ) )
151 divid 9451 . . . . . . . . . . . . 13  |-  ( ( ( ( K  x.  A ) ^ N
)  e.  CC  /\  ( ( K  x.  A ) ^ N
)  =/=  0 )  ->  ( ( ( K  x.  A ) ^ N )  / 
( ( K  x.  A ) ^ N
) )  =  1 )
152150, 151syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( K  x.  A ) ^ N )  /  (
( K  x.  A
) ^ N ) )  =  1 )
153 addid2 8995 . . . . . . . . . . . . . . 15  |-  ( ( ( K  x.  A
) ^ N )  e.  CC  ->  (
0  +  ( ( K  x.  A ) ^ N ) )  =  ( ( K  x.  A ) ^ N ) )
154149, 153syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  ( ( K  x.  A
) ^ N ) )  =  ( ( K  x.  A ) ^ N ) )
155 0le1 9297 . . . . . . . . . . . . . . . 16  |-  0  <_  1
156155a1i 10 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <_  1 )
15757, 2, 453jca 1132 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 0  e.  RR  /\  1  e.  RR  /\  ( ( K  x.  A ) ^ N
)  e.  RR ) )
158 leadd1 9242 . . . . . . . . . . . . . . . 16  |-  ( ( 0  e.  RR  /\  1  e.  RR  /\  (
( K  x.  A
) ^ N )  e.  RR )  -> 
( 0  <_  1  <->  ( 0  +  ( ( K  x.  A ) ^ N ) )  <_  ( 1  +  ( ( K  x.  A ) ^ N
) ) ) )
159157, 158syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 0  <_  1  <->  ( 0  +  ( ( K  x.  A ) ^ N ) )  <_  ( 1  +  ( ( K  x.  A ) ^ N
) ) ) )
160156, 159mpbid 201 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  ( ( K  x.  A
) ^ N ) )  <_  ( 1  +  ( ( K  x.  A ) ^ N ) ) )
161154, 160eqbrtrrd 4045 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( K  x.  A ) ^ N
)  <_  ( 1  +  ( ( K  x.  A ) ^ N ) ) )
1622, 45jca 518 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1  e.  RR  /\  ( ( K  x.  A ) ^ N
)  e.  RR ) )
163 readdcl 8820 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  RR  /\  ( ( K  x.  A ) ^ N
)  e.  RR )  ->  ( 1  +  ( ( K  x.  A ) ^ N
) )  e.  RR )
164162, 163syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  +  ( ( K  x.  A
) ^ N ) )  e.  RR )
165 nnz 10045 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  NN  ->  N  e.  ZZ )
1666, 165syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  ZZ )
167 nngt0 9775 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( K  e.  NN  ->  0  <  K )
16815, 167syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  0  <  K )
16939, 168jca 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( K  e.  RR  /\  0  <  K ) )
1705, 54jca 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A  e.  RR  /\  0  <  A ) )
171169, 170jca 518 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( K  e.  RR  /\  0  < 
K )  /\  ( A  e.  RR  /\  0  <  A ) ) )
172 mulgt0 8900 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( K  e.  RR  /\  0  <  K )  /\  ( A  e.  RR  /\  0  < 
A ) )  -> 
0  <  ( K  x.  A ) )
173171, 172syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  <  ( K  x.  A ) )
17442, 166, 1733jca 1132 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( K  x.  A )  e.  RR  /\  N  e.  ZZ  /\  0  <  ( K  x.  A ) ) )
175 expgt0 11135 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  x.  A
)  e.  RR  /\  N  e.  ZZ  /\  0  <  ( K  x.  A
) )  ->  0  <  ( ( K  x.  A ) ^ N
) )
176174, 175syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <  ( ( K  x.  A ) ^ N ) )
17745, 176jca 518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( K  x.  A ) ^ N )  e.  RR  /\  0  <  ( ( K  x.  A ) ^ N ) ) )
17845, 164, 1773jca 1132 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( K  x.  A ) ^ N )  e.  RR  /\  ( 1  +  ( ( K  x.  A
) ^ N ) )  e.  RR  /\  ( ( ( K  x.  A ) ^ N )  e.  RR  /\  0  <  ( ( K  x.  A ) ^ N ) ) ) )
179 lediv1 9621 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  x.  A ) ^ N
)  e.  RR  /\  ( 1  +  ( ( K  x.  A
) ^ N ) )  e.  RR  /\  ( ( ( K  x.  A ) ^ N )  e.  RR  /\  0  <  ( ( K  x.  A ) ^ N ) ) )  ->  ( (
( K  x.  A
) ^ N )  <_  ( 1  +  ( ( K  x.  A ) ^ N
) )  <->  ( (
( K  x.  A
) ^ N )  /  ( ( K  x.  A ) ^ N ) )  <_ 
( ( 1  +  ( ( K  x.  A ) ^ N
) )  /  (
( K  x.  A
) ^ N ) ) ) )
180178, 179syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( K  x.  A ) ^ N )  <_  (
1  +  ( ( K  x.  A ) ^ N ) )  <-> 
( ( ( K  x.  A ) ^ N )  /  (
( K  x.  A
) ^ N ) )  <_  ( (
1  +  ( ( K  x.  A ) ^ N ) )  /  ( ( K  x.  A ) ^ N ) ) ) )
181161, 180mpbid 201 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( K  x.  A ) ^ N )  /  (
( K  x.  A
) ^ N ) )  <_  ( (
1  +  ( ( K  x.  A ) ^ N ) )  /  ( ( K  x.  A ) ^ N ) ) )
182152, 181eqbrtrrd 4045 . . . . . . . . . . 11  |-  ( ph  ->  1  <_  ( (
1  +  ( ( K  x.  A ) ^ N ) )  /  ( ( K  x.  A ) ^ N ) ) )
18347, 52, 83jca 1132 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( K  e.  CC  /\  A  e.  CC  /\  N  e.  NN0 ) )
184 mulexp 11141 . . . . . . . . . . . . . 14  |-  ( ( K  e.  CC  /\  A  e.  CC  /\  N  e.  NN0 )  ->  (
( K  x.  A
) ^ N )  =  ( ( K ^ N )  x.  ( A ^ N
) ) )
185183, 184syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( K  x.  A ) ^ N
)  =  ( ( K ^ N )  x.  ( A ^ N ) ) )
186185oveq2d 5874 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  +  ( ( K  x.  A
) ^ N ) )  =  ( 1  +  ( ( K ^ N )  x.  ( A ^ N
) ) ) )
187186oveq1d 5873 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  +  ( ( K  x.  A ) ^ N
) )  /  (
( K  x.  A
) ^ N ) )  =  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) ) )
188182, 187breqtrd 4047 . . . . . . . . . 10  |-  ( ph  ->  1  <_  ( (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) ) )
189146, 188jca 518 . . . . . . . . 9  |-  ( ph  ->  ( 0  <_  (
( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  /\  1  <_  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N
) ) )  / 
( ( K  x.  A ) ^ N
) ) ) )
190134, 189jca 518 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  e.  RR  /\  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) )  e.  RR )  /\  (
0  <_  ( (
1  -  ( A ^ N ) ) ^ ( K ^ N ) )  /\  1  <_  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N
) ) )  / 
( ( K  x.  A ) ^ N
) ) ) ) )
191 lemulge11 9618 . . . . . . . 8  |-  ( ( ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  e.  RR  /\  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) )  e.  RR )  /\  ( 0  <_  (
( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  /\  1  <_  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N
) ) )  / 
( ( K  x.  A ) ^ N
) ) ) )  ->  ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  <_  (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N
) ) )  / 
( ( K  x.  A ) ^ N
) ) ) )
192190, 191syl 15 . . . . . . 7  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  <_  ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) ) ) )
193 ax-1cn 8795 . . . . . . . . . . . . . 14  |-  1  e.  CC
194193a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  1  e.  CC )
19552, 8jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  e.  CC  /\  N  e.  NN0 )
)
196 expcl 11121 . . . . . . . . . . . . . 14  |-  ( ( A  e.  CC  /\  N  e.  NN0 )  -> 
( A ^ N
)  e.  CC )
197195, 196syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A ^ N
)  e.  CC )
198194, 197jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  e.  CC  /\  ( A ^ N
)  e.  CC ) )
199 subcl 9051 . . . . . . . . . . . 12  |-  ( ( 1  e.  CC  /\  ( A ^ N )  e.  CC )  -> 
( 1  -  ( A ^ N ) )  e.  CC )
200198, 199syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  -  ( A ^ N ) )  e.  CC )
201200, 20jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) )  e.  CC  /\  ( K ^ N
)  e.  NN0 )
)
202 expcl 11121 . . . . . . . . . 10  |-  ( ( ( 1  -  ( A ^ N ) )  e.  CC  /\  ( K ^ N )  e. 
NN0 )  ->  (
( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  e.  CC )
203201, 202syl 15 . . . . . . . . 9  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  e.  CC )
20447, 8jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( K  e.  CC  /\  N  e.  NN0 )
)
205 expcl 11121 . . . . . . . . . . . . . 14  |-  ( ( K  e.  CC  /\  N  e.  NN0 )  -> 
( K ^ N
)  e.  CC )
206204, 205syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( K ^ N
)  e.  CC )
207206, 197jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( K ^ N )  e.  CC  /\  ( A ^ N
)  e.  CC ) )
208 mulcl 8821 . . . . . . . . . . . 12  |-  ( ( ( K ^ N
)  e.  CC  /\  ( A ^ N )  e.  CC )  -> 
( ( K ^ N )  x.  ( A ^ N ) )  e.  CC )
209207, 208syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( ( K ^ N )  x.  ( A ^ N ) )  e.  CC )
210194, 209jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( 1  e.  CC  /\  ( ( K ^ N )  x.  ( A ^ N ) )  e.  CC ) )
211 addcl 8819 . . . . . . . . . 10  |-  ( ( 1  e.  CC  /\  ( ( K ^ N )  x.  ( A ^ N ) )  e.  CC )  -> 
( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) )  e.  CC )
212210, 211syl 15 . . . . . . . . 9  |-  ( ph  ->  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) )  e.  CC )
213203, 212, 1503jca 1132 . . . . . . . 8  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  e.  CC  /\  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) )  e.  CC  /\  ( ( ( K  x.  A ) ^ N )  e.  CC  /\  ( ( K  x.  A ) ^ N
)  =/=  0 ) ) )
214 divass 9442 . . . . . . . 8  |-  ( ( ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  e.  CC  /\  (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  e.  CC  /\  (
( ( K  x.  A ) ^ N
)  e.  CC  /\  ( ( K  x.  A ) ^ N
)  =/=  0 ) )  ->  ( (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  /  (
( K  x.  A
) ^ N ) )  =  ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) ) ) )
215213, 214syl 15 . . . . . . 7  |-  ( ph  ->  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) ) )  /  (
( K  x.  A
) ^ N ) )  =  ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) ) ) )
216192, 215breqtrrd 4049 . . . . . 6  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  <_  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) ) )  /  (
( K  x.  A
) ^ N ) ) )
21723, 146jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  e.  RR  /\  0  <_  ( (
1  -  ( A ^ N ) ) ^ ( K ^ N ) ) ) )
218112, 123, 2173jca 1132 . . . . . . . . 9  |-  ( ph  ->  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  e.  RR  /\  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) )  e.  RR  /\  (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  e.  RR  /\  0  <_  ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) ) ) ) )
219 mulcom 8823 . . . . . . . . . . . 12  |-  ( ( ( K ^ N
)  e.  CC  /\  ( A ^ N )  e.  CC )  -> 
( ( K ^ N )  x.  ( A ^ N ) )  =  ( ( A ^ N )  x.  ( K ^ N
) ) )
220207, 219syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( ( K ^ N )  x.  ( A ^ N ) )  =  ( ( A ^ N )  x.  ( K ^ N
) ) )
221220oveq2d 5874 . . . . . . . . . 10  |-  ( ph  ->  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) )  =  ( 1  +  ( ( A ^ N )  x.  ( K ^ N
) ) ) )
222 renegcl 9110 . . . . . . . . . . . . . . 15  |-  ( 1  e.  RR  ->  -u 1  e.  RR )
2232, 222syl 15 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u 1  e.  RR )
224223, 57, 113jca 1132 . . . . . . . . . . . . 13  |-  ( ph  ->  ( -u 1  e.  RR  /\  0  e.  RR  /\  ( A ^ N )  e.  RR ) )
225 le0neg2 9283 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  RR  ->  (
0  <_  1  <->  -u 1  <_ 
0 ) )
2261, 225ax-mp 8 . . . . . . . . . . . . . . . 16  |-  ( 0  <_  1  <->  -u 1  <_ 
0 )
227155, 226mpbi 199 . . . . . . . . . . . . . . 15  |-  -u 1  <_  0
228227a1i 10 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u 1  <_  0
)
2295, 8, 1353jca 1132 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A  e.  RR  /\  N  e.  NN0  /\  0  <_  A ) )
230 expge0 11138 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  N  e.  NN0  /\  0  <_  A )  ->  0  <_  ( A ^ N
) )
231229, 230syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <_  ( A ^ N ) )
232228, 231jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( -u 1  <_ 
0  /\  0  <_  ( A ^ N ) ) )
233 letr 8914 . . . . . . . . . . . . 13  |-  ( (
-u 1  e.  RR  /\  0  e.  RR  /\  ( A ^ N )  e.  RR )  -> 
( ( -u 1  <_  0  /\  0  <_ 
( A ^ N
) )  ->  -u 1  <_  ( A ^ N
) ) )
234224, 232, 233sylc 56 . . . . . . . . . . . 12  |-  ( ph  -> 
-u 1  <_  ( A ^ N ) )
23511, 20, 2343jca 1132 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A ^ N )  e.  RR  /\  ( K ^ N
)  e.  NN0  /\  -u 1  <_  ( A ^ N ) ) )
236 bernneq 11227 . . . . . . . . . . 11  |-  ( ( ( A ^ N
)  e.  RR  /\  ( K ^ N )  e.  NN0  /\  -u 1  <_  ( A ^ N
) )  ->  (
1  +  ( ( A ^ N )  x.  ( K ^ N ) ) )  <_  ( ( 1  +  ( A ^ N ) ) ^
( K ^ N
) ) )
237235, 236syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( 1  +  ( ( A ^ N
)  x.  ( K ^ N ) ) )  <_  ( (
1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )
238221, 237eqbrtrd 4043 . . . . . . . . 9  |-  ( ph  ->  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) )  <_  ( (
1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )
239218, 238jca 518 . . . . . . . 8  |-  ( ph  ->  ( ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N
) ) )  e.  RR  /\  ( ( 1  +  ( A ^ N ) ) ^ ( K ^ N ) )  e.  RR  /\  ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  e.  RR  /\  0  <_ 
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) ) ) )  /\  (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  <_  ( ( 1  +  ( A ^ N ) ) ^
( K ^ N
) ) ) )
240 lemul2a 9611 . . . . . . . 8  |-  ( ( ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  e.  RR  /\  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) )  e.  RR  /\  (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  e.  RR  /\  0  <_  ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) ) ) )  /\  (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  <_  ( ( 1  +  ( A ^ N ) ) ^
( K ^ N
) ) )  -> 
( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  <_  ( (
( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) ) ) )
241239, 240syl 15 . . . . . . 7  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  <_  ( (
( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) ) ) )
242115, 126, 1773jca 1132 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) ) )  e.  RR  /\  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
( 1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )  e.  RR  /\  ( ( ( K  x.  A ) ^ N )  e.  RR  /\  0  <  ( ( K  x.  A ) ^ N ) ) ) )
243 lediv1 9621 . . . . . . . 8  |-  ( ( ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  e.  RR  /\  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
( 1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )  e.  RR  /\  ( ( ( K  x.  A ) ^ N )  e.  RR  /\  0  <  ( ( K  x.  A ) ^ N ) ) )  ->  ( (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  <_  (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N ) ) ^
( K ^ N
) ) )  <->  ( (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  /  (
( K  x.  A
) ^ N ) )  <_  ( (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N ) ) ^
( K ^ N
) ) )  / 
( ( K  x.  A ) ^ N
) ) ) )
244242, 243syl 15 . . . . . . 7  |-  ( ph  ->  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) ) )  <_  (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N ) ) ^
( K ^ N
) ) )  <->  ( (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  /  (
( K  x.  A
) ^ N ) )  <_  ( (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N ) ) ^
( K ^ N
) ) )  / 
( ( K  x.  A ) ^ N
) ) ) )
245241, 244mpbid 201 . . . . . 6  |-  ( ph  ->  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) ) )  /  (
( K  x.  A
) ^ N ) )  <_  ( (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N ) ) ^
( K ^ N
) ) )  / 
( ( K  x.  A ) ^ N
) ) )
246216, 245jca 518 . . . . 5  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  <_  (
( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  /  ( ( K  x.  A ) ^ N ) )  /\  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) ) )  /  (
( K  x.  A
) ^ N ) )  <_  ( (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N ) ) ^
( K ^ N
) ) )  / 
( ( K  x.  A ) ^ N
) ) ) )
247 letr 8914 . . . . 5  |-  ( ( ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  e.  RR  /\  (
( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  /  ( ( K  x.  A ) ^ N ) )  e.  RR  /\  (
( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
( 1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) )  e.  RR )  -> 
( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  <_ 
( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) ) )  /  (
( K  x.  A
) ^ N ) )  /\  ( ( ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) ) )  /  (
( K  x.  A
) ^ N ) )  <_  ( (
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N ) ) ^
( K ^ N
) ) )  / 
( ( K  x.  A ) ^ N
) ) )  -> 
( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  <_  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) ) ) )
248130, 246, 247sylc 56 . . . 4  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  <_  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) ) )
249 addcl 8819 . . . . . . . . . . 11  |-  ( ( 1  e.  CC  /\  ( A ^ N )  e.  CC )  -> 
( 1  +  ( A ^ N ) )  e.  CC )
250198, 249syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( 1  +  ( A ^ N ) )  e.  CC )
251200, 250, 203jca 1132 . . . . . . . . 9  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) )  e.  CC  /\  ( 1  +  ( A ^ N ) )  e.  CC  /\  ( K ^ N )  e.  NN0 ) )
252 mulexp 11141 . . . . . . . . 9  |-  ( ( ( 1  -  ( A ^ N ) )  e.  CC  /\  (
1  +  ( A ^ N ) )  e.  CC  /\  ( K ^ N )  e. 
NN0 )  ->  (
( ( 1  -  ( A ^ N
) )  x.  (
1  +  ( A ^ N ) ) ) ^ ( K ^ N ) )  =  ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) ) ) )
253251, 252syl 15 . . . . . . . 8  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) )  x.  ( 1  +  ( A ^ N ) ) ) ^ ( K ^ N ) )  =  ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) ) ) )
254253eqcomd 2288 . . . . . . 7  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
( 1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )  =  ( ( ( 1  -  ( A ^ N ) )  x.  ( 1  +  ( A ^ N
) ) ) ^
( K ^ N
) ) )
255200, 250jca 518 . . . . . . . . 9  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) )  e.  CC  /\  ( 1  +  ( A ^ N ) )  e.  CC ) )
256 mulcom 8823 . . . . . . . . 9  |-  ( ( ( 1  -  ( A ^ N ) )  e.  CC  /\  (
1  +  ( A ^ N ) )  e.  CC )  -> 
( ( 1  -  ( A ^ N
) )  x.  (
1  +  ( A ^ N ) ) )  =  ( ( 1  +  ( A ^ N ) )  x.  ( 1  -  ( A ^ N
) ) ) )
257255, 256syl 15 . . . . . . . 8  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) )  x.  (
1  +  ( A ^ N ) ) )  =  ( ( 1  +  ( A ^ N ) )  x.  ( 1  -  ( A ^ N
) ) ) )
258257oveq1d 5873 . . . . . . 7  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) )  x.  ( 1  +  ( A ^ N ) ) ) ^ ( K ^ N ) )  =  ( ( ( 1  +  ( A ^ N ) )  x.  ( 1  -  ( A ^ N
) ) ) ^
( K ^ N
) ) )
259254, 258eqtrd 2315 . . . . . 6  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
( 1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )  =  ( ( ( 1  +  ( A ^ N ) )  x.  ( 1  -  ( A ^ N ) ) ) ^ ( K ^ N ) ) )
260 subsq 11210 . . . . . . . . 9  |-  ( ( 1  e.  CC  /\  ( A ^ N )  e.  CC )  -> 
( ( 1 ^ 2 )  -  (
( A ^ N
) ^ 2 ) )  =  ( ( 1  +  ( A ^ N ) )  x.  ( 1  -  ( A ^ N
) ) ) )
261198, 260syl 15 . . . . . . . 8  |-  ( ph  ->  ( ( 1 ^ 2 )  -  (
( A ^ N
) ^ 2 ) )  =  ( ( 1  +  ( A ^ N ) )  x.  ( 1  -  ( A ^ N
) ) ) )
262 sq1 11198 . . . . . . . . . 10  |-  ( 1 ^ 2 )  =  1
263262a1i 10 . . . . . . . . 9  |-  ( ph  ->  ( 1 ^ 2 )  =  1 )
26452, 8, 253jca 1132 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  e.  CC  /\  N  e.  NN0  /\  2  e.  NN0 ) )
265 expmul 11147 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  N  e.  NN0  /\  2  e.  NN0 )  ->  ( A ^ ( N  x.  2 ) )  =  ( ( A ^ N ) ^ 2 ) )
266264, 265syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( A ^ ( N  x.  2 ) )  =  ( ( A ^ N ) ^ 2 ) )
267266eqcomd 2288 . . . . . . . . . 10  |-  ( ph  ->  ( ( A ^ N ) ^ 2 )  =  ( A ^ ( N  x.  2 ) ) )
268 nncn 9754 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  N  e.  CC )
2696, 268syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  CC )
270 2cn 9816 . . . . . . . . . . . . . 14  |-  2  e.  CC
271270a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  2  e.  CC )
272269, 271jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  e.  CC  /\  2  e.  CC ) )
273 mulcom 8823 . . . . . . . . . . . 12  |-  ( ( N  e.  CC  /\  2  e.  CC )  ->  ( N  x.  2 )  =  ( 2  x.  N ) )
274272, 273syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( N  x.  2 )  =  ( 2  x.  N ) )
275274oveq2d 5874 . . . . . . . . . 10  |-  ( ph  ->  ( A ^ ( N  x.  2 ) )  =  ( A ^ ( 2  x.  N ) ) )
276267, 275eqtrd 2315 . . . . . . . . 9  |-  ( ph  ->  ( ( A ^ N ) ^ 2 )  =  ( A ^ ( 2  x.  N ) ) )
277263, 276oveq12d 5876 . . . . . . . 8  |-  ( ph  ->  ( ( 1 ^ 2 )  -  (
( A ^ N
) ^ 2 ) )  =  ( 1  -  ( A ^
( 2  x.  N
) ) ) )
278261, 277eqtr3d 2317 . . . . . . 7  |-  ( ph  ->  ( ( 1  +  ( A ^ N
) )  x.  (
1  -  ( A ^ N ) ) )  =  ( 1  -  ( A ^
( 2  x.  N
) ) ) )
279278oveq1d 5873 . . . . . 6  |-  ( ph  ->  ( ( ( 1  +  ( A ^ N ) )  x.  ( 1  -  ( A ^ N ) ) ) ^ ( K ^ N ) )  =  ( ( 1  -  ( A ^
( 2  x.  N
) ) ) ^
( K ^ N
) ) )
280259, 279eqtrd 2315 . . . . 5  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
( 1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )  =  ( ( 1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) ) )
281280oveq1d 5873 . . . 4  |-  ( ph  ->  ( ( ( ( 1  -  ( A ^ N ) ) ^ ( K ^ N ) )  x.  ( ( 1  +  ( A ^ N
) ) ^ ( K ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) )  =  ( ( ( 1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) )  / 
( ( K  x.  A ) ^ N
) ) )
282248, 281breqtrd 4047 . . 3  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  <_  ( ( ( 1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) )  / 
( ( K  x.  A ) ^ N
) ) )
28337, 2jca 518 . . . . . 6  |-  ( ph  ->  ( ( ( 1  -  ( A ^
( 2  x.  N
) ) ) ^
( K ^ N
) )  e.  RR  /\  1  e.  RR ) )
284137, 28jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  e.  RR  /\  0  <_  A  /\  A  <_  1
)  /\  ( 2  x.  N )  e. 
NN0 ) )
285 exple1 11161 . . . . . . . . . . 11  |-  ( ( ( A  e.  RR  /\  0  <_  A  /\  A  <_  1 )  /\  ( 2  x.  N
)  e.  NN0 )  ->  ( A ^ (
2  x.  N ) )  <_  1 )
286284, 285syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( A ^ (
2  x.  N ) )  <_  1 )
287 subge0 9287 . . . . . . . . . . 11  |-  ( ( 1  e.  RR  /\  ( A ^ ( 2  x.  N ) )  e.  RR )  -> 
( 0  <_  (
1  -  ( A ^ ( 2  x.  N ) ) )  <-> 
( A ^ (
2  x.  N ) )  <_  1 ) )
28832, 287syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( 0  <_  (
1  -  ( A ^ ( 2  x.  N ) ) )  <-> 
( A ^ (
2  x.  N ) )  <_  1 ) )
289286, 288mpbird 223 . . . . . . . . 9  |-  ( ph  ->  0  <_  ( 1  -  ( A ^
( 2  x.  N
) ) ) )
29034, 20, 2893jca 1132 . . . . . . . 8  |-  ( ph  ->  ( ( 1  -  ( A ^ (
2  x.  N ) ) )  e.  RR  /\  ( K ^ N
)  e.  NN0  /\  0  <_  ( 1  -  ( A ^ (
2  x.  N ) ) ) ) )
291 expge0 11138 . . . . . . . 8  |-  ( ( ( 1  -  ( A ^ ( 2  x.  N ) ) )  e.  RR  /\  ( K ^ N )  e. 
NN0  /\  0  <_  ( 1  -  ( A ^ ( 2  x.  N ) ) ) )  ->  0  <_  ( ( 1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) ) )
292290, 291syl 15 . . . . . . 7  |-  ( ph  ->  0  <_  ( (
1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) ) )
293 subid 9067 . . . . . . . . . . . . 13  |-  ( 1  e.  CC  ->  (
1  -  1 )  =  0 )
294193, 293ax-mp 8 . . . . . . . . . . . 12  |-  ( 1  -  1 )  =  0
2955, 28, 1353jca 1132 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  e.  RR  /\  ( 2  x.  N
)  e.  NN0  /\  0  <_  A ) )
296 expge0 11138 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  ( 2  x.  N
)  e.  NN0  /\  0  <_  A )  -> 
0  <_  ( A ^ ( 2  x.  N ) ) )
297295, 296syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( A ^ ( 2  x.  N ) ) )
298294, 297syl5eqbr 4056 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  -  1 )  <_  ( A ^ ( 2  x.  N ) ) )
2992, 31, 23jca 1132 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  e.  RR  /\  ( A ^ (
2  x.  N ) )  e.  RR  /\  1  e.  RR )
)
300 suble 9252 . . . . . . . . . . . 12  |-  ( ( 1  e.  RR  /\  ( A ^ ( 2  x.  N ) )  e.  RR  /\  1  e.  RR )  ->  (
( 1  -  ( A ^ ( 2  x.  N ) ) )  <_  1  <->  ( 1  -  1 )  <_ 
( A ^ (
2  x.  N ) ) ) )
301299, 300syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  -  ( A ^ (
2  x.  N ) ) )  <_  1  <->  ( 1  -  1 )  <_  ( A ^
( 2  x.  N
) ) ) )
302298, 301mpbird 223 . . . . . . . . . 10  |-  ( ph  ->  ( 1  -  ( A ^ ( 2  x.  N ) ) )  <_  1 )
30334, 289, 3023jca 1132 . . . . . . . . 9  |-  ( ph  ->  ( ( 1  -  ( A ^ (
2  x.  N ) ) )  e.  RR  /\  0  <_  ( 1  -  ( A ^
( 2  x.  N
) ) )  /\  ( 1  -  ( A ^ ( 2  x.  N ) ) )  <_  1 ) )
304303, 20jca 518 . . . . . . . 8  |-  ( ph  ->  ( ( ( 1  -  ( A ^
( 2  x.  N
) ) )  e.  RR  /\  0  <_ 
( 1  -  ( A ^ ( 2  x.  N ) ) )  /\  ( 1  -  ( A ^ (
2  x.  N ) ) )  <_  1
)  /\  ( K ^ N )  e.  NN0 ) )
305 exple1 11161 . . . . . . . 8  |-  ( ( ( ( 1  -  ( A ^ (
2  x.  N ) ) )  e.  RR  /\  0  <_  ( 1  -  ( A ^
( 2  x.  N
) ) )  /\  ( 1  -  ( A ^ ( 2  x.  N ) ) )  <_  1 )  /\  ( K ^ N )  e.  NN0 )  -> 
( ( 1  -  ( A ^ (
2  x.  N ) ) ) ^ ( K ^ N ) )  <_  1 )
306304, 305syl 15 . . . . . . 7  |-  ( ph  ->  ( ( 1  -  ( A ^ (
2  x.  N ) ) ) ^ ( K ^ N ) )  <_  1 )
307292, 306jca 518 . . . . . 6  |-  ( ph  ->  ( 0  <_  (
( 1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) )  /\  ( ( 1  -  ( A ^ (
2  x.  N ) ) ) ^ ( K ^ N ) )  <_  1 ) )
308283, 307jca 518 . . . . 5  |-  ( ph  ->  ( ( ( ( 1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) )  e.  RR  /\  1  e.  RR )  /\  (
0  <_  ( (
1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) )  /\  ( ( 1  -  ( A ^ (
2  x.  N ) ) ) ^ ( K ^ N ) )  <_  1 ) ) )
30984, 45jca 518 . . . . . 6  |-  ( ph  ->  ( ( ( K  x.  D ) ^ N )  e.  RR  /\  ( ( K  x.  A ) ^ N
)  e.  RR ) )
310 rpgt0 10365 . . . . . . . . . . . . 13  |-  ( D  e.  RR+  ->  0  < 
D )
31176, 310syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  D )
31278, 311jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( D  e.  RR  /\  0  <  D ) )
313169, 312jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( ( K  e.  RR  /\  0  < 
K )  /\  ( D  e.  RR  /\  0  <  D ) ) )
314 mulgt0 8900 . . . . . . . . . 10  |-  ( ( ( K  e.  RR  /\  0  <  K )  /\  ( D  e.  RR  /\  0  < 
D ) )  -> 
0  <  ( K  x.  D ) )
315313, 314syl 15 . . . . . . . . 9  |-  ( ph  ->  0  <  ( K  x.  D ) )
31681, 166, 3153jca 1132 . . . . . . . 8  |-  ( ph  ->  ( ( K  x.  D )  e.  RR  /\  N  e.  ZZ  /\  0  <  ( K  x.  D ) ) )
317 expgt0 11135 . . . . . . . 8  |-  ( ( ( K  x.  D
)  e.  RR  /\  N  e.  ZZ  /\  0  <  ( K  x.  D
) )  ->  0  <  ( ( K  x.  D ) ^ N
) )
318316, 317syl 15 . . . . . . 7  |-  ( ph  ->  0  <  ( ( K  x.  D ) ^ N ) )
31981, 42, 83jca 1132 . . . . . . . . 9  |-  ( ph  ->  ( ( K  x.  D )  e.  RR  /\  ( K  x.  A
)  e.  RR  /\  N  e.  NN0 ) )
32057, 39jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  e.  RR  /\  K  e.  RR ) )
321 ltle 8910 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  K  e.  RR )  ->  ( 0  <  K  ->  0  <_  K )
)
322320, 168, 321sylc 56 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  K )
32339, 322jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( K  e.  RR  /\  0  <_  K )
)
32457, 78jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  e.  RR  /\  D  e.  RR ) )
325 ltle 8910 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  D  e.  RR )  ->  ( 0  <  D  ->  0  <_  D )
)
326324, 311, 325sylc 56 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  D )
32778, 326jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( D  e.  RR  /\  0  <_  D )
)
328323, 327jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( ( K  e.  RR  /\  0  <_  K )  /\  ( D  e.  RR  /\  0  <_  D ) ) )
329 mulge0 9291 . . . . . . . . . . 11  |-  ( ( ( K  e.  RR  /\  0  <_  K )  /\  ( D  e.  RR  /\  0  <_  D )
)  ->  0  <_  ( K  x.  D ) )
330328, 329syl 15 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( K  x.  D ) )
33178, 5, 3233jca 1132 . . . . . . . . . . . 12  |-  ( ph  ->  ( D  e.  RR  /\  A  e.  RR  /\  ( K  e.  RR  /\  0  <_  K )
) )
332 stoweidlem1.8 . . . . . . . . . . . 12  |-  ( ph  ->  D  <_  A )
333331, 332jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( ( D  e.  RR  /\  A  e.  RR  /\  ( K  e.  RR  /\  0  <_  K ) )  /\  D  <_  A ) )
334 lemul2a 9611 . . . . . . . . . . 11  |-  ( ( ( D  e.  RR  /\  A  e.  RR  /\  ( K  e.  RR  /\  0  <_  K )
)  /\  D  <_  A )  ->  ( K  x.  D )  <_  ( K  x.  A )
)
335333, 334syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( K  x.  D
)  <_  ( K  x.  A ) )
336330, 335jca 518 . . . . . . . . 9  |-  ( ph  ->  ( 0  <_  ( K  x.  D )  /\  ( K  x.  D
)  <_  ( K  x.  A ) ) )
337319, 336jca 518 . . . . . . . 8  |-  ( ph  ->  ( ( ( K  x.  D )  e.  RR  /\  ( K  x.  A )  e.  RR  /\  N  e. 
NN0 )  /\  (
0  <_  ( K  x.  D )  /\  ( K  x.  D )  <_  ( K  x.  A
) ) ) )
338 leexp1a 11160 . . . . . . . 8  |-  ( ( ( ( K  x.  D )  e.  RR  /\  ( K  x.  A
)  e.  RR  /\  N  e.  NN0 )  /\  ( 0  <_  ( K  x.  D )  /\  ( K  x.  D
)  <_  ( K  x.  A ) ) )  ->  ( ( K  x.  D ) ^ N )  <_  (
( K  x.  A
) ^ N ) )
339337, 338syl 15 . . . . . . 7  |-  ( ph  ->  ( ( K  x.  D ) ^ N
)  <_  ( ( K  x.  A ) ^ N ) )
340318, 339jca 518 . . . . . 6  |-  ( ph  ->  ( 0  <  (
( K  x.  D
) ^ N )  /\  ( ( K  x.  D ) ^ N )  <_  (
( K  x.  A
) ^ N ) ) )
341309, 340jca 518 . . . . 5  |-  ( ph  ->  ( ( ( ( K  x.  D ) ^ N )  e.  RR  /\  ( ( K  x.  A ) ^ N )  e.  RR )  /\  (
0  <  ( ( K  x.  D ) ^ N )  /\  (
( K  x.  D
) ^ N )  <_  ( ( K  x.  A ) ^ N ) ) ) )
342308, 341jca 518 . . . 4  |-  ( ph  ->  ( ( ( ( ( 1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) )  e.  RR  /\  1  e.  RR )  /\  (
0  <_  ( (
1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) )  /\  ( ( 1  -  ( A ^ (
2  x.  N ) ) ) ^ ( K ^ N ) )  <_  1 ) )  /\  ( ( ( ( K  x.  D
) ^ N )  e.  RR  /\  (
( K  x.  A
) ^ N )  e.  RR )  /\  ( 0  <  (
( K  x.  D
) ^ N )  /\  ( ( K  x.  D ) ^ N )  <_  (
( K  x.  A
) ^ N ) ) ) ) )
343 lediv12a 9649 . . . 4  |-  ( ( ( ( ( ( 1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) )  e.  RR  /\  1  e.  RR )  /\  (
0  <_  ( (
1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) )  /\  ( ( 1  -  ( A ^ (
2  x.  N ) ) ) ^ ( K ^ N ) )  <_  1 ) )  /\  ( ( ( ( K  x.  D
) ^ N )  e.  RR  /\  (
( K  x.  A
) ^ N )  e.  RR )  /\  ( 0  <  (
( K  x.  D
) ^ N )  /\  ( ( K  x.  D ) ^ N )  <_  (
( K  x.  A
) ^ N ) ) ) )  -> 
( ( ( 1  -  ( A ^
( 2  x.  N
) ) ) ^
( K ^ N
) )  /  (
( K  x.  A
) ^ N ) )  <_  ( 1  /  ( ( K  x.  D ) ^ N ) ) )
344342, 343syl 15 . . 3  |-  ( ph  ->  ( ( ( 1  -  ( A ^
( 2  x.  N
) ) ) ^
( K ^ N
) )  /  (
( K  x.  A
) ^ N ) )  <_  ( 1  /  ( ( K  x.  D ) ^ N ) ) )
345282, 344jca 518 . 2  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  <_  (
( ( 1  -  ( A ^ (
2  x.  N ) ) ) ^ ( K ^ N ) )  /  ( ( K  x.  A ) ^ N ) )  /\  ( ( ( 1  -  ( A ^
( 2  x.  N
) ) ) ^
( K ^ N
) )  /  (
( K  x.  A
) ^ N ) )  <_  ( 1  /  ( ( K  x.  D ) ^ N ) ) ) )
346 letr 8914 . 2  |-  ( ( ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  e.  RR  /\  (
( ( 1  -  ( A ^ (
2  x.  N ) ) ) ^ ( K ^ N ) )  /  ( ( K  x.  A ) ^ N ) )  e.  RR  /\  ( 1  /  ( ( K  x.  D ) ^ N ) )  e.  RR )  ->  (
( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  <_  (
( ( 1  -  ( A ^ (
2  x.  N ) ) ) ^ ( K ^ N ) )  /  ( ( K  x.  A ) ^ N ) )  /\  ( ( ( 1  -  ( A ^
( 2  x.  N
) ) ) ^
( K ^ N
) )  /  (
( K  x.  A
) ^ N ) )  <_  ( 1  /  ( ( K  x.  D ) ^ N ) ) )  ->  ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  <_  (
1  /  ( ( K  x.  D ) ^ N ) ) ) )
347103, 345, 346sylc 56 1  |-  ( ph  ->  ( ( 1  -  ( A ^ N
) ) ^ ( K ^ N ) )  <_  ( 1  / 
( ( K  x.  D ) ^ N
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684    =/= wne 2446   class class class wbr 4023  (class class class)co 5858   CCcc 8735   RRcr 8736   0cc0 8737   1c1 8738    + caddc 8740    x. cmul 8742    < clt 8867    <_ cle 8868    - cmin 9037   -ucneg 9038    / cdiv 9423   NNcn 9746   2c2 9795   NN0cn0 9965   ZZcz 10024   RR+crp 10354   ^cexp 11104
This theorem is referenced by:  stoweidlem25  27774
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-n0 9966  df-z 10025  df-uz 10231  df-rp 10355  df-seq 11047  df-exp 11105
  Copyright terms: Public domain W3C validator