Step |
Hyp |
Ref |
Expression |
1 |
|
id |
⊢ ( 𝑍 ⊆ ℕ → 𝑍 ⊆ ℕ ) |
2 |
|
nnssz |
⊢ ℕ ⊆ ℤ |
3 |
1 2
|
sstrdi |
⊢ ( 𝑍 ⊆ ℕ → 𝑍 ⊆ ℤ ) |
4 |
3
|
adantr |
⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → 𝑍 ⊆ ℤ ) |
5 |
|
simpr |
⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → 𝑍 ∈ Fin ) |
6 |
|
0nnn |
⊢ ¬ 0 ∈ ℕ |
7 |
6
|
nelir |
⊢ 0 ∉ ℕ |
8 |
|
ssel |
⊢ ( 𝑍 ⊆ ℕ → ( 0 ∈ 𝑍 → 0 ∈ ℕ ) ) |
9 |
8
|
nelcon3d |
⊢ ( 𝑍 ⊆ ℕ → ( 0 ∉ ℕ → 0 ∉ 𝑍 ) ) |
10 |
7 9
|
mpi |
⊢ ( 𝑍 ⊆ ℕ → 0 ∉ 𝑍 ) |
11 |
10
|
adantr |
⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → 0 ∉ 𝑍 ) |
12 |
|
lcmfn0val |
⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( lcm ‘ 𝑍 ) = inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ) |
13 |
4 5 11 12
|
syl3anc |
⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → ( lcm ‘ 𝑍 ) = inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ) |