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 mulid1d
 |-  ( 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 mulid1d
 |-  ( ( 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 ) ) )