Theorem aaliou3lem5

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

	Ref	Expression
Hypotheses	aaliou3lem.c	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
	aaliou3lem.d	⊢ 𝐿 = Σ 𝑏 ∈ ℕ ( 𝐹 ‘ 𝑏 )
	aaliou3lem.e	⊢ 𝐻 = ( 𝑐 ∈ ℕ ↦ Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) )
Assertion	aaliou3lem5	⊢ ( 𝐴 ∈ ℕ → ( 𝐻 ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		aaliou3lem.c	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
2		aaliou3lem.d	⊢ 𝐿 = Σ 𝑏 ∈ ℕ ( 𝐹 ‘ 𝑏 )
3		aaliou3lem.e	⊢ 𝐻 = ( 𝑐 ∈ ℕ ↦ Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) )
4		oveq2	⊢ ( 𝑐 = 𝐴 → ( 1 ... 𝑐 ) = ( 1 ... 𝐴 ) )
5	4	sumeq1d	⊢ ( 𝑐 = 𝐴 → Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) = Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) )
6		sumex	⊢ Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) ∈ V
7	5 3 6	fvmpt	⊢ ( 𝐴 ∈ ℕ → ( 𝐻 ‘ 𝐴 ) = Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) )
8		fzfid	⊢ ( 𝐴 ∈ ℕ → ( 1 ... 𝐴 ) ∈ Fin )
9		elfznn	⊢ ( 𝑏 ∈ ( 1 ... 𝐴 ) → 𝑏 ∈ ℕ )
10	9	adantl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → 𝑏 ∈ ℕ )
11		fveq2	⊢ ( 𝑎 = 𝑏 → ( ! ‘ 𝑎 ) = ( ! ‘ 𝑏 ) )
12	11	negeqd	⊢ ( 𝑎 = 𝑏 → - ( ! ‘ 𝑎 ) = - ( ! ‘ 𝑏 ) )
13	12	oveq2d	⊢ ( 𝑎 = 𝑏 → ( 2 ↑ - ( ! ‘ 𝑎 ) ) = ( 2 ↑ - ( ! ‘ 𝑏 ) ) )
14		ovex	⊢ ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ V
15	13 1 14	fvmpt	⊢ ( 𝑏 ∈ ℕ → ( 𝐹 ‘ 𝑏 ) = ( 2 ↑ - ( ! ‘ 𝑏 ) ) )
16		2rp	⊢ 2 ∈ ℝ+
17		nnnn0	⊢ ( 𝑏 ∈ ℕ → 𝑏 ∈ ℕ0 )
18	17	faccld	⊢ ( 𝑏 ∈ ℕ → ( ! ‘ 𝑏 ) ∈ ℕ )
19	18	nnzd	⊢ ( 𝑏 ∈ ℕ → ( ! ‘ 𝑏 ) ∈ ℤ )
20	19	znegcld	⊢ ( 𝑏 ∈ ℕ → - ( ! ‘ 𝑏 ) ∈ ℤ )
21		rpexpcl	⊢ ( ( 2 ∈ ℝ+ ∧ - ( ! ‘ 𝑏 ) ∈ ℤ ) → ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ ℝ+ )
22	16 20 21	sylancr	⊢ ( 𝑏 ∈ ℕ → ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ ℝ+ )
23	22	rpred	⊢ ( 𝑏 ∈ ℕ → ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ ℝ )
24	15 23	eqeltrd	⊢ ( 𝑏 ∈ ℕ → ( 𝐹 ‘ 𝑏 ) ∈ ℝ )
25	10 24	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℝ )
26	8 25	fsumrecl	⊢ ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) ∈ ℝ )
27	7 26	eqeltrd	⊢ ( 𝐴 ∈ ℕ → ( 𝐻 ‘ 𝐴 ) ∈ ℝ )