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 26514 |
. 2
⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) |
5 | | eldif 3897 |
. . . 4
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ ¬ 𝑃 ∈
{2})) |
6 | | prm23ge5 16516 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈
(ℤ≥‘5))) |
7 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑃 = 2 → (𝑃 ∈ {2} ↔ 2 ∈
{2})) |
8 | 7 | notbid 318 |
. . . . . . . 8
⊢ (𝑃 = 2 → (¬ 𝑃 ∈ {2} ↔ ¬ 2
∈ {2})) |
9 | | 2ex 12050 |
. . . . . . . . . . . 12
⊢ 2 ∈
V |
10 | 9 | snid 4597 |
. . . . . . . . . . 11
⊢ 2 ∈
{2} |
11 | 10 | 2a1i 12 |
. . . . . . . . . 10
⊢ (𝑃 = 2 → (∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) ≠ (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) → 2 ∈ {2})) |
12 | 11 | necon1bd 2961 |
. . . . . . . . 9
⊢ (𝑃 = 2 → (¬ 2 ∈ {2}
→ ∏𝑘 ∈
(1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
13 | 12 | a1dd 50 |
. . . . . . . 8
⊢ (𝑃 = 2 → (¬ 2 ∈ {2}
→ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))))) |
14 | 8, 13 | sylbid 239 |
. . . . . . 7
⊢ (𝑃 = 2 → (¬ 𝑃 ∈ {2} → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))))) |
15 | | gausslemma2d.m |
. . . . . . . . . 10
⊢ 𝑀 = (⌊‘(𝑃 / 4)) |
16 | | 3lt4 12147 |
. . . . . . . . . . . 12
⊢ 3 <
4 |
17 | | breq1 5077 |
. . . . . . . . . . . 12
⊢ (𝑃 = 3 → (𝑃 < 4 ↔ 3 < 4)) |
18 | 16, 17 | mpbiri 257 |
. . . . . . . . . . 11
⊢ (𝑃 = 3 → 𝑃 < 4) |
19 | | 3nn0 12251 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℕ0 |
20 | | eleq1 2826 |
. . . . . . . . . . . . 13
⊢ (𝑃 = 3 → (𝑃 ∈ ℕ0 ↔ 3 ∈
ℕ0)) |
21 | 19, 20 | mpbiri 257 |
. . . . . . . . . . . 12
⊢ (𝑃 = 3 → 𝑃 ∈
ℕ0) |
22 | | 4nn 12056 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℕ |
23 | | divfl0 13544 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ0
∧ 4 ∈ ℕ) → (𝑃 < 4 ↔ (⌊‘(𝑃 / 4)) = 0)) |
24 | 21, 22, 23 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝑃 = 3 → (𝑃 < 4 ↔ (⌊‘(𝑃 / 4)) = 0)) |
25 | 18, 24 | mpbid 231 |
. . . . . . . . . 10
⊢ (𝑃 = 3 →
(⌊‘(𝑃 / 4)) =
0) |
26 | 15, 25 | eqtrid 2790 |
. . . . . . . . 9
⊢ (𝑃 = 3 → 𝑀 = 0) |
27 | | oveq2 7283 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 = 0 → (1...𝑀) = (1...0)) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 = 0 ∧ 𝜑) → (1...𝑀) = (1...0)) |
29 | | fz10 13277 |
. . . . . . . . . . . . . . 15
⊢ (1...0) =
∅ |
30 | 28, 29 | eqtrdi 2794 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 = 0 ∧ 𝜑) → (1...𝑀) = ∅) |
31 | 30 | prodeq1d 15631 |
. . . . . . . . . . . . 13
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = ∏𝑘 ∈ ∅ (𝑅‘𝑘)) |
32 | | prod0 15653 |
. . . . . . . . . . . . 13
⊢
∏𝑘 ∈
∅ (𝑅‘𝑘) = 1 |
33 | 31, 32 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = 1) |
34 | | oveq1 7282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 = 0 → (𝑀 + 1) = (0 + 1)) |
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 = 0 ∧ 𝜑) → (𝑀 + 1) = (0 + 1)) |
36 | | 0p1e1 12095 |
. . . . . . . . . . . . . . 15
⊢ (0 + 1) =
1 |
37 | 35, 36 | eqtrdi 2794 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 = 0 ∧ 𝜑) → (𝑀 + 1) = 1) |
38 | 37 | oveq1d 7290 |
. . . . . . . . . . . . 13
⊢ ((𝑀 = 0 ∧ 𝜑) → ((𝑀 + 1)...𝐻) = (1...𝐻)) |
39 | 38 | prodeq1d 15631 |
. . . . . . . . . . . 12
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) |
40 | 33, 39 | oveq12d 7293 |
. . . . . . . . . . 11
⊢ ((𝑀 = 0 ∧ 𝜑) → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) = (1 · ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘))) |
41 | | fzfid 13693 |
. . . . . . . . . . . . 13
⊢ ((𝑀 = 0 ∧ 𝜑) → (1...𝐻) ∈ Fin) |
42 | | oveq1 7282 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑘 → (𝑥 · 2) = (𝑘 · 2)) |
43 | 42 | breq1d 5084 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑘 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑘 · 2) < (𝑃 / 2))) |
44 | 42 | oveq2d 7291 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑘 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑘 · 2))) |
45 | 43, 42, 44 | ifbieq12d 4487 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑘 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
46 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑘 ∈ (1...𝐻)) |
47 | | elfzelz 13256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...𝐻) → 𝑘 ∈ ℤ) |
48 | 47 | zcnd 12427 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...𝐻) → 𝑘 ∈ ℂ) |
49 | | 2cnd 12051 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...𝐻) → 2 ∈ ℂ) |
50 | 48, 49 | mulcld 10995 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1...𝐻) → (𝑘 · 2) ∈ ℂ) |
51 | 50 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑘 · 2) ∈ ℂ) |
52 | | eldifi 4061 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
53 | | prmz 16380 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
54 | 53 | zcnd 12427 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
55 | 1, 52, 54 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑃 ∈ ℂ) |
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑃 ∈ ℂ) |
57 | 56, 51 | subcld 11332 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑃 − (𝑘 · 2)) ∈
ℂ) |
58 | 51, 57 | ifcld 4505 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))) ∈
ℂ) |
59 | 3, 45, 46, 58 | fvmptd3 6898 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
60 | 59, 58 | eqeltrd 2839 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℂ) |
61 | 60 | adantll 711 |
. . . . . . . . . . . . 13
⊢ (((𝑀 = 0 ∧ 𝜑) ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℂ) |
62 | 41, 61 | fprodcl 15662 |
. . . . . . . . . . . 12
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) ∈ ℂ) |
63 | 62 | mulid2d 10993 |
. . . . . . . . . . 11
⊢ ((𝑀 = 0 ∧ 𝜑) → (1 · ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) |
64 | 40, 63 | eqtr2d 2779 |
. . . . . . . . . 10
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
65 | 64 | ex 413 |
. . . . . . . . 9
⊢ (𝑀 = 0 → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
66 | 26, 65 | syl 17 |
. . . . . . . 8
⊢ (𝑃 = 3 → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
67 | 66 | a1d 25 |
. . . . . . 7
⊢ (𝑃 = 3 → (¬ 𝑃 ∈ {2} → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))))) |
68 | 1, 15 | gausslemma2dlem0d 26507 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
69 | 68 | nn0red 12294 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℝ) |
70 | 69 | ltp1d 11905 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
71 | | fzdisj 13283 |
. . . . . . . . . . . 12
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
73 | 72 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
74 | | eluzelre 12593 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈
(ℤ≥‘5) → 𝑃 ∈ ℝ) |
75 | | 4re 12057 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 4 ∈
ℝ |
76 | 75 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈
(ℤ≥‘5) → 4 ∈ ℝ) |
77 | | 4ne0 12081 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 4 ≠
0 |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈
(ℤ≥‘5) → 4 ≠ 0) |
79 | 74, 76, 78 | redivcld 11803 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈
(ℤ≥‘5) → (𝑃 / 4) ∈ ℝ) |
80 | 79 | flcld 13518 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈
(ℤ≥‘5) → (⌊‘(𝑃 / 4)) ∈ ℤ) |
81 | | nnrp 12741 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
82 | 22, 81 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 4 ∈
ℝ+ |
83 | | eluz2 12588 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈
(ℤ≥‘5) ↔ (5 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 5 ≤
𝑃)) |
84 | | 4lt5 12150 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 4 <
5 |
85 | | 5re 12060 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 5 ∈
ℝ |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → 5 ∈ ℝ) |
87 | | zre 12323 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℤ → 𝑃 ∈
ℝ) |
88 | 87 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → 𝑃
∈ ℝ) |
89 | | ltleletr 11068 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((4
∈ ℝ ∧ 5 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((4 < 5 ∧ 5
≤ 𝑃) → 4 ≤ 𝑃)) |
90 | 75, 86, 88, 89 | mp3an2i 1465 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → ((4 < 5 ∧ 5 ≤ 𝑃) → 4 ≤ 𝑃)) |
91 | 84, 90 | mpani 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → (5 ≤ 𝑃 → 4 ≤ 𝑃)) |
92 | 91 | 3impia 1116 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ ∧ 5 ≤ 𝑃) → 4 ≤ 𝑃) |
93 | 83, 92 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈
(ℤ≥‘5) → 4 ≤ 𝑃) |
94 | | divge1 12798 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((4
∈ ℝ+ ∧ 𝑃 ∈ ℝ ∧ 4 ≤ 𝑃) → 1 ≤ (𝑃 / 4)) |
95 | 82, 74, 93, 94 | mp3an2i 1465 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈
(ℤ≥‘5) → 1 ≤ (𝑃 / 4)) |
96 | | 1zzd 12351 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈
(ℤ≥‘5) → 1 ∈ ℤ) |
97 | | flge 13525 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 / 4) ∈ ℝ ∧ 1
∈ ℤ) → (1 ≤ (𝑃 / 4) ↔ 1 ≤ (⌊‘(𝑃 / 4)))) |
98 | 79, 96, 97 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈
(ℤ≥‘5) → (1 ≤ (𝑃 / 4) ↔ 1 ≤ (⌊‘(𝑃 / 4)))) |
99 | 95, 98 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈
(ℤ≥‘5) → 1 ≤ (⌊‘(𝑃 / 4))) |
100 | | elnnz1 12346 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘(𝑃 /
4)) ∈ ℕ ↔ ((⌊‘(𝑃 / 4)) ∈ ℤ ∧ 1 ≤
(⌊‘(𝑃 /
4)))) |
101 | 80, 99, 100 | sylanbrc 583 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈
(ℤ≥‘5) → (⌊‘(𝑃 / 4)) ∈ ℕ) |
102 | 101 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → (⌊‘(𝑃 / 4)) ∈ ℕ) |
103 | | oddprm 16511 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
104 | 103 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → ((𝑃 − 1) / 2) ∈
ℕ) |
105 | | prmuz2 16401 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
106 | 52, 105 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
(ℤ≥‘2)) |
107 | 106 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → 𝑃 ∈
(ℤ≥‘2)) |
108 | | fldiv4lem1div2uz2 13556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈
(ℤ≥‘2) → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2)) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2)) |
110 | 102, 104,
109 | 3jca 1127 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2))) |
111 | 110 | ex 413 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈
(ℤ≥‘5) → ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2)))) |
112 | 1, 111 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 ∈ (ℤ≥‘5)
→ ((⌊‘(𝑃 /
4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧
(⌊‘(𝑃 / 4))
≤ ((𝑃 − 1) /
2)))) |
113 | 112 | impcom 408 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2))) |
114 | 2 | oveq2i 7286 |
. . . . . . . . . . . . . 14
⊢
(1...𝐻) =
(1...((𝑃 − 1) /
2)) |
115 | 15, 114 | eleq12i 2831 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (1...𝐻) ↔ (⌊‘(𝑃 / 4)) ∈ (1...((𝑃 − 1) / 2))) |
116 | | elfz1b 13325 |
. . . . . . . . . . . . 13
⊢
((⌊‘(𝑃 /
4)) ∈ (1...((𝑃 −
1) / 2)) ↔ ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2))) |
117 | 115, 116 | bitri 274 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ (1...𝐻) ↔ ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2))) |
118 | 113, 117 | sylibr 233 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → 𝑀 ∈ (1...𝐻)) |
119 | | fzsplit 13282 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (1...𝐻) → (1...𝐻) = ((1...𝑀) ∪ ((𝑀 + 1)...𝐻))) |
120 | 118, 119 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → (1...𝐻) = ((1...𝑀) ∪ ((𝑀 + 1)...𝐻))) |
121 | | fzfid 13693 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → (1...𝐻) ∈ Fin) |
122 | 60 | adantll 711 |
. . . . . . . . . 10
⊢ (((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℂ) |
123 | 73, 120, 121, 122 | fprodsplit 15676 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
124 | 123 | ex 413 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘5) → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
125 | 124 | a1d 25 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘5) → (¬ 𝑃 ∈ {2} → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))))) |
126 | 14, 67, 125 | 3jaoi 1426 |
. . . . . 6
⊢ ((𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈ (ℤ≥‘5))
→ (¬ 𝑃 ∈ {2}
→ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))))) |
127 | 6, 126 | syl 17 |
. . . . 5
⊢ (𝑃 ∈ ℙ → (¬
𝑃 ∈ {2} → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))))) |
128 | 127 | imp 407 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 ∈ {2}) → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
129 | 5, 128 | sylbi 216 |
. . 3
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
130 | 1, 129 | mpcom 38 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
131 | 4, 130 | eqtrd 2778 |
1
⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |