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 biimtrdi ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ 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 ‘ 𝑍 ) ↔ ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘 ) ) ) )