Metamath Proof Explorer

Theorem aaliou3lem8

Description: Lemma for aaliou3 . (Contributed by Stefan O'Rear, 20-Nov-2014)

Ref Expression
Assertion aaliou3lem8 
|- ( ( A e. NN /\ B e. RR+ ) -> E. x e. NN ( 2 x. ( 2 ^ -u ( ! ` ( x + 1 ) ) ) ) <_ ( B / ( ( 2 ^ ( ! ` x ) ) ^ A ) ) )

Proof

Step Hyp Ref Expression
1 2rp 
 |-  2 e. RR+
2 rpdivcl 
 |-  ( ( 2 e. RR+ /\ B e. RR+ ) -> ( 2 / B ) e. RR+ )
3 1 2 mpan 
 |-  ( B e. RR+ -> ( 2 / B ) e. RR+ )
4 3 rpred 
 |-  ( B e. RR+ -> ( 2 / B ) e. RR )
5 2re 
 |-  2 e. RR
6 1lt2 
 |-  1 < 2
7 expnbnd 
 |-  ( ( ( 2 / B ) e. RR /\ 2 e. RR /\ 1 < 2 ) -> E. a e. NN ( 2 / B ) < ( 2 ^ a ) )
8 5 6 7 mp3an23 
 |-  ( ( 2 / B ) e. RR -> E. a e. NN ( 2 / B ) < ( 2 ^ a ) )
9 4 8 syl 
 |-  ( B e. RR+ -> E. a e. NN ( 2 / B ) < ( 2 ^ a ) )
10 9 adantl 
 |-  ( ( A e. NN /\ B e. RR+ ) -> E. a e. NN ( 2 / B ) < ( 2 ^ a ) )
11 simprl 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> a e. NN )
12 simpll 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> A e. NN )
13 nnaddm1cl 
 |-  ( ( a e. NN /\ A e. NN ) -> ( ( a + A ) - 1 ) e. NN )
14 11 12 13 syl2anc 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( a + A ) - 1 ) e. NN )
15 simplr 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> B e. RR+ )
16 rerpdivcl 
 |-  ( ( 2 e. RR /\ B e. RR+ ) -> ( 2 / B ) e. RR )
17 5 15 16 sylancr 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 / B ) e. RR )
18 11 nnnn0d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> a e. NN0 )
19 reexpcl 
 |-  ( ( 2 e. RR /\ a e. NN0 ) -> ( 2 ^ a ) e. RR )
20 5 18 19 sylancr 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 ^ a ) e. RR )
21 11 12 nnaddcld 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( a + A ) e. NN )
22 nnm1nn0 
 |-  ( ( a + A ) e. NN -> ( ( a + A ) - 1 ) e. NN0 )
23 21 22 syl 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( a + A ) - 1 ) e. NN0 )
24 peano2nn0 
 |-  ( ( ( a + A ) - 1 ) e. NN0 -> ( ( ( a + A ) - 1 ) + 1 ) e. NN0 )
25 23 24 syl 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( ( a + A ) - 1 ) + 1 ) e. NN0 )
26 25 faccld 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) e. NN )
27 26 nnzd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) e. ZZ )
28 23 faccld 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ! ` ( ( a + A ) - 1 ) ) e. NN )
29 28 nnzd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ! ` ( ( a + A ) - 1 ) ) e. ZZ )
30 12 nnzd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> A e. ZZ )
31 29 30 zmulcld 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) e. ZZ )
32 27 31 zsubcld 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) e. ZZ )
33 rpexpcl 
 |-  ( ( 2 e. RR+ /\ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) e. ZZ ) -> ( 2 ^ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) e. RR+ )
34 1 32 33 sylancr 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 ^ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) e. RR+ )
35 34 rpred 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 ^ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) e. RR )
36 simprr 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 / B ) < ( 2 ^ a ) )
37 17 20 36 ltled 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 / B ) <_ ( 2 ^ a ) )
38 5 a1i 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> 2 e. RR )
39 1le2 
 |-  1 <_ 2
40 39 a1i 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> 1 <_ 2 )
41 11 nnred 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> a e. RR )
42 28 nnred 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ! ` ( ( a + A ) - 1 ) ) e. RR )
43 18 nn0ge0d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> 0 <_ a )
44 28 nnge1d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> 1 <_ ( ! ` ( ( a + A ) - 1 ) ) )
45 41 42 43 44 lemulge12d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> a <_ ( ( ! ` ( ( a + A ) - 1 ) ) x. a ) )
46 facp1 
 |-  ( ( ( a + A ) - 1 ) e. NN0 -> ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) = ( ( ! ` ( ( a + A ) - 1 ) ) x. ( ( ( a + A ) - 1 ) + 1 ) ) )
47 23 46 syl 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) = ( ( ! ` ( ( a + A ) - 1 ) ) x. ( ( ( a + A ) - 1 ) + 1 ) ) )
48 47 oveq1d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) = ( ( ( ! ` ( ( a + A ) - 1 ) ) x. ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) )
49 28 nncnd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ! ` ( ( a + A ) - 1 ) ) e. CC )
50 25 nn0cnd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( ( a + A ) - 1 ) + 1 ) e. CC )
51 12 nncnd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> A e. CC )
52 49 50 51 subdid 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( ! ` ( ( a + A ) - 1 ) ) x. ( ( ( ( a + A ) - 1 ) + 1 ) - A ) ) = ( ( ( ! ` ( ( a + A ) - 1 ) ) x. ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) )
53 11 nncnd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> a e. CC )
54 21 nncnd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( a + A ) e. CC )
55 1cnd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> 1 e. CC )
56 54 55 npcand 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( ( a + A ) - 1 ) + 1 ) = ( a + A ) )
57 53 51 56 mvrraddd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( ( ( a + A ) - 1 ) + 1 ) - A ) = a )
58 57 oveq2d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( ! ` ( ( a + A ) - 1 ) ) x. ( ( ( ( a + A ) - 1 ) + 1 ) - A ) ) = ( ( ! ` ( ( a + A ) - 1 ) ) x. a ) )
59 48 52 58 3eqtr2d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) = ( ( ! ` ( ( a + A ) - 1 ) ) x. a ) )
60 45 59 breqtrrd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> a <_ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) )
61 11 nnzd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> a e. ZZ )
62 eluz 
 |-  ( ( a e. ZZ /\ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) e. ZZ ) -> ( ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) e. ( ZZ>= ` a ) <-> a <_ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) )
63 61 32 62 syl2anc 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) e. ( ZZ>= ` a ) <-> a <_ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) )
64 60 63 mpbird 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) e. ( ZZ>= ` a ) )
65 38 40 64 leexp2ad 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 ^ a ) <_ ( 2 ^ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) )
66 17 20 35 37 65 letrd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 / B ) <_ ( 2 ^ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) )
67 rpcnne0 
 |-  ( 2 e. RR+ -> ( 2 e. CC /\ 2 =/= 0 ) )
68 1 67 mp1i 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 e. CC /\ 2 =/= 0 ) )
69 expsub 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) e. ZZ /\ ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) e. ZZ ) ) -> ( 2 ^ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) = ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) / ( 2 ^ ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) )
70 68 27 31 69 syl12anc 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 ^ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) = ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) / ( 2 ^ ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) )
71 2cn 
 |-  2 e. CC
72 71 a1i 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> 2 e. CC )
73 12 nnnn0d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> A e. NN0 )
74 28 nnnn0d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ! ` ( ( a + A ) - 1 ) ) e. NN0 )
75 72 73 74 expmuld 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 ^ ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) = ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) )
76 75 oveq2d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) / ( 2 ^ ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) = ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) )
77 rpexpcl 
 |-  ( ( 2 e. RR+ /\ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) e. ZZ ) -> ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) e. RR+ )
78 1 27 77 sylancr 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) e. RR+ )
79 78 rpcnd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) e. CC )
80 rpexpcl 
 |-  ( ( 2 e. RR+ /\ ( ! ` ( ( a + A ) - 1 ) ) e. ZZ ) -> ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) e. RR+ )
81 1 29 80 sylancr 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) e. RR+ )
82 81 30 rpexpcld 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) e. RR+ )
83 82 rpcnd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) e. CC )
84 82 rpne0d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) =/= 0 )
85 79 83 84 divrecd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) = ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) )
86 70 76 85 3eqtrrd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) = ( 2 ^ ( ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) - ( ( ! ` ( ( a + A ) - 1 ) ) x. A ) ) ) )
87 66 86 breqtrrd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 / B ) <_ ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) )
88 82 rpreccld 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) e. RR+ )
89 78 88 rpmulcld 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) e. RR+ )
90 89 rpred 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) e. RR )
91 38 90 15 ledivmuld 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( 2 / B ) <_ ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) <-> 2 <_ ( B x. ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) ) ) )
92 87 91 mpbid 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> 2 <_ ( B x. ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) ) )
93 15 rpcnd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> B e. CC )
94 88 rpcnd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) e. CC )
95 93 79 94 mul12d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( B x. ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) ) = ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) x. ( B x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) ) )
96 92 95 breqtrd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> 2 <_ ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) x. ( B x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) ) )
97 15 88 rpmulcld 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( B x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) e. RR+ )
98 97 rpred 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( B x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) e. RR )
99 38 98 78 ledivmuld 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ( 2 / ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) <_ ( B x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) <-> 2 <_ ( ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) x. ( B x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) ) ) )
100 96 99 mpbird 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 / ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) <_ ( B x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) )
101 26 nnnn0d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) e. NN0 )
102 expneg 
 |-  ( ( 2 e. CC /\ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) e. NN0 ) -> ( 2 ^ -u ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) = ( 1 / ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) )
103 71 101 102 sylancr 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 ^ -u ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) = ( 1 / ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) )
104 103 oveq2d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 x. ( 2 ^ -u ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) = ( 2 x. ( 1 / ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) ) )
105 78 rpne0d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) =/= 0 )
106 72 79 105 divrecd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 / ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) = ( 2 x. ( 1 / ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) ) )
107 104 106 eqtr4d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 x. ( 2 ^ -u ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) = ( 2 / ( 2 ^ ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) )
108 93 83 84 divrecd 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( B / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) = ( B x. ( 1 / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) )
109 100 107 108 3brtr4d 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> ( 2 x. ( 2 ^ -u ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) <_ ( B / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) )
110 fvoveq1 
 |-  ( x = ( ( a + A ) - 1 ) -> ( ! ` ( x + 1 ) ) = ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) )
111 110 negeqd 
 |-  ( x = ( ( a + A ) - 1 ) -> -u ( ! ` ( x + 1 ) ) = -u ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) )
112 111 oveq2d 
 |-  ( x = ( ( a + A ) - 1 ) -> ( 2 ^ -u ( ! ` ( x + 1 ) ) ) = ( 2 ^ -u ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) )
113 112 oveq2d 
 |-  ( x = ( ( a + A ) - 1 ) -> ( 2 x. ( 2 ^ -u ( ! ` ( x + 1 ) ) ) ) = ( 2 x. ( 2 ^ -u ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) )
114 fveq2 
 |-  ( x = ( ( a + A ) - 1 ) -> ( ! ` x ) = ( ! ` ( ( a + A ) - 1 ) ) )
115 114 oveq2d 
 |-  ( x = ( ( a + A ) - 1 ) -> ( 2 ^ ( ! ` x ) ) = ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) )
116 115 oveq1d 
 |-  ( x = ( ( a + A ) - 1 ) -> ( ( 2 ^ ( ! ` x ) ) ^ A ) = ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) )
117 116 oveq2d 
 |-  ( x = ( ( a + A ) - 1 ) -> ( B / ( ( 2 ^ ( ! ` x ) ) ^ A ) ) = ( B / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) )
118 113 117 breq12d 
 |-  ( x = ( ( a + A ) - 1 ) -> ( ( 2 x. ( 2 ^ -u ( ! ` ( x + 1 ) ) ) ) <_ ( B / ( ( 2 ^ ( ! ` x ) ) ^ A ) ) <-> ( 2 x. ( 2 ^ -u ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) <_ ( B / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) )
119 118 rspcev 
 |-  ( ( ( ( a + A ) - 1 ) e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( ( ( a + A ) - 1 ) + 1 ) ) ) ) <_ ( B / ( ( 2 ^ ( ! ` ( ( a + A ) - 1 ) ) ) ^ A ) ) ) -> E. x e. NN ( 2 x. ( 2 ^ -u ( ! ` ( x + 1 ) ) ) ) <_ ( B / ( ( 2 ^ ( ! ` x ) ) ^ A ) ) )
120 14 109 119 syl2anc 
 |-  ( ( ( A e. NN /\ B e. RR+ ) /\ ( a e. NN /\ ( 2 / B ) < ( 2 ^ a ) ) ) -> E. x e. NN ( 2 x. ( 2 ^ -u ( ! ` ( x + 1 ) ) ) ) <_ ( B / ( ( 2 ^ ( ! ` x ) ) ^ A ) ) )
121 10 120 rexlimddv 
 |-  ( ( A e. NN /\ B e. RR+ ) -> E. x e. NN ( 2 x. ( 2 ^ -u ( ! ` ( x + 1 ) ) ) ) <_ ( B / ( ( 2 ^ ( ! ` x ) ) ^ A ) ) )