Metamath Proof Explorer

Theorem aaliou3lem5

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

Ref Expression
Hypotheses aaliou3lem.c ⊢ F = a ∈ ℕ ⟼ 2 − a !
aaliou3lem.d ⊢ L = ∑ b ∈ ℕ F ⁡ b
aaliou3lem.e ⊢ H = c ∈ ℕ ⟼ ∑ b = 1 c F ⁡ b
Assertion aaliou3lem5 ⊢ A ∈ ℕ → H ⁡ A ∈ ℝ

Proof

Step Hyp Ref Expression
1 aaliou3lem.c ⊢ F = a ∈ ℕ ⟼ 2 − a !
2 aaliou3lem.d ⊢ L = ∑ b ∈ ℕ F ⁡ b
3 aaliou3lem.e ⊢ H = c ∈ ℕ ⟼ ∑ b = 1 c F ⁡ b
4 oveq2 ⊢ c = A → 1 … c = 1 … A
5 4 sumeq1d ⊢ c = A → ∑ b = 1 c F ⁡ b = ∑ b = 1 A F ⁡ b
6 sumex ⊢ ∑ b = 1 A F ⁡ b ∈ V
7 5 3 6 fvmpt ⊢ A ∈ ℕ → H ⁡ A = ∑ b = 1 A F ⁡ b
8 fzfid ⊢ A ∈ ℕ → 1 … A ∈ Fin
9 elfznn ⊢ b ∈ 1 … A → b ∈ ℕ
10 9 adantl ⊢ A ∈ ℕ ∧ b ∈ 1 … A → b ∈ ℕ
11 fveq2 ⊢ a = b → a ! = b !
12 11 negeqd ⊢ a = b → − a ! = − b !
13 12 oveq2d ⊢ a = b → 2 − a ! = 2 − b !
14 ovex ⊢ 2 − b ! ∈ V
15 13 1 14 fvmpt ⊢ b ∈ ℕ → F ⁡ b = 2 − b !
16 2rp ⊢ 2 ∈ ℝ +
17 nnnn0 ⊢ b ∈ ℕ → b ∈ ℕ 0
18 17 faccld ⊢ b ∈ ℕ → b ! ∈ ℕ
19 18 nnzd ⊢ b ∈ ℕ → b ! ∈ ℤ
20 19 znegcld ⊢ b ∈ ℕ → − b ! ∈ ℤ
21 rpexpcl ⊢ 2 ∈ ℝ + ∧ − b ! ∈ ℤ → 2 − b ! ∈ ℝ +
22 16 20 21 sylancr ⊢ b ∈ ℕ → 2 − b ! ∈ ℝ +
23 22 rpred ⊢ b ∈ ℕ → 2 − b ! ∈ ℝ
24 15 23 eqeltrd ⊢ b ∈ ℕ → F ⁡ b ∈ ℝ
25 10 24 syl ⊢ A ∈ ℕ ∧ b ∈ 1 … A → F ⁡ b ∈ ℝ
26 8 25 fsumrecl ⊢ A ∈ ℕ → ∑ b = 1 A F ⁡ b ∈ ℝ
27 7 26 eqeltrd ⊢ A ∈ ℕ → H ⁡ A ∈ ℝ