Metamath Proof Explorer

Theorem aaliou3lem1

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

Ref Expression
Hypothesis aaliou3lem.a ⊢ G = c ∈ ℤ ≥ A ⟼ 2 − A ! ⁢ 1 2 c − A
Assertion aaliou3lem1 ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → G ⁡ B ∈ ℝ

Proof

Step Hyp Ref Expression
1 aaliou3lem.a ⊢ G = c ∈ ℤ ≥ A ⟼ 2 − A ! ⁢ 1 2 c − A
2 oveq1 ⊢ c = B → c − A = B − A
3 2 oveq2d ⊢ c = B → 1 2 c − A = 1 2 B − A
4 3 oveq2d ⊢ c = B → 2 − A ! ⁢ 1 2 c − A = 2 − A ! ⁢ 1 2 B − A
5 ovex ⊢ 2 − A ! ⁢ 1 2 B − A ∈ V
6 4 1 5 fvmpt ⊢ B ∈ ℤ ≥ A → G ⁡ B = 2 − A ! ⁢ 1 2 B − A
7 6 adantl ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → G ⁡ B = 2 − A ! ⁢ 1 2 B − A
8 2rp ⊢ 2 ∈ ℝ +
9 simpl ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → A ∈ ℕ
10 9 nnnn0d ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → A ∈ ℕ 0
11 10 faccld ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → A ! ∈ ℕ
12 11 nnzd ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → A ! ∈ ℤ
13 12 znegcld ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → − A ! ∈ ℤ
14 rpexpcl ⊢ 2 ∈ ℝ + ∧ − A ! ∈ ℤ → 2 − A ! ∈ ℝ +
15 8 13 14 sylancr ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → 2 − A ! ∈ ℝ +
16 halfre ⊢ 1 2 ∈ ℝ
17 halfgt0 ⊢ 0 < 1 2
18 16 17 elrpii ⊢ 1 2 ∈ ℝ +
19 eluzelz ⊢ B ∈ ℤ ≥ A → B ∈ ℤ
20 nnz ⊢ A ∈ ℕ → A ∈ ℤ
21 zsubcl ⊢ B ∈ ℤ ∧ A ∈ ℤ → B − A ∈ ℤ
22 19 20 21 syl2anr ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → B − A ∈ ℤ
23 rpexpcl ⊢ 1 2 ∈ ℝ + ∧ B − A ∈ ℤ → 1 2 B − A ∈ ℝ +
24 18 22 23 sylancr ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → 1 2 B − A ∈ ℝ +
25 15 24 rpmulcld ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → 2 − A ! ⁢ 1 2 B − A ∈ ℝ +
26 25 rpred ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → 2 − A ! ⁢ 1 2 B − A ∈ ℝ
27 7 26 eqeltrd ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → G ⁡ B ∈ ℝ