Step | Hyp | Ref
| Expression |
1 | | prmoval 15737 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) |
2 | | eqidd 2623 |
. . . . . 6
⊢ (𝑘 ∈ (1...𝑁) → (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1)) = (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))) |
3 | | simpr 477 |
. . . . . . . 8
⊢ ((𝑘 ∈ (1...𝑁) ∧ 𝑚 = 𝑘) → 𝑚 = 𝑘) |
4 | 3 | eleq1d 2686 |
. . . . . . 7
⊢ ((𝑘 ∈ (1...𝑁) ∧ 𝑚 = 𝑘) → (𝑚 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
5 | 4, 3 | ifbieq1d 4109 |
. . . . . 6
⊢ ((𝑘 ∈ (1...𝑁) ∧ 𝑚 = 𝑘) → if(𝑚 ∈ ℙ, 𝑚, 1) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
6 | | elfznn 12370 |
. . . . . 6
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ) |
7 | | 1nn 11031 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℕ) |
9 | 6, 8 | ifcld 4131 |
. . . . . 6
⊢ (𝑘 ∈ (1...𝑁) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
10 | 2, 5, 6, 9 | fvmptd 6288 |
. . . . 5
⊢ (𝑘 ∈ (1...𝑁) → ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
11 | 10 | eqcomd 2628 |
. . . 4
⊢ (𝑘 ∈ (1...𝑁) → if(𝑘 ∈ ℙ, 𝑘, 1) = ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) |
12 | 11 | prodeq2i 14649 |
. . 3
⊢
∏𝑘 ∈
(1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1) = ∏𝑘 ∈ (1...𝑁)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) |
13 | 1, 12 | syl6eq 2672 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) |
14 | | fzfid 12772 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ∈
Fin) |
15 | | fz1ssnn 12372 |
. . . 4
⊢
(1...𝑁) ⊆
ℕ |
16 | 14, 15 | jctil 560 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((1...𝑁) ⊆
ℕ ∧ (1...𝑁)
∈ Fin)) |
17 | | fzssz 12343 |
. . . . 5
⊢
(1...𝑁) ⊆
ℤ |
18 | 17 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ⊆
ℤ) |
19 | | 0nelfz1 12360 |
. . . . 5
⊢ 0 ∉
(1...𝑁) |
20 | 19 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 0 ∉ (1...𝑁)) |
21 | | lcmfn0cl 15339 |
. . . 4
⊢
(((1...𝑁) ⊆
ℤ ∧ (1...𝑁)
∈ Fin ∧ 0 ∉ (1...𝑁)) → (lcm‘(1...𝑁)) ∈
ℕ) |
22 | 18, 14, 20, 21 | syl3anc 1326 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (lcm‘(1...𝑁)) ∈ ℕ) |
23 | | id 22 |
. . . . . 6
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℕ) |
24 | 7 | a1i 11 |
. . . . . 6
⊢ (𝑚 ∈ ℕ → 1 ∈
ℕ) |
25 | 23, 24 | ifcld 4131 |
. . . . 5
⊢ (𝑚 ∈ ℕ → if(𝑚 ∈ ℙ, 𝑚, 1) ∈
ℕ) |
26 | 25 | adantl 482 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑚 ∈ ℕ)
→ if(𝑚 ∈ ℙ,
𝑚, 1) ∈
ℕ) |
27 | | eqid 2622 |
. . . 4
⊢ (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1)) = (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1)) |
28 | 26, 27 | fmptd 6385 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑚 ∈ ℕ
↦ if(𝑚 ∈
ℙ, 𝑚,
1)):ℕ⟶ℕ) |
29 | | simpr 477 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ (1...𝑁)) |
30 | 29 | adantr 481 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) ∧ 𝑥 ∈ ((1...𝑁) ∖ {𝑘})) → 𝑘 ∈ (1...𝑁)) |
31 | | eldifi 3732 |
. . . . . . 7
⊢ (𝑥 ∈ ((1...𝑁) ∖ {𝑘}) → 𝑥 ∈ (1...𝑁)) |
32 | 31 | adantl 482 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) ∧ 𝑥 ∈ ((1...𝑁) ∖ {𝑘})) → 𝑥 ∈ (1...𝑁)) |
33 | | eldif 3584 |
. . . . . . . 8
⊢ (𝑥 ∈ ((1...𝑁) ∖ {𝑘}) ↔ (𝑥 ∈ (1...𝑁) ∧ ¬ 𝑥 ∈ {𝑘})) |
34 | | velsn 4193 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑘} ↔ 𝑥 = 𝑘) |
35 | 34 | biimpri 218 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → 𝑥 ∈ {𝑘}) |
36 | 35 | equcoms 1947 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑥 → 𝑥 ∈ {𝑘}) |
37 | 36 | necon3bi 2820 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ {𝑘} → 𝑘 ≠ 𝑥) |
38 | 37 | adantl 482 |
. . . . . . . 8
⊢ ((𝑥 ∈ (1...𝑁) ∧ ¬ 𝑥 ∈ {𝑘}) → 𝑘 ≠ 𝑥) |
39 | 33, 38 | sylbi 207 |
. . . . . . 7
⊢ (𝑥 ∈ ((1...𝑁) ∖ {𝑘}) → 𝑘 ≠ 𝑥) |
40 | 39 | adantl 482 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) ∧ 𝑥 ∈ ((1...𝑁) ∖ {𝑘})) → 𝑘 ≠ 𝑥) |
41 | 27 | fvprmselgcd1 15749 |
. . . . . 6
⊢ ((𝑘 ∈ (1...𝑁) ∧ 𝑥 ∈ (1...𝑁) ∧ 𝑘 ≠ 𝑥) → (((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) gcd ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑥)) = 1) |
42 | 30, 32, 40, 41 | syl3anc 1326 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) ∧ 𝑥 ∈ ((1...𝑁) ∖ {𝑘})) → (((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) gcd ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑥)) = 1) |
43 | 42 | ralrimiva 2966 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → ∀𝑥 ∈ ((1...𝑁) ∖ {𝑘})(((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) gcd ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑥)) = 1) |
44 | 43 | ralrimiva 2966 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ∀𝑘 ∈
(1...𝑁)∀𝑥 ∈ ((1...𝑁) ∖ {𝑘})(((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) gcd ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑥)) = 1) |
45 | | eqidd 2623 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1)) = (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))) |
46 | | simpr 477 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) ∧ 𝑚 = 𝑘) → 𝑚 = 𝑘) |
47 | 46 | eleq1d 2686 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) ∧ 𝑚 = 𝑘) → (𝑚 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
48 | 47, 46 | ifbieq1d 4109 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) ∧ 𝑚 = 𝑘) → if(𝑚 ∈ ℙ, 𝑚, 1) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
49 | 15, 29 | sseldi 3601 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℕ) |
50 | 17, 29 | sseldi 3601 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℤ) |
51 | | 1zzd 11408 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → 1 ∈
ℤ) |
52 | 50, 51 | ifcld 4131 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
53 | 45, 48, 49, 52 | fvmptd 6288 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
54 | | elfzuz2 12346 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → 𝑁 ∈
(ℤ≥‘1)) |
55 | 54 | adantl 482 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → 𝑁 ∈
(ℤ≥‘1)) |
56 | | eluzfz1 12348 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑁)) |
57 | 55, 56 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → 1 ∈ (1...𝑁)) |
58 | 29, 57 | ifcld 4131 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ (1...𝑁)) |
59 | 16 | adantr 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → ((1...𝑁) ⊆ ℕ ∧
(1...𝑁) ∈
Fin)) |
60 | 17 | 2a1i 12 |
. . . . . . . 8
⊢
((1...𝑁) ∈ Fin
→ ((1...𝑁) ⊆
ℕ → (1...𝑁)
⊆ ℤ)) |
61 | 60 | imdistanri 727 |
. . . . . . 7
⊢
(((1...𝑁) ⊆
ℕ ∧ (1...𝑁)
∈ Fin) → ((1...𝑁)
⊆ ℤ ∧ (1...𝑁) ∈ Fin)) |
62 | | dvdslcmf 15344 |
. . . . . . 7
⊢
(((1...𝑁) ⊆
ℤ ∧ (1...𝑁)
∈ Fin) → ∀𝑥 ∈ (1...𝑁)𝑥 ∥ (lcm‘(1...𝑁))) |
63 | 59, 61, 62 | 3syl 18 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → ∀𝑥 ∈ (1...𝑁)𝑥 ∥ (lcm‘(1...𝑁))) |
64 | | breq1 4656 |
. . . . . . 7
⊢ (𝑥 = if(𝑘 ∈ ℙ, 𝑘, 1) → (𝑥 ∥ (lcm‘(1...𝑁)) ↔ if(𝑘 ∈ ℙ, 𝑘, 1) ∥ (lcm‘(1...𝑁)))) |
65 | 64 | rspcv 3305 |
. . . . . 6
⊢ (if(𝑘 ∈ ℙ, 𝑘, 1) ∈ (1...𝑁) → (∀𝑥 ∈ (1...𝑁)𝑥 ∥ (lcm‘(1...𝑁)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∥ (lcm‘(1...𝑁)))) |
66 | 58, 63, 65 | sylc 65 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∥ (lcm‘(1...𝑁))) |
67 | 53, 66 | eqbrtrd 4675 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (1...𝑁)) → ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) ∥ (lcm‘(1...𝑁))) |
68 | 67 | ralrimiva 2966 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ∀𝑘 ∈
(1...𝑁)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) ∥ (lcm‘(1...𝑁))) |
69 | | coprmproddvds 15377 |
. . 3
⊢
((((1...𝑁) ⊆
ℕ ∧ (1...𝑁)
∈ Fin) ∧ ((lcm‘(1...𝑁)) ∈ ℕ ∧ (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1)):ℕ⟶ℕ) ∧
(∀𝑘 ∈
(1...𝑁)∀𝑥 ∈ ((1...𝑁) ∖ {𝑘})(((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) gcd ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑥)) = 1 ∧ ∀𝑘 ∈ (1...𝑁)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) ∥ (lcm‘(1...𝑁)))) → ∏𝑘 ∈ (1...𝑁)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) ∥ (lcm‘(1...𝑁))) |
70 | 16, 22, 28, 44, 68, 69 | syl122anc 1335 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ∏𝑘 ∈
(1...𝑁)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) ∥ (lcm‘(1...𝑁))) |
71 | 13, 70 | eqbrtrd 4675 |
1
⊢ (𝑁 ∈ ℕ0
→ (#p‘𝑁) ∥ (lcm‘(1...𝑁))) |