Metamath Proof Explorer

Theorem aaliou3lem2

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

Ref Expression
Hypotheses aaliou3lem.a 
|- G = ( c e. ( ZZ>= ` A ) |-> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( c - A ) ) ) )
aaliou3lem.b 
|- F = ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) )
Assertion aaliou3lem2 
|- ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( F ` B ) e. ( 0 (,] ( G ` B ) ) )

Proof

Step Hyp Ref Expression
1 aaliou3lem.a 
 |-  G = ( c e. ( ZZ>= ` A ) |-> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( c - A ) ) ) )
2 aaliou3lem.b 
 |-  F = ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) )
3 eluznn 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> B e. NN )
4 fveq2 
 |-  ( a = B -> ( ! ` a ) = ( ! ` B ) )
5 4 negeqd 
 |-  ( a = B -> -u ( ! ` a ) = -u ( ! ` B ) )
6 5 oveq2d 
 |-  ( a = B -> ( 2 ^ -u ( ! ` a ) ) = ( 2 ^ -u ( ! ` B ) ) )
7 ovex 
 |-  ( 2 ^ -u ( ! ` B ) ) e. _V
8 6 2 7 fvmpt 
 |-  ( B e. NN -> ( F ` B ) = ( 2 ^ -u ( ! ` B ) ) )
9 3 8 syl 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( F ` B ) = ( 2 ^ -u ( ! ` B ) ) )
10 2rp 
 |-  2 e. RR+
11 3 nnnn0d 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> B e. NN0 )
12 11 faccld 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( ! ` B ) e. NN )
13 12 nnzd 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( ! ` B ) e. ZZ )
14 13 znegcld 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> -u ( ! ` B ) e. ZZ )
15 rpexpcl 
 |-  ( ( 2 e. RR+ /\ -u ( ! ` B ) e. ZZ ) -> ( 2 ^ -u ( ! ` B ) ) e. RR+ )
16 10 14 15 sylancr 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( 2 ^ -u ( ! ` B ) ) e. RR+ )
17 9 16 eqeltrd 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( F ` B ) e. RR+ )
18 17 rpred 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( F ` B ) e. RR )
19 17 rpgt0d 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> 0 < ( F ` B ) )
20 fveq2 
 |-  ( b = A -> ( F ` b ) = ( F ` A ) )
21 fveq2 
 |-  ( b = A -> ( G ` b ) = ( G ` A ) )
22 20 21 breq12d 
 |-  ( b = A -> ( ( F ` b ) <_ ( G ` b ) <-> ( F ` A ) <_ ( G ` A ) ) )
23 22 imbi2d 
 |-  ( b = A -> ( ( A e. NN -> ( F ` b ) <_ ( G ` b ) ) <-> ( A e. NN -> ( F ` A ) <_ ( G ` A ) ) ) )
24 fveq2 
 |-  ( b = d -> ( F ` b ) = ( F ` d ) )
25 fveq2 
 |-  ( b = d -> ( G ` b ) = ( G ` d ) )
26 24 25 breq12d 
 |-  ( b = d -> ( ( F ` b ) <_ ( G ` b ) <-> ( F ` d ) <_ ( G ` d ) ) )
27 26 imbi2d 
 |-  ( b = d -> ( ( A e. NN -> ( F ` b ) <_ ( G ` b ) ) <-> ( A e. NN -> ( F ` d ) <_ ( G ` d ) ) ) )
28 fveq2 
 |-  ( b = ( d + 1 ) -> ( F ` b ) = ( F ` ( d + 1 ) ) )
29 fveq2 
 |-  ( b = ( d + 1 ) -> ( G ` b ) = ( G ` ( d + 1 ) ) )
30 28 29 breq12d 
 |-  ( b = ( d + 1 ) -> ( ( F ` b ) <_ ( G ` b ) <-> ( F ` ( d + 1 ) ) <_ ( G ` ( d + 1 ) ) ) )
31 30 imbi2d 
 |-  ( b = ( d + 1 ) -> ( ( A e. NN -> ( F ` b ) <_ ( G ` b ) ) <-> ( A e. NN -> ( F ` ( d + 1 ) ) <_ ( G ` ( d + 1 ) ) ) ) )
32 fveq2 
 |-  ( b = B -> ( F ` b ) = ( F ` B ) )
33 fveq2 
 |-  ( b = B -> ( G ` b ) = ( G ` B ) )
34 32 33 breq12d 
 |-  ( b = B -> ( ( F ` b ) <_ ( G ` b ) <-> ( F ` B ) <_ ( G ` B ) ) )
35 34 imbi2d 
 |-  ( b = B -> ( ( A e. NN -> ( F ` b ) <_ ( G ` b ) ) <-> ( A e. NN -> ( F ` B ) <_ ( G ` B ) ) ) )
36 nnnn0 
 |-  ( A e. NN -> A e. NN0 )
37 36 faccld 
 |-  ( A e. NN -> ( ! ` A ) e. NN )
38 37 nnzd 
 |-  ( A e. NN -> ( ! ` A ) e. ZZ )
39 38 znegcld 
 |-  ( A e. NN -> -u ( ! ` A ) e. ZZ )
40 rpexpcl 
 |-  ( ( 2 e. RR+ /\ -u ( ! ` A ) e. ZZ ) -> ( 2 ^ -u ( ! ` A ) ) e. RR+ )
41 10 39 40 sylancr 
 |-  ( A e. NN -> ( 2 ^ -u ( ! ` A ) ) e. RR+ )
42 41 rpred 
 |-  ( A e. NN -> ( 2 ^ -u ( ! ` A ) ) e. RR )
43 42 leidd 
 |-  ( A e. NN -> ( 2 ^ -u ( ! ` A ) ) <_ ( 2 ^ -u ( ! ` A ) ) )
44 nncn 
 |-  ( A e. NN -> A e. CC )
45 44 subidd 
 |-  ( A e. NN -> ( A - A ) = 0 )
46 45 oveq2d 
 |-  ( A e. NN -> ( ( 1 / 2 ) ^ ( A - A ) ) = ( ( 1 / 2 ) ^ 0 ) )
47 halfcn 
 |-  ( 1 / 2 ) e. CC
48 exp0 
 |-  ( ( 1 / 2 ) e. CC -> ( ( 1 / 2 ) ^ 0 ) = 1 )
49 47 48 ax-mp 
 |-  ( ( 1 / 2 ) ^ 0 ) = 1
50 46 49 eqtrdi 
 |-  ( A e. NN -> ( ( 1 / 2 ) ^ ( A - A ) ) = 1 )
51 50 oveq2d 
 |-  ( A e. NN -> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( A - A ) ) ) = ( ( 2 ^ -u ( ! ` A ) ) x. 1 ) )
52 41 rpcnd 
 |-  ( A e. NN -> ( 2 ^ -u ( ! ` A ) ) e. CC )
53 52 mulridd 
 |-  ( A e. NN -> ( ( 2 ^ -u ( ! ` A ) ) x. 1 ) = ( 2 ^ -u ( ! ` A ) ) )
54 51 53 eqtrd 
 |-  ( A e. NN -> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( A - A ) ) ) = ( 2 ^ -u ( ! ` A ) ) )
55 43 54 breqtrrd 
 |-  ( A e. NN -> ( 2 ^ -u ( ! ` A ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( A - A ) ) ) )
56 fveq2 
 |-  ( a = A -> ( ! ` a ) = ( ! ` A ) )
57 56 negeqd 
 |-  ( a = A -> -u ( ! ` a ) = -u ( ! ` A ) )
58 57 oveq2d 
 |-  ( a = A -> ( 2 ^ -u ( ! ` a ) ) = ( 2 ^ -u ( ! ` A ) ) )
59 ovex 
 |-  ( 2 ^ -u ( ! ` A ) ) e. _V
60 58 2 59 fvmpt 
 |-  ( A e. NN -> ( F ` A ) = ( 2 ^ -u ( ! ` A ) ) )
61 nnz 
 |-  ( A e. NN -> A e. ZZ )
62 uzid 
 |-  ( A e. ZZ -> A e. ( ZZ>= ` A ) )
63 oveq1 
 |-  ( c = A -> ( c - A ) = ( A - A ) )
64 63 oveq2d 
 |-  ( c = A -> ( ( 1 / 2 ) ^ ( c - A ) ) = ( ( 1 / 2 ) ^ ( A - A ) ) )
65 64 oveq2d 
 |-  ( c = A -> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( c - A ) ) ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( A - A ) ) ) )
66 ovex 
 |-  ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( A - A ) ) ) e. _V
67 65 1 66 fvmpt 
 |-  ( A e. ( ZZ>= ` A ) -> ( G ` A ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( A - A ) ) ) )
68 61 62 67 3syl 
 |-  ( A e. NN -> ( G ` A ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( A - A ) ) ) )
69 55 60 68 3brtr4d 
 |-  ( A e. NN -> ( F ` A ) <_ ( G ` A ) )
70 eluznn 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> d e. NN )
71 70 nnnn0d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> d e. NN0 )
72 71 faccld 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ! ` d ) e. NN )
73 72 nnzd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ! ` d ) e. ZZ )
74 73 znegcld 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> -u ( ! ` d ) e. ZZ )
75 rpexpcl 
 |-  ( ( 2 e. RR+ /\ -u ( ! ` d ) e. ZZ ) -> ( 2 ^ -u ( ! ` d ) ) e. RR+ )
76 10 74 75 sylancr 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 2 ^ -u ( ! ` d ) ) e. RR+ )
77 76 rpred 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 2 ^ -u ( ! ` d ) ) e. RR )
78 76 rpge0d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> 0 <_ ( 2 ^ -u ( ! ` d ) ) )
79 simpl 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> A e. NN )
80 79 nnnn0d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> A e. NN0 )
81 80 faccld 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ! ` A ) e. NN )
82 81 nnzd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ! ` A ) e. ZZ )
83 82 znegcld 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> -u ( ! ` A ) e. ZZ )
84 10 83 40 sylancr 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 2 ^ -u ( ! ` A ) ) e. RR+ )
85 halfre 
 |-  ( 1 / 2 ) e. RR
86 halfgt0 
 |-  0 < ( 1 / 2 )
87 85 86 elrpii 
 |-  ( 1 / 2 ) e. RR+
88 eluzelz 
 |-  ( d e. ( ZZ>= ` A ) -> d e. ZZ )
89 zsubcl 
 |-  ( ( d e. ZZ /\ A e. ZZ ) -> ( d - A ) e. ZZ )
90 88 61 89 syl2anr 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( d - A ) e. ZZ )
91 rpexpcl 
 |-  ( ( ( 1 / 2 ) e. RR+ /\ ( d - A ) e. ZZ ) -> ( ( 1 / 2 ) ^ ( d - A ) ) e. RR+ )
92 87 90 91 sylancr 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( 1 / 2 ) ^ ( d - A ) ) e. RR+ )
93 84 92 rpmulcld 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) e. RR+ )
94 93 rpred 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) e. RR )
95 77 78 94 jca31 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( ( 2 ^ -u ( ! ` d ) ) e. RR /\ 0 <_ ( 2 ^ -u ( ! ` d ) ) ) /\ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) e. RR ) )
96 95 adantr 
 |-  ( ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) /\ ( 2 ^ -u ( ! ` d ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) ) -> ( ( ( 2 ^ -u ( ! ` d ) ) e. RR /\ 0 <_ ( 2 ^ -u ( ! ` d ) ) ) /\ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) e. RR ) )
97 88 adantl 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> d e. ZZ )
98 74 97 zmulcld 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( -u ( ! ` d ) x. d ) e. ZZ )
99 rpexpcl 
 |-  ( ( 2 e. RR+ /\ ( -u ( ! ` d ) x. d ) e. ZZ ) -> ( 2 ^ ( -u ( ! ` d ) x. d ) ) e. RR+ )
100 10 98 99 sylancr 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 2 ^ ( -u ( ! ` d ) x. d ) ) e. RR+ )
101 100 rpred 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 2 ^ ( -u ( ! ` d ) x. d ) ) e. RR )
102 100 rpge0d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> 0 <_ ( 2 ^ ( -u ( ! ` d ) x. d ) ) )
103 85 a1i 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 1 / 2 ) e. RR )
104 101 102 103 jca31 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( ( 2 ^ ( -u ( ! ` d ) x. d ) ) e. RR /\ 0 <_ ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) /\ ( 1 / 2 ) e. RR ) )
105 104 adantr 
 |-  ( ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) /\ ( 2 ^ -u ( ! ` d ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) ) -> ( ( ( 2 ^ ( -u ( ! ` d ) x. d ) ) e. RR /\ 0 <_ ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) /\ ( 1 / 2 ) e. RR ) )
106 simpr 
 |-  ( ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) /\ ( 2 ^ -u ( ! ` d ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) ) -> ( 2 ^ -u ( ! ` d ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) )
107 2re 
 |-  2 e. RR
108 1le2 
 |-  1 <_ 2
109 72 nncnd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ! ` d ) e. CC )
110 97 zcnd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> d e. CC )
111 109 110 mulneg1d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( -u ( ! ` d ) x. d ) = -u ( ( ! ` d ) x. d ) )
112 72 70 nnmulcld 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( ! ` d ) x. d ) e. NN )
113 112 nnge1d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> 1 <_ ( ( ! ` d ) x. d ) )
114 1re 
 |-  1 e. RR
115 112 nnred 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( ! ` d ) x. d ) e. RR )
116 leneg 
 |-  ( ( 1 e. RR /\ ( ( ! ` d ) x. d ) e. RR ) -> ( 1 <_ ( ( ! ` d ) x. d ) <-> -u ( ( ! ` d ) x. d ) <_ -u 1 ) )
117 114 115 116 sylancr 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 1 <_ ( ( ! ` d ) x. d ) <-> -u ( ( ! ` d ) x. d ) <_ -u 1 ) )
118 113 117 mpbid 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> -u ( ( ! ` d ) x. d ) <_ -u 1 )
119 111 118 eqbrtrd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( -u ( ! ` d ) x. d ) <_ -u 1 )
120 neg1z 
 |-  -u 1 e. ZZ
121 eluz 
 |-  ( ( ( -u ( ! ` d ) x. d ) e. ZZ /\ -u 1 e. ZZ ) -> ( -u 1 e. ( ZZ>= ` ( -u ( ! ` d ) x. d ) ) <-> ( -u ( ! ` d ) x. d ) <_ -u 1 ) )
122 98 120 121 sylancl 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( -u 1 e. ( ZZ>= ` ( -u ( ! ` d ) x. d ) ) <-> ( -u ( ! ` d ) x. d ) <_ -u 1 ) )
123 119 122 mpbird 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> -u 1 e. ( ZZ>= ` ( -u ( ! ` d ) x. d ) ) )
124 leexp2a 
 |-  ( ( 2 e. RR /\ 1 <_ 2 /\ -u 1 e. ( ZZ>= ` ( -u ( ! ` d ) x. d ) ) ) -> ( 2 ^ ( -u ( ! ` d ) x. d ) ) <_ ( 2 ^ -u 1 ) )
125 107 108 123 124 mp3an12i 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 2 ^ ( -u ( ! ` d ) x. d ) ) <_ ( 2 ^ -u 1 ) )
126 2cn 
 |-  2 e. CC
127 expn1 
 |-  ( 2 e. CC -> ( 2 ^ -u 1 ) = ( 1 / 2 ) )
128 126 127 ax-mp 
 |-  ( 2 ^ -u 1 ) = ( 1 / 2 )
129 125 128 breqtrdi 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 2 ^ ( -u ( ! ` d ) x. d ) ) <_ ( 1 / 2 ) )
130 129 adantr 
 |-  ( ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) /\ ( 2 ^ -u ( ! ` d ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) ) -> ( 2 ^ ( -u ( ! ` d ) x. d ) ) <_ ( 1 / 2 ) )
131 lemul12a 
 |-  ( ( ( ( ( 2 ^ -u ( ! ` d ) ) e. RR /\ 0 <_ ( 2 ^ -u ( ! ` d ) ) ) /\ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) e. RR ) /\ ( ( ( 2 ^ ( -u ( ! ` d ) x. d ) ) e. RR /\ 0 <_ ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) /\ ( 1 / 2 ) e. RR ) ) -> ( ( ( 2 ^ -u ( ! ` d ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) /\ ( 2 ^ ( -u ( ! ` d ) x. d ) ) <_ ( 1 / 2 ) ) -> ( ( 2 ^ -u ( ! ` d ) ) x. ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) <_ ( ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) x. ( 1 / 2 ) ) ) )
132 131 3impia 
 |-  ( ( ( ( ( 2 ^ -u ( ! ` d ) ) e. RR /\ 0 <_ ( 2 ^ -u ( ! ` d ) ) ) /\ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) e. RR ) /\ ( ( ( 2 ^ ( -u ( ! ` d ) x. d ) ) e. RR /\ 0 <_ ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) /\ ( 1 / 2 ) e. RR ) /\ ( ( 2 ^ -u ( ! ` d ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) /\ ( 2 ^ ( -u ( ! ` d ) x. d ) ) <_ ( 1 / 2 ) ) ) -> ( ( 2 ^ -u ( ! ` d ) ) x. ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) <_ ( ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) x. ( 1 / 2 ) ) )
133 96 105 106 130 132 syl112anc 
 |-  ( ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) /\ ( 2 ^ -u ( ! ` d ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) ) -> ( ( 2 ^ -u ( ! ` d ) ) x. ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) <_ ( ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) x. ( 1 / 2 ) ) )
134 133 ex 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( 2 ^ -u ( ! ` d ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) -> ( ( 2 ^ -u ( ! ` d ) ) x. ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) <_ ( ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) x. ( 1 / 2 ) ) ) )
135 facp1 
 |-  ( d e. NN0 -> ( ! ` ( d + 1 ) ) = ( ( ! ` d ) x. ( d + 1 ) ) )
136 71 135 syl 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ! ` ( d + 1 ) ) = ( ( ! ` d ) x. ( d + 1 ) ) )
137 136 negeqd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> -u ( ! ` ( d + 1 ) ) = -u ( ( ! ` d ) x. ( d + 1 ) ) )
138 ax-1cn 
 |-  1 e. CC
139 addcom 
 |-  ( ( d e. CC /\ 1 e. CC ) -> ( d + 1 ) = ( 1 + d ) )
140 110 138 139 sylancl 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( d + 1 ) = ( 1 + d ) )
141 140 oveq2d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( -u ( ! ` d ) x. ( d + 1 ) ) = ( -u ( ! ` d ) x. ( 1 + d ) ) )
142 peano2cn 
 |-  ( d e. CC -> ( d + 1 ) e. CC )
143 110 142 syl 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( d + 1 ) e. CC )
144 109 143 mulneg1d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( -u ( ! ` d ) x. ( d + 1 ) ) = -u ( ( ! ` d ) x. ( d + 1 ) ) )
145 74 zcnd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> -u ( ! ` d ) e. CC )
146 1cnd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> 1 e. CC )
147 145 146 110 adddid 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( -u ( ! ` d ) x. ( 1 + d ) ) = ( ( -u ( ! ` d ) x. 1 ) + ( -u ( ! ` d ) x. d ) ) )
148 145 mulridd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( -u ( ! ` d ) x. 1 ) = -u ( ! ` d ) )
149 148 oveq1d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( -u ( ! ` d ) x. 1 ) + ( -u ( ! ` d ) x. d ) ) = ( -u ( ! ` d ) + ( -u ( ! ` d ) x. d ) ) )
150 147 149 eqtrd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( -u ( ! ` d ) x. ( 1 + d ) ) = ( -u ( ! ` d ) + ( -u ( ! ` d ) x. d ) ) )
151 141 144 150 3eqtr3d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> -u ( ( ! ` d ) x. ( d + 1 ) ) = ( -u ( ! ` d ) + ( -u ( ! ` d ) x. d ) ) )
152 137 151 eqtrd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> -u ( ! ` ( d + 1 ) ) = ( -u ( ! ` d ) + ( -u ( ! ` d ) x. d ) ) )
153 152 oveq2d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 2 ^ -u ( ! ` ( d + 1 ) ) ) = ( 2 ^ ( -u ( ! ` d ) + ( -u ( ! ` d ) x. d ) ) ) )
154 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
155 expaddz 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( -u ( ! ` d ) e. ZZ /\ ( -u ( ! ` d ) x. d ) e. ZZ ) ) -> ( 2 ^ ( -u ( ! ` d ) + ( -u ( ! ` d ) x. d ) ) ) = ( ( 2 ^ -u ( ! ` d ) ) x. ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) )
156 154 155 mpan 
 |-  ( ( -u ( ! ` d ) e. ZZ /\ ( -u ( ! ` d ) x. d ) e. ZZ ) -> ( 2 ^ ( -u ( ! ` d ) + ( -u ( ! ` d ) x. d ) ) ) = ( ( 2 ^ -u ( ! ` d ) ) x. ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) )
157 74 98 156 syl2anc 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 2 ^ ( -u ( ! ` d ) + ( -u ( ! ` d ) x. d ) ) ) = ( ( 2 ^ -u ( ! ` d ) ) x. ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) )
158 153 157 eqtrd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 2 ^ -u ( ! ` ( d + 1 ) ) ) = ( ( 2 ^ -u ( ! ` d ) ) x. ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) )
159 44 adantr 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> A e. CC )
160 110 146 159 addsubd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( d + 1 ) - A ) = ( ( d - A ) + 1 ) )
161 160 oveq2d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) = ( ( 1 / 2 ) ^ ( ( d - A ) + 1 ) ) )
162 uznn0sub 
 |-  ( d e. ( ZZ>= ` A ) -> ( d - A ) e. NN0 )
163 162 adantl 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( d - A ) e. NN0 )
164 expp1 
 |-  ( ( ( 1 / 2 ) e. CC /\ ( d - A ) e. NN0 ) -> ( ( 1 / 2 ) ^ ( ( d - A ) + 1 ) ) = ( ( ( 1 / 2 ) ^ ( d - A ) ) x. ( 1 / 2 ) ) )
165 47 163 164 sylancr 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( 1 / 2 ) ^ ( ( d - A ) + 1 ) ) = ( ( ( 1 / 2 ) ^ ( d - A ) ) x. ( 1 / 2 ) ) )
166 161 165 eqtrd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) = ( ( ( 1 / 2 ) ^ ( d - A ) ) x. ( 1 / 2 ) ) )
167 166 oveq2d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( ( 1 / 2 ) ^ ( d - A ) ) x. ( 1 / 2 ) ) ) )
168 84 rpcnd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 2 ^ -u ( ! ` A ) ) e. CC )
169 92 rpcnd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( 1 / 2 ) ^ ( d - A ) ) e. CC )
170 47 a1i 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( 1 / 2 ) e. CC )
171 168 169 170 mulassd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) x. ( 1 / 2 ) ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( ( 1 / 2 ) ^ ( d - A ) ) x. ( 1 / 2 ) ) ) )
172 167 171 eqtr4d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) ) = ( ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) x. ( 1 / 2 ) ) )
173 158 172 breq12d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( 2 ^ -u ( ! ` ( d + 1 ) ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) ) <-> ( ( 2 ^ -u ( ! ` d ) ) x. ( 2 ^ ( -u ( ! ` d ) x. d ) ) ) <_ ( ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) x. ( 1 / 2 ) ) ) )
174 134 173 sylibrd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( 2 ^ -u ( ! ` d ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) -> ( 2 ^ -u ( ! ` ( d + 1 ) ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) ) ) )
175 fveq2 
 |-  ( a = d -> ( ! ` a ) = ( ! ` d ) )
176 175 negeqd 
 |-  ( a = d -> -u ( ! ` a ) = -u ( ! ` d ) )
177 176 oveq2d 
 |-  ( a = d -> ( 2 ^ -u ( ! ` a ) ) = ( 2 ^ -u ( ! ` d ) ) )
178 ovex 
 |-  ( 2 ^ -u ( ! ` d ) ) e. _V
179 177 2 178 fvmpt 
 |-  ( d e. NN -> ( F ` d ) = ( 2 ^ -u ( ! ` d ) ) )
180 70 179 syl 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( F ` d ) = ( 2 ^ -u ( ! ` d ) ) )
181 oveq1 
 |-  ( c = d -> ( c - A ) = ( d - A ) )
182 181 oveq2d 
 |-  ( c = d -> ( ( 1 / 2 ) ^ ( c - A ) ) = ( ( 1 / 2 ) ^ ( d - A ) ) )
183 182 oveq2d 
 |-  ( c = d -> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( c - A ) ) ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) )
184 ovex 
 |-  ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) e. _V
185 183 1 184 fvmpt 
 |-  ( d e. ( ZZ>= ` A ) -> ( G ` d ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) )
186 185 adantl 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( G ` d ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) )
187 180 186 breq12d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( F ` d ) <_ ( G ` d ) <-> ( 2 ^ -u ( ! ` d ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( d - A ) ) ) ) )
188 70 peano2nnd 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( d + 1 ) e. NN )
189 fveq2 
 |-  ( a = ( d + 1 ) -> ( ! ` a ) = ( ! ` ( d + 1 ) ) )
190 189 negeqd 
 |-  ( a = ( d + 1 ) -> -u ( ! ` a ) = -u ( ! ` ( d + 1 ) ) )
191 190 oveq2d 
 |-  ( a = ( d + 1 ) -> ( 2 ^ -u ( ! ` a ) ) = ( 2 ^ -u ( ! ` ( d + 1 ) ) ) )
192 ovex 
 |-  ( 2 ^ -u ( ! ` ( d + 1 ) ) ) e. _V
193 191 2 192 fvmpt 
 |-  ( ( d + 1 ) e. NN -> ( F ` ( d + 1 ) ) = ( 2 ^ -u ( ! ` ( d + 1 ) ) ) )
194 188 193 syl 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( F ` ( d + 1 ) ) = ( 2 ^ -u ( ! ` ( d + 1 ) ) ) )
195 peano2uz 
 |-  ( d e. ( ZZ>= ` A ) -> ( d + 1 ) e. ( ZZ>= ` A ) )
196 oveq1 
 |-  ( c = ( d + 1 ) -> ( c - A ) = ( ( d + 1 ) - A ) )
197 196 oveq2d 
 |-  ( c = ( d + 1 ) -> ( ( 1 / 2 ) ^ ( c - A ) ) = ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) )
198 197 oveq2d 
 |-  ( c = ( d + 1 ) -> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( c - A ) ) ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) ) )
199 ovex 
 |-  ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) ) e. _V
200 198 1 199 fvmpt 
 |-  ( ( d + 1 ) e. ( ZZ>= ` A ) -> ( G ` ( d + 1 ) ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) ) )
201 195 200 syl 
 |-  ( d e. ( ZZ>= ` A ) -> ( G ` ( d + 1 ) ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) ) )
202 201 adantl 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( G ` ( d + 1 ) ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) ) )
203 194 202 breq12d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( F ` ( d + 1 ) ) <_ ( G ` ( d + 1 ) ) <-> ( 2 ^ -u ( ! ` ( d + 1 ) ) ) <_ ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( ( d + 1 ) - A ) ) ) ) )
204 174 187 203 3imtr4d 
 |-  ( ( A e. NN /\ d e. ( ZZ>= ` A ) ) -> ( ( F ` d ) <_ ( G ` d ) -> ( F ` ( d + 1 ) ) <_ ( G ` ( d + 1 ) ) ) )
205 204 expcom 
 |-  ( d e. ( ZZ>= ` A ) -> ( A e. NN -> ( ( F ` d ) <_ ( G ` d ) -> ( F ` ( d + 1 ) ) <_ ( G ` ( d + 1 ) ) ) ) )
206 205 a2d 
 |-  ( d e. ( ZZ>= ` A ) -> ( ( A e. NN -> ( F ` d ) <_ ( G ` d ) ) -> ( A e. NN -> ( F ` ( d + 1 ) ) <_ ( G ` ( d + 1 ) ) ) ) )
207 23 27 31 35 69 206 uzind4i 
 |-  ( B e. ( ZZ>= ` A ) -> ( A e. NN -> ( F ` B ) <_ ( G ` B ) ) )
208 207 impcom 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( F ` B ) <_ ( G ` B ) )
209 0xr 
 |-  0 e. RR*
210 1 aaliou3lem1 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( G ` B ) e. RR )
211 elioc2 
 |-  ( ( 0 e. RR* /\ ( G ` B ) e. RR ) -> ( ( F ` B ) e. ( 0 (,] ( G ` B ) ) <-> ( ( F ` B ) e. RR /\ 0 < ( F ` B ) /\ ( F ` B ) <_ ( G ` B ) ) ) )
212 209 210 211 sylancr 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( ( F ` B ) e. ( 0 (,] ( G ` B ) ) <-> ( ( F ` B ) e. RR /\ 0 < ( F ` B ) /\ ( F ` B ) <_ ( G ` B ) ) ) )
213 18 19 208 212 mpbir3and 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( F ` B ) e. ( 0 (,] ( G ` B ) ) )