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