This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fprodfac

Description: Factorial using product notation. (Contributed by Scott Fenton, 15-Dec-2017)

Ref Expression
Assertion fprodfac ( 𝐴 ∈ ℕ0 → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
2 facnn ⊢ ( 𝐴 ∈ ℕ → ( ! ‘ 𝐴 ) = ( seq 1 ( · , I ) ‘ 𝐴 ) )
3 vex ⊢ 𝑘 ∈ V
4 fvi ⊢ ( 𝑘 ∈ V → ( I ‘ 𝑘 ) = 𝑘 )
5 3 4 mp1i ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → ( I ‘ 𝑘 ) = 𝑘 )
6 elnnuz ⊢ ( 𝐴 ∈ ℕ ↔ 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
7 6 biimpi ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
8 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝐴 ) → 𝑘 ∈ ℕ )
9 8 nncnd ⊢ ( 𝑘 ∈ ( 1 ... 𝐴 ) → 𝑘 ∈ ℂ )
10 9 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝐴 ) ) → 𝑘 ∈ ℂ )
11 5 7 10 fprodser ⊢ ( 𝐴 ∈ ℕ → ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 = ( seq 1 ( · , I ) ‘ 𝐴 ) )
12 2 11 eqtr4d ⊢ ( 𝐴 ∈ ℕ → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 )
13 prod0 ⊢ ∏ 𝑘 ∈ ∅ 𝑘 = 1
14 13 eqcomi ⊢ 1 = ∏ 𝑘 ∈ ∅ 𝑘
15 fveq2 ⊢ ( 𝐴 = 0 → ( ! ‘ 𝐴 ) = ( ! ‘ 0 ) )
16 fac0 ⊢ ( ! ‘ 0 ) = 1
17 15 16 eqtrdi ⊢ ( 𝐴 = 0 → ( ! ‘ 𝐴 ) = 1 )
18 oveq2 ⊢ ( 𝐴 = 0 → ( 1 ... 𝐴 ) = ( 1 ... 0 ) )
19 fz10 ⊢ ( 1 ... 0 ) = ∅
20 18 19 eqtrdi ⊢ ( 𝐴 = 0 → ( 1 ... 𝐴 ) = ∅ )
21 20 prodeq1d ⊢ ( 𝐴 = 0 → ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 = ∏ 𝑘 ∈ ∅ 𝑘 )
22 14 17 21 3eqtr4a ⊢ ( 𝐴 = 0 → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 )
23 12 22 jaoi ⊢ ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 )
24 1 23 sylbi ⊢ ( 𝐴 ∈ ℕ0 → ( ! ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 1 ... 𝐴 ) 𝑘 )