gausslemma2dlem7

	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))$
	gausslemma2d.m	$⊢ M = ⌊\frac{P}{4}⌋$
	gausslemma2d.n	$⊢ N = H - M$
Assertion	gausslemma2dlem7	$⊢ φ \to {(- 1)}^{N} 2^{H} \mod P = 1$

Proof

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		gausslemma2d.m	$⊢ M = ⌊\frac{P}{4}⌋$
5		gausslemma2d.n	$⊢ N = H - M$
6	1 2 3 4 5	gausslemma2dlem6	$⊢ φ \to H! \mod P = {(- 1)}^{N} 2^{H} H! \mod P$
7	1 2	gausslemma2dlem0b	$⊢ φ \to H \in ℕ$
8	7	nnnn0d	$⊢ φ \to H \in ℕ_{0}$
9	8	faccld	$⊢ φ \to H! \in ℕ$
10	9	nncnd	$⊢ φ \to H! \in ℂ$
11	10	mullidd	$⊢ φ \to 1 H! = H!$
12	11	eqcomd	$⊢ φ \to H! = 1 H!$
13	12	oveq1d	$⊢ φ \to H! \mod P = 1 H! \mod P$
14	13	eqeq1d	$⊢ φ \to (H! \mod P = {(- 1)}^{N} 2^{H} H! \mod P \leftrightarrow 1 H! \mod P = {(- 1)}^{N} 2^{H} H! \mod P)$
15		1zzd	$⊢ φ \to 1 \in ℤ$
16		neg1z	$⊢ - 1 \in ℤ$
17	1 4 2 5	gausslemma2dlem0h	$⊢ φ \to N \in ℕ_{0}$
18		zexpcl	$⊢ (- 1 \in ℤ \land N \in ℕ_{0}) \to {(- 1)}^{N} \in ℤ$
19	16 17 18	sylancr	$⊢ φ \to {(- 1)}^{N} \in ℤ$
20		2z	$⊢ 2 \in ℤ$
21		zexpcl	$⊢ (2 \in ℤ \land H \in ℕ_{0}) \to 2^{H} \in ℤ$
22	20 8 21	sylancr	$⊢ φ \to 2^{H} \in ℤ$
23	19 22	zmulcld	$⊢ φ \to {(- 1)}^{N} 2^{H} \in ℤ$
24	9	nnzd	$⊢ φ \to H! \in ℤ$
25		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
26		prmnn	$⊢ P \in ℙ \to P \in ℕ$
27	1 25 26	3syl	$⊢ φ \to P \in ℕ$
28	1 2	gausslemma2dlem0c	$⊢ φ \to H! \gcd P = 1$
29		cncongrcoprm	$⊢ ((1 \in ℤ \land {(- 1)}^{N} 2^{H} \in ℤ \land H! \in ℤ) \land (P \in ℕ \land H! \gcd P = 1)) \to (1 H! \mod P = {(- 1)}^{N} 2^{H} H! \mod P \leftrightarrow 1 \mod P = {(- 1)}^{N} 2^{H} \mod P)$
30	15 23 24 27 28 29	syl32anc	$⊢ φ \to (1 H! \mod P = {(- 1)}^{N} 2^{H} H! \mod P \leftrightarrow 1 \mod P = {(- 1)}^{N} 2^{H} \mod P)$
31	14 30	bitrd	$⊢ φ \to (H! \mod P = {(- 1)}^{N} 2^{H} H! \mod P \leftrightarrow 1 \mod P = {(- 1)}^{N} 2^{H} \mod P)$
32		simpr	$⊢ (φ \land 1 \mod P = {(- 1)}^{N} 2^{H} \mod P) \to 1 \mod P = {(- 1)}^{N} 2^{H} \mod P$
33	26	nnred	$⊢ P \in ℙ \to P \in ℝ$
34		prmgt1	$⊢ P \in ℙ \to 1 < P$
35	33 34	jca	$⊢ P \in ℙ \to (P \in ℝ \land 1 < P)$
36		1mod	$⊢ (P \in ℝ \land 1 < P) \to 1 \mod P = 1$
37	1 25 35 36	4syl	$⊢ φ \to 1 \mod P = 1$
38	37	adantr	$⊢ (φ \land 1 \mod P = {(- 1)}^{N} 2^{H} \mod P) \to 1 \mod P = 1$
39	32 38	eqtr3d	$⊢ (φ \land 1 \mod P = {(- 1)}^{N} 2^{H} \mod P) \to {(- 1)}^{N} 2^{H} \mod P = 1$
40	39	ex	$⊢ φ \to (1 \mod P = {(- 1)}^{N} 2^{H} \mod P \to {(- 1)}^{N} 2^{H} \mod P = 1)$
41	31 40	sylbid	$⊢ φ \to (H! \mod P = {(- 1)}^{N} 2^{H} H! \mod P \to {(- 1)}^{N} 2^{H} \mod P = 1)$
42	6 41	mpd	$⊢ φ \to {(- 1)}^{N} 2^{H} \mod P = 1$

Metamath Proof Explorer

Theorem gausslemma2dlem7

Proof