Theorem fprod0diag

Description: Two ways to express "the product of A ( j , k ) over the triangular region M <_ j , M <_ k , j + k <_ N . Compare fsum0diag . (Contributed by Scott Fenton, 2-Feb-2018)

	Ref	Expression
Hypothesis	fprod0diag.1	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ) → 𝐴 ∈ ℂ )
Assertion	fprod0diag	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 0 ... 𝑁 ) ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐴 = ∏ 𝑘 ∈ ( 0 ... 𝑁 ) ∏ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fprod0diag.1	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ) → 𝐴 ∈ ℂ )
2		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
3		fzfid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 0 ... ( 𝑁 − 𝑗 ) ) ∈ Fin )
4		fsum0diaglem	⊢ ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) ) )
5		fsum0diaglem	⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) ) → ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) )
6	4 5	impbii	⊢ ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) ) )
7	6	a1i	⊢ ( 𝜑 → ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) ) ) )
8	2 2 3 7 1	fprodcom2	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 0 ... 𝑁 ) ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐴 = ∏ 𝑘 ∈ ( 0 ... 𝑁 ) ∏ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) 𝐴 )