Metamath Proof Explorer

Theorem aaliou3lem1

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

Ref Expression
Hypothesis aaliou3lem.a 
|- G = ( c e. ( ZZ>= ` A ) |-> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( c - A ) ) ) )
Assertion aaliou3lem1 
|- ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( G ` B ) e. RR )

Proof

Step Hyp Ref Expression
1 aaliou3lem.a 
 |-  G = ( c e. ( ZZ>= ` A ) |-> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( c - A ) ) ) )
2 oveq1 
 |-  ( c = B -> ( c - A ) = ( B - A ) )
3 2 oveq2d 
 |-  ( c = B -> ( ( 1 / 2 ) ^ ( c - A ) ) = ( ( 1 / 2 ) ^ ( B - A ) ) )
4 3 oveq2d 
 |-  ( c = B -> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( c - A ) ) ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( B - A ) ) ) )
5 ovex 
 |-  ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( B - A ) ) ) e. _V
6 4 1 5 fvmpt 
 |-  ( B e. ( ZZ>= ` A ) -> ( G ` B ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( B - A ) ) ) )
7 6 adantl 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( G ` B ) = ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( B - A ) ) ) )
8 2rp 
 |-  2 e. RR+
9 simpl 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> A e. NN )
10 9 nnnn0d 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> A e. NN0 )
11 10 faccld 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( ! ` A ) e. NN )
12 11 nnzd 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( ! ` A ) e. ZZ )
13 12 znegcld 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> -u ( ! ` A ) e. ZZ )
14 rpexpcl 
 |-  ( ( 2 e. RR+ /\ -u ( ! ` A ) e. ZZ ) -> ( 2 ^ -u ( ! ` A ) ) e. RR+ )
15 8 13 14 sylancr 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( 2 ^ -u ( ! ` A ) ) e. RR+ )
16 halfre 
 |-  ( 1 / 2 ) e. RR
17 halfgt0 
 |-  0 < ( 1 / 2 )
18 16 17 elrpii 
 |-  ( 1 / 2 ) e. RR+
19 eluzelz 
 |-  ( B e. ( ZZ>= ` A ) -> B e. ZZ )
20 nnz 
 |-  ( A e. NN -> A e. ZZ )
21 zsubcl 
 |-  ( ( B e. ZZ /\ A e. ZZ ) -> ( B - A ) e. ZZ )
22 19 20 21 syl2anr 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( B - A ) e. ZZ )
23 rpexpcl 
 |-  ( ( ( 1 / 2 ) e. RR+ /\ ( B - A ) e. ZZ ) -> ( ( 1 / 2 ) ^ ( B - A ) ) e. RR+ )
24 18 22 23 sylancr 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( ( 1 / 2 ) ^ ( B - A ) ) e. RR+ )
25 15 24 rpmulcld 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( B - A ) ) ) e. RR+ )
26 25 rpred 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( B - A ) ) ) e. RR )
27 7 26 eqeltrd 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> ( G ` B ) e. RR )