Metamath Proof Explorer


Theorem lcmineqlem4

Description: Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. F is found in lcmineqlem6 . (Contributed by metakunt, 10-May-2024)

Ref Expression
Hypotheses lcmineqlem4.1 ( 𝜑𝑁 ∈ ℕ )
lcmineqlem4.2 ( 𝜑𝑀 ∈ ℕ )
lcmineqlem4.3 ( 𝜑𝑀𝑁 )
lcmineqlem4.4 ( 𝜑𝐾 ∈ ( 0 ... ( 𝑁𝑀 ) ) )
Assertion lcmineqlem4 ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝐾 ) ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 lcmineqlem4.1 ( 𝜑𝑁 ∈ ℕ )
2 lcmineqlem4.2 ( 𝜑𝑀 ∈ ℕ )
3 lcmineqlem4.3 ( 𝜑𝑀𝑁 )
4 lcmineqlem4.4 ( 𝜑𝐾 ∈ ( 0 ... ( 𝑁𝑀 ) ) )
5 breq1 ( 𝑘 = ( 𝑀 + 𝐾 ) → ( 𝑘 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ↔ ( 𝑀 + 𝐾 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
6 fzssz ( 1 ... 𝑁 ) ⊆ ℤ
7 fzfi ( 1 ... 𝑁 ) ∈ Fin
8 6 7 pm3.2i ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin )
9 8 a1i ( 𝜑 → ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ) )
10 dvdslcmf ( ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
11 9 10 syl ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
12 1zzd ( 𝜑 → 1 ∈ ℤ )
13 2 nnzd ( 𝜑𝑀 ∈ ℤ )
14 0zd ( 𝜑 → 0 ∈ ℤ )
15 1 nnzd ( 𝜑𝑁 ∈ ℤ )
16 15 13 zsubcld ( 𝜑 → ( 𝑁𝑀 ) ∈ ℤ )
17 2 nnred ( 𝜑𝑀 ∈ ℝ )
18 17 leidd ( 𝜑𝑀𝑀 )
19 fznn ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑀 ∈ ℕ ∧ 𝑀𝑀 ) ) )
20 13 19 syl ( 𝜑 → ( 𝑀 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑀 ∈ ℕ ∧ 𝑀𝑀 ) ) )
21 2 18 20 mpbir2and ( 𝜑𝑀 ∈ ( 1 ... 𝑀 ) )
22 1cnd ( 𝜑 → 1 ∈ ℂ )
23 22 addid1d ( 𝜑 → ( 1 + 0 ) = 1 )
24 23 eqcomd ( 𝜑 → 1 = ( 1 + 0 ) )
25 1 nncnd ( 𝜑𝑁 ∈ ℂ )
26 2 nncnd ( 𝜑𝑀 ∈ ℂ )
27 25 26 npcand ( 𝜑 → ( ( 𝑁𝑀 ) + 𝑀 ) = 𝑁 )
28 eqcom ( ( ( 𝑁𝑀 ) + 𝑀 ) = 𝑁𝑁 = ( ( 𝑁𝑀 ) + 𝑀 ) )
29 28 a1i ( 𝜑 → ( ( ( 𝑁𝑀 ) + 𝑀 ) = 𝑁𝑁 = ( ( 𝑁𝑀 ) + 𝑀 ) ) )
30 25 26 jca ( 𝜑 → ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) )
31 subcl ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝑁𝑀 ) ∈ ℂ )
32 30 31 syl ( 𝜑 → ( 𝑁𝑀 ) ∈ ℂ )
33 32 26 jca ( 𝜑 → ( ( 𝑁𝑀 ) ∈ ℂ ∧ 𝑀 ∈ ℂ ) )
34 addcom ( ( ( 𝑁𝑀 ) ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑁𝑀 ) + 𝑀 ) = ( 𝑀 + ( 𝑁𝑀 ) ) )
35 33 34 syl ( 𝜑 → ( ( 𝑁𝑀 ) + 𝑀 ) = ( 𝑀 + ( 𝑁𝑀 ) ) )
36 eqeq2 ( ( ( 𝑁𝑀 ) + 𝑀 ) = ( 𝑀 + ( 𝑁𝑀 ) ) → ( 𝑁 = ( ( 𝑁𝑀 ) + 𝑀 ) ↔ 𝑁 = ( 𝑀 + ( 𝑁𝑀 ) ) ) )
37 35 36 syl ( 𝜑 → ( 𝑁 = ( ( 𝑁𝑀 ) + 𝑀 ) ↔ 𝑁 = ( 𝑀 + ( 𝑁𝑀 ) ) ) )
38 29 37 bitrd ( 𝜑 → ( ( ( 𝑁𝑀 ) + 𝑀 ) = 𝑁𝑁 = ( 𝑀 + ( 𝑁𝑀 ) ) ) )
39 38 pm5.74i ( ( 𝜑 → ( ( 𝑁𝑀 ) + 𝑀 ) = 𝑁 ) ↔ ( 𝜑𝑁 = ( 𝑀 + ( 𝑁𝑀 ) ) ) )
40 27 39 mpbi ( 𝜑𝑁 = ( 𝑀 + ( 𝑁𝑀 ) ) )
41 12 13 14 16 21 4 24 40 fzadd2d ( 𝜑 → ( 𝑀 + 𝐾 ) ∈ ( 1 ... 𝑁 ) )
42 5 11 41 rspcdva ( 𝜑 → ( 𝑀 + 𝐾 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
43 fz1ssnn ( 1 ... 𝑁 ) ⊆ ℕ
44 43 7 pm3.2i ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( 1 ... 𝑁 ) ∈ Fin )
45 lcmfnncl ( ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
46 44 45 ax-mp ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ
47 46 a1i ( 𝜑 → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
48 elfznn0 ( 𝐾 ∈ ( 0 ... ( 𝑁𝑀 ) ) → 𝐾 ∈ ℕ0 )
49 4 48 syl ( 𝜑𝐾 ∈ ℕ0 )
50 nnnn0addcl ( ( 𝑀 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 + 𝐾 ) ∈ ℕ )
51 2 49 50 syl2anc ( 𝜑 → ( 𝑀 + 𝐾 ) ∈ ℕ )
52 nndivdvds ( ( ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ ∧ ( 𝑀 + 𝐾 ) ∈ ℕ ) → ( ( 𝑀 + 𝐾 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ↔ ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝐾 ) ) ∈ ℕ ) )
53 47 51 52 syl2anc ( 𝜑 → ( ( 𝑀 + 𝐾 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ↔ ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝐾 ) ) ∈ ℕ ) )
54 42 53 mpbid ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝐾 ) ) ∈ ℕ )
55 54 nnzd ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝐾 ) ) ∈ ℤ )