gausslemma2dlem1

	Ref	Expression
Hypotheses	gausslemma2d.p	$⊢ φ \to P \in (ℙ ∖ \{2\})$
	gausslemma2d.h	$⊢ H = \frac{P - 1}{2}$
	gausslemma2d.r	$⊢ R = (x \in (1 \dots H) ⟼ if (x \cdot 2 < \frac{P}{2}, x \cdot 2, P - x \cdot 2))$
Assertion	gausslemma2dlem1	$⊢ φ \to H! = \prod_{k = 1}^{H} R (k)$

Step	Hyp	Ref	Expression
1		gausslemma2d.p	$⊢ φ \to P \in (ℙ ∖ \{2\})$
2		gausslemma2d.h	$⊢ H = \frac{P - 1}{2}$
3		gausslemma2d.r	$⊢ R = (x \in (1 \dots H) ⟼ if (x \cdot 2 < \frac{P}{2}, x \cdot 2, P - x \cdot 2))$
4	1 2	gausslemma2dlem0b	$⊢ φ \to H \in ℕ$
5	4	nnnn0d	$⊢ φ \to H \in ℕ_{0}$
6		fprodfac	$⊢ H \in ℕ_{0} \to H! = \prod_{l = 1}^{H} l$
7	5 6	syl	$⊢ φ \to H! = \prod_{l = 1}^{H} l$
8		id	$⊢ l = R (k) \to l = R (k)$
9		fzfid	$⊢ φ \to (1 \dots H) \in Fin$
10		fzfi	$⊢ (1 \dots H) \in Fin$
11		ovex	$⊢ x \cdot 2 \in V$
12		ovex	$⊢ P - x \cdot 2 \in V$
13	11 12	ifex	$⊢ if (x \cdot 2 < \frac{P}{2}, x \cdot 2, P - x \cdot 2) \in V$
14	13 3	fnmpti	$⊢ R Fn (1 \dots H)$
15	1 2 3	gausslemma2dlem1a	$⊢ φ \to ran R = (1 \dots H)$
16		rneqdmfinf1o	$⊢ ((1 \dots H) \in Fin \land R Fn (1 \dots H) \land ran R = (1 \dots H)) \to R : (1 \dots H) \underset{1-1 onto}{⟶} (1 \dots H)$
17	10 14 15 16	mp3an12i	$⊢ φ \to R : (1 \dots H) \underset{1-1 onto}{⟶} (1 \dots H)$
18		eqidd	$⊢ (φ \land k \in (1 \dots H)) \to R (k) = R (k)$
19		elfzelz	$⊢ l \in (1 \dots H) \to l \in ℤ$
20	19	zcnd	$⊢ l \in (1 \dots H) \to l \in ℂ$
21	20	adantl	$⊢ (φ \land l \in (1 \dots H)) \to l \in ℂ$
22	8 9 17 18 21	fprodf1o	$⊢ φ \to \prod_{l = 1}^{H} l = \prod_{k = 1}^{H} R (k)$
23	7 22	eqtrd	$⊢ φ \to H! = \prod_{k = 1}^{H} R (k)$

Metamath Proof Explorer