Metamath Proof Explorer


Theorem lcmfunsnlem1

Description: Lemma for lcmfdvds and lcmfunsnlem (Induction step part 1). (Contributed by AV, 25-Aug-2020)

Ref Expression
Assertion lcmfunsnlem1 ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚𝑦 𝑚𝑘 → ( lcm𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm𝑦 ) lcm 𝑛 ) ) ) → ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) )

Proof

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 ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) )