Theorem aaliou3lem5

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	aaliou3lem5	|- ( A e. NN -> ( H ` A ) e. RR )

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		fzfid	|- ( A e. NN -> ( 1 ... A ) e. Fin )
9		elfznn	|- ( b e. ( 1 ... A ) -> b e. NN )
10	9	adantl	|- ( ( A e. NN /\ b e. ( 1 ... A ) ) -> b e. NN )
11		fveq2	|- ( a = b -> ( ! ` a ) = ( ! ` b ) )
12	11	negeqd	|- ( a = b -> -u ( ! ` a ) = -u ( ! ` b ) )
13	12	oveq2d	|- ( a = b -> ( 2 ^ -u ( ! ` a ) ) = ( 2 ^ -u ( ! ` b ) ) )
14		ovex	|- ( 2 ^ -u ( ! ` b ) ) e. _V
15	13 1 14	fvmpt	|- ( b e. NN -> ( F ` b ) = ( 2 ^ -u ( ! ` b ) ) )
16		2rp	|- 2 e. RR+
17		nnnn0	|- ( b e. NN -> b e. NN0 )
18	17	faccld	|- ( b e. NN -> ( ! ` b ) e. NN )
19	18	nnzd	|- ( b e. NN -> ( ! ` b ) e. ZZ )
20	19	znegcld	|- ( b e. NN -> -u ( ! ` b ) e. ZZ )
21		rpexpcl	|- ( ( 2 e. RR+ /\ -u ( ! ` b ) e. ZZ ) -> ( 2 ^ -u ( ! ` b ) ) e. RR+ )
22	16 20 21	sylancr	|- ( b e. NN -> ( 2 ^ -u ( ! ` b ) ) e. RR+ )
23	22	rpred	|- ( b e. NN -> ( 2 ^ -u ( ! ` b ) ) e. RR )
24	15 23	eqeltrd	|- ( b e. NN -> ( F ` b ) e. RR )
25	10 24	syl	|- ( ( A e. NN /\ b e. ( 1 ... A ) ) -> ( F ` b ) e. RR )
26	8 25	fsumrecl	|- ( A e. NN -> sum_ b e. ( 1 ... A ) ( F ` b ) e. RR )
27	7 26	eqeltrd	|- ( A e. NN -> ( H ` A ) e. RR )