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