Step |
Hyp |
Ref |
Expression |
1 |
|
nfv |
⊢ Ⅎ 𝑘 ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) |
2 |
|
nfra1 |
⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) |
3 |
|
nfv |
⊢ Ⅎ 𝑘 ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) |
4 |
2 3
|
nfan |
⊢ Ⅎ 𝑘 ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) |
5 |
1 4
|
nfan |
⊢ Ⅎ 𝑘 ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) |
6 |
|
breq2 |
⊢ ( 𝑘 = 𝑙 → ( 𝑚 ∥ 𝑘 ↔ 𝑚 ∥ 𝑙 ) ) |
7 |
6
|
ralbidv |
⊢ ( 𝑘 = 𝑙 → ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 ↔ ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 ) ) |
8 |
|
breq2 |
⊢ ( 𝑘 = 𝑙 → ( ( lcm ‘ 𝑦 ) ∥ 𝑘 ↔ ( lcm ‘ 𝑦 ) ∥ 𝑙 ) ) |
9 |
7 8
|
imbi12d |
⊢ ( 𝑘 = 𝑙 → ( ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ↔ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → ( lcm ‘ 𝑦 ) ∥ 𝑙 ) ) ) |
10 |
9
|
cbvralvw |
⊢ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ↔ ∀ 𝑙 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → ( lcm ‘ 𝑦 ) ∥ 𝑙 ) ) |
11 |
|
breq2 |
⊢ ( 𝑙 = 𝑘 → ( 𝑚 ∥ 𝑙 ↔ 𝑚 ∥ 𝑘 ) ) |
12 |
11
|
ralbidv |
⊢ ( 𝑙 = 𝑘 → ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 ↔ ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 ) ) |
13 |
|
breq2 |
⊢ ( 𝑙 = 𝑘 → ( ( lcm ‘ 𝑦 ) ∥ 𝑙 ↔ ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) |
14 |
12 13
|
imbi12d |
⊢ ( 𝑙 = 𝑘 → ( ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → ( lcm ‘ 𝑦 ) ∥ 𝑙 ) ↔ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ) |
15 |
14
|
rspcv |
⊢ ( 𝑘 ∈ ℤ → ( ∀ 𝑙 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → ( lcm ‘ 𝑦 ) ∥ 𝑙 ) → ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ) |
16 |
15
|
adantl |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → ( ∀ 𝑙 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → ( lcm ‘ 𝑦 ) ∥ 𝑙 ) → ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ) |
17 |
|
sneq |
⊢ ( 𝑛 = 𝑧 → { 𝑛 } = { 𝑧 } ) |
18 |
17
|
uneq2d |
⊢ ( 𝑛 = 𝑧 → ( 𝑦 ∪ { 𝑛 } ) = ( 𝑦 ∪ { 𝑧 } ) ) |
19 |
18
|
fveq2d |
⊢ ( 𝑛 = 𝑧 → ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) |
20 |
|
oveq2 |
⊢ ( 𝑛 = 𝑧 → ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) |
21 |
19 20
|
eqeq12d |
⊢ ( 𝑛 = 𝑧 → ( ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ↔ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) ) |
22 |
21
|
rspcv |
⊢ ( 𝑧 ∈ ℤ → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) ) |
23 |
22
|
3ad2ant1 |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) ) |
24 |
23
|
adantr |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) ) |
25 |
|
simpr |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℤ ) |
26 |
|
lcmfcl |
⊢ ( ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℕ0 ) |
27 |
26
|
nn0zd |
⊢ ( ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℤ ) |
28 |
27
|
3adant1 |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℤ ) |
29 |
28
|
adantr |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → ( lcm ‘ 𝑦 ) ∈ ℤ ) |
30 |
|
simpl1 |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → 𝑧 ∈ ℤ ) |
31 |
25 29 30
|
3jca |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ℤ ∧ ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) |
32 |
31
|
adantr |
⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) ∧ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) → ( 𝑘 ∈ ℤ ∧ ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) |
33 |
32
|
adantr |
⊢ ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) ∧ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 ) → ( 𝑘 ∈ ℤ ∧ ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) |
34 |
|
ssun1 |
⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) |
35 |
|
ssralv |
⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 ) ) |
36 |
34 35
|
mp1i |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 ) ) |
37 |
36
|
imim1d |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → ( ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ) |
38 |
37
|
imp31 |
⊢ ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) ∧ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 ) → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) |
39 |
|
snidg |
⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ { 𝑧 } ) |
40 |
39
|
olcd |
⊢ ( 𝑧 ∈ ℤ → ( 𝑧 ∈ 𝑦 ∨ 𝑧 ∈ { 𝑧 } ) ) |
41 |
|
elun |
⊢ ( 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑧 ∈ 𝑦 ∨ 𝑧 ∈ { 𝑧 } ) ) |
42 |
40 41
|
sylibr |
⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) ) |
43 |
|
breq1 |
⊢ ( 𝑚 = 𝑧 → ( 𝑚 ∥ 𝑘 ↔ 𝑧 ∥ 𝑘 ) ) |
44 |
43
|
rspcv |
⊢ ( 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘 ) ) |
45 |
42 44
|
syl |
⊢ ( 𝑧 ∈ ℤ → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘 ) ) |
46 |
45
|
3ad2ant1 |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘 ) ) |
47 |
46
|
adantr |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘 ) ) |
48 |
47
|
adantr |
⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) ∧ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘 ) ) |
49 |
48
|
imp |
⊢ ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) ∧ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 ) → 𝑧 ∥ 𝑘 ) |
50 |
38 49
|
jca |
⊢ ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) ∧ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 ) → ( ( lcm ‘ 𝑦 ) ∥ 𝑘 ∧ 𝑧 ∥ 𝑘 ) ) |
51 |
|
lcmdvds |
⊢ ( ( 𝑘 ∈ ℤ ∧ ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( ( lcm ‘ 𝑦 ) ∥ 𝑘 ∧ 𝑧 ∥ 𝑘 ) → ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∥ 𝑘 ) ) |
52 |
33 50 51
|
sylc |
⊢ ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) ∧ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 ) → ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∥ 𝑘 ) |
53 |
|
breq1 |
⊢ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ↔ ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∥ 𝑘 ) ) |
54 |
52 53
|
syl5ibrcom |
⊢ ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) ∧ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) |
55 |
54
|
ex |
⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) ∧ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) |
56 |
55
|
com23 |
⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) ∧ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) |
57 |
56
|
ex |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → ( ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) ) |
58 |
24 57
|
syl5d |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → ( ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) ) |
59 |
16 58
|
syld |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → ( ∀ 𝑙 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → ( lcm ‘ 𝑦 ) ∥ 𝑙 ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) ) |
60 |
10 59
|
syl5bi |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) ) |
61 |
60
|
impd |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑘 ∈ ℤ ) → ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) |
62 |
61
|
impancom |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( 𝑘 ∈ ℤ → ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) |
63 |
5 62
|
ralrimi |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) |