Metamath Proof Explorer

Theorem aaliou3lem7

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 aaliou3lem7 
|- ( A e. NN -> ( ( H ` A ) =/= L /\ ( abs ` ( L - ( H ` A ) ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) )

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 peano2nn 
 |-  ( A e. NN -> ( A + 1 ) e. NN )
5 eqid 
 |-  ( c e. ( ZZ>= ` ( A + 1 ) ) |-> ( ( 2 ^ -u ( ! ` ( A + 1 ) ) ) x. ( ( 1 / 2 ) ^ ( c - ( A + 1 ) ) ) ) ) = ( c e. ( ZZ>= ` ( A + 1 ) ) |-> ( ( 2 ^ -u ( ! ` ( A + 1 ) ) ) x. ( ( 1 / 2 ) ^ ( c - ( A + 1 ) ) ) ) )
6 5 1 aaliou3lem3 
 |-  ( ( A + 1 ) e. NN -> ( seq ( A + 1 ) ( + , F ) e. dom ~~> /\ sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) e. RR+ /\ sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) )
7 3simpc 
 |-  ( ( seq ( A + 1 ) ( + , F ) e. dom ~~> /\ sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) e. RR+ /\ sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) -> ( sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) e. RR+ /\ sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) )
8 4 6 7 3syl 
 |-  ( A e. NN -> ( sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) e. RR+ /\ sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) )
9 nncn 
 |-  ( A e. NN -> A e. CC )
10 ax-1cn 
 |-  1 e. CC
11 pncan 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) - 1 ) = A )
12 9 10 11 sylancl 
 |-  ( A e. NN -> ( ( A + 1 ) - 1 ) = A )
13 12 oveq2d 
 |-  ( A e. NN -> ( 1 ... ( ( A + 1 ) - 1 ) ) = ( 1 ... A ) )
14 13 sumeq1d 
 |-  ( A e. NN -> sum_ b e. ( 1 ... ( ( A + 1 ) - 1 ) ) ( F ` b ) = sum_ b e. ( 1 ... A ) ( F ` b ) )
15 14 oveq1d 
 |-  ( A e. NN -> ( sum_ b e. ( 1 ... ( ( A + 1 ) - 1 ) ) ( F ` b ) + sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) ) = ( sum_ b e. ( 1 ... A ) ( F ` b ) + sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) ) )
16 nnuz 
 |-  NN = ( ZZ>= ` 1 )
17 eqid 
 |-  ( ZZ>= ` ( A + 1 ) ) = ( ZZ>= ` ( A + 1 ) )
18 eqidd 
 |-  ( ( A e. NN /\ b e. NN ) -> ( F ` b ) = ( F ` b ) )
19 fveq2 
 |-  ( a = b -> ( ! ` a ) = ( ! ` b ) )
20 19 negeqd 
 |-  ( a = b -> -u ( ! ` a ) = -u ( ! ` b ) )
21 20 oveq2d 
 |-  ( a = b -> ( 2 ^ -u ( ! ` a ) ) = ( 2 ^ -u ( ! ` b ) ) )
22 ovex 
 |-  ( 2 ^ -u ( ! ` b ) ) e. _V
23 21 1 22 fvmpt 
 |-  ( b e. NN -> ( F ` b ) = ( 2 ^ -u ( ! ` b ) ) )
24 2rp 
 |-  2 e. RR+
25 nnnn0 
 |-  ( b e. NN -> b e. NN0 )
26 faccl 
 |-  ( b e. NN0 -> ( ! ` b ) e. NN )
27 25 26 syl 
 |-  ( b e. NN -> ( ! ` b ) e. NN )
28 27 nnzd 
 |-  ( b e. NN -> ( ! ` b ) e. ZZ )
29 28 znegcld 
 |-  ( b e. NN -> -u ( ! ` b ) e. ZZ )
30 rpexpcl 
 |-  ( ( 2 e. RR+ /\ -u ( ! ` b ) e. ZZ ) -> ( 2 ^ -u ( ! ` b ) ) e. RR+ )
31 24 29 30 sylancr 
 |-  ( b e. NN -> ( 2 ^ -u ( ! ` b ) ) e. RR+ )
32 31 rpcnd 
 |-  ( b e. NN -> ( 2 ^ -u ( ! ` b ) ) e. CC )
33 23 32 eqeltrd 
 |-  ( b e. NN -> ( F ` b ) e. CC )
34 33 adantl 
 |-  ( ( A e. NN /\ b e. NN ) -> ( F ` b ) e. CC )
35 1nn 
 |-  1 e. NN
36 eqid 
 |-  ( c e. ( ZZ>= ` 1 ) |-> ( ( 2 ^ -u ( ! ` 1 ) ) x. ( ( 1 / 2 ) ^ ( c - 1 ) ) ) ) = ( c e. ( ZZ>= ` 1 ) |-> ( ( 2 ^ -u ( ! ` 1 ) ) x. ( ( 1 / 2 ) ^ ( c - 1 ) ) ) )
37 36 1 aaliou3lem3 
 |-  ( 1 e. NN -> ( seq 1 ( + , F ) e. dom ~~> /\ sum_ b e. ( ZZ>= ` 1 ) ( F ` b ) e. RR+ /\ sum_ b e. ( ZZ>= ` 1 ) ( F ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` 1 ) ) ) ) )
38 37 simp1d 
 |-  ( 1 e. NN -> seq 1 ( + , F ) e. dom ~~> )
39 35 38 mp1i 
 |-  ( A e. NN -> seq 1 ( + , F ) e. dom ~~> )
40 16 17 4 18 34 39 isumsplit 
 |-  ( A e. NN -> sum_ b e. NN ( F ` b ) = ( sum_ b e. ( 1 ... ( ( A + 1 ) - 1 ) ) ( F ` b ) + sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) ) )
41 oveq2 
 |-  ( c = A -> ( 1 ... c ) = ( 1 ... A ) )
42 41 sumeq1d 
 |-  ( c = A -> sum_ b e. ( 1 ... c ) ( F ` b ) = sum_ b e. ( 1 ... A ) ( F ` b ) )
43 sumex 
 |-  sum_ b e. ( 1 ... A ) ( F ` b ) e. _V
44 42 3 43 fvmpt 
 |-  ( A e. NN -> ( H ` A ) = sum_ b e. ( 1 ... A ) ( F ` b ) )
45 44 oveq1d 
 |-  ( A e. NN -> ( ( H ` A ) + sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) ) = ( sum_ b e. ( 1 ... A ) ( F ` b ) + sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) ) )
46 15 40 45 3eqtr4rd 
 |-  ( A e. NN -> ( ( H ` A ) + sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) ) = sum_ b e. NN ( F ` b ) )
47 46 2 eqtr4di 
 |-  ( A e. NN -> ( ( H ` A ) + sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) ) = L )
48 1 2 3 aaliou3lem4 
 |-  L e. RR
49 48 recni 
 |-  L e. CC
50 49 a1i 
 |-  ( A e. NN -> L e. CC )
51 1 2 3 aaliou3lem5 
 |-  ( A e. NN -> ( H ` A ) e. RR )
52 51 recnd 
 |-  ( A e. NN -> ( H ` A ) e. CC )
53 6 simp2d 
 |-  ( ( A + 1 ) e. NN -> sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) e. RR+ )
54 4 53 syl 
 |-  ( A e. NN -> sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) e. RR+ )
55 54 rpcnd 
 |-  ( A e. NN -> sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) e. CC )
56 50 52 55 subaddd 
 |-  ( A e. NN -> ( ( L - ( H ` A ) ) = sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) <-> ( ( H ` A ) + sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) ) = L ) )
57 47 56 mpbird 
 |-  ( A e. NN -> ( L - ( H ` A ) ) = sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) )
58 57 eqcomd 
 |-  ( A e. NN -> sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) = ( L - ( H ` A ) ) )
59 eleq1 
 |-  ( sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) = ( L - ( H ` A ) ) -> ( sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) e. RR+ <-> ( L - ( H ` A ) ) e. RR+ ) )
60 breq1 
 |-  ( sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) = ( L - ( H ` A ) ) -> ( sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) <-> ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) )
61 59 60 anbi12d 
 |-  ( sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) = ( L - ( H ` A ) ) -> ( ( sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) e. RR+ /\ sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) <-> ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) )
62 58 61 syl 
 |-  ( A e. NN -> ( ( sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) e. RR+ /\ sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) <-> ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) )
63 51 adantr 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( H ` A ) e. RR )
64 simprl 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( L - ( H ` A ) ) e. RR+ )
65 difrp 
 |-  ( ( ( H ` A ) e. RR /\ L e. RR ) -> ( ( H ` A ) < L <-> ( L - ( H ` A ) ) e. RR+ ) )
66 63 48 65 sylancl 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( ( H ` A ) < L <-> ( L - ( H ` A ) ) e. RR+ ) )
67 64 66 mpbird 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( H ` A ) < L )
68 63 67 ltned 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( H ` A ) =/= L )
69 nnnn0 
 |-  ( ( A + 1 ) e. NN -> ( A + 1 ) e. NN0 )
70 faccl 
 |-  ( ( A + 1 ) e. NN0 -> ( ! ` ( A + 1 ) ) e. NN )
71 4 69 70 3syl 
 |-  ( A e. NN -> ( ! ` ( A + 1 ) ) e. NN )
72 71 nnzd 
 |-  ( A e. NN -> ( ! ` ( A + 1 ) ) e. ZZ )
73 72 znegcld 
 |-  ( A e. NN -> -u ( ! ` ( A + 1 ) ) e. ZZ )
74 rpexpcl 
 |-  ( ( 2 e. RR+ /\ -u ( ! ` ( A + 1 ) ) e. ZZ ) -> ( 2 ^ -u ( ! ` ( A + 1 ) ) ) e. RR+ )
75 24 73 74 sylancr 
 |-  ( A e. NN -> ( 2 ^ -u ( ! ` ( A + 1 ) ) ) e. RR+ )
76 rpmulcl 
 |-  ( ( 2 e. RR+ /\ ( 2 ^ -u ( ! ` ( A + 1 ) ) ) e. RR+ ) -> ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) e. RR+ )
77 24 75 76 sylancr 
 |-  ( A e. NN -> ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) e. RR+ )
78 77 adantr 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) e. RR+ )
79 78 rpred 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) e. RR )
80 63 79 resubcld 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( ( H ` A ) - ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) e. RR )
81 48 a1i 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> L e. RR )
82 63 78 ltsubrpd 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( ( H ` A ) - ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) < ( H ` A ) )
83 80 63 81 82 67 lttrd 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( ( H ` A ) - ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) < L )
84 80 81 83 ltled 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( ( H ` A ) - ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) <_ L )
85 simprr 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) )
86 81 63 79 lesubadd2d 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) <-> L <_ ( ( H ` A ) + ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) )
87 85 86 mpbid 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> L <_ ( ( H ` A ) + ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) )
88 81 63 79 absdifled 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( ( abs ` ( L - ( H ` A ) ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) <-> ( ( ( H ` A ) - ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) <_ L /\ L <_ ( ( H ` A ) + ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) ) )
89 84 87 88 mpbir2and 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( abs ` ( L - ( H ` A ) ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) )
90 68 89 jca 
 |-  ( ( A e. NN /\ ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) -> ( ( H ` A ) =/= L /\ ( abs ` ( L - ( H ` A ) ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) )
91 90 ex 
 |-  ( A e. NN -> ( ( ( L - ( H ` A ) ) e. RR+ /\ ( L - ( H ` A ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) -> ( ( H ` A ) =/= L /\ ( abs ` ( L - ( H ` A ) ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) )
92 62 91 sylbid 
 |-  ( A e. NN -> ( ( sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) e. RR+ /\ sum_ b e. ( ZZ>= ` ( A + 1 ) ) ( F ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) -> ( ( H ` A ) =/= L /\ ( abs ` ( L - ( H ` A ) ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) ) )
93 8 92 mpd 
 |-  ( A e. NN -> ( ( H ` A ) =/= L /\ ( abs ` ( L - ( H ` A ) ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( A + 1 ) ) ) ) ) )