Proof of Theorem gausslemma2dlem4
Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
2 | | gausslemma2d.h |
. . 3
⊢ 𝐻 = ((𝑃 − 1) / 2) |
3 | | gausslemma2d.r |
. . 3
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
4 | 1, 2, 3 | gausslemma2dlem1 15177 |
. 2
⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) |
5 | | gausslemma2d.m |
. . . . . 6
⊢ 𝑀 = (⌊‘(𝑃 / 4)) |
6 | | 3lt4 9154 |
. . . . . . . 8
⊢ 3 <
4 |
7 | | breq1 4032 |
. . . . . . . 8
⊢ (𝑃 = 3 → (𝑃 < 4 ↔ 3 < 4)) |
8 | 6, 7 | mpbiri 168 |
. . . . . . 7
⊢ (𝑃 = 3 → 𝑃 < 4) |
9 | | 3nn0 9258 |
. . . . . . . . 9
⊢ 3 ∈
ℕ0 |
10 | | eleq1 2256 |
. . . . . . . . 9
⊢ (𝑃 = 3 → (𝑃 ∈ ℕ0 ↔ 3 ∈
ℕ0)) |
11 | 9, 10 | mpbiri 168 |
. . . . . . . 8
⊢ (𝑃 = 3 → 𝑃 ∈
ℕ0) |
12 | | 4nn 9145 |
. . . . . . . 8
⊢ 4 ∈
ℕ |
13 | | divfl0 10365 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℕ0
∧ 4 ∈ ℕ) → (𝑃 < 4 ↔ (⌊‘(𝑃 / 4)) = 0)) |
14 | 11, 12, 13 | sylancl 413 |
. . . . . . 7
⊢ (𝑃 = 3 → (𝑃 < 4 ↔ (⌊‘(𝑃 / 4)) = 0)) |
15 | 8, 14 | mpbid 147 |
. . . . . 6
⊢ (𝑃 = 3 →
(⌊‘(𝑃 / 4)) =
0) |
16 | 5, 15 | eqtrid 2238 |
. . . . 5
⊢ (𝑃 = 3 → 𝑀 = 0) |
17 | | oveq2 5926 |
. . . . . . . . . . . 12
⊢ (𝑀 = 0 → (1...𝑀) = (1...0)) |
18 | 17 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝑀 = 0 ∧ 𝜑) → (1...𝑀) = (1...0)) |
19 | | fz10 10112 |
. . . . . . . . . . 11
⊢ (1...0) =
∅ |
20 | 18, 19 | eqtrdi 2242 |
. . . . . . . . . 10
⊢ ((𝑀 = 0 ∧ 𝜑) → (1...𝑀) = ∅) |
21 | 20 | prodeq1d 11707 |
. . . . . . . . 9
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = ∏𝑘 ∈ ∅ (𝑅‘𝑘)) |
22 | | prod0 11728 |
. . . . . . . . 9
⊢
∏𝑘 ∈
∅ (𝑅‘𝑘) = 1 |
23 | 21, 22 | eqtrdi 2242 |
. . . . . . . 8
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = 1) |
24 | | oveq1 5925 |
. . . . . . . . . . . 12
⊢ (𝑀 = 0 → (𝑀 + 1) = (0 + 1)) |
25 | 24 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝑀 = 0 ∧ 𝜑) → (𝑀 + 1) = (0 + 1)) |
26 | | 0p1e1 9096 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
27 | 25, 26 | eqtrdi 2242 |
. . . . . . . . . 10
⊢ ((𝑀 = 0 ∧ 𝜑) → (𝑀 + 1) = 1) |
28 | 27 | oveq1d 5933 |
. . . . . . . . 9
⊢ ((𝑀 = 0 ∧ 𝜑) → ((𝑀 + 1)...𝐻) = (1...𝐻)) |
29 | 28 | prodeq1d 11707 |
. . . . . . . 8
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) |
30 | 23, 29 | oveq12d 5936 |
. . . . . . 7
⊢ ((𝑀 = 0 ∧ 𝜑) → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) = (1 · ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘))) |
31 | | 1zzd 9344 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℤ) |
32 | 1, 2 | gausslemma2dlem0b 15166 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ ℕ) |
33 | 32 | nnzd 9438 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ ℤ) |
34 | 31, 33 | fzfigd 10502 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝐻) ∈ Fin) |
35 | 34 | adantl 277 |
. . . . . . . . 9
⊢ ((𝑀 = 0 ∧ 𝜑) → (1...𝐻) ∈ Fin) |
36 | | oveq1 5925 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑘 → (𝑥 · 2) = (𝑘 · 2)) |
37 | 36 | breq1d 4039 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑘 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑘 · 2) < (𝑃 / 2))) |
38 | 36 | oveq2d 5934 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑘 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑘 · 2))) |
39 | 37, 36, 38 | ifbieq12d 3583 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
40 | | simpr 110 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑘 ∈ (1...𝐻)) |
41 | 40 | elfzelzd 10092 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑘 ∈ ℤ) |
42 | | 2z 9345 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
43 | 42 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 2 ∈ ℤ) |
44 | 41, 43 | zmulcld 9445 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑘 · 2) ∈ ℤ) |
45 | 1 | eldifad 3164 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈ ℙ) |
46 | | prmz 12249 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
47 | 45, 46 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℤ) |
48 | 47 | adantr 276 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑃 ∈ ℤ) |
49 | 48, 44 | zsubcld 9444 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑃 − (𝑘 · 2)) ∈
ℤ) |
50 | | zq 9691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 · 2) ∈ ℤ
→ (𝑘 · 2)
∈ ℚ) |
51 | 44, 50 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑘 · 2) ∈ ℚ) |
52 | | 2nn 9143 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℕ |
53 | | znq 9689 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℤ ∧ 2 ∈
ℕ) → (𝑃 / 2)
∈ ℚ) |
54 | 47, 52, 53 | sylancl 413 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 / 2) ∈ ℚ) |
55 | 54 | adantr 276 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℚ) |
56 | | qdclt 10315 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 · 2) ∈ ℚ
∧ (𝑃 / 2) ∈
ℚ) → DECID (𝑘 · 2) < (𝑃 / 2)) |
57 | 51, 55, 56 | syl2anc 411 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → DECID (𝑘 · 2) < (𝑃 / 2)) |
58 | 44, 49, 57 | ifcldcd 3593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))) ∈
ℤ) |
59 | 3, 39, 40, 58 | fvmptd3 5651 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
60 | 59, 58 | eqeltrd 2270 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℤ) |
61 | 60 | zcnd 9440 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℂ) |
62 | 61 | adantll 476 |
. . . . . . . . 9
⊢ (((𝑀 = 0 ∧ 𝜑) ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℂ) |
63 | 35, 62 | fprodcl 11750 |
. . . . . . . 8
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) ∈ ℂ) |
64 | 63 | mullidd 8037 |
. . . . . . 7
⊢ ((𝑀 = 0 ∧ 𝜑) → (1 · ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) |
65 | 30, 64 | eqtr2d 2227 |
. . . . . 6
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
66 | 65 | ex 115 |
. . . . 5
⊢ (𝑀 = 0 → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
67 | 16, 66 | syl 14 |
. . . 4
⊢ (𝑃 = 3 → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
68 | 67 | impcom 125 |
. . 3
⊢ ((𝜑 ∧ 𝑃 = 3) → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
69 | 1, 5 | gausslemma2dlem0d 15168 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
70 | 69 | nn0red 9294 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
71 | 70 | ltp1d 8949 |
. . . . . . 7
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
72 | | fzdisj 10118 |
. . . . . . 7
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
73 | 71, 72 | syl 14 |
. . . . . 6
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
74 | 73 | adantl 277 |
. . . . 5
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
75 | | eluzelz 9601 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(ℤ≥‘5) → 𝑃 ∈ ℤ) |
76 | | znq 9689 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℤ ∧ 4 ∈
ℕ) → (𝑃 / 4)
∈ ℚ) |
77 | 75, 12, 76 | sylancl 413 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘5) → (𝑃 / 4) ∈ ℚ) |
78 | 77 | flqcld 10346 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘5) → (⌊‘(𝑃 / 4)) ∈ ℤ) |
79 | | nnrp 9729 |
. . . . . . . . . . . . . . . 16
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
80 | 12, 79 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℝ+ |
81 | | eluzelre 9602 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(ℤ≥‘5) → 𝑃 ∈ ℝ) |
82 | | eluz2 9598 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈
(ℤ≥‘5) ↔ (5 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 5 ≤
𝑃)) |
83 | | 4lt5 9157 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 <
5 |
84 | | 4re 9059 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ∈
ℝ |
85 | | 5re 9061 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 5 ∈
ℝ |
86 | 85 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → 5 ∈ ℝ) |
87 | | zre 9321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℤ → 𝑃 ∈
ℝ) |
88 | 87 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → 𝑃
∈ ℝ) |
89 | | ltleletr 8101 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((4
∈ ℝ ∧ 5 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((4 < 5 ∧ 5
≤ 𝑃) → 4 ≤ 𝑃)) |
90 | 84, 86, 88, 89 | mp3an2i 1353 |
. . . . . . . . . . . . . . . . . 18
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → ((4 < 5 ∧ 5 ≤ 𝑃) → 4 ≤ 𝑃)) |
91 | 83, 90 | mpani 430 |
. . . . . . . . . . . . . . . . 17
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → (5 ≤ 𝑃 → 4 ≤ 𝑃)) |
92 | 91 | 3impia 1202 |
. . . . . . . . . . . . . . . 16
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ ∧ 5 ≤ 𝑃) → 4 ≤ 𝑃) |
93 | 82, 92 | sylbi 121 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(ℤ≥‘5) → 4 ≤ 𝑃) |
94 | | divge1 9789 |
. . . . . . . . . . . . . . 15
⊢ ((4
∈ ℝ+ ∧ 𝑃 ∈ ℝ ∧ 4 ≤ 𝑃) → 1 ≤ (𝑃 / 4)) |
95 | 80, 81, 93, 94 | mp3an2i 1353 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘5) → 1 ≤ (𝑃 / 4)) |
96 | | 1zzd 9344 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(ℤ≥‘5) → 1 ∈ ℤ) |
97 | | flqge 10351 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 / 4) ∈ ℚ ∧ 1
∈ ℤ) → (1 ≤ (𝑃 / 4) ↔ 1 ≤ (⌊‘(𝑃 / 4)))) |
98 | 77, 96, 97 | syl2anc 411 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘5) → (1 ≤ (𝑃 / 4) ↔ 1 ≤ (⌊‘(𝑃 / 4)))) |
99 | 95, 98 | mpbid 147 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘5) → 1 ≤ (⌊‘(𝑃 / 4))) |
100 | | elnnz1 9340 |
. . . . . . . . . . . . 13
⊢
((⌊‘(𝑃 /
4)) ∈ ℕ ↔ ((⌊‘(𝑃 / 4)) ∈ ℤ ∧ 1 ≤
(⌊‘(𝑃 /
4)))) |
101 | 78, 99, 100 | sylanbrc 417 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈
(ℤ≥‘5) → (⌊‘(𝑃 / 4)) ∈ ℕ) |
102 | 101 | adantl 277 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → (⌊‘(𝑃 / 4)) ∈ ℕ) |
103 | | oddprm 12397 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
104 | 103 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → ((𝑃 − 1) / 2) ∈
ℕ) |
105 | | eldifi 3281 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
106 | | prmuz2 12269 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
107 | 105, 106 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
(ℤ≥‘2)) |
108 | 107 | adantr 276 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → 𝑃 ∈
(ℤ≥‘2)) |
109 | | fldiv4lem1div2uz2 10375 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈
(ℤ≥‘2) → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2)) |
110 | 108, 109 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2)) |
111 | 102, 104,
110 | 3jca 1179 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2))) |
112 | 111 | ex 115 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈
(ℤ≥‘5) → ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2)))) |
113 | 1, 112 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 ∈ (ℤ≥‘5)
→ ((⌊‘(𝑃 /
4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧
(⌊‘(𝑃 / 4))
≤ ((𝑃 − 1) /
2)))) |
114 | 113 | impcom 125 |
. . . . . . 7
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2))) |
115 | 2 | oveq2i 5929 |
. . . . . . . . 9
⊢
(1...𝐻) =
(1...((𝑃 − 1) /
2)) |
116 | 5, 115 | eleq12i 2261 |
. . . . . . . 8
⊢ (𝑀 ∈ (1...𝐻) ↔ (⌊‘(𝑃 / 4)) ∈ (1...((𝑃 − 1) / 2))) |
117 | | elfz1b 10156 |
. . . . . . . 8
⊢
((⌊‘(𝑃 /
4)) ∈ (1...((𝑃 −
1) / 2)) ↔ ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2))) |
118 | 116, 117 | bitri 184 |
. . . . . . 7
⊢ (𝑀 ∈ (1...𝐻) ↔ ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2))) |
119 | 114, 118 | sylibr 134 |
. . . . . 6
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → 𝑀 ∈ (1...𝐻)) |
120 | | fzsplit 10117 |
. . . . . 6
⊢ (𝑀 ∈ (1...𝐻) → (1...𝐻) = ((1...𝑀) ∪ ((𝑀 + 1)...𝐻))) |
121 | 119, 120 | syl 14 |
. . . . 5
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → (1...𝐻) = ((1...𝑀) ∪ ((𝑀 + 1)...𝐻))) |
122 | 34 | adantl 277 |
. . . . 5
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → (1...𝐻) ∈ Fin) |
123 | 61 | adantll 476 |
. . . . 5
⊢ (((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℂ) |
124 | 74, 121, 122, 123 | fprodsplit 11740 |
. . . 4
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
125 | 124 | ancoms 268 |
. . 3
⊢ ((𝜑 ∧ 𝑃 ∈ (ℤ≥‘5))
→ ∏𝑘 ∈
(1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
126 | | 2re 9052 |
. . . . . . 7
⊢ 2 ∈
ℝ |
127 | 126 | a1i 9 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℝ) |
128 | | oddprmgt2 12272 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 2 < 𝑃) |
129 | 1, 128 | syl 14 |
. . . . . 6
⊢ (𝜑 → 2 < 𝑃) |
130 | 127, 129 | gtned 8132 |
. . . . 5
⊢ (𝜑 → 𝑃 ≠ 2) |
131 | 130 | neneqd 2385 |
. . . 4
⊢ (𝜑 → ¬ 𝑃 = 2) |
132 | | prm23ge5 12402 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈
(ℤ≥‘5))) |
133 | 45, 132 | syl 14 |
. . . . . 6
⊢ (𝜑 → (𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈
(ℤ≥‘5))) |
134 | | 3orass 983 |
. . . . . 6
⊢ ((𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈ (ℤ≥‘5))
↔ (𝑃 = 2 ∨ (𝑃 = 3 ∨ 𝑃 ∈
(ℤ≥‘5)))) |
135 | 133, 134 | sylib 122 |
. . . . 5
⊢ (𝜑 → (𝑃 = 2 ∨ (𝑃 = 3 ∨ 𝑃 ∈
(ℤ≥‘5)))) |
136 | 135 | ord 725 |
. . . 4
⊢ (𝜑 → (¬ 𝑃 = 2 → (𝑃 = 3 ∨ 𝑃 ∈
(ℤ≥‘5)))) |
137 | 131, 136 | mpd 13 |
. . 3
⊢ (𝜑 → (𝑃 = 3 ∨ 𝑃 ∈
(ℤ≥‘5))) |
138 | 68, 125, 137 | mpjaodan 799 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
139 | 4, 138 | eqtrd 2226 |
1
⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |