Step |
Hyp |
Ref |
Expression |
1 |
|
lcmfn0val |
⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( lcm ‘ 𝑍 ) = inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } , ℝ , < ) ) |
2 |
1
|
adantr |
⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) → ( lcm ‘ 𝑍 ) = inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } , ℝ , < ) ) |
3 |
|
ssrab2 |
⊢ { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } ⊆ ℕ |
4 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
5 |
3 4
|
sseqtri |
⊢ { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } ⊆ ( ℤ≥ ‘ 1 ) |
6 |
|
simpr |
⊢ ( ( 𝑍 ⊆ ℤ ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) → ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) |
7 |
|
breq2 |
⊢ ( 𝑘 = 𝐾 → ( 𝑚 ∥ 𝑘 ↔ 𝑚 ∥ 𝐾 ) ) |
8 |
7
|
ralbidv |
⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 ↔ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) |
9 |
8
|
elrab |
⊢ ( 𝐾 ∈ { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } ↔ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) |
10 |
6 9
|
sylibr |
⊢ ( ( 𝑍 ⊆ ℤ ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) → 𝐾 ∈ { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } ) |
11 |
|
infssuzle |
⊢ ( ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝐾 ∈ { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } ) → inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } , ℝ , < ) ≤ 𝐾 ) |
12 |
5 10 11
|
sylancr |
⊢ ( ( 𝑍 ⊆ ℤ ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) → inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } , ℝ , < ) ≤ 𝐾 ) |
13 |
12
|
3ad2antl1 |
⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) → inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } , ℝ , < ) ≤ 𝐾 ) |
14 |
2 13
|
eqbrtrd |
⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) → ( lcm ‘ 𝑍 ) ≤ 𝐾 ) |
15 |
14
|
ex |
⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) → ( lcm ‘ 𝑍 ) ≤ 𝐾 ) ) |