Metamath Proof Explorer

Theorem aaliou3lem6

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

Ref Expression
Hypotheses aaliou3lem.c 
|- F = ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) )
aaliou3lem.d 
|- L = sum_ b e. NN ( F ` b )
aaliou3lem.e 
|- H = ( c e. NN |-> sum_ b e. ( 1 ... c ) ( F ` b ) )
Assertion aaliou3lem6 
|- ( A e. NN -> ( ( H ` A ) x. ( 2 ^ ( ! ` A ) ) ) e. ZZ )

Proof

Step Hyp Ref Expression
1 aaliou3lem.c 
 |-  F = ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) )
2 aaliou3lem.d 
 |-  L = sum_ b e. NN ( F ` b )
3 aaliou3lem.e 
 |-  H = ( c e. NN |-> sum_ b e. ( 1 ... c ) ( F ` b ) )
4 oveq2 
 |-  ( c = A -> ( 1 ... c ) = ( 1 ... A ) )
5 4 sumeq1d 
 |-  ( c = A -> sum_ b e. ( 1 ... c ) ( F ` b ) = sum_ b e. ( 1 ... A ) ( F ` b ) )
6 sumex 
 |-  sum_ b e. ( 1 ... A ) ( F ` b ) e. _V
7 5 3 6 fvmpt 
 |-  ( A e. NN -> ( H ` A ) = sum_ b e. ( 1 ... A ) ( F ` b ) )
8 7 oveq1d 
 |-  ( A e. NN -> ( ( H ` A ) x. ( 2 ^ ( ! ` A ) ) ) = ( sum_ b e. ( 1 ... A ) ( F ` b ) x. ( 2 ^ ( ! ` A ) ) ) )
9 fzfid 
 |-  ( A e. NN -> ( 1 ... A ) e. Fin )
10 2rp 
 |-  2 e. RR+
11 nnnn0 
 |-  ( A e. NN -> A e. NN0 )
12 11 faccld 
 |-  ( A e. NN -> ( ! ` A ) e. NN )
13 12 nnzd 
 |-  ( A e. NN -> ( ! ` A ) e. ZZ )
14 rpexpcl 
 |-  ( ( 2 e. RR+ /\ ( ! ` A ) e. ZZ ) -> ( 2 ^ ( ! ` A ) ) e. RR+ )
15 10 13 14 sylancr 
 |-  ( A e. NN -> ( 2 ^ ( ! ` A ) ) e. RR+ )
16 15 rpcnd 
 |-  ( A e. NN -> ( 2 ^ ( ! ` A ) ) e. CC )
17 elfznn 
 |-  ( b e. ( 1 ... A ) -> b e. NN )
18 fveq2 
 |-  ( a = b -> ( ! ` a ) = ( ! ` b ) )
19 18 negeqd 
 |-  ( a = b -> -u ( ! ` a ) = -u ( ! ` b ) )
20 19 oveq2d 
 |-  ( a = b -> ( 2 ^ -u ( ! ` a ) ) = ( 2 ^ -u ( ! ` b ) ) )
21 ovex 
 |-  ( 2 ^ -u ( ! ` b ) ) e. _V
22 20 1 21 fvmpt 
 |-  ( b e. NN -> ( F ` b ) = ( 2 ^ -u ( ! ` b ) ) )
23 17 22 syl 
 |-  ( b e. ( 1 ... A ) -> ( F ` b ) = ( 2 ^ -u ( ! ` b ) ) )
24 23 adantl 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( F ` b ) = ( 2 ^ -u ( ! ` b ) ) )
25 17 adantl 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> b e. NN )
26 25 nnnn0d 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> b e. NN0 )
27 26 faccld 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ! ` b ) e. NN )
28 27 nnzd 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ! ` b ) e. ZZ )
29 28 znegcld 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> -u ( ! ` b ) e. ZZ )
30 rpexpcl 
 |-  ( ( 2 e. RR+ /\ -u ( ! ` b ) e. ZZ ) -> ( 2 ^ -u ( ! ` b ) ) e. RR+ )
31 10 29 30 sylancr 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( 2 ^ -u ( ! ` b ) ) e. RR+ )
32 31 rpcnd 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( 2 ^ -u ( ! ` b ) ) e. CC )
33 24 32 eqeltrd 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( F ` b ) e. CC )
34 9 16 33 fsummulc1 
 |-  ( A e. NN -> ( sum_ b e. ( 1 ... A ) ( F ` b ) x. ( 2 ^ ( ! ` A ) ) ) = sum_ b e. ( 1 ... A ) ( ( F ` b ) x. ( 2 ^ ( ! ` A ) ) ) )
35 24 oveq1d 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ( F ` b ) x. ( 2 ^ ( ! ` A ) ) ) = ( ( 2 ^ -u ( ! ` b ) ) x. ( 2 ^ ( ! ` A ) ) ) )
36 13 adantr 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ! ` A ) e. ZZ )
37 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
38 expaddz 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( -u ( ! ` b ) e. ZZ /\ ( ! ` A ) e. ZZ ) ) -> ( 2 ^ ( -u ( ! ` b ) + ( ! ` A ) ) ) = ( ( 2 ^ -u ( ! ` b ) ) x. ( 2 ^ ( ! ` A ) ) ) )
39 37 38 mpan 
 |-  ( ( -u ( ! ` b ) e. ZZ /\ ( ! ` A ) e. ZZ ) -> ( 2 ^ ( -u ( ! ` b ) + ( ! ` A ) ) ) = ( ( 2 ^ -u ( ! ` b ) ) x. ( 2 ^ ( ! ` A ) ) ) )
40 29 36 39 syl2anc 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( 2 ^ ( -u ( ! ` b ) + ( ! ` A ) ) ) = ( ( 2 ^ -u ( ! ` b ) ) x. ( 2 ^ ( ! ` A ) ) ) )
41 2z 
 |-  2 e. ZZ
42 29 zcnd 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> -u ( ! ` b ) e. CC )
43 36 zcnd 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ! ` A ) e. CC )
44 42 43 addcomd 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( -u ( ! ` b ) + ( ! ` A ) ) = ( ( ! ` A ) + -u ( ! ` b ) ) )
45 27 nncnd 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ! ` b ) e. CC )
46 43 45 negsubd 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ( ! ` A ) + -u ( ! ` b ) ) = ( ( ! ` A ) - ( ! ` b ) ) )
47 44 46 eqtrd 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( -u ( ! ` b ) + ( ! ` A ) ) = ( ( ! ` A ) - ( ! ` b ) ) )
48 11 adantr 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> A e. NN0 )
49 elfzle2 
 |-  ( b e. ( 1 ... A ) -> b <_ A )
50 49 adantl 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> b <_ A )
51 facwordi 
 |-  ( ( b e. NN0 /\ A e. NN0 /\ b <_ A ) -> ( ! ` b ) <_ ( ! ` A ) )
52 26 48 50 51 syl3anc 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ! ` b ) <_ ( ! ` A ) )
53 27 nnnn0d 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ! ` b ) e. NN0 )
54 48 faccld 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ! ` A ) e. NN )
55 54 nnnn0d 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ! ` A ) e. NN0 )
56 nn0sub 
 |-  ( ( ( ! ` b ) e. NN0 /\ ( ! ` A ) e. NN0 ) -> ( ( ! ` b ) <_ ( ! ` A ) <-> ( ( ! ` A ) - ( ! ` b ) ) e. NN0 ) )
57 53 55 56 syl2anc 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ( ! ` b ) <_ ( ! ` A ) <-> ( ( ! ` A ) - ( ! ` b ) ) e. NN0 ) )
58 52 57 mpbid 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ( ! ` A ) - ( ! ` b ) ) e. NN0 )
59 47 58 eqeltrd 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( -u ( ! ` b ) + ( ! ` A ) ) e. NN0 )
60 zexpcl 
 |-  ( ( 2 e. ZZ /\ ( -u ( ! ` b ) + ( ! ` A ) ) e. NN0 ) -> ( 2 ^ ( -u ( ! ` b ) + ( ! ` A ) ) ) e. ZZ )
61 41 59 60 sylancr 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( 2 ^ ( -u ( ! ` b ) + ( ! ` A ) ) ) e. ZZ )
62 40 61 eqeltrrd 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ( 2 ^ -u ( ! ` b ) ) x. ( 2 ^ ( ! ` A ) ) ) e. ZZ )
63 35 62 eqeltrd 
 |-  ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( ( F ` b ) x. ( 2 ^ ( ! ` A ) ) ) e. ZZ )
64 9 63 fsumzcl 
 |-  ( A e. NN -> sum_ b e. ( 1 ... A ) ( ( F ` b ) x. ( 2 ^ ( ! ` A ) ) ) e. ZZ )
65 34 64 eqeltrd 
 |-  ( A e. NN -> ( sum_ b e. ( 1 ... A ) ( F ` b ) x. ( 2 ^ ( ! ` A ) ) ) e. ZZ )
66 8 65 eqeltrd 
 |-  ( A e. NN -> ( ( H ` A ) x. ( 2 ^ ( ! ` A ) ) ) e. ZZ )