Step |
Hyp |
Ref |
Expression |
1 |
|
ssel |
⊢ ( 𝑍 ⊆ ℤ → ( 𝑥 ∈ 𝑍 → 𝑥 ∈ ℤ ) ) |
2 |
1
|
ad2antrr |
⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ 0 ∈ 𝑍 ) → ( 𝑥 ∈ 𝑍 → 𝑥 ∈ ℤ ) ) |
3 |
2
|
imp |
⊢ ( ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ 0 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑍 ) → 𝑥 ∈ ℤ ) |
4 |
|
dvds0 |
⊢ ( 𝑥 ∈ ℤ → 𝑥 ∥ 0 ) |
5 |
3 4
|
syl |
⊢ ( ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ 0 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑍 ) → 𝑥 ∥ 0 ) |
6 |
|
lcmf0val |
⊢ ( ( 𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍 ) → ( lcm ‘ 𝑍 ) = 0 ) |
7 |
6
|
ad4ant13 |
⊢ ( ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ 0 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑍 ) → ( lcm ‘ 𝑍 ) = 0 ) |
8 |
5 7
|
breqtrrd |
⊢ ( ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ 0 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑍 ) → 𝑥 ∥ ( lcm ‘ 𝑍 ) ) |
9 |
8
|
ralrimiva |
⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ 0 ∈ 𝑍 ) → ∀ 𝑥 ∈ 𝑍 𝑥 ∥ ( lcm ‘ 𝑍 ) ) |
10 |
|
df-nel |
⊢ ( 0 ∉ 𝑍 ↔ ¬ 0 ∈ 𝑍 ) |
11 |
|
lcmfcllem |
⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( lcm ‘ 𝑍 ) ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑍 𝑥 ∥ 𝑛 } ) |
12 |
11
|
3expa |
⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ 0 ∉ 𝑍 ) → ( lcm ‘ 𝑍 ) ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑍 𝑥 ∥ 𝑛 } ) |
13 |
10 12
|
sylan2br |
⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ ¬ 0 ∈ 𝑍 ) → ( lcm ‘ 𝑍 ) ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑍 𝑥 ∥ 𝑛 } ) |
14 |
|
lcmfn0cl |
⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( lcm ‘ 𝑍 ) ∈ ℕ ) |
15 |
14
|
3expa |
⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ 0 ∉ 𝑍 ) → ( lcm ‘ 𝑍 ) ∈ ℕ ) |
16 |
10 15
|
sylan2br |
⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ ¬ 0 ∈ 𝑍 ) → ( lcm ‘ 𝑍 ) ∈ ℕ ) |
17 |
|
breq2 |
⊢ ( 𝑛 = ( lcm ‘ 𝑍 ) → ( 𝑥 ∥ 𝑛 ↔ 𝑥 ∥ ( lcm ‘ 𝑍 ) ) ) |
18 |
17
|
ralbidv |
⊢ ( 𝑛 = ( lcm ‘ 𝑍 ) → ( ∀ 𝑥 ∈ 𝑍 𝑥 ∥ 𝑛 ↔ ∀ 𝑥 ∈ 𝑍 𝑥 ∥ ( lcm ‘ 𝑍 ) ) ) |
19 |
18
|
elrab3 |
⊢ ( ( lcm ‘ 𝑍 ) ∈ ℕ → ( ( lcm ‘ 𝑍 ) ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑍 𝑥 ∥ 𝑛 } ↔ ∀ 𝑥 ∈ 𝑍 𝑥 ∥ ( lcm ‘ 𝑍 ) ) ) |
20 |
16 19
|
syl |
⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ ¬ 0 ∈ 𝑍 ) → ( ( lcm ‘ 𝑍 ) ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑍 𝑥 ∥ 𝑛 } ↔ ∀ 𝑥 ∈ 𝑍 𝑥 ∥ ( lcm ‘ 𝑍 ) ) ) |
21 |
13 20
|
mpbid |
⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ ¬ 0 ∈ 𝑍 ) → ∀ 𝑥 ∈ 𝑍 𝑥 ∥ ( lcm ‘ 𝑍 ) ) |
22 |
9 21
|
pm2.61dan |
⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ∀ 𝑥 ∈ 𝑍 𝑥 ∥ ( lcm ‘ 𝑍 ) ) |