This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lcmfunsnlem2

Description: Lemma for lcmfunsn and lcmfunsnlem (Induction step part 2). (Contributed by AV, 26-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑛 ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin )
2 nfv ⊢ Ⅎ 𝑛 ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 )
3 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 )
4 2 3 nfan ⊢ Ⅎ 𝑛 ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) )
5 1 4 nfan ⊢ Ⅎ 𝑛 ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) )
6 0z ⊢ 0 ∈ ℤ
7 eqoreldif ⊢ ( 0 ∈ ℤ → ( 𝑛 ∈ ℤ ↔ ( 𝑛 = 0 ∨ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ) )
8 6 7 ax-mp ⊢ ( 𝑛 ∈ ℤ ↔ ( 𝑛 = 0 ∨ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) )
9 simp2 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → 𝑦 ⊆ ℤ )
10 snssi ⊢ ( 𝑧 ∈ ℤ → { 𝑧 } ⊆ ℤ )
11 10 3ad2ant1 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → { 𝑧 } ⊆ ℤ )
12 9 11 unssd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ )
13 snssi ⊢ ( 0 ∈ ℤ → { 0 } ⊆ ℤ )
14 6 13 mp1i ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → { 0 } ⊆ ℤ )
15 12 14 unssd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 0 } ) ⊆ ℤ )
16 c0ex ⊢ 0 ∈ V
17 16 snid ⊢ 0 ∈ { 0 }
18 17 olci ⊢ ( 0 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 0 ∈ { 0 } )
19 elun ⊢ ( 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 0 } ) ↔ ( 0 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 0 ∈ { 0 } ) )
20 18 19 mpbir ⊢ 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 0 } )
21 lcmf0val ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 0 } ) ⊆ ℤ ∧ 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 0 } ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 0 } ) ) = 0 )
22 15 20 21 sylancl ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 0 } ) ) = 0 )
23 22 adantr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 = 0 ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 0 } ) ) = 0 )
24 sneq ⊢ ( 𝑛 = 0 → { 𝑛 } = { 0 } )
25 24 adantl ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 = 0 ) → { 𝑛 } = { 0 } )
26 25 uneq2d ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 = 0 ) → ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) = ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 0 } ) )
27 26 fveq2d ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 = 0 ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 0 } ) ) )
28 oveq2 ⊢ ( 𝑛 = 0 → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 0 ) )
29 snfi ⊢ { 𝑧 } ∈ Fin
30 unfi ⊢ ( ( 𝑦 ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
31 29 30 mpan2 ⊢ ( 𝑦 ∈ Fin → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
32 31 3ad2ant3 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
33 lcmfcl ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ0 )
34 12 32 33 syl2anc ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ0 )
35 34 nn0zd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ )
36 lcm0val ⊢ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 0 ) = 0 )
37 35 36 syl ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 0 ) = 0 )
38 28 37 sylan9eqr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 = 0 ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) = 0 )
39 23 27 38 3eqtr4d ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 = 0 ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) )
40 39 ex ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑛 = 0 → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
41 40 adantr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( 𝑛 = 0 → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
42 41 com12 ⊢ ( 𝑛 = 0 → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
43 9 adantl ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → 𝑦 ⊆ ℤ )
44 11 adantl ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → { 𝑧 } ⊆ ℤ )
45 43 44 unssd ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ )
46 elun1 ⊢ ( 0 ∈ 𝑦 → 0 ∈ ( 𝑦 ∪ { 𝑧 } ) )
47 46 ad2antrr ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → 0 ∈ ( 𝑦 ∪ { 𝑧 } ) )
48 lcmf0val ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ 0 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 )
49 45 47 48 syl2anc ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 )
50 49 oveq2d ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 𝑛 lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( 𝑛 lcm 0 ) )
51 eldifi ⊢ ( 𝑛 ∈ ( ℤ ∖ { 0 } ) → 𝑛 ∈ ℤ )
52 lcm0val ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 lcm 0 ) = 0 )
53 51 52 syl ⊢ ( 𝑛 ∈ ( ℤ ∖ { 0 } ) → ( 𝑛 lcm 0 ) = 0 )
54 53 ad2antlr ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 𝑛 lcm 0 ) = 0 )
55 50 54 eqtrd ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 𝑛 lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = 0 )
56 simp3 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → 𝑦 ∈ Fin )
57 56 29 30 sylancl ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
58 12 57 33 syl2anc ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ0 )
59 58 nn0zd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ )
60 51 adantl ⊢ ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) → 𝑛 ∈ ℤ )
61 lcmcom ⊢ ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) = ( 𝑛 lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) )
62 59 60 61 syl2anr ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) = ( 𝑛 lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) )
63 12 adantl ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ )
64 51 snssd ⊢ ( 𝑛 ∈ ( ℤ ∖ { 0 } ) → { 𝑛 } ⊆ ℤ )
65 64 ad2antlr ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → { 𝑛 } ⊆ ℤ )
66 63 65 unssd ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ )
67 46 orcd ⊢ ( 0 ∈ 𝑦 → ( 0 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 0 ∈ { 𝑛 } ) )
68 elun ⊢ ( 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ↔ ( 0 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 0 ∈ { 𝑛 } ) )
69 67 68 sylibr ⊢ ( 0 ∈ 𝑦 → 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) )
70 69 ad2antrr ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) )
71 lcmf0val ⊢ ( ( ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ ∧ 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = 0 )
72 66 70 71 syl2anc ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = 0 )
73 55 62 72 3eqtr4rd ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) )
74 73 a1d ⊢ ( ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
75 74 expimpd ⊢ ( ( 0 ∈ 𝑦 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
76 75 ex ⊢ ( 0 ∈ 𝑦 → ( 𝑛 ∈ ( ℤ ∖ { 0 } ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
77 elsng ⊢ ( 0 ∈ ℤ → ( 0 ∈ { 𝑧 } ↔ 0 = 𝑧 ) )
78 eqcom ⊢ ( 0 = 𝑧 ↔ 𝑧 = 0 )
79 77 78 bitrdi ⊢ ( 0 ∈ ℤ → ( 0 ∈ { 𝑧 } ↔ 𝑧 = 0 ) )
80 6 79 ax-mp ⊢ ( 0 ∈ { 𝑧 } ↔ 𝑧 = 0 )
81 80 biimpri ⊢ ( 𝑧 = 0 → 0 ∈ { 𝑧 } )
82 81 ad2antrr ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → 0 ∈ { 𝑧 } )
83 82 olcd ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 0 ∈ 𝑦 ∨ 0 ∈ { 𝑧 } ) )
84 elun ⊢ ( 0 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 0 ∈ 𝑦 ∨ 0 ∈ { 𝑧 } ) )
85 83 84 sylibr ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → 0 ∈ ( 𝑦 ∪ { 𝑧 } ) )
86 12 85 48 syl2an2 ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 )
87 86 oveq2d ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 𝑛 lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( 𝑛 lcm 0 ) )
88 51 ad2antlr ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → 𝑛 ∈ ℤ )
89 88 52 syl ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 𝑛 lcm 0 ) = 0 )
90 87 89 eqtrd ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 𝑛 lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = 0 )
91 59 88 61 syl2an2 ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) = ( 𝑛 lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) )
92 12 adantl ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ )
93 64 ad2antlr ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → { 𝑛 } ⊆ ℤ )
94 92 93 unssd ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ )
95 sneq ⊢ ( 𝑧 = 0 → { 𝑧 } = { 0 } )
96 17 95 eleqtrrid ⊢ ( 𝑧 = 0 → 0 ∈ { 𝑧 } )
97 96 ad2antrr ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → 0 ∈ { 𝑧 } )
98 97 olcd ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 0 ∈ 𝑦 ∨ 0 ∈ { 𝑧 } ) )
99 98 84 sylibr ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → 0 ∈ ( 𝑦 ∪ { 𝑧 } ) )
100 99 orcd ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 0 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 0 ∈ { 𝑛 } ) )
101 100 68 sylibr ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) )
102 94 101 71 syl2anc ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = 0 )
103 90 91 102 3eqtr4rd ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) )
104 103 a1d ⊢ ( ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
105 104 expimpd ⊢ ( ( 𝑧 = 0 ∧ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
106 105 ex ⊢ ( 𝑧 = 0 → ( 𝑛 ∈ ( ℤ ∖ { 0 } ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
107 ioran ⊢ ( ¬ ( 0 ∈ 𝑦 ∨ 𝑧 = 0 ) ↔ ( ¬ 0 ∈ 𝑦 ∧ ¬ 𝑧 = 0 ) )
108 df-nel ⊢ ( 0 ∉ 𝑦 ↔ ¬ 0 ∈ 𝑦 )
109 df-ne ⊢ ( 𝑧 ≠ 0 ↔ ¬ 𝑧 = 0 )
110 108 109 anbi12i ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ) ↔ ( ¬ 0 ∈ 𝑦 ∧ ¬ 𝑧 = 0 ) )
111 107 110 bitr4i ⊢ ( ¬ ( 0 ∈ 𝑦 ∨ 𝑧 = 0 ) ↔ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ) )
112 eldif ⊢ ( 𝑛 ∈ ( ℤ ∖ { 0 } ) ↔ ( 𝑛 ∈ ℤ ∧ ¬ 𝑛 ∈ { 0 } ) )
113 velsn ⊢ ( 𝑛 ∈ { 0 } ↔ 𝑛 = 0 )
114 113 bicomi ⊢ ( 𝑛 = 0 ↔ 𝑛 ∈ { 0 } )
115 114 necon3abii ⊢ ( 𝑛 ≠ 0 ↔ ¬ 𝑛 ∈ { 0 } )
116 lcmfunsnlem2lem2 ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) )
117 116 exp520 ⊢ ( 0 ∉ 𝑦 → ( 𝑧 ≠ 0 → ( 𝑛 ≠ 0 → ( 𝑛 ∈ ℤ → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) ) ) )
118 117 imp ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ) → ( 𝑛 ≠ 0 → ( 𝑛 ∈ ℤ → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) ) )
119 115 118 biimtrrid ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ) → ( ¬ 𝑛 ∈ { 0 } → ( 𝑛 ∈ ℤ → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) ) )
120 119 impcomd ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ) → ( ( 𝑛 ∈ ℤ ∧ ¬ 𝑛 ∈ { 0 } ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
121 112 120 biimtrid ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ) → ( 𝑛 ∈ ( ℤ ∖ { 0 } ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
122 111 121 sylbi ⊢ ( ¬ ( 0 ∈ 𝑦 ∨ 𝑧 = 0 ) → ( 𝑛 ∈ ( ℤ ∖ { 0 } ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
123 76 106 122 ecase3 ⊢ ( 𝑛 ∈ ( ℤ ∖ { 0 } ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
124 42 123 jaoi ⊢ ( ( 𝑛 = 0 ∨ 𝑛 ∈ ( ℤ ∖ { 0 } ) ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
125 8 124 sylbi ⊢ ( 𝑛 ∈ ℤ → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
126 125 com12 ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( 𝑛 ∈ ℤ → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
127 5 126 ralrimi ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) )