Metamath Proof Explorer

Theorem stoweidlem1

Description: Lemma for stoweid . This lemma is used by Lemma 1 in BrosowskiDeutsh p. 90; the key step uses Bernoulli's inequality bernneq . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses 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 stoweidlem1 
|- ( ph -> ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) <_ ( 1 / ( ( K x. D ) ^ N ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem1.1 
 |-  ( ph -> N e. NN )
2 stoweidlem1.2 
 |-  ( ph -> K e. NN )
3 stoweidlem1.3 
 |-  ( ph -> D e. RR+ )
4 stoweidlem1.5 
 |-  ( ph -> A e. RR+ )
5 stoweidlem1.6 
 |-  ( ph -> 0 <_ A )
6 stoweidlem1.7 
 |-  ( ph -> A <_ 1 )
7 stoweidlem1.8 
 |-  ( ph -> D <_ A )
8 1re 
 |-  1 e. RR
9 8 a1i 
 |-  ( ph -> 1 e. RR )
10 4 rpred 
 |-  ( ph -> A e. RR )
11 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
12 10 11 reexpcld 
 |-  ( ph -> ( A ^ N ) e. RR )
13 9 12 resubcld 
 |-  ( ph -> ( 1 - ( A ^ N ) ) e. RR )
14 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
15 14 11 nn0expcld 
 |-  ( ph -> ( K ^ N ) e. NN0 )
16 13 15 reexpcld 
 |-  ( ph -> ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) e. RR )
17 2nn0 
 |-  2 e. NN0
18 17 a1i 
 |-  ( ph -> 2 e. NN0 )
19 18 11 nn0mulcld 
 |-  ( ph -> ( 2 x. N ) e. NN0 )
20 10 19 reexpcld 
 |-  ( ph -> ( A ^ ( 2 x. N ) ) e. RR )
21 9 20 resubcld 
 |-  ( ph -> ( 1 - ( A ^ ( 2 x. N ) ) ) e. RR )
22 21 15 reexpcld 
 |-  ( ph -> ( ( 1 - ( A ^ ( 2 x. N ) ) ) ^ ( K ^ N ) ) e. RR )
23 2 nnred 
 |-  ( ph -> K e. RR )
24 23 10 remulcld 
 |-  ( ph -> ( K x. A ) e. RR )
25 24 11 reexpcld 
 |-  ( ph -> ( ( K x. A ) ^ N ) e. RR )
26 2 nncnd 
 |-  ( ph -> K e. CC )
27 4 rpcnd 
 |-  ( ph -> A e. CC )
28 2 nnne0d 
 |-  ( ph -> K =/= 0 )
29 4 rpne0d 
 |-  ( ph -> A =/= 0 )
30 26 27 28 29 mulne0d 
 |-  ( ph -> ( K x. A ) =/= 0 )
31 26 27 mulcld 
 |-  ( ph -> ( K x. A ) e. CC )
32 expne0 
 |-  ( ( ( K x. A ) e. CC /\ N e. NN ) -> ( ( ( K x. A ) ^ N ) =/= 0 <-> ( K x. A ) =/= 0 ) )
33 31 1 32 syl2anc 
 |-  ( ph -> ( ( ( K x. A ) ^ N ) =/= 0 <-> ( K x. A ) =/= 0 ) )
34 30 33 mpbird 
 |-  ( ph -> ( ( K x. A ) ^ N ) =/= 0 )
35 22 25 34 redivcld 
 |-  ( ph -> ( ( ( 1 - ( A ^ ( 2 x. N ) ) ) ^ ( K ^ N ) ) / ( ( K x. A ) ^ N ) ) e. RR )
36 3 rpred 
 |-  ( ph -> D e. RR )
37 23 36 remulcld 
 |-  ( ph -> ( K x. D ) e. RR )
38 37 11 reexpcld 
 |-  ( ph -> ( ( K x. D ) ^ N ) e. RR )
39 3 rpcnd 
 |-  ( ph -> D e. CC )
40 3 rpne0d 
 |-  ( ph -> D =/= 0 )
41 26 39 28 40 mulne0d 
 |-  ( ph -> ( K x. D ) =/= 0 )
42 26 39 mulcld 
 |-  ( ph -> ( K x. D ) e. CC )
43 expne0 
 |-  ( ( ( K x. D ) e. CC /\ N e. NN ) -> ( ( ( K x. D ) ^ N ) =/= 0 <-> ( K x. D ) =/= 0 ) )
44 42 1 43 syl2anc 
 |-  ( ph -> ( ( ( K x. D ) ^ N ) =/= 0 <-> ( K x. D ) =/= 0 ) )
45 41 44 mpbird 
 |-  ( ph -> ( ( K x. D ) ^ N ) =/= 0 )
46 9 38 45 redivcld 
 |-  ( ph -> ( 1 / ( ( K x. D ) ^ N ) ) e. RR )
47 23 11 reexpcld 
 |-  ( ph -> ( K ^ N ) e. RR )
48 47 12 remulcld 
 |-  ( ph -> ( ( K ^ N ) x. ( A ^ N ) ) e. RR )
49 9 48 readdcld 
 |-  ( ph -> ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) e. RR )
50 16 49 remulcld 
 |-  ( ph -> ( ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) x. ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) ) e. RR )
51 50 25 34 redivcld 
 |-  ( ph -> ( ( ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) x. ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) ) / ( ( K x. A ) ^ N ) ) e. RR )
52 9 12 readdcld 
 |-  ( ph -> ( 1 + ( A ^ N ) ) e. RR )
53 52 15 reexpcld 
 |-  ( ph -> ( ( 1 + ( A ^ N ) ) ^ ( K ^ N ) ) e. RR )
54 16 53 remulcld 
 |-  ( ph -> ( ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) x. ( ( 1 + ( A ^ N ) ) ^ ( K ^ N ) ) ) e. RR )
55 54 25 34 redivcld 
 |-  ( ph -> ( ( ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) x. ( ( 1 + ( A ^ N ) ) ^ ( K ^ N ) ) ) / ( ( K x. A ) ^ N ) ) e. RR )
56 49 25 34 redivcld 
 |-  ( ph -> ( ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) / ( ( K x. A ) ^ N ) ) e. RR )
57 exple1 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A <_ 1 ) /\ N e. NN0 ) -> ( A ^ N ) <_ 1 )
58 10 5 6 11 57 syl31anc 
 |-  ( ph -> ( A ^ N ) <_ 1 )
59 9 12 subge0d 
 |-  ( ph -> ( 0 <_ ( 1 - ( A ^ N ) ) <-> ( A ^ N ) <_ 1 ) )
60 58 59 mpbird 
 |-  ( ph -> 0 <_ ( 1 - ( A ^ N ) ) )
61 13 15 60 expge0d 
 |-  ( ph -> 0 <_ ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) )
62 31 11 expcld 
 |-  ( ph -> ( ( K x. A ) ^ N ) e. CC )
63 62 34 dividd 
 |-  ( ph -> ( ( ( K x. A ) ^ N ) / ( ( K x. A ) ^ N ) ) = 1 )
64 62 addlidd 
 |-  ( ph -> ( 0 + ( ( K x. A ) ^ N ) ) = ( ( K x. A ) ^ N ) )
65 0red 
 |-  ( ph -> 0 e. RR )
66 0le1 
 |-  0 <_ 1
67 66 a1i 
 |-  ( ph -> 0 <_ 1 )
68 65 9 25 67 leadd1dd 
 |-  ( ph -> ( 0 + ( ( K x. A ) ^ N ) ) <_ ( 1 + ( ( K x. A ) ^ N ) ) )
69 64 68 eqbrtrrd 
 |-  ( ph -> ( ( K x. A ) ^ N ) <_ ( 1 + ( ( K x. A ) ^ N ) ) )
70 9 25 readdcld 
 |-  ( ph -> ( 1 + ( ( K x. A ) ^ N ) ) e. RR )
71 1 nnzd 
 |-  ( ph -> N e. ZZ )
72 2 nngt0d 
 |-  ( ph -> 0 < K )
73 4 rpgt0d 
 |-  ( ph -> 0 < A )
74 23 10 72 73 mulgt0d 
 |-  ( ph -> 0 < ( K x. A ) )
75 expgt0 
 |-  ( ( ( K x. A ) e. RR /\ N e. ZZ /\ 0 < ( K x. A ) ) -> 0 < ( ( K x. A ) ^ N ) )
76 24 71 74 75 syl3anc 
 |-  ( ph -> 0 < ( ( K x. A ) ^ N ) )
77 lediv1 
 |-  ( ( ( ( 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 ) ) ) )
78 25 70 25 76 77 syl112anc 
 |-  ( 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 ) ) ) )
79 69 78 mpbid 
 |-  ( ph -> ( ( ( K x. A ) ^ N ) / ( ( K x. A ) ^ N ) ) <_ ( ( 1 + ( ( K x. A ) ^ N ) ) / ( ( K x. A ) ^ N ) ) )
80 63 79 eqbrtrrd 
 |-  ( ph -> 1 <_ ( ( 1 + ( ( K x. A ) ^ N ) ) / ( ( K x. A ) ^ N ) ) )
81 26 27 11 mulexpd 
 |-  ( ph -> ( ( K x. A ) ^ N ) = ( ( K ^ N ) x. ( A ^ N ) ) )
82 81 oveq2d 
 |-  ( ph -> ( 1 + ( ( K x. A ) ^ N ) ) = ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) )
83 82 oveq1d 
 |-  ( ph -> ( ( 1 + ( ( K x. A ) ^ N ) ) / ( ( K x. A ) ^ N ) ) = ( ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) / ( ( K x. A ) ^ N ) ) )
84 80 83 breqtrd 
 |-  ( ph -> 1 <_ ( ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) / ( ( K x. A ) ^ N ) ) )
85 16 56 61 84 lemulge11d 
 |-  ( ph -> ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) <_ ( ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) x. ( ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) / ( ( K x. A ) ^ N ) ) ) )
86 1cnd 
 |-  ( ph -> 1 e. CC )
87 27 11 expcld 
 |-  ( ph -> ( A ^ N ) e. CC )
88 86 87 subcld 
 |-  ( ph -> ( 1 - ( A ^ N ) ) e. CC )
89 88 15 expcld 
 |-  ( ph -> ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) e. CC )
90 26 11 expcld 
 |-  ( ph -> ( K ^ N ) e. CC )
91 90 87 mulcld 
 |-  ( ph -> ( ( K ^ N ) x. ( A ^ N ) ) e. CC )
92 86 91 addcld 
 |-  ( ph -> ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) e. CC )
93 89 92 62 34 divassd 
 |-  ( 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 ) ) ) )
94 85 93 breqtrrd 
 |-  ( ph -> ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) <_ ( ( ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) x. ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) ) / ( ( K x. A ) ^ N ) ) )
95 90 87 mulcomd 
 |-  ( ph -> ( ( K ^ N ) x. ( A ^ N ) ) = ( ( A ^ N ) x. ( K ^ N ) ) )
96 95 oveq2d 
 |-  ( ph -> ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) = ( 1 + ( ( A ^ N ) x. ( K ^ N ) ) ) )
97 9 renegcld 
 |-  ( ph -> -u 1 e. RR )
98 le0neg2 
 |-  ( 1 e. RR -> ( 0 <_ 1 <-> -u 1 <_ 0 ) )
99 8 98 ax-mp 
 |-  ( 0 <_ 1 <-> -u 1 <_ 0 )
100 66 99 mpbi 
 |-  -u 1 <_ 0
101 100 a1i 
 |-  ( ph -> -u 1 <_ 0 )
102 10 11 5 expge0d 
 |-  ( ph -> 0 <_ ( A ^ N ) )
103 97 65 12 101 102 letrd 
 |-  ( ph -> -u 1 <_ ( A ^ N ) )
104 bernneq 
 |-  ( ( ( A ^ N ) e. RR /\ ( K ^ N ) e. NN0 /\ -u 1 <_ ( A ^ N ) ) -> ( 1 + ( ( A ^ N ) x. ( K ^ N ) ) ) <_ ( ( 1 + ( A ^ N ) ) ^ ( K ^ N ) ) )
105 12 15 103 104 syl3anc 
 |-  ( ph -> ( 1 + ( ( A ^ N ) x. ( K ^ N ) ) ) <_ ( ( 1 + ( A ^ N ) ) ^ ( K ^ N ) ) )
106 96 105 eqbrtrd 
 |-  ( ph -> ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) <_ ( ( 1 + ( A ^ N ) ) ^ ( K ^ N ) ) )
107 49 53 16 61 106 lemul2ad 
 |-  ( ph -> ( ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) x. ( 1 + ( ( K ^ N ) x. ( A ^ N ) ) ) ) <_ ( ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) x. ( ( 1 + ( A ^ N ) ) ^ ( K ^ N ) ) ) )
108 lediv1 
 |-  ( ( ( ( ( 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 ) ) ) )
109 50 54 25 76 108 syl112anc 
 |-  ( 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 ) ) ) )
110 107 109 mpbid 
 |-  ( 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 ) ) )
111 16 51 55 94 110 letrd 
 |-  ( ph -> ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) <_ ( ( ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) x. ( ( 1 + ( A ^ N ) ) ^ ( K ^ N ) ) ) / ( ( K x. A ) ^ N ) ) )
112 86 87 addcld 
 |-  ( ph -> ( 1 + ( A ^ N ) ) e. CC )
113 88 112 mulcomd 
 |-  ( ph -> ( ( 1 - ( A ^ N ) ) x. ( 1 + ( A ^ N ) ) ) = ( ( 1 + ( A ^ N ) ) x. ( 1 - ( A ^ N ) ) ) )
114 113 oveq1d 
 |-  ( ph -> ( ( ( 1 - ( A ^ N ) ) x. ( 1 + ( A ^ N ) ) ) ^ ( K ^ N ) ) = ( ( ( 1 + ( A ^ N ) ) x. ( 1 - ( A ^ N ) ) ) ^ ( K ^ N ) ) )
115 88 112 15 mulexpd 
 |-  ( ph -> ( ( ( 1 - ( A ^ N ) ) x. ( 1 + ( A ^ N ) ) ) ^ ( K ^ N ) ) = ( ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) x. ( ( 1 + ( A ^ N ) ) ^ ( K ^ N ) ) ) )
116 subsq 
 |-  ( ( 1 e. CC /\ ( A ^ N ) e. CC ) -> ( ( 1 ^ 2 ) - ( ( A ^ N ) ^ 2 ) ) = ( ( 1 + ( A ^ N ) ) x. ( 1 - ( A ^ N ) ) ) )
117 86 87 116 syl2anc 
 |-  ( ph -> ( ( 1 ^ 2 ) - ( ( A ^ N ) ^ 2 ) ) = ( ( 1 + ( A ^ N ) ) x. ( 1 - ( A ^ N ) ) ) )
118 sq1 
 |-  ( 1 ^ 2 ) = 1
119 118 a1i 
 |-  ( ph -> ( 1 ^ 2 ) = 1 )
120 27 18 11 expmuld 
 |-  ( ph -> ( A ^ ( N x. 2 ) ) = ( ( A ^ N ) ^ 2 ) )
121 1 nncnd 
 |-  ( ph -> N e. CC )
122 2cnd 
 |-  ( ph -> 2 e. CC )
123 121 122 mulcomd 
 |-  ( ph -> ( N x. 2 ) = ( 2 x. N ) )
124 123 oveq2d 
 |-  ( ph -> ( A ^ ( N x. 2 ) ) = ( A ^ ( 2 x. N ) ) )
125 120 124 eqtr3d 
 |-  ( ph -> ( ( A ^ N ) ^ 2 ) = ( A ^ ( 2 x. N ) ) )
126 119 125 oveq12d 
 |-  ( ph -> ( ( 1 ^ 2 ) - ( ( A ^ N ) ^ 2 ) ) = ( 1 - ( A ^ ( 2 x. N ) ) ) )
127 117 126 eqtr3d 
 |-  ( ph -> ( ( 1 + ( A ^ N ) ) x. ( 1 - ( A ^ N ) ) ) = ( 1 - ( A ^ ( 2 x. N ) ) ) )
128 127 oveq1d 
 |-  ( ph -> ( ( ( 1 + ( A ^ N ) ) x. ( 1 - ( A ^ N ) ) ) ^ ( K ^ N ) ) = ( ( 1 - ( A ^ ( 2 x. N ) ) ) ^ ( K ^ N ) ) )
129 114 115 128 3eqtr3d 
 |-  ( ph -> ( ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) x. ( ( 1 + ( A ^ N ) ) ^ ( K ^ N ) ) ) = ( ( 1 - ( A ^ ( 2 x. N ) ) ) ^ ( K ^ N ) ) )
130 129 oveq1d 
 |-  ( 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 ) ) )
131 111 130 breqtrd 
 |-  ( ph -> ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) <_ ( ( ( 1 - ( A ^ ( 2 x. N ) ) ) ^ ( K ^ N ) ) / ( ( K x. A ) ^ N ) ) )
132 22 9 jca 
 |-  ( ph -> ( ( ( 1 - ( A ^ ( 2 x. N ) ) ) ^ ( K ^ N ) ) e. RR /\ 1 e. RR ) )
133 exple1 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A <_ 1 ) /\ ( 2 x. N ) e. NN0 ) -> ( A ^ ( 2 x. N ) ) <_ 1 )
134 10 5 6 19 133 syl31anc 
 |-  ( ph -> ( A ^ ( 2 x. N ) ) <_ 1 )
135 9 20 subge0d 
 |-  ( ph -> ( 0 <_ ( 1 - ( A ^ ( 2 x. N ) ) ) <-> ( A ^ ( 2 x. N ) ) <_ 1 ) )
136 134 135 mpbird 
 |-  ( ph -> 0 <_ ( 1 - ( A ^ ( 2 x. N ) ) ) )
137 21 15 136 expge0d 
 |-  ( ph -> 0 <_ ( ( 1 - ( A ^ ( 2 x. N ) ) ) ^ ( K ^ N ) ) )
138 1m1e0 
 |-  ( 1 - 1 ) = 0
139 10 19 5 expge0d 
 |-  ( ph -> 0 <_ ( A ^ ( 2 x. N ) ) )
140 138 139 eqbrtrid 
 |-  ( ph -> ( 1 - 1 ) <_ ( A ^ ( 2 x. N ) ) )
141 9 9 20 140 subled 
 |-  ( ph -> ( 1 - ( A ^ ( 2 x. N ) ) ) <_ 1 )
142 exple1 
 |-  ( ( ( ( 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 )
143 21 136 141 15 142 syl31anc 
 |-  ( ph -> ( ( 1 - ( A ^ ( 2 x. N ) ) ) ^ ( K ^ N ) ) <_ 1 )
144 132 137 143 jca32 
 |-  ( 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 ) ) )
145 38 25 jca 
 |-  ( ph -> ( ( ( K x. D ) ^ N ) e. RR /\ ( ( K x. A ) ^ N ) e. RR ) )
146 3 rpgt0d 
 |-  ( ph -> 0 < D )
147 23 36 72 146 mulgt0d 
 |-  ( ph -> 0 < ( K x. D ) )
148 expgt0 
 |-  ( ( ( K x. D ) e. RR /\ N e. ZZ /\ 0 < ( K x. D ) ) -> 0 < ( ( K x. D ) ^ N ) )
149 37 71 147 148 syl3anc 
 |-  ( ph -> 0 < ( ( K x. D ) ^ N ) )
150 65 23 72 ltled 
 |-  ( ph -> 0 <_ K )
151 65 36 146 ltled 
 |-  ( ph -> 0 <_ D )
152 23 36 150 151 mulge0d 
 |-  ( ph -> 0 <_ ( K x. D ) )
153 36 10 23 150 7 lemul2ad 
 |-  ( ph -> ( K x. D ) <_ ( K x. A ) )
154 leexp1a 
 |-  ( ( ( ( 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 ) )
155 37 24 11 152 153 154 syl32anc 
 |-  ( ph -> ( ( K x. D ) ^ N ) <_ ( ( K x. A ) ^ N ) )
156 149 155 jca 
 |-  ( ph -> ( 0 < ( ( K x. D ) ^ N ) /\ ( ( K x. D ) ^ N ) <_ ( ( K x. A ) ^ N ) ) )
157 lediv12a 
 |-  ( ( ( ( ( ( 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 ) ) )
158 144 145 156 157 syl12anc 
 |-  ( ph -> ( ( ( 1 - ( A ^ ( 2 x. N ) ) ) ^ ( K ^ N ) ) / ( ( K x. A ) ^ N ) ) <_ ( 1 / ( ( K x. D ) ^ N ) ) )
159 16 35 46 131 158 letrd 
 |-  ( ph -> ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) <_ ( 1 / ( ( K x. D ) ^ N ) ) )