Metamath Proof Explorer

Theorem iprodfac

Description: An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017)

Ref Expression
Assertion iprodfac ⊢ A ∈ ℕ 0 → A ! = ∏ k ∈ ℕ 1 + 1 k A 1 + A k

Proof

Step Hyp Ref Expression
1 nnuz ⊢ ℕ = ℤ ≥ 1
2 1zzd ⊢ A ∈ ℕ 0 → 1 ∈ ℤ
3 facne0 ⊢ A ∈ ℕ 0 → A ! ≠ 0
4 eqid ⊢ x ∈ ℕ ⟼ 1 + 1 x A 1 + A x = x ∈ ℕ ⟼ 1 + 1 x A 1 + A x
5 4 faclim ⊢ A ∈ ℕ 0 → seq 1 × x ∈ ℕ ⟼ 1 + 1 x A 1 + A x ⇝ A !
6 oveq2 ⊢ x = k → 1 x = 1 k
7 6 oveq2d ⊢ x = k → 1 + 1 x = 1 + 1 k
8 7 oveq1d ⊢ x = k → 1 + 1 x A = 1 + 1 k A
9 oveq2 ⊢ x = k → A x = A k
10 9 oveq2d ⊢ x = k → 1 + A x = 1 + A k
11 8 10 oveq12d ⊢ x = k → 1 + 1 x A 1 + A x = 1 + 1 k A 1 + A k
12 ovex ⊢ 1 + 1 k A 1 + A k ∈ V
13 11 4 12 fvmpt ⊢ k ∈ ℕ → x ∈ ℕ ⟼ 1 + 1 x A 1 + A x ⁡ k = 1 + 1 k A 1 + A k
14 13 adantl ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → x ∈ ℕ ⟼ 1 + 1 x A 1 + A x ⁡ k = 1 + 1 k A 1 + A k
15 1rp ⊢ 1 ∈ ℝ +
16 15 a1i ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → 1 ∈ ℝ +
17 simpr ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → k ∈ ℕ
18 17 nnrpd ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → k ∈ ℝ +
19 18 rpreccld ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → 1 k ∈ ℝ +
20 16 19 rpaddcld ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → 1 + 1 k ∈ ℝ +
21 nn0z ⊢ A ∈ ℕ 0 → A ∈ ℤ
22 21 adantr ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → A ∈ ℤ
23 20 22 rpexpcld ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → 1 + 1 k A ∈ ℝ +
24 1cnd ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → 1 ∈ ℂ
25 nn0nndivcl ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → A k ∈ ℝ
26 25 recnd ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → A k ∈ ℂ
27 24 26 addcomd ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → 1 + A k = A k + 1
28 nn0ge0div ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → 0 ≤ A k
29 25 28 ge0p1rpd ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → A k + 1 ∈ ℝ +
30 27 29 eqeltrd ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → 1 + A k ∈ ℝ +
31 23 30 rpdivcld ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → 1 + 1 k A 1 + A k ∈ ℝ +
32 31 rpcnd ⊢ A ∈ ℕ 0 ∧ k ∈ ℕ → 1 + 1 k A 1 + A k ∈ ℂ
33 1 2 3 5 14 32 iprodn0 ⊢ A ∈ ℕ 0 → ∏ k ∈ ℕ 1 + 1 k A 1 + A k = A !
34 33 eqcomd ⊢ A ∈ ℕ 0 → A ! = ∏ k ∈ ℕ 1 + 1 k A 1 + A k