Metamath Proof Explorer

Theorem gausslemma2dlem4

Description: Lemma 4 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 ) )
Assertion gausslemma2dlem4 ( 𝜑 → ( ! ‘ 𝐻 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) )

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 1 2 3 gausslemma2dlem1 ⊢ ( 𝜑 → ( ! ‘ 𝐻 ) = ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) )
6 eldif ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 ∈ { 2 } ) )
7 prm23ge5 ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) )
8 eleq1 ⊢ ( 𝑃 = 2 → ( 𝑃 ∈ { 2 } ↔ 2 ∈ { 2 } ) )
9 8 notbid ⊢ ( 𝑃 = 2 → ( ¬ 𝑃 ∈ { 2 } ↔ ¬ 2 ∈ { 2 } ) )
10 2ex ⊢ 2 ∈ V
11 10 snid ⊢ 2 ∈ { 2 }
12 11 2a1i ⊢ ( 𝑃 = 2 → ( ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ≠ ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) → 2 ∈ { 2 } ) )
13 12 necon1bd ⊢ ( 𝑃 = 2 → ( ¬ 2 ∈ { 2 } → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) ) )
14 13 a1dd ⊢ ( 𝑃 = 2 → ( ¬ 2 ∈ { 2 } → ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) ) ) )
15 9 14 sylbid ⊢ ( 𝑃 = 2 → ( ¬ 𝑃 ∈ { 2 } → ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) ) ) )
16 3lt4 ⊢ 3 < 4
17 breq1 ⊢ ( 𝑃 = 3 → ( 𝑃 < 4 ↔ 3 < 4 ) )
18 16 17 mpbiri ⊢ ( 𝑃 = 3 → 𝑃 < 4 )
19 3nn0 ⊢ 3 ∈ ℕ0
20 eleq1 ⊢ ( 𝑃 = 3 → ( 𝑃 ∈ ℕ0 ↔ 3 ∈ ℕ0 ) )
21 19 20 mpbiri ⊢ ( 𝑃 = 3 → 𝑃 ∈ ℕ0 )
22 4nn ⊢ 4 ∈ ℕ
23 divfl0 ⊢ ( ( 𝑃 ∈ ℕ0 ∧ 4 ∈ ℕ ) → ( 𝑃 < 4 ↔ ( ⌊ ‘ ( 𝑃 / 4 ) ) = 0 ) )
24 21 22 23 sylancl ⊢ ( 𝑃 = 3 → ( 𝑃 < 4 ↔ ( ⌊ ‘ ( 𝑃 / 4 ) ) = 0 ) )
25 18 24 mpbid ⊢ ( 𝑃 = 3 → ( ⌊ ‘ ( 𝑃 / 4 ) ) = 0 )
26 4 25 eqtrid ⊢ ( 𝑃 = 3 → 𝑀 = 0 )
27 oveq2 ⊢ ( 𝑀 = 0 → ( 1 ... 𝑀 ) = ( 1 ... 0 ) )
28 27 adantr ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ( 1 ... 𝑀 ) = ( 1 ... 0 ) )
29 fz10 ⊢ ( 1 ... 0 ) = ∅
30 28 29 eqtrdi ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ( 1 ... 𝑀 ) = ∅ )
31 30 prodeq1d ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ∏ 𝑘 ∈ ∅ ( 𝑅 ‘ 𝑘 ) )
32 prod0 ⊢ ∏ 𝑘 ∈ ∅ ( 𝑅 ‘ 𝑘 ) = 1
33 31 32 eqtrdi ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = 1 )
34 oveq1 ⊢ ( 𝑀 = 0 → ( 𝑀 + 1 ) = ( 0 + 1 ) )
35 34 adantr ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ( 𝑀 + 1 ) = ( 0 + 1 ) )
36 0p1e1 ⊢ ( 0 + 1 ) = 1
37 35 36 eqtrdi ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ( 𝑀 + 1 ) = 1 )
38 37 oveq1d ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ( ( 𝑀 + 1 ) ... 𝐻 ) = ( 1 ... 𝐻 ) )
39 38 prodeq1d ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) )
40 33 39 oveq12d ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) = ( 1 · ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) )
41 fzfid ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ( 1 ... 𝐻 ) ∈ Fin )
42 oveq1 ⊢ ( 𝑥 = 𝑘 → ( 𝑥 · 2 ) = ( 𝑘 · 2 ) )
43 42 breq1d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ↔ ( 𝑘 · 2 ) < ( 𝑃 / 2 ) ) )
44 42 oveq2d ⊢ ( 𝑥 = 𝑘 → ( 𝑃 − ( 𝑥 · 2 ) ) = ( 𝑃 − ( 𝑘 · 2 ) ) )
45 43 42 44 ifbieq12d ⊢ ( 𝑥 = 𝑘 → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = if ( ( 𝑘 · 2 ) < ( 𝑃 / 2 ) , ( 𝑘 · 2 ) , ( 𝑃 − ( 𝑘 · 2 ) ) ) )
46 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → 𝑘 ∈ ( 1 ... 𝐻 ) )
47 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... 𝐻 ) → 𝑘 ∈ ℤ )
48 47 zcnd ⊢ ( 𝑘 ∈ ( 1 ... 𝐻 ) → 𝑘 ∈ ℂ )
49 2cnd ⊢ ( 𝑘 ∈ ( 1 ... 𝐻 ) → 2 ∈ ℂ )
50 48 49 mulcld ⊢ ( 𝑘 ∈ ( 1 ... 𝐻 ) → ( 𝑘 · 2 ) ∈ ℂ )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → ( 𝑘 · 2 ) ∈ ℂ )
52 eldifi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
53 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
54 53 zcnd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
55 1 52 54 3syl ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → 𝑃 ∈ ℂ )
57 56 51 subcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 − ( 𝑘 · 2 ) ) ∈ ℂ )
58 51 57 ifcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → if ( ( 𝑘 · 2 ) < ( 𝑃 / 2 ) , ( 𝑘 · 2 ) , ( 𝑃 − ( 𝑘 · 2 ) ) ) ∈ ℂ )
59 3 45 46 58 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → ( 𝑅 ‘ 𝑘 ) = if ( ( 𝑘 · 2 ) < ( 𝑃 / 2 ) , ( 𝑘 · 2 ) , ( 𝑃 − ( 𝑘 · 2 ) ) ) )
60 59 58 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → ( 𝑅 ‘ 𝑘 ) ∈ ℂ )
61 60 adantll ⊢ ( ( ( 𝑀 = 0 ∧ 𝜑 ) ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → ( 𝑅 ‘ 𝑘 ) ∈ ℂ )
62 41 61 fprodcl ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ∈ ℂ )
63 62 mulid2d ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ( 1 · ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) )
64 40 63 eqtr2d ⊢ ( ( 𝑀 = 0 ∧ 𝜑 ) → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) )
65 64 ex ⊢ ( 𝑀 = 0 → ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) ) )
66 26 65 syl ⊢ ( 𝑃 = 3 → ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) ) )
67 66 a1d ⊢ ( 𝑃 = 3 → ( ¬ 𝑃 ∈ { 2 } → ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) ) ) )
68 1 4 gausslemma2dlem0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
69 68 nn0red ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
70 69 ltp1d ⊢ ( 𝜑 → 𝑀 < ( 𝑀 + 1 ) )
71 fzdisj ⊢ ( 𝑀 < ( 𝑀 + 1 ) → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝐻 ) ) = ∅ )
72 70 71 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝐻 ) ) = ∅ )
73 72 adantl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝜑 ) → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝐻 ) ) = ∅ )
74 eluzelre ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → 𝑃 ∈ ℝ )
75 4re ⊢ 4 ∈ ℝ
76 75 a1i ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → 4 ∈ ℝ )
77 4ne0 ⊢ 4 ≠ 0
78 77 a1i ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → 4 ≠ 0 )
79 74 76 78 redivcld ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → ( 𝑃 / 4 ) ∈ ℝ )
80 79 flcld ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℤ )
81 nnrp ⊢ ( 4 ∈ ℕ → 4 ∈ ℝ+ )
82 22 81 ax-mp ⊢ 4 ∈ ℝ+
83 eluz2 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) ↔ ( 5 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 5 ≤ 𝑃 ) )
84 4lt5 ⊢ 4 < 5
85 5re ⊢ 5 ∈ ℝ
86 85 a1i ⊢ ( ( 5 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → 5 ∈ ℝ )
87 zre ⊢ ( 𝑃 ∈ ℤ → 𝑃 ∈ ℝ )
88 87 adantl ⊢ ( ( 5 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → 𝑃 ∈ ℝ )
89 ltleletr ⊢ ( ( 4 ∈ ℝ ∧ 5 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 4 < 5 ∧ 5 ≤ 𝑃 ) → 4 ≤ 𝑃 ) )
90 75 86 88 89 mp3an2i ⊢ ( ( 5 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 4 < 5 ∧ 5 ≤ 𝑃 ) → 4 ≤ 𝑃 ) )
91 84 90 mpani ⊢ ( ( 5 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 5 ≤ 𝑃 → 4 ≤ 𝑃 ) )
92 91 3impia ⊢ ( ( 5 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 5 ≤ 𝑃 ) → 4 ≤ 𝑃 )
93 83 92 sylbi ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → 4 ≤ 𝑃 )
94 divge1 ⊢ ( ( 4 ∈ ℝ+ ∧ 𝑃 ∈ ℝ ∧ 4 ≤ 𝑃 ) → 1 ≤ ( 𝑃 / 4 ) )
95 82 74 93 94 mp3an2i ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → 1 ≤ ( 𝑃 / 4 ) )
96 1zzd ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → 1 ∈ ℤ )
97 flge ⊢ ( ( ( 𝑃 / 4 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( 1 ≤ ( 𝑃 / 4 ) ↔ 1 ≤ ( ⌊ ‘ ( 𝑃 / 4 ) ) ) )
98 79 96 97 syl2anc ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → ( 1 ≤ ( 𝑃 / 4 ) ↔ 1 ≤ ( ⌊ ‘ ( 𝑃 / 4 ) ) ) )
99 95 98 mpbid ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → 1 ≤ ( ⌊ ‘ ( 𝑃 / 4 ) ) )
100 elnnz1 ⊢ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ ↔ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℤ ∧ 1 ≤ ( ⌊ ‘ ( 𝑃 / 4 ) ) ) )
101 80 99 100 sylanbrc ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ )
102 101 adantl ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ )
103 oddprm ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
104 103 adantr ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
105 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
106 52 105 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
107 106 adantr ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
108 fldiv4lem1div2uz2 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
109 107 108 syl ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
110 102 104 109 3jca ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
111 110 ex ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) )
112 1 111 syl ⊢ ( 𝜑 → ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) )
113 112 impcom ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝜑 ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
114 2 oveq2i ⊢ ( 1 ... 𝐻 ) = ( 1 ... ( ( 𝑃 − 1 ) / 2 ) )
115 4 114 eleq12i ⊢ ( 𝑀 ∈ ( 1 ... 𝐻 ) ↔ ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
116 elfz1b ⊢ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
117 115 116 bitri ⊢ ( 𝑀 ∈ ( 1 ... 𝐻 ) ↔ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
118 113 117 sylibr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝜑 ) → 𝑀 ∈ ( 1 ... 𝐻 ) )
119 fzsplit ⊢ ( 𝑀 ∈ ( 1 ... 𝐻 ) → ( 1 ... 𝐻 ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝐻 ) ) )
120 118 119 syl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝜑 ) → ( 1 ... 𝐻 ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝐻 ) ) )
121 fzfid ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝜑 ) → ( 1 ... 𝐻 ) ∈ Fin )
122 60 adantll ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → ( 𝑅 ‘ 𝑘 ) ∈ ℂ )
123 73 120 121 122 fprodsplit ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝜑 ) → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) )
124 123 ex ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) ) )
125 124 a1d ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → ( ¬ 𝑃 ∈ { 2 } → ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) ) ) )
126 15 67 125 3jaoi ⊢ ( ( 𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) → ( ¬ 𝑃 ∈ { 2 } → ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) ) ) )
127 7 126 syl ⊢ ( 𝑃 ∈ ℙ → ( ¬ 𝑃 ∈ { 2 } → ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) ) ) )
128 127 imp ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 ∈ { 2 } ) → ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) ) )
129 6 128 sylbi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) ) )
130 1 129 mpcom ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) )
131 5 130 eqtrd ⊢ ( 𝜑 → ( ! ‘ 𝐻 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) )