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 25091 |
. 2
⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) |
5 | | eldif 3584 |
. . . 4
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ ¬ 𝑃 ∈
{2})) |
6 | | prm23ge5 15520 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈
(ℤ≥‘5))) |
7 | | eleq1 2689 |
. . . . . . . . 9
⊢ (𝑃 = 2 → (𝑃 ∈ {2} ↔ 2 ∈
{2})) |
8 | 7 | notbid 308 |
. . . . . . . 8
⊢ (𝑃 = 2 → (¬ 𝑃 ∈ {2} ↔ ¬ 2
∈ {2})) |
9 | | 2ex 11092 |
. . . . . . . . . . . 12
⊢ 2 ∈
V |
10 | 9 | snid 4208 |
. . . . . . . . . . 11
⊢ 2 ∈
{2} |
11 | 10 | 2a1i 12 |
. . . . . . . . . 10
⊢ (𝑃 = 2 → (∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) ≠ (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) → 2 ∈ {2})) |
12 | 11 | necon1bd 2812 |
. . . . . . . . 9
⊢ (𝑃 = 2 → (¬ 2 ∈ {2}
→ ∏𝑘 ∈
(1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
13 | 12 | a1dd 50 |
. . . . . . . 8
⊢ (𝑃 = 2 → (¬ 2 ∈ {2}
→ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))))) |
14 | 8, 13 | sylbid 230 |
. . . . . . 7
⊢ (𝑃 = 2 → (¬ 𝑃 ∈ {2} → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))))) |
15 | | gausslemma2d.m |
. . . . . . . . . 10
⊢ 𝑀 = (⌊‘(𝑃 / 4)) |
16 | | 3lt4 11197 |
. . . . . . . . . . . 12
⊢ 3 <
4 |
17 | | breq1 4656 |
. . . . . . . . . . . 12
⊢ (𝑃 = 3 → (𝑃 < 4 ↔ 3 < 4)) |
18 | 16, 17 | mpbiri 248 |
. . . . . . . . . . 11
⊢ (𝑃 = 3 → 𝑃 < 4) |
19 | | 3nn0 11310 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℕ0 |
20 | | eleq1 2689 |
. . . . . . . . . . . . 13
⊢ (𝑃 = 3 → (𝑃 ∈ ℕ0 ↔ 3 ∈
ℕ0)) |
21 | 19, 20 | mpbiri 248 |
. . . . . . . . . . . 12
⊢ (𝑃 = 3 → 𝑃 ∈
ℕ0) |
22 | | 4nn 11187 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℕ |
23 | | divfl0 12625 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ0
∧ 4 ∈ ℕ) → (𝑃 < 4 ↔ (⌊‘(𝑃 / 4)) = 0)) |
24 | 21, 22, 23 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝑃 = 3 → (𝑃 < 4 ↔ (⌊‘(𝑃 / 4)) = 0)) |
25 | 18, 24 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝑃 = 3 →
(⌊‘(𝑃 / 4)) =
0) |
26 | 15, 25 | syl5eq 2668 |
. . . . . . . . 9
⊢ (𝑃 = 3 → 𝑀 = 0) |
27 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 = 0 → (1...𝑀) = (1...0)) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 = 0 ∧ 𝜑) → (1...𝑀) = (1...0)) |
29 | | fz10 12362 |
. . . . . . . . . . . . . . 15
⊢ (1...0) =
∅ |
30 | 28, 29 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 = 0 ∧ 𝜑) → (1...𝑀) = ∅) |
31 | 30 | prodeq1d 14651 |
. . . . . . . . . . . . 13
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = ∏𝑘 ∈ ∅ (𝑅‘𝑘)) |
32 | | prod0 14673 |
. . . . . . . . . . . . 13
⊢
∏𝑘 ∈
∅ (𝑅‘𝑘) = 1 |
33 | 31, 32 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = 1) |
34 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 = 0 → (𝑀 + 1) = (0 + 1)) |
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 = 0 ∧ 𝜑) → (𝑀 + 1) = (0 + 1)) |
36 | | 0p1e1 11132 |
. . . . . . . . . . . . . . 15
⊢ (0 + 1) =
1 |
37 | 35, 36 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 = 0 ∧ 𝜑) → (𝑀 + 1) = 1) |
38 | 37 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((𝑀 = 0 ∧ 𝜑) → ((𝑀 + 1)...𝐻) = (1...𝐻)) |
39 | 38 | prodeq1d 14651 |
. . . . . . . . . . . 12
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) |
40 | 33, 39 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ ((𝑀 = 0 ∧ 𝜑) → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) = (1 · ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘))) |
41 | | fzfid 12772 |
. . . . . . . . . . . . 13
⊢ ((𝑀 = 0 ∧ 𝜑) → (1...𝐻) ∈ Fin) |
42 | 3 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))) |
43 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑘 → (𝑥 · 2) = (𝑘 · 2)) |
44 | 43 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑘 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑘 · 2) < (𝑃 / 2))) |
45 | 43 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑘 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑘 · 2))) |
46 | 44, 43, 45 | ifbieq12d 4113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑘 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
48 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑘 ∈ (1...𝐻)) |
49 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...𝐻) → 𝑘 ∈ ℤ) |
50 | 49 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...𝐻) → 𝑘 ∈ ℂ) |
51 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...𝐻) → 2 ∈ ℂ) |
52 | 50, 51 | mulcld 10060 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1...𝐻) → (𝑘 · 2) ∈ ℂ) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑘 · 2) ∈ ℂ) |
54 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
55 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
56 | 55 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
57 | 1, 54, 56 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑃 ∈ ℂ) |
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑃 ∈ ℂ) |
59 | 58, 53 | subcld 10392 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑃 − (𝑘 · 2)) ∈
ℂ) |
60 | 53, 59 | ifcld 4131 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))) ∈
ℂ) |
61 | 42, 47, 48, 60 | fvmptd 6288 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
62 | 61, 60 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℂ) |
63 | 62 | adantll 750 |
. . . . . . . . . . . . 13
⊢ (((𝑀 = 0 ∧ 𝜑) ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℂ) |
64 | 41, 63 | fprodcl 14682 |
. . . . . . . . . . . 12
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) ∈ ℂ) |
65 | 64 | mulid2d 10058 |
. . . . . . . . . . 11
⊢ ((𝑀 = 0 ∧ 𝜑) → (1 · ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) = ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘)) |
66 | 40, 65 | eqtr2d 2657 |
. . . . . . . . . 10
⊢ ((𝑀 = 0 ∧ 𝜑) → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
67 | 66 | ex 450 |
. . . . . . . . 9
⊢ (𝑀 = 0 → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
68 | 26, 67 | syl 17 |
. . . . . . . 8
⊢ (𝑃 = 3 → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
69 | 68 | a1d 25 |
. . . . . . 7
⊢ (𝑃 = 3 → (¬ 𝑃 ∈ {2} → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))))) |
70 | 1, 15 | gausslemma2dlem0d 25084 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
71 | 70 | nn0red 11352 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℝ) |
72 | 71 | ltp1d 10954 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
73 | | fzdisj 12368 |
. . . . . . . . . . . 12
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
75 | 74 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
76 | | eluzelre 11698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈
(ℤ≥‘5) → 𝑃 ∈ ℝ) |
77 | | 4re 11097 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 4 ∈
ℝ |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈
(ℤ≥‘5) → 4 ∈ ℝ) |
79 | | 4ne0 11117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 4 ≠
0 |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈
(ℤ≥‘5) → 4 ≠ 0) |
81 | 76, 78, 80 | redivcld 10853 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈
(ℤ≥‘5) → (𝑃 / 4) ∈ ℝ) |
82 | 81 | flcld 12599 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈
(ℤ≥‘5) → (⌊‘(𝑃 / 4)) ∈ ℤ) |
83 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
84 | 22, 83 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 4 ∈
ℝ+ |
85 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈
(ℤ≥‘5) ↔ (5 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 5 ≤
𝑃)) |
86 | | 4lt5 11200 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 4 <
5 |
87 | | 5re 11099 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 5 ∈
ℝ |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → 5 ∈ ℝ) |
89 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℤ → 𝑃 ∈
ℝ) |
90 | 89 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → 𝑃
∈ ℝ) |
91 | | ltleletr 10130 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((4
∈ ℝ ∧ 5 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((4 < 5 ∧ 5
≤ 𝑃) → 4 ≤ 𝑃)) |
92 | 77, 88, 90, 91 | mp3an2i 1429 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → ((4 < 5 ∧ 5 ≤ 𝑃) → 4 ≤ 𝑃)) |
93 | 86, 92 | mpani 712 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ) → (5 ≤ 𝑃 → 4 ≤ 𝑃)) |
94 | 93 | 3impia 1261 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((5
∈ ℤ ∧ 𝑃
∈ ℤ ∧ 5 ≤ 𝑃) → 4 ≤ 𝑃) |
95 | 85, 94 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈
(ℤ≥‘5) → 4 ≤ 𝑃) |
96 | | divge1 11898 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((4
∈ ℝ+ ∧ 𝑃 ∈ ℝ ∧ 4 ≤ 𝑃) → 1 ≤ (𝑃 / 4)) |
97 | 84, 76, 95, 96 | mp3an2i 1429 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈
(ℤ≥‘5) → 1 ≤ (𝑃 / 4)) |
98 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈
(ℤ≥‘5) → 1 ∈ ℤ) |
99 | | flge 12606 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 / 4) ∈ ℝ ∧ 1
∈ ℤ) → (1 ≤ (𝑃 / 4) ↔ 1 ≤ (⌊‘(𝑃 / 4)))) |
100 | 81, 98, 99 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈
(ℤ≥‘5) → (1 ≤ (𝑃 / 4) ↔ 1 ≤ (⌊‘(𝑃 / 4)))) |
101 | 97, 100 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈
(ℤ≥‘5) → 1 ≤ (⌊‘(𝑃 / 4))) |
102 | | elnnz1 11403 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘(𝑃 /
4)) ∈ ℕ ↔ ((⌊‘(𝑃 / 4)) ∈ ℤ ∧ 1 ≤
(⌊‘(𝑃 /
4)))) |
103 | 82, 101, 102 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈
(ℤ≥‘5) → (⌊‘(𝑃 / 4)) ∈ ℕ) |
104 | 103 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → (⌊‘(𝑃 / 4)) ∈ ℕ) |
105 | | oddprm 15515 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
106 | 105 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → ((𝑃 − 1) / 2) ∈
ℕ) |
107 | | prmuz2 15408 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
108 | 54, 107 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
(ℤ≥‘2)) |
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → 𝑃 ∈
(ℤ≥‘2)) |
110 | | fldiv4lem1div2uz2 12637 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈
(ℤ≥‘2) → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2)) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2)) |
112 | 104, 106,
111 | 3jca 1242 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∈
(ℤ≥‘5)) → ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2))) |
113 | 112 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈
(ℤ≥‘5) → ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2)))) |
114 | 1, 113 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 ∈ (ℤ≥‘5)
→ ((⌊‘(𝑃 /
4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧
(⌊‘(𝑃 / 4))
≤ ((𝑃 − 1) /
2)))) |
115 | 114 | impcom 446 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2))) |
116 | 2 | oveq2i 6661 |
. . . . . . . . . . . . . 14
⊢
(1...𝐻) =
(1...((𝑃 − 1) /
2)) |
117 | 15, 116 | eleq12i 2694 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (1...𝐻) ↔ (⌊‘(𝑃 / 4)) ∈ (1...((𝑃 − 1) / 2))) |
118 | | elfz1b 12409 |
. . . . . . . . . . . . 13
⊢
((⌊‘(𝑃 /
4)) ∈ (1...((𝑃 −
1) / 2)) ↔ ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2))) |
119 | 117, 118 | bitri 264 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ (1...𝐻) ↔ ((⌊‘(𝑃 / 4)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (⌊‘(𝑃 /
4)) ≤ ((𝑃 − 1) /
2))) |
120 | 115, 119 | sylibr 224 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → 𝑀 ∈ (1...𝐻)) |
121 | | fzsplit 12367 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (1...𝐻) → (1...𝐻) = ((1...𝑀) ∪ ((𝑀 + 1)...𝐻))) |
122 | 120, 121 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → (1...𝐻) = ((1...𝑀) ∪ ((𝑀 + 1)...𝐻))) |
123 | | fzfid 12772 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → (1...𝐻) ∈ Fin) |
124 | 62 | adantll 750 |
. . . . . . . . . 10
⊢ (((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) ∧ 𝑘 ∈ (1...𝐻)) → (𝑅‘𝑘) ∈ ℂ) |
125 | 75, 122, 123, 124 | fprodsplit 14696 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘5) ∧ 𝜑) → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
126 | 125 | ex 450 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘5) → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
127 | 126 | a1d 25 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘5) → (¬ 𝑃 ∈ {2} → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))))) |
128 | 14, 69, 127 | 3jaoi 1391 |
. . . . . 6
⊢ ((𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈ (ℤ≥‘5))
→ (¬ 𝑃 ∈ {2}
→ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))))) |
129 | 6, 128 | syl 17 |
. . . . 5
⊢ (𝑃 ∈ ℙ → (¬
𝑃 ∈ {2} → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))))) |
130 | 129 | imp 445 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ ¬
𝑃 ∈ {2}) → (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
131 | 5, 130 | sylbi 207 |
. . 3
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)))) |
132 | 1, 131 | mpcom 38 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑅‘𝑘) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
133 | 4, 132 | eqtrd 2656 |
1
⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |