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 15105 |
. 2
⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) |
5 | | gausslemma2d.m |
. . . . . 6
⊢ 𝑀 = (⌊‘(𝑃 / 4)) |
6 | | 3lt4 9140 |
. . . . . . . 8
⊢ 3 <
4 |
7 | | breq1 4028 |
. . . . . . . 8
⊢ (𝑃 = 3 → (𝑃 < 4 ↔ 3 < 4)) |
8 | 6, 7 | mpbiri 168 |
. . . . . . 7
⊢ (𝑃 = 3 → 𝑃 < 4) |
9 | | 3nn0 9244 |
. . . . . . . . 9
⊢ 3 ∈
ℕ0 |
10 | | eleq1 2252 |
. . . . . . . . 9
⊢ (𝑃 = 3 → (𝑃 ∈ ℕ0 ↔ 3 ∈
ℕ0)) |
11 | 9, 10 | mpbiri 168 |
. . . . . . . 8
⊢ (𝑃 = 3 → 𝑃 ∈
ℕ0) |
12 | | 4nn 9131 |
. . . . . . . 8
⊢ 4 ∈
ℕ |
13 | | divfl0 10351 |
. . . . . . . 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 2234 |
. . . . 5
⊢ (𝑃 = 3 → 𝑀 = 0) |
17 | | oveq2 5914 |
. . . . . . . . . . . 12
⊢ (𝑀 = 0 → (1...𝑀) = (1...0)) |
18 | 17 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝑀 = 0 ∧ 𝜑) → (1...𝑀) = (1...0)) |
19 | | fz10 10098 |
. . . . . . . . . . 11
⊢ (1...0) =
∅ |
20 | 18, 19 | eqtrdi 2238 |
. . . . . . . . . 10
⊢ ((𝑀 = 0 ∧ 𝜑) → (1...𝑀) = ∅) |
21 | 20 | prodeq1d 11681 |
. . . . . . . . 9
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = ∏𝑘 ∈ ∅ (𝑅‘𝑘)) |
22 | | prod0 11702 |
. . . . . . . . 9
⊢
∏𝑘 ∈
∅ (𝑅‘𝑘) = 1 |
23 | 21, 22 | eqtrdi 2238 |
. . . . . . . 8
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = 1) |
24 | | oveq1 5913 |
. . . . . . . . . . . 12
⊢ (𝑀 = 0 → (𝑀 + 1) = (0 + 1)) |
25 | 24 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝑀 = 0 ∧ 𝜑) → (𝑀 + 1) = (0 + 1)) |
26 | | 0p1e1 9082 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
27 | 25, 26 | eqtrdi 2238 |
. . . . . . . . . 10
⊢ ((𝑀 = 0 ∧ 𝜑) → (𝑀 + 1) = 1) |
28 | 27 | oveq1d 5921 |
. . . . . . . . 9
⊢ ((𝑀 = 0 ∧ 𝜑) → ((𝑀 + 1)...𝐻) = (1...𝐻)) |
29 | 28 | prodeq1d 11681 |
. . . . . . . 8
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) |
30 | 23, 29 | oveq12d 5924 |
. . . . . . 7
⊢ ((𝑀 = 0 ∧ 𝜑) → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) = (1 · ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘))) |
31 | | 1zzd 9330 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℤ) |
32 | 1, 2 | gausslemma2dlem0b 15094 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ ℕ) |
33 | 32 | nnzd 9424 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ ℤ) |
34 | 31, 33 | fzfigd 10488 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝐻) ∈ Fin) |
35 | 34 | adantl 277 |
. . . . . . . . 9
⊢ ((𝑀 = 0 ∧ 𝜑) → (1...𝐻) ∈ Fin) |
36 | | oveq1 5913 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑘 → (𝑥 · 2) = (𝑘 · 2)) |
37 | 36 | breq1d 4035 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑘 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑘 · 2) < (𝑃 / 2))) |
38 | 36 | oveq2d 5922 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑘 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑘 · 2))) |
39 | 37, 36, 38 | ifbieq12d 3579 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
40 | | simpr 110 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑘 ∈ (1...𝐻)) |
41 | 40 | elfzelzd 10078 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑘 ∈ ℤ) |
42 | | 2z 9331 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
43 | 42 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 2 ∈ ℤ) |
44 | 41, 43 | zmulcld 9431 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑘 · 2) ∈ ℤ) |
45 | 1 | eldifad 3160 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈ ℙ) |
46 | | prmz 12223 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
47 | 45, 46 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℤ) |
48 | 47 | adantr 276 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑃 ∈ ℤ) |
49 | 48, 44 | zsubcld 9430 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑃 − (𝑘 · 2)) ∈
ℤ) |
50 | | zq 9677 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 · 2) ∈ ℤ
→ (𝑘 · 2)
∈ ℚ) |
51 | 44, 50 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑘 · 2) ∈ ℚ) |
52 | | 2nn 9129 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℕ |
53 | | znq 9675 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℤ ∧ 2 ∈
ℕ) → (𝑃 / 2)
∈ ℚ) |
54 | 47, 52, 53 | sylancl 413 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 / 2) ∈ ℚ) |
55 | 54 | adantr 276 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℚ) |
56 | | qdclt 10301 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 · 2) ∈ ℚ
∧ (𝑃 / 2) ∈
ℚ) → DECID (𝑘 · 2) < (𝑃 / 2)) |
57 | 51, 55, 56 | syl2anc 411 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → DECID (𝑘 · 2) < (𝑃 / 2)) |
58 | 44, 49, 57 | ifcldcd 3589 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))) ∈
ℤ) |
59 | 3, 39, 40, 58 | fvmptd3 5639 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
60 | 59, 58 | eqeltrd 2266 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℤ) |
61 | 60 | zcnd 9426 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℂ) |
62 | 61 | adantll 476 |
. . . . . . . . 9
⊢ (((𝑀 = 0 ∧ 𝜑) ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℂ) |
63 | 35, 62 | fprodcl 11724 |
. . . . . . . 8
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) ∈ ℂ) |
64 | 63 | mullidd 8023 |
. . . . . . 7
⊢ ((𝑀 = 0 ∧ 𝜑) → (1 · ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) |
65 | 30, 64 | eqtr2d 2223 |
. . . . . 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 15096 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
70 | 69 | nn0red 9280 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
71 | 70 | ltp1d 8935 |
. . . . . . 7
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
72 | | fzdisj 10104 |
. . . . . . 7
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
73 | 71, 72 | syl 14 |
. . . . . 6
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
74 | 73 | adantl 277 |
. . . . 5
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
75 | | eluzelz 9587 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(ℤ≥‘5) → 𝑃 ∈ ℤ) |
76 | | znq 9675 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℤ ∧ 4 ∈
ℕ) → (𝑃 / 4)
∈ ℚ) |
77 | 75, 12, 76 | sylancl 413 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘5) → (𝑃 / 4) ∈ ℚ) |
78 | 77 | flqcld 10332 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘5) → (⌊‘(𝑃 / 4)) ∈ ℤ) |
79 | | nnrp 9715 |
. . . . . . . . . . . . . . . 16
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
80 | 12, 79 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℝ+ |
81 | | eluzelre 9588 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(ℤ≥‘5) → 𝑃 ∈ ℝ) |
82 | | eluz2 9584 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈
(ℤ≥‘5) ↔ (5 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 5 ≤
𝑃)) |
83 | | 4lt5 9143 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 <
5 |
84 | | 4re 9045 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ∈
ℝ |
85 | | 5re 9047 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 5 ∈
ℝ |
86 | 85 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → 5 ∈ ℝ) |
87 | | zre 9307 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℤ → 𝑃 ∈
ℝ) |
88 | 87 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → 𝑃
∈ ℝ) |
89 | | ltleletr 8087 |
. . . . . . . . . . . . . . . . . . 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 9775 |
. . . . . . . . . . . . . . 15
⊢ ((4
∈ ℝ+ ∧ 𝑃 ∈ ℝ ∧ 4 ≤ 𝑃) → 1 ≤ (𝑃 / 4)) |
95 | 80, 81, 93, 94 | mp3an2i 1353 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘5) → 1 ≤ (𝑃 / 4)) |
96 | | 1zzd 9330 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(ℤ≥‘5) → 1 ∈ ℤ) |
97 | | flqge 10337 |
. . . . . . . . . . . . . . 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 9326 |
. . . . . . . . . . . . 13
⊢
((⌊‘(𝑃 /
4)) ∈ ℕ ↔ ((⌊‘(𝑃 / 4)) ∈ ℤ ∧ 1 ≤
(⌊‘(𝑃 /
4)))) |
101 | 78, 99, 100 | sylanbrc 417 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈
(ℤ≥‘5) → (⌊‘(𝑃 / 4)) ∈ ℕ) |
102 | 101 | adantl 277 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → (⌊‘(𝑃 / 4)) ∈ ℕ) |
103 | | oddprm 12371 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
104 | 103 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → ((𝑃 − 1) / 2) ∈
ℕ) |
105 | | eldifi 3277 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
106 | | prmuz2 12243 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
107 | 105, 106 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
(ℤ≥‘2)) |
108 | 107 | adantr 276 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → 𝑃 ∈
(ℤ≥‘2)) |
109 | | fldiv4lem1div2uz2 10361 |
. . . . . . . . . . . 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 5917 |
. . . . . . . . 9
⊢
(1...𝐻) =
(1...((𝑃 − 1) /
2)) |
116 | 5, 115 | eleq12i 2257 |
. . . . . . . 8
⊢ (𝑀 ∈ (1...𝐻) ↔ (⌊‘(𝑃 / 4)) ∈ (1...((𝑃 − 1) / 2))) |
117 | | elfz1b 10142 |
. . . . . . . 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 10103 |
. . . . . 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 11714 |
. . . 4
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
125 | 124 | ancoms 268 |
. . 3
⊢ ((𝜑 ∧ 𝑃 ∈ (ℤ≥‘5))
→ ∏𝑘 ∈
(1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
126 | | 2re 9038 |
. . . . . . 7
⊢ 2 ∈
ℝ |
127 | 126 | a1i 9 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℝ) |
128 | | oddprmgt2 12246 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 2 < 𝑃) |
129 | 1, 128 | syl 14 |
. . . . . 6
⊢ (𝜑 → 2 < 𝑃) |
130 | 127, 129 | gtned 8118 |
. . . . 5
⊢ (𝜑 → 𝑃 ≠ 2) |
131 | 130 | neneqd 2381 |
. . . 4
⊢ (𝜑 → ¬ 𝑃 = 2) |
132 | | prm23ge5 12376 |
. . . . . . 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 2222 |
1
⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |