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

Theorem stoweidlem1 27852
Description: Lemma for stoweid 27914. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 11243. (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 8853 . . . . . . . 8  |-  1  e.  RR
21a1i 10 . . . . . . 7  |-  ( ph  ->  1  e.  RR )
3 stoweidlem1.5 . . . . . . . . . 10  |-  ( ph  ->  A  e.  RR+ )
4 rpre 10376 . . . . . . . . . 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 9988 . . . . . . . . . 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 11136 . . . . . . . 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 9127 . . . . . 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 9988 . . . . . . . 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 11133 . . . . . 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 11136 . . . 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 9998 . . . . . . . . . . . . . 14  |-  2  e.  NN0
2524a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  2  e.  NN0 )
2625, 8jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  e.  NN0  /\  N  e.  NN0 )
)
27 nn0mulcl 10016 . . . . . . . . . . . 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 11136 . . . . . . . . . 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 9127 . . . . . . . 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 11136 . . . . . 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 9769 . . . . . . . . . 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 8838 . . . . . . . 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 11136 . . . . . 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 9991 . . . . . . . . . 10  |-  ( K  e.  NN0  ->  K  e.  CC )
4717, 46syl 15 . . . . . . . . 9  |-  ( ph  ->  K  e.  CC )
48 nnne0 9794 . . . . . . . . . 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 10378 . . . . . . . . . 10  |-  ( A  e.  RR+  ->  A  e.  CC )
523, 51syl 15 . . . . . . . . 9  |-  ( ph  ->  A  e.  CC )
53 rpgt0 10381 . . . . . . . . . . . 12  |-  ( A  e.  RR+  ->  0  < 
A )
543, 53syl 15 . . . . . . . . . . 11  |-  ( ph  ->  0  <  A )
5554olcd 382 . . . . . . . . . 10  |-  ( ph  ->  ( A  <  0  \/  0  <  A ) )
56 0re 8854 . . . . . . . . . . . . 13  |-  0  e.  RR
5756a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  0  e.  RR )
585, 57jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( A  e.  RR  /\  0  e.  RR ) )
59 lttri2 8920 . . . . . . . . . . 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 9426 . . . . . . 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 8837 . . . . . . . . 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 11149 . . . . . . 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 9495 . . . 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 10376 . . . . . . . . . 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 8838 . . . . . . . 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 11136 . . . . . 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 10378 . . . . . . . . . 10  |-  ( D  e.  RR+  ->  D  e.  CC )
8676, 85syl 15 . . . . . . . . 9  |-  ( ph  ->  D  e.  CC )
87 rpne0 10385 . . . . . . . . . 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 9426 . . . . . . 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 8837 . . . . . . . . 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 11149 . . . . . . 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 9495 . . . 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 11136 . . . . . . . . . . . . . . 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 8838 . . . . . . . . . . . . 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 8836 . . . . . . . . . . 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 8838 . . . . . . . . 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 9495 . . . . . . 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 8836 . . . . . . . . . . . . 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 11136 . . . . . . . . . . 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 8838 . . . . . . . . 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 9495 . . . . . . 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 9495 . . . . . . . . . . 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 11177 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  RR  /\  0  <_  A  /\  A  <_  1 )  /\  N  e.  NN0 )  -> 
( A ^ N
)  <_  1 )
140138, 139syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A ^ N
)  <_  1 )
141 subge0 9303 . . . . . . . . . . . . . 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 11154 . . . . . . . . . . 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 11137 . . . . . . . . . . . . . . 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 9467 . . . . . . . . . . . . 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 9011 . . . . . . . . . . . . . . 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 9313 . . . . . . . . . . . . . . . 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 9258 . . . . . . . . . . . . . . . 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 4061 . . . . . . . . . . . . 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 8836 . . . . . . . . . . . . . . . 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 10061 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  NN  ->  N  e.  ZZ )
1666, 165syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  ZZ )
167 nngt0 9791 . . . . . . . . . . . . . . . . . . . . . 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 8916 . . . . . . . . . . . . . . . . . . 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 11151 . . . . . . . . . . . . . . . . 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 9637 . . . . . . . . . . . . . 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 4061 . . . . . . . . . . 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 11157 . . . . . . . . . . . . . 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 5890 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  +  ( ( K  x.  A
) ^ N ) )  =  ( 1  +  ( ( K ^ N )  x.  ( A ^ N
) ) ) )
187186oveq1d 5889 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  +  ( ( K  x.  A ) ^ N
) )  /  (
( K  x.  A
) ^ N ) )  =  ( ( 1  +  ( ( K ^ N )  x.  ( A ^ N ) ) )  /  ( ( K  x.  A ) ^ N ) ) )
188182, 187breqtrd 4063 . . . . . . . . . 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 9634 . . . . . . . 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 8811 . . . . . . . . . . . . . 14  |-  1  e.  CC
194193a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  1  e.  CC )
19552, 8jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  e.  CC  /\  N  e.  NN0 )
)
196 expcl 11137 . . . . . . . . . . . . . 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 9067 . . . . . . . . . . . 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 11137 . . . . . . . . . 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 11137 . . . . . . . . . . . . . 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 8837 . . . . . . . . . . . 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 8835 . . . . . . . . . 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 9458 . . . . . . . 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 4065 . . . . . 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 8839 . . . . . . . . . . . 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 5890 . . . . . . . . . 10  |-  ( ph  ->  ( 1  +  ( ( K ^ N
)  x.  ( A ^ N ) ) )  =  ( 1  +  ( ( A ^ N )  x.  ( K ^ N
) ) ) )
222 renegcl 9126 . . . . . . . . . . . . . . 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 9299 . . . . . . . . . . . . . . . . 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 11154 . . . . . . . . . . . . . . 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 8930 . . . . . . . . . . . . 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 11243 . . . . . . . . . . 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 4059 . . . . . . . . 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 9627 . . . . . . . 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 9637 . . . . . . . 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 8930 . . . . 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 8835 . . . . . . . . . . 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 11157 . . . . . . . . 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 2301 . . . . . . 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 8839 . . . . . . . . 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 5889 . . . . . . 7  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) )  x.  ( 1  +  ( A ^ N ) ) ) ^ ( K ^ N ) )  =  ( ( ( 1  +  ( A ^ N ) )  x.  ( 1  -  ( A ^ N
) ) ) ^
( K ^ N
) ) )
259254, 258eqtrd 2328 . . . . . 6  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
( 1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )  =  ( ( ( 1  +  ( A ^ N ) )  x.  ( 1  -  ( A ^ N ) ) ) ^ ( K ^ N ) ) )
260 subsq 11226 . . . . . . . . 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 11214 . . . . . . . . . 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 11163 . . . . . . . . . . . 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 2301 . . . . . . . . . 10  |-  ( ph  ->  ( ( A ^ N ) ^ 2 )  =  ( A ^ ( N  x.  2 ) ) )
268 nncn 9770 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  N  e.  CC )
2696, 268syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  CC )
270 2cn 9832 . . . . . . . . . . . . . 14  |-  2  e.  CC
271270a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  2  e.  CC )
272269, 271jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  e.  CC  /\  2  e.  CC ) )
273 mulcom 8839 . . . . . . . . . . . 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 5890 . . . . . . . . . 10  |-  ( ph  ->  ( A ^ ( N  x.  2 ) )  =  ( A ^ ( 2  x.  N ) ) )
276267, 275eqtrd 2328 . . . . . . . . 9  |-  ( ph  ->  ( ( A ^ N ) ^ 2 )  =  ( A ^ ( 2  x.  N ) ) )
277263, 276oveq12d 5892 . . . . . . . 8  |-  ( ph  ->  ( ( 1 ^ 2 )  -  (
( A ^ N
) ^ 2 ) )  =  ( 1  -  ( A ^
( 2  x.  N
) ) ) )
278261, 277eqtr3d 2330 . . . . . . 7  |-  ( ph  ->  ( ( 1  +  ( A ^ N
) )  x.  (
1  -  ( A ^ N ) ) )  =  ( 1  -  ( A ^
( 2  x.  N
) ) ) )
279278oveq1d 5889 . . . . . 6  |-  ( ph  ->  ( ( ( 1  +  ( A ^ N ) )  x.  ( 1  -  ( A ^ N ) ) ) ^ ( K ^ N ) )  =  ( ( 1  -  ( A ^
( 2  x.  N
) ) ) ^
( K ^ N
) ) )
280259, 279eqtrd 2328 . . . . 5  |-  ( ph  ->  ( ( ( 1  -  ( A ^ N ) ) ^
( K ^ N
) )  x.  (
( 1  +  ( A ^ N ) ) ^ ( K ^ N ) ) )  =  ( ( 1  -  ( A ^ ( 2  x.  N ) ) ) ^ ( K ^ N ) ) )
281280oveq1d 5889 . . . 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 4063 . . 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 11177 . . . . . . . . . . 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 9303 . . . . . . . . . . 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 11154 . . . . . . . 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 9083 . . . . . . . . . . . . 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 11154 . . . . . . . . . . . . 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 4072 . . . . . . . . . . 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 9268 . . . . . . . . . . . 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 11177 . . . . . . . 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 10381 . . . . . . . . . . . . 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 8916 . . . . . . . . . 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 11151 . . . . . . . 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 8926 . . . . . . . . . . . . . 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 8926 . . . . . . . . . . . . . 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 9307 . . . . . . . . . . 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 9627 . . . . . . . . . . 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 11176 . . . . . . . 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 9665 . . . 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 8930 . 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 1632    e. wcel 1696    =/= wne 2459   class class class wbr 4039  (class class class)co 5874   CCcc 8751   RRcr 8752   0cc0 8753   1c1 8754    + caddc 8756    x. cmul 8758    < clt 8883    <_ cle 8884    - cmin 9053   -ucneg 9054    / cdiv 9439   NNcn 9762   2c2 9811   NN0cn0 9981   ZZcz 10040   RR+crp 10370   ^cexp 11120
This theorem is referenced by:  stoweidlem25  27876
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830
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 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-2nd 6139  df-riota 6320  df-recs 6404  df-rdg 6439  df-er 6676  df-en 6880  df-dom 6881  df-sdom 6882  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-div 9440  df-nn 9763  df-2 9820  df-n0 9982  df-z 10041  df-uz 10247  df-rp 10371  df-seq 11063  df-exp 11121
  Copyright terms: Public domain W3C validator