Step | Hyp | Ref
| Expression |
1 | | peano2nn0 12016 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
2 | | prmoval 16469 |
. . 3
⊢ ((𝑁 + 1) ∈ ℕ0
→ (#p‘(𝑁 + 1)) = ∏𝑘 ∈ (1...(𝑁 + 1))if(𝑘 ∈ ℙ, 𝑘, 1)) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (#p‘(𝑁 + 1)) = ∏𝑘 ∈ (1...(𝑁 + 1))if(𝑘 ∈ ℙ, 𝑘, 1)) |
4 | | nn0p1nn 12015 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
5 | | elnnuz 12364 |
. . . 4
⊢ ((𝑁 + 1) ∈ ℕ ↔
(𝑁 + 1) ∈
(ℤ≥‘1)) |
6 | 4, 5 | sylib 221 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(ℤ≥‘1)) |
7 | | elfzelz 12998 |
. . . . . 6
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
8 | 7 | zcnd 12169 |
. . . . 5
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℂ) |
9 | 8 | adantl 485 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ∈
ℂ) |
10 | | 1cnd 10714 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...(𝑁 + 1))) → 1 ∈
ℂ) |
11 | 9, 10 | ifcld 4460 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...(𝑁 + 1))) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈
ℂ) |
12 | | eleq1 2820 |
. . . 4
⊢ (𝑘 = (𝑁 + 1) → (𝑘 ∈ ℙ ↔ (𝑁 + 1) ∈ ℙ)) |
13 | | id 22 |
. . . 4
⊢ (𝑘 = (𝑁 + 1) → 𝑘 = (𝑁 + 1)) |
14 | 12, 13 | ifbieq1d 4438 |
. . 3
⊢ (𝑘 = (𝑁 + 1) → if(𝑘 ∈ ℙ, 𝑘, 1) = if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) |
15 | 6, 11, 14 | fprodm1 15413 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ∏𝑘 ∈
(1...(𝑁 + 1))if(𝑘 ∈ ℙ, 𝑘, 1) = (∏𝑘 ∈ (1...((𝑁 + 1) − 1))if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1))) |
16 | | nn0cn 11986 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
17 | | pncan1 11142 |
. . . . . . 7
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
19 | 18 | oveq2d 7186 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (1...((𝑁 + 1)
− 1)) = (1...𝑁)) |
20 | 19 | prodeq1d 15367 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ∏𝑘 ∈
(1...((𝑁 + 1) −
1))if(𝑘 ∈ ℙ,
𝑘, 1) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
21 | 20 | oveq1d 7185 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (∏𝑘 ∈
(1...((𝑁 + 1) −
1))if(𝑘 ∈ ℙ,
𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = (∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1))) |
22 | | prmoval 16469 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
23 | 22 | eqcomd 2744 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) =
(#p‘𝑁)) |
24 | 23 | adantl 485 |
. . . . . 6
⊢ (((𝑁 + 1) ∈ ℙ ∧ 𝑁 ∈ ℕ0)
→ ∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) =
(#p‘𝑁)) |
25 | 24 | oveq1d 7185 |
. . . . 5
⊢ (((𝑁 + 1) ∈ ℙ ∧ 𝑁 ∈ ℕ0)
→ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · (𝑁 + 1)) = ((#p‘𝑁) · (𝑁 + 1))) |
26 | | iftrue 4420 |
. . . . . . . 8
⊢ ((𝑁 + 1) ∈ ℙ →
if((𝑁 + 1) ∈ ℙ,
(𝑁 + 1), 1) = (𝑁 + 1)) |
27 | 26 | oveq2d 7186 |
. . . . . . 7
⊢ ((𝑁 + 1) ∈ ℙ →
(∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = (∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · (𝑁 + 1))) |
28 | | iftrue 4420 |
. . . . . . 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 484 |
. . . . 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 260 |
. . . 4
⊢ (((𝑁 + 1) ∈ ℙ ∧ 𝑁 ∈ ℕ0)
→ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))) |
32 | | fzfid 13432 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ∈
Fin) |
33 | | elfznn 13027 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ) |
34 | | 1nn 11727 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ |
35 | 34 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℕ) |
36 | 33, 35 | ifcld 4460 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑁) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
37 | 36 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
38 | 32, 37 | fprodnncl 15401 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) ∈
ℕ) |
39 | 38 | nncnd 11732 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) ∈
ℂ) |
40 | 39 | adantl 485 |
. . . . . . 7
⊢ ((¬
(𝑁 + 1) ∈ ℙ
∧ 𝑁 ∈
ℕ0) → ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℂ) |
41 | 40 | mulid1d 10736 |
. . . . . 6
⊢ ((¬
(𝑁 + 1) ∈ ℙ
∧ 𝑁 ∈
ℕ0) → (∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · 1) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
42 | 22 | adantl 485 |
. . . . . 6
⊢ ((¬
(𝑁 + 1) ∈ ℙ
∧ 𝑁 ∈
ℕ0) → (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
43 | 41, 42 | eqtr4d 2776 |
. . . . 5
⊢ ((¬
(𝑁 + 1) ∈ ℙ
∧ 𝑁 ∈
ℕ0) → (∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · 1) = (#p‘𝑁)) |
44 | | iffalse 4423 |
. . . . . . . 8
⊢ (¬
(𝑁 + 1) ∈ ℙ
→ if((𝑁 + 1) ∈
ℙ, (𝑁 + 1), 1) =
1) |
45 | 44 | oveq2d 7186 |
. . . . . . 7
⊢ (¬
(𝑁 + 1) ∈ ℙ
→ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = (∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · 1)) |
46 | | iffalse 4423 |
. . . . . . 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 484 |
. . . . 5
⊢ ((¬
(𝑁 + 1) ∈ ℙ
∧ 𝑁 ∈
ℕ0) → ((∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))
↔ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · 1) =
(#p‘𝑁))) |
49 | 43, 48 | mpbird 260 |
. . . 4
⊢ ((¬
(𝑁 + 1) ∈ ℙ
∧ 𝑁 ∈
ℕ0) → (∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))) |
50 | 31, 49 | pm2.61ian 812 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))) |
51 | 21, 50 | eqtrd 2773 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (∏𝑘 ∈
(1...((𝑁 + 1) −
1))if(𝑘 ∈ ℙ,
𝑘, 1) · if((𝑁 + 1) ∈ ℙ, (𝑁 + 1), 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))) |
52 | 3, 15, 51 | 3eqtrd 2777 |
1
⊢ (𝑁 ∈ ℕ0
→ (#p‘(𝑁 + 1)) = if((𝑁 + 1) ∈ ℙ,
((#p‘𝑁)
· (𝑁 + 1)),
(#p‘𝑁))) |