Step | Hyp | Ref
| Expression |
1 | | peano2nn0 12273 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
2 | | prmoval 16734 |
. . 3
⊢ ((𝑁 + 1) ∈ ℕ0
→ (#p‘(𝑁 + 1)) = ∏𝑘 ∈ (1...(𝑁 + 1))if(𝑘 ∈ ℙ, 𝑘, 1)) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (#p‘(𝑁 + 1)) = ∏𝑘 ∈ (1...(𝑁 + 1))if(𝑘 ∈ ℙ, 𝑘, 1)) |
4 | | nn0p1nn 12272 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
5 | | elnnuz 12622 |
. . . 4
⊢ ((𝑁 + 1) ∈ ℕ ↔
(𝑁 + 1) ∈
(ℤ≥‘1)) |
6 | 4, 5 | sylib 217 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(ℤ≥‘1)) |
7 | | elfzelz 13256 |
. . . . . 6
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
8 | 7 | zcnd 12427 |
. . . . 5
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℂ) |
9 | 8 | adantl 482 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ∈
ℂ) |
10 | | 1cnd 10970 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...(𝑁 + 1))) → 1 ∈
ℂ) |
11 | 9, 10 | ifcld 4505 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...(𝑁 + 1))) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈
ℂ) |
12 | | eleq1 2826 |
. . . 4
⊢ (𝑘 = (𝑁 + 1) → (𝑘 ∈ ℙ ↔ (𝑁 + 1) ∈ ℙ)) |
13 | | id 22 |
. . . 4
⊢ (𝑘 = (𝑁 + 1) → 𝑘 = (𝑁 + 1)) |
14 | 12, 13 | ifbieq1d 4483 |
. . 3
⊢ (𝑘 = (𝑁 + 1) → if(𝑘 ∈ ℙ, 𝑘, 1) = if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) |
15 | 6, 11, 14 | fprodm1 15677 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ∏𝑘 ∈
(1...(𝑁 + 1))if(𝑘 ∈ ℙ, 𝑘, 1) = (∏𝑘 ∈ (1...((𝑁 + 1) − 1))if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1))) |
16 | | nn0cn 12243 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
17 | | pncan1 11399 |
. . . . . . 7
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
19 | 18 | oveq2d 7291 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (1...((𝑁 + 1)
− 1)) = (1...𝑁)) |
20 | 19 | prodeq1d 15631 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ∏𝑘 ∈
(1...((𝑁 + 1) −
1))if(𝑘 ∈ ℙ,
𝑘, 1) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
21 | 20 | oveq1d 7290 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (∏𝑘 ∈
(1...((𝑁 + 1) −
1))if(𝑘 ∈ ℙ,
𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = (∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1))) |
22 | | prmoval 16734 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
23 | 22 | eqcomd 2744 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) =
(#p‘𝑁)) |
24 | 23 | adantl 482 |
. . . . . 6
⊢ (((𝑁 + 1) ∈ ℙ ∧ 𝑁 ∈ ℕ0)
→ ∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) =
(#p‘𝑁)) |
25 | 24 | oveq1d 7290 |
. . . . 5
⊢ (((𝑁 + 1) ∈ ℙ ∧ 𝑁 ∈ ℕ0)
→ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · (𝑁 + 1)) = ((#p‘𝑁) · (𝑁 + 1))) |
26 | | iftrue 4465 |
. . . . . . . 8
⊢ ((𝑁 + 1) ∈ ℙ →
if((𝑁 + 1) ∈ ℙ,
(𝑁 + 1), 1) = (𝑁 + 1)) |
27 | 26 | oveq2d 7291 |
. . . . . . 7
⊢ ((𝑁 + 1) ∈ ℙ →
(∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = (∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · (𝑁 + 1))) |
28 | | iftrue 4465 |
. . . . . . 7
⊢ ((𝑁 + 1) ∈ ℙ →
if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁)) =
((#p‘𝑁)
· (𝑁 +
1))) |
29 | 27, 28 | eqeq12d 2754 |
. . . . . 6
⊢ ((𝑁 + 1) ∈ ℙ →
((∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))
↔ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · (𝑁 + 1)) = ((#p‘𝑁) · (𝑁 + 1)))) |
30 | 29 | adantr 481 |
. . . . 5
⊢ (((𝑁 + 1) ∈ ℙ ∧ 𝑁 ∈ ℕ0)
→ ((∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))
↔ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · (𝑁 + 1)) = ((#p‘𝑁) · (𝑁 + 1)))) |
31 | 25, 30 | mpbird 256 |
. . . 4
⊢ (((𝑁 + 1) ∈ ℙ ∧ 𝑁 ∈ ℕ0)
→ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))) |
32 | | fzfid 13693 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ∈
Fin) |
33 | | elfznn 13285 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ) |
34 | | 1nn 11984 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ |
35 | 34 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℕ) |
36 | 33, 35 | ifcld 4505 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑁) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
37 | 36 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
38 | 32, 37 | fprodnncl 15665 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) ∈
ℕ) |
39 | 38 | nncnd 11989 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) ∈
ℂ) |
40 | 39 | adantl 482 |
. . . . . . 7
⊢ ((¬
(𝑁 + 1) ∈ ℙ
∧ 𝑁 ∈
ℕ0) → ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℂ) |
41 | 40 | mulid1d 10992 |
. . . . . 6
⊢ ((¬
(𝑁 + 1) ∈ ℙ
∧ 𝑁 ∈
ℕ0) → (∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · 1) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
42 | 22 | adantl 482 |
. . . . . 6
⊢ ((¬
(𝑁 + 1) ∈ ℙ
∧ 𝑁 ∈
ℕ0) → (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
43 | 41, 42 | eqtr4d 2781 |
. . . . 5
⊢ ((¬
(𝑁 + 1) ∈ ℙ
∧ 𝑁 ∈
ℕ0) → (∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · 1) = (#p‘𝑁)) |
44 | | iffalse 4468 |
. . . . . . . 8
⊢ (¬
(𝑁 + 1) ∈ ℙ
→ if((𝑁 + 1) ∈
ℙ, (𝑁 + 1), 1) =
1) |
45 | 44 | oveq2d 7291 |
. . . . . . 7
⊢ (¬
(𝑁 + 1) ∈ ℙ
→ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = (∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · 1)) |
46 | | iffalse 4468 |
. . . . . . 7
⊢ (¬
(𝑁 + 1) ∈ ℙ
→ if((𝑁 + 1) ∈
ℙ, ((#p‘𝑁) · (𝑁 + 1)), (#p‘𝑁)) = (#p‘𝑁)) |
47 | 45, 46 | eqeq12d 2754 |
. . . . . 6
⊢ (¬
(𝑁 + 1) ∈ ℙ
→ ((∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))
↔ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · 1) =
(#p‘𝑁))) |
48 | 47 | adantr 481 |
. . . . 5
⊢ ((¬
(𝑁 + 1) ∈ ℙ
∧ 𝑁 ∈
ℕ0) → ((∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))
↔ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · 1) =
(#p‘𝑁))) |
49 | 43, 48 | mpbird 256 |
. . . 4
⊢ ((¬
(𝑁 + 1) ∈ ℙ
∧ 𝑁 ∈
ℕ0) → (∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))) |
50 | 31, 49 | pm2.61ian 809 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))) |
51 | 21, 50 | eqtrd 2778 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (∏𝑘 ∈
(1...((𝑁 + 1) −
1))if(𝑘 ∈ ℙ,
𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))) |
52 | 3, 15, 51 | 3eqtrd 2782 |
1
⊢ (𝑁 ∈ ℕ0
→ (#p‘(𝑁 + 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))) |