This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prmodvdslcmf

Description: The primorial of a nonnegative integer divides the least common multiple of all positive integers less than or equal to the integer. (Contributed by AV, 19-Aug-2020) (Revised by AV, 29-Aug-2020)

Ref Expression
Assertion prmodvdslcmf ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 prmoval ⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
2 eqidd ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) = ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) )
3 simpr ⊢ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑚 = 𝑘 ) → 𝑚 = 𝑘 )
4 3 eleq1d ⊢ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑚 = 𝑘 ) → ( 𝑚 ∈ ℙ ↔ 𝑘 ∈ ℙ ) )
5 4 3 ifbieq1d ⊢ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑚 = 𝑘 ) → if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) = if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
6 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
7 1nn ⊢ 1 ∈ ℕ
8 7 a1i ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 1 ∈ ℕ )
9 6 8 ifcld ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℕ )
10 2 5 6 9 fvmptd ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
11 10 eqcomd ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑘 ) )
12 11 prodeq2i ⊢ ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑘 )
13 1 12 eqtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑘 ) )
14 fzfid ⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ∈ Fin )
15 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
16 14 15 jctil ⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( 1 ... 𝑁 ) ∈ Fin ) )
17 fzssz ⊢ ( 1 ... 𝑁 ) ⊆ ℤ
18 17 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ⊆ ℤ )
19 0nelfz1 ⊢ 0 ∉ ( 1 ... 𝑁 )
20 19 a1i ⊢ ( 𝑁 ∈ ℕ0 → 0 ∉ ( 1 ... 𝑁 ) )
21 lcmfn0cl ⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ∧ 0 ∉ ( 1 ... 𝑁 ) ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
22 18 14 20 21 syl3anc ⊢ ( 𝑁 ∈ ℕ0 → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
23 id ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ )
24 7 a1i ⊢ ( 𝑚 ∈ ℕ → 1 ∈ ℕ )
25 23 24 ifcld ⊢ ( 𝑚 ∈ ℕ → if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ∈ ℕ )
26 25 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ) → if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ∈ ℕ )
27 26 fmpttd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) : ℕ ⟶ ℕ )
28 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ( 1 ... 𝑁 ) )
29 28 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑥 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑘 } ) ) → 𝑘 ∈ ( 1 ... 𝑁 ) )
30 eldifi ⊢ ( 𝑥 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑘 } ) → 𝑥 ∈ ( 1 ... 𝑁 ) )
31 30 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑥 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑘 } ) ) → 𝑥 ∈ ( 1 ... 𝑁 ) )
32 eldif ⊢ ( 𝑥 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑘 } ) ↔ ( 𝑥 ∈ ( 1 ... 𝑁 ) ∧ ¬ 𝑥 ∈ { 𝑘 } ) )
33 velsn ⊢ ( 𝑥 ∈ { 𝑘 } ↔ 𝑥 = 𝑘 )
34 33 biimpri ⊢ ( 𝑥 = 𝑘 → 𝑥 ∈ { 𝑘 } )
35 34 equcoms ⊢ ( 𝑘 = 𝑥 → 𝑥 ∈ { 𝑘 } )
36 35 necon3bi ⊢ ( ¬ 𝑥 ∈ { 𝑘 } → 𝑘 ≠ 𝑥 )
37 32 36 simplbiim ⊢ ( 𝑥 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑘 } ) → 𝑘 ≠ 𝑥 )
38 37 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑥 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑘 } ) ) → 𝑘 ≠ 𝑥 )
39 eqid ⊢ ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) = ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) )
40 39 fvprmselgcd1 ⊢ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ∧ 𝑘 ≠ 𝑥 ) → ( ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑘 ) gcd ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑥 ) ) = 1 )
41 29 31 38 40 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑥 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑘 } ) ) → ( ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑘 ) gcd ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑥 ) ) = 1 )
42 41 ralrimiva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ∀ 𝑥 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑘 } ) ( ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑘 ) gcd ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑥 ) ) = 1 )
43 42 ralrimiva ⊢ ( 𝑁 ∈ ℕ0 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ∀ 𝑥 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑘 } ) ( ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑘 ) gcd ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑥 ) ) = 1 )
44 eqidd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) = ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) )
45 simpr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑚 = 𝑘 ) → 𝑚 = 𝑘 )
46 45 eleq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑚 = 𝑘 ) → ( 𝑚 ∈ ℙ ↔ 𝑘 ∈ ℙ ) )
47 46 45 ifbieq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑚 = 𝑘 ) → if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) = if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
48 15 28 sselid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
49 17 28 sselid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
50 1zzd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℤ )
51 49 50 ifcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℤ )
52 44 47 48 51 fvmptd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
53 breq1 ⊢ ( 𝑥 = if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) → ( 𝑥 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ↔ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
54 16 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( 1 ... 𝑁 ) ∈ Fin ) )
55 17 2a1i ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( ( 1 ... 𝑁 ) ⊆ ℕ → ( 1 ... 𝑁 ) ⊆ ℤ ) )
56 55 imdistanri ⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ) )
57 dvdslcmf ⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ∀ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑥 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
58 54 56 57 3syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ∀ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑥 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
59 elfzuz2 ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
60 59 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
61 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑁 ) )
62 60 61 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ( 1 ... 𝑁 ) )
63 28 62 ifcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ( 1 ... 𝑁 ) )
64 53 58 63 rspcdva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
65 52 64 eqbrtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑘 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
66 65 ralrimiva ⊢ ( 𝑁 ∈ ℕ0 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑘 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
67 coprmproddvds ⊢ ( ( ( ( 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 ... 𝑁 ) ) )
68 16 22 27 43 66 67 syl122anc ⊢ ( 𝑁 ∈ ℕ0 → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) ) ‘ 𝑘 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
69 13 68 eqbrtrd ⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )