Theorem gausslemma2dlem6

Description: Lemma 6 for gausslemma2d . (Contributed by AV, 16-Jun-2021)

	Ref	Expression
Hypotheses	gausslemma2d.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
	gausslemma2d.h	⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
	gausslemma2d.r	⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
	gausslemma2d.m	⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
	gausslemma2d.n	⊢ 𝑁 = ( 𝐻 − 𝑀 )
Assertion	gausslemma2dlem6	⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		gausslemma2d.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2		gausslemma2d.h	⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
3		gausslemma2d.r	⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
4		gausslemma2d.m	⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
5		gausslemma2d.n	⊢ 𝑁 = ( 𝐻 − 𝑀 )
6	1 2 3 4	gausslemma2dlem4	⊢ ( 𝜑 → ( ! ‘ 𝐻 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) )
7	6	oveq1d	⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) mod 𝑃 ) )
8		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
9	1 2 3 4	gausslemma2dlem2	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) )
11		rspa	⊢ ( ( ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) )
12	11	expcom	⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) ) )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) ) )
14		elfzelz	⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → 𝑘 ∈ ℤ )
15		2z	⊢ 2 ∈ ℤ
16	15	a1i	⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → 2 ∈ ℤ )
17	14 16	zmulcld	⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → ( 𝑘 · 2 ) ∈ ℤ )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑘 · 2 ) ∈ ℤ )
19		eleq1	⊢ ( ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) → ( ( 𝑅 ‘ 𝑘 ) ∈ ℤ ↔ ( 𝑘 · 2 ) ∈ ℤ ) )
20	18 19	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) → ( 𝑅 ‘ 𝑘 ) ∈ ℤ ) )
21	13 20	syld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) → ( 𝑅 ‘ 𝑘 ) ∈ ℤ ) )
22	10 21	mpd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑅 ‘ 𝑘 ) ∈ ℤ )
23	8 22	fprodzcl	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) ∈ ℤ )
24		fzfid	⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝐻 ) ∈ Fin )
25	1 2 3 4	gausslemma2dlem3	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) )
27		rspa	⊢ ( ( ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) )
28	27	expcom	⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) ) )
29	28	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) ) )
30	1	gausslemma2dlem0a	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
31	30	nnzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
32		elfzelz	⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → 𝑘 ∈ ℤ )
33	15	a1i	⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → 2 ∈ ℤ )
34	32 33	zmulcld	⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( 𝑘 · 2 ) ∈ ℤ )
35		zsubcl	⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑘 · 2 ) ∈ ℤ ) → ( 𝑃 − ( 𝑘 · 2 ) ) ∈ ℤ )
36	31 34 35	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑃 − ( 𝑘 · 2 ) ) ∈ ℤ )
37		eleq1	⊢ ( ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) → ( ( 𝑅 ‘ 𝑘 ) ∈ ℤ ↔ ( 𝑃 − ( 𝑘 · 2 ) ) ∈ ℤ ) )
38	36 37	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) → ( 𝑅 ‘ 𝑘 ) ∈ ℤ ) )
39	29 38	syld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) → ( 𝑅 ‘ 𝑘 ) ∈ ℤ ) )
40	26 39	mpd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑅 ‘ 𝑘 ) ∈ ℤ )
41	24 40	fprodzcl	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ∈ ℤ )
42	41	zred	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ∈ ℝ )
43		nnoddn2prm	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) )
44		nnrp	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ+ )
45	44	adantr	⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → 𝑃 ∈ ℝ+ )
46	1 43 45	3syl	⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
47		modmulmodr	⊢ ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) ∈ ℤ ∧ ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) mod 𝑃 ) )
48	47	eqcomd	⊢ ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) ∈ ℤ ∧ ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) ) mod 𝑃 ) )
49	23 42 46 48	syl3anc	⊢ ( 𝜑 → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) ) mod 𝑃 ) )
50	1 2 3 4 5	gausslemma2dlem5	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) mod 𝑃 ) )
51	50	oveq2d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) mod 𝑃 ) ) )
52	51	oveq1d	⊢ ( 𝜑 → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) mod 𝑃 ) ) mod 𝑃 ) )
53		neg1rr	⊢ - 1 ∈ ℝ
54	53	a1i	⊢ ( 𝜑 → - 1 ∈ ℝ )
55	1 4 2 5	gausslemma2dlem0h	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
56	54 55	reexpcld	⊢ ( 𝜑 → ( - 1 ↑ 𝑁 ) ∈ ℝ )
57	32	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → 𝑘 ∈ ℤ )
58	15	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → 2 ∈ ℤ )
59	57 58	zmulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑘 · 2 ) ∈ ℤ )
60	24 59	fprodzcl	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ∈ ℤ )
61	60	zred	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ∈ ℝ )
62	56 61	remulcld	⊢ ( 𝜑 → ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ∈ ℝ )
63		modmulmodr	⊢ ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) ∈ ℤ ∧ ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) mod 𝑃 ) )
64	23 62 46 63	syl3anc	⊢ ( 𝜑 → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) mod 𝑃 ) )
65	9	prodeq2d	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑘 · 2 ) )
66	65	oveq1d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑘 · 2 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) )
67		fzfid	⊢ ( 𝜑 → ( 1 ... 𝐻 ) ∈ Fin )
68		elfzelz	⊢ ( 𝑘 ∈ ( 1 ... 𝐻 ) → 𝑘 ∈ ℤ )
69	68	zcnd	⊢ ( 𝑘 ∈ ( 1 ... 𝐻 ) → 𝑘 ∈ ℂ )
70	69	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → 𝑘 ∈ ℂ )
71		2cn	⊢ 2 ∈ ℂ
72	71	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → 2 ∈ ℂ )
73	67 70 72	fprodmul	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑘 · 2 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 𝑘 · ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 2 ) )
74	1 4	gausslemma2dlem0d	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
75	74	nn0red	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
76	75	ltp1d	⊢ ( 𝜑 → 𝑀 < ( 𝑀 + 1 ) )
77		fzdisj	⊢ ( 𝑀 < ( 𝑀 + 1 ) → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝐻 ) ) = ∅ )
78	76 77	syl	⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝐻 ) ) = ∅ )
79		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
80		nn0pzuz	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 1 ∈ ℤ ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
81	74 79 80	syl2anc	⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
82	74	nn0zd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
83	1 2	gausslemma2dlem0b	⊢ ( 𝜑 → 𝐻 ∈ ℕ )
84	83	nnzd	⊢ ( 𝜑 → 𝐻 ∈ ℤ )
85	1 4 2	gausslemma2dlem0g	⊢ ( 𝜑 → 𝑀 ≤ 𝐻 )
86		eluz2	⊢ ( 𝐻 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑀 ≤ 𝐻 ) )
87	82 84 85 86	syl3anbrc	⊢ ( 𝜑 → 𝐻 ∈ ( ℤ≥ ‘ 𝑀 ) )
88		fzsplit2	⊢ ( ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝐻 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 ... 𝐻 ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝐻 ) ) )
89	81 87 88	syl2anc	⊢ ( 𝜑 → ( 1 ... 𝐻 ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝐻 ) ) )
90	15	a1i	⊢ ( 𝑘 ∈ ( 1 ... 𝐻 ) → 2 ∈ ℤ )
91	68 90	zmulcld	⊢ ( 𝑘 ∈ ( 1 ... 𝐻 ) → ( 𝑘 · 2 ) ∈ ℤ )
92	91	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → ( 𝑘 · 2 ) ∈ ℤ )
93	92	zcnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → ( 𝑘 · 2 ) ∈ ℂ )
94	78 89 67 93	fprodsplit	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑘 · 2 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑘 · 2 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) )
95		nnnn0	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 )
96	95	anim1i	⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑃 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑃 ) )
97	43 96	syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑃 ) )
98		nn0oddm1d2	⊢ ( 𝑃 ∈ ℕ0 → ( ¬ 2 ∥ 𝑃 ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) )
99	98	biimpa	⊢ ( ( 𝑃 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑃 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
100	2 99	eqeltrid	⊢ ( ( 𝑃 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑃 ) → 𝐻 ∈ ℕ0 )
101	1 97 100	3syl	⊢ ( 𝜑 → 𝐻 ∈ ℕ0 )
102		fprodfac	⊢ ( 𝐻 ∈ ℕ0 → ( ! ‘ 𝐻 ) = ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 𝑘 )
103	101 102	syl	⊢ ( 𝜑 → ( ! ‘ 𝐻 ) = ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 𝑘 )
104	103	eqcomd	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 𝑘 = ( ! ‘ 𝐻 ) )
105		fzfi	⊢ ( 1 ... 𝐻 ) ∈ Fin
106	105 71	pm3.2i	⊢ ( ( 1 ... 𝐻 ) ∈ Fin ∧ 2 ∈ ℂ )
107		fprodconst	⊢ ( ( ( 1 ... 𝐻 ) ∈ Fin ∧ 2 ∈ ℂ ) → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 2 = ( 2 ↑ ( ♯ ‘ ( 1 ... 𝐻 ) ) ) )
108	106 107	mp1i	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 2 = ( 2 ↑ ( ♯ ‘ ( 1 ... 𝐻 ) ) ) )
109	104 108	oveq12d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 𝑘 · ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 2 ) = ( ( ! ‘ 𝐻 ) · ( 2 ↑ ( ♯ ‘ ( 1 ... 𝐻 ) ) ) ) )
110		hashfz1	⊢ ( 𝐻 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝐻 ) ) = 𝐻 )
111	101 110	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝐻 ) ) = 𝐻 )
112	111	oveq2d	⊢ ( 𝜑 → ( 2 ↑ ( ♯ ‘ ( 1 ... 𝐻 ) ) ) = ( 2 ↑ 𝐻 ) )
113	112	oveq2d	⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) · ( 2 ↑ ( ♯ ‘ ( 1 ... 𝐻 ) ) ) ) = ( ( ! ‘ 𝐻 ) · ( 2 ↑ 𝐻 ) ) )
114	101	faccld	⊢ ( 𝜑 → ( ! ‘ 𝐻 ) ∈ ℕ )
115	114	nncnd	⊢ ( 𝜑 → ( ! ‘ 𝐻 ) ∈ ℂ )
116		2nn0	⊢ 2 ∈ ℕ0
117		nn0expcl	⊢ ( ( 2 ∈ ℕ0 ∧ 𝐻 ∈ ℕ0 ) → ( 2 ↑ 𝐻 ) ∈ ℕ0 )
118	117	nn0cnd	⊢ ( ( 2 ∈ ℕ0 ∧ 𝐻 ∈ ℕ0 ) → ( 2 ↑ 𝐻 ) ∈ ℂ )
119	116 101 118	sylancr	⊢ ( 𝜑 → ( 2 ↑ 𝐻 ) ∈ ℂ )
120	115 119	mulcomd	⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) · ( 2 ↑ 𝐻 ) ) = ( ( 2 ↑ 𝐻 ) · ( ! ‘ 𝐻 ) ) )
121	109 113 120	3eqtrd	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 𝑘 · ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 2 ) = ( ( 2 ↑ 𝐻 ) · ( ! ‘ 𝐻 ) ) )
122	73 94 121	3eqtr3d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑘 · 2 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) = ( ( 2 ↑ 𝐻 ) · ( ! ‘ 𝐻 ) ) )
123	66 122	eqtrd	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) = ( ( 2 ↑ 𝐻 ) · ( ! ‘ 𝐻 ) ) )
124	123	oveq2d	⊢ ( 𝜑 → ( ( - 1 ↑ 𝑁 ) · ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( 2 ↑ 𝐻 ) · ( ! ‘ 𝐻 ) ) ) )
125	23	zcnd	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) ∈ ℂ )
126	56	recnd	⊢ ( 𝜑 → ( - 1 ↑ 𝑁 ) ∈ ℂ )
127	60	zcnd	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ∈ ℂ )
128	125 126 127	mul12d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) )
129	126 119 115	mulassd	⊢ ( 𝜑 → ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( 2 ↑ 𝐻 ) · ( ! ‘ 𝐻 ) ) ) )
130	124 128 129	3eqtr4d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) )
131	130	oveq1d	⊢ ( 𝜑 → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) )
132	52 64 131	3eqtrd	⊢ ( 𝜑 → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) )
133	7 49 132	3eqtrd	⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) )