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