Metamath Proof Explorer


Theorem lcmf

Description: Characterization of the least common multiple of a set of integers (without 0): A positiven integer is the least common multiple of a set of integers iff it divides each of the elements of the set and every integer which divides each of the elements of the set is greater than or equal to this integer. (Contributed by AV, 22-Aug-2020)

Ref Expression
Assertion lcmf ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( 𝐾 = ( lcm𝑍 ) ↔ ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvdslcmf ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) )
2 1 3adant3 ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) )
3 lcmfledvds ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑚𝑍 𝑚𝑘 ) → ( lcm𝑍 ) ≤ 𝑘 ) )
4 3 expdimp ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ∧ 𝑘 ∈ ℕ ) → ( ∀ 𝑚𝑍 𝑚𝑘 → ( lcm𝑍 ) ≤ 𝑘 ) )
5 4 ralrimiva ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘 → ( lcm𝑍 ) ≤ 𝑘 ) )
6 2 5 jca ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘 → ( lcm𝑍 ) ≤ 𝑘 ) ) )
7 6 adantl ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘 → ( lcm𝑍 ) ≤ 𝑘 ) ) )
8 breq2 ( 𝐾 = ( lcm𝑍 ) → ( 𝑚𝐾𝑚 ∥ ( lcm𝑍 ) ) )
9 8 ralbidv ( 𝐾 = ( lcm𝑍 ) → ( ∀ 𝑚𝑍 𝑚𝐾 ↔ ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) ) )
10 breq1 ( 𝐾 = ( lcm𝑍 ) → ( 𝐾𝑘 ↔ ( lcm𝑍 ) ≤ 𝑘 ) )
11 10 imbi2d ( 𝐾 = ( lcm𝑍 ) → ( ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ↔ ( ∀ 𝑚𝑍 𝑚𝑘 → ( lcm𝑍 ) ≤ 𝑘 ) ) )
12 11 ralbidv ( 𝐾 = ( lcm𝑍 ) → ( ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ↔ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘 → ( lcm𝑍 ) ≤ 𝑘 ) ) )
13 9 12 anbi12d ( 𝐾 = ( lcm𝑍 ) → ( ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) ↔ ( ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘 → ( lcm𝑍 ) ≤ 𝑘 ) ) ) )
14 7 13 syl5ibrcom ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( 𝐾 = ( lcm𝑍 ) → ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) ) )
15 lcmfn0cl ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( lcm𝑍 ) ∈ ℕ )
16 15 adantl ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( lcm𝑍 ) ∈ ℕ )
17 breq2 ( 𝑘 = ( lcm𝑍 ) → ( 𝑚𝑘𝑚 ∥ ( lcm𝑍 ) ) )
18 17 ralbidv ( 𝑘 = ( lcm𝑍 ) → ( ∀ 𝑚𝑍 𝑚𝑘 ↔ ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) ) )
19 breq2 ( 𝑘 = ( lcm𝑍 ) → ( 𝐾𝑘𝐾 ≤ ( lcm𝑍 ) ) )
20 18 19 imbi12d ( 𝑘 = ( lcm𝑍 ) → ( ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ↔ ( ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) → 𝐾 ≤ ( lcm𝑍 ) ) ) )
21 20 rspcv ( ( lcm𝑍 ) ∈ ℕ → ( ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) → ( ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) → 𝐾 ≤ ( lcm𝑍 ) ) ) )
22 16 21 syl ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) → ( ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) → 𝐾 ≤ ( lcm𝑍 ) ) ) )
23 22 adantld ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) → ( ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) → 𝐾 ≤ ( lcm𝑍 ) ) ) )
24 2 adantl ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) )
25 nnre ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ )
26 15 nnred ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( lcm𝑍 ) ∈ ℝ )
27 leloe ( ( 𝐾 ∈ ℝ ∧ ( lcm𝑍 ) ∈ ℝ ) → ( 𝐾 ≤ ( lcm𝑍 ) ↔ ( 𝐾 < ( lcm𝑍 ) ∨ 𝐾 = ( lcm𝑍 ) ) ) )
28 25 26 27 syl2an ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( 𝐾 ≤ ( lcm𝑍 ) ↔ ( 𝐾 < ( lcm𝑍 ) ∨ 𝐾 = ( lcm𝑍 ) ) ) )
29 lcmfledvds ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( ( 𝐾 ∈ ℕ ∧ ∀ 𝑚𝑍 𝑚𝐾 ) → ( lcm𝑍 ) ≤ 𝐾 ) )
30 29 expd ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( 𝐾 ∈ ℕ → ( ∀ 𝑚𝑍 𝑚𝐾 → ( lcm𝑍 ) ≤ 𝐾 ) ) )
31 30 impcom ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ∀ 𝑚𝑍 𝑚𝐾 → ( lcm𝑍 ) ≤ 𝐾 ) )
32 lenlt ( ( ( lcm𝑍 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( lcm𝑍 ) ≤ 𝐾 ↔ ¬ 𝐾 < ( lcm𝑍 ) ) )
33 26 25 32 syl2anr ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ( lcm𝑍 ) ≤ 𝐾 ↔ ¬ 𝐾 < ( lcm𝑍 ) ) )
34 pm2.21 ( ¬ 𝐾 < ( lcm𝑍 ) → ( 𝐾 < ( lcm𝑍 ) → 𝐾 = ( lcm𝑍 ) ) )
35 33 34 syl6bi ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ( lcm𝑍 ) ≤ 𝐾 → ( 𝐾 < ( lcm𝑍 ) → 𝐾 = ( lcm𝑍 ) ) ) )
36 31 35 syldc ( ∀ 𝑚𝑍 𝑚𝐾 → ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( 𝐾 < ( lcm𝑍 ) → 𝐾 = ( lcm𝑍 ) ) ) )
37 36 adantr ( ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) → ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( 𝐾 < ( lcm𝑍 ) → 𝐾 = ( lcm𝑍 ) ) ) )
38 37 com13 ( 𝐾 < ( lcm𝑍 ) → ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) → 𝐾 = ( lcm𝑍 ) ) ) )
39 2a1 ( 𝐾 = ( lcm𝑍 ) → ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) → 𝐾 = ( lcm𝑍 ) ) ) )
40 38 39 jaoi ( ( 𝐾 < ( lcm𝑍 ) ∨ 𝐾 = ( lcm𝑍 ) ) → ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) → 𝐾 = ( lcm𝑍 ) ) ) )
41 40 com12 ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ( 𝐾 < ( lcm𝑍 ) ∨ 𝐾 = ( lcm𝑍 ) ) → ( ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) → 𝐾 = ( lcm𝑍 ) ) ) )
42 28 41 sylbid ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( 𝐾 ≤ ( lcm𝑍 ) → ( ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) → 𝐾 = ( lcm𝑍 ) ) ) )
43 24 42 embantd ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ( ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) → 𝐾 ≤ ( lcm𝑍 ) ) → ( ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) → 𝐾 = ( lcm𝑍 ) ) ) )
44 43 com23 ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) → ( ( ∀ 𝑚𝑍 𝑚 ∥ ( lcm𝑍 ) → 𝐾 ≤ ( lcm𝑍 ) ) → 𝐾 = ( lcm𝑍 ) ) ) )
45 23 44 mpdd ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) → 𝐾 = ( lcm𝑍 ) ) )
46 14 45 impbid ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ) → ( 𝐾 = ( lcm𝑍 ) ↔ ( ∀ 𝑚𝑍 𝑚𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚𝑍 𝑚𝑘𝐾𝑘 ) ) ) )