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

Metamath Proof Explorer

Theorem lcmfunsnlem2lem1

Description: Lemma 1 for lcmfunsnlem2 . (Contributed by AV, 26-Aug-2020)

Ref Expression
Assertion lcmfunsnlem2lem1 ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ∀ 𝑘 ∈ ℕ ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ≤ 𝑘 ) )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑘 ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 )
2 nfv ⊢ Ⅎ 𝑘 𝑛 ∈ ℤ
3 nfv ⊢ Ⅎ 𝑘 ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin )
4 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 )
5 nfv ⊢ Ⅎ 𝑘 ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 )
6 4 5 nfan ⊢ Ⅎ 𝑘 ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) )
7 3 6 nfan ⊢ Ⅎ 𝑘 ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) )
8 2 7 nfan ⊢ Ⅎ 𝑘 ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) )
9 1 8 nfan ⊢ Ⅎ 𝑘 ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) )
10 simprr ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → 𝑘 ∈ ℕ )
11 simp2 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → 𝑦 ⊆ ℤ )
12 snssi ⊢ ( 𝑧 ∈ ℤ → { 𝑧 } ⊆ ℤ )
13 12 3ad2ant1 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → { 𝑧 } ⊆ ℤ )
14 11 13 unssd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ )
15 simp3 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → 𝑦 ∈ Fin )
16 snfi ⊢ { 𝑧 } ∈ Fin
17 unfi ⊢ ( ( 𝑦 ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
18 15 16 17 sylancl ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
19 14 18 jca ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ) )
20 lcmfcl ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ0 )
21 19 20 syl ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ0 )
22 21 nn0zd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ )
23 22 adantl ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ )
24 23 adantr ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ )
25 simprl ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → 𝑛 ∈ ℤ )
26 10 24 25 3jca ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → ( 𝑘 ∈ ℕ ∧ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) )
27 14 adantl ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ )
28 18 adantl ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
29 df-nel ⊢ ( 0 ∉ 𝑦 ↔ ¬ 0 ∈ 𝑦 )
30 29 biimpi ⊢ ( 0 ∉ 𝑦 → ¬ 0 ∈ 𝑦 )
31 elsni ⊢ ( 0 ∈ { 𝑧 } → 0 = 𝑧 )
32 31 eqcomd ⊢ ( 0 ∈ { 𝑧 } → 𝑧 = 0 )
33 32 necon3ai ⊢ ( 𝑧 ≠ 0 → ¬ 0 ∈ { 𝑧 } )
34 30 33 anim12i ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ) → ( ¬ 0 ∈ 𝑦 ∧ ¬ 0 ∈ { 𝑧 } ) )
35 34 3adant3 ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ¬ 0 ∈ 𝑦 ∧ ¬ 0 ∈ { 𝑧 } ) )
36 df-nel ⊢ ( 0 ∉ ( 𝑦 ∪ { 𝑧 } ) ↔ ¬ 0 ∈ ( 𝑦 ∪ { 𝑧 } ) )
37 ioran ⊢ ( ¬ ( 0 ∈ 𝑦 ∨ 0 ∈ { 𝑧 } ) ↔ ( ¬ 0 ∈ 𝑦 ∧ ¬ 0 ∈ { 𝑧 } ) )
38 elun ⊢ ( 0 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 0 ∈ 𝑦 ∨ 0 ∈ { 𝑧 } ) )
39 37 38 xchnxbir ⊢ ( ¬ 0 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( ¬ 0 ∈ 𝑦 ∧ ¬ 0 ∈ { 𝑧 } ) )
40 36 39 bitri ⊢ ( 0 ∉ ( 𝑦 ∪ { 𝑧 } ) ↔ ( ¬ 0 ∈ 𝑦 ∧ ¬ 0 ∈ { 𝑧 } ) )
41 35 40 sylibr ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → 0 ∉ ( 𝑦 ∪ { 𝑧 } ) )
42 41 adantr ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → 0 ∉ ( 𝑦 ∪ { 𝑧 } ) )
43 27 28 42 3jca ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ∧ 0 ∉ ( 𝑦 ∪ { 𝑧 } ) ) )
44 43 adantr ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ∧ 0 ∉ ( 𝑦 ∪ { 𝑧 } ) ) )
45 lcmfn0cl ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ∧ 0 ∉ ( 𝑦 ∪ { 𝑧 } ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ )
46 44 45 syl ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ )
47 46 nnne0d ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ≠ 0 )
48 47 neneqd ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → ¬ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 )
49 neneq ⊢ ( 𝑛 ≠ 0 → ¬ 𝑛 = 0 )
50 49 3ad2ant3 ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ¬ 𝑛 = 0 )
51 50 ad2antrr ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → ¬ 𝑛 = 0 )
52 48 51 jca ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → ( ¬ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∧ ¬ 𝑛 = 0 ) )
53 ioran ⊢ ( ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) ↔ ( ¬ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∧ ¬ 𝑛 = 0 ) )
54 52 53 sylibr ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) )
55 26 54 jca ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑘 ∈ ℕ ∧ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) ) )
56 55 exp43 ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑛 ∈ ℤ → ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ∧ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) ) ) ) ) )
57 56 adantrd ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( 𝑛 ∈ ℤ → ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ∧ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) ) ) ) ) )
58 57 com23 ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( 𝑛 ∈ ℤ → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ∧ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) ) ) ) ) )
59 58 imp32 ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ∧ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) ) ) )
60 59 imp ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ ∧ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) ) )
61 60 adantr ⊢ ( ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) ∧ 𝑘 ∈ ℕ ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → ( ( 𝑘 ∈ ℕ ∧ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) ) )
62 sneq ⊢ ( 𝑛 = 𝑧 → { 𝑛 } = { 𝑧 } )
63 62 uneq2d ⊢ ( 𝑛 = 𝑧 → ( 𝑦 ∪ { 𝑛 } ) = ( 𝑦 ∪ { 𝑧 } ) )
64 63 fveq2d ⊢ ( 𝑛 = 𝑧 → ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) )
65 oveq2 ⊢ ( 𝑛 = 𝑧 → ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) )
66 64 65 eqeq12d ⊢ ( 𝑛 = 𝑧 → ( ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ↔ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
67 66 rspcv ⊢ ( 𝑧 ∈ ℤ → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
68 67 3ad2ant1 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
69 nnz ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
70 69 adantl ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℤ )
71 70 adantl ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → 𝑘 ∈ ℤ )
72 lcmfcl ⊢ ( ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℕ0 )
73 72 nn0zd ⊢ ( ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℤ )
74 73 3adant1 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℤ )
75 74 ad2antrr ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → ( lcm ‘ 𝑦 ) ∈ ℤ )
76 simpll1 ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → 𝑧 ∈ ℤ )
77 71 75 76 3jca ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) → ( 𝑘 ∈ ℤ ∧ ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) )
78 77 ad2antrr ⊢ ( ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → ( 𝑘 ∈ ℤ ∧ ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) )
79 elun1 ⊢ ( 𝑚 ∈ 𝑦 → 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) )
80 79 orcd ⊢ ( 𝑚 ∈ 𝑦 → ( 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 𝑚 ∈ { 𝑛 } ) )
81 elun ⊢ ( 𝑚 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ↔ ( 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 𝑚 ∈ { 𝑛 } ) )
82 80 81 sylibr ⊢ ( 𝑚 ∈ 𝑦 → 𝑚 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) )
83 breq1 ⊢ ( 𝑖 = 𝑚 → ( 𝑖 ∥ 𝑘 ↔ 𝑚 ∥ 𝑘 ) )
84 83 rspcv ⊢ ( 𝑚 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → 𝑚 ∥ 𝑘 ) )
85 82 84 syl ⊢ ( 𝑚 ∈ 𝑦 → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → 𝑚 ∥ 𝑘 ) )
86 85 com12 ⊢ ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( 𝑚 ∈ 𝑦 → 𝑚 ∥ 𝑘 ) )
87 86 adantl ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → ( 𝑚 ∈ 𝑦 → 𝑚 ∥ 𝑘 ) )
88 87 ralrimiv ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 )
89 88 adantr ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) ∧ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) ) → ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 )
90 breq2 ⊢ ( 𝑘 = 𝑙 → ( 𝑚 ∥ 𝑘 ↔ 𝑚 ∥ 𝑙 ) )
91 90 ralbidv ⊢ ( 𝑘 = 𝑙 → ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 ↔ ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 ) )
92 breq2 ⊢ ( 𝑘 = 𝑙 → ( ( lcm ‘ 𝑦 ) ∥ 𝑘 ↔ ( lcm ‘ 𝑦 ) ∥ 𝑙 ) )
93 91 92 imbi12d ⊢ ( 𝑘 = 𝑙 → ( ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ↔ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → ( lcm ‘ 𝑦 ) ∥ 𝑙 ) ) )
94 93 cbvralvw ⊢ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ↔ ∀ 𝑙 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → ( lcm ‘ 𝑦 ) ∥ 𝑙 ) )
95 70 adantr ⊢ ( ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → 𝑘 ∈ ℤ )
96 95 adantl ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) ∧ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) ) → 𝑘 ∈ ℤ )
97 breq2 ⊢ ( 𝑙 = 𝑘 → ( 𝑚 ∥ 𝑙 ↔ 𝑚 ∥ 𝑘 ) )
98 97 ralbidv ⊢ ( 𝑙 = 𝑘 → ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 ↔ ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 ) )
99 breq2 ⊢ ( 𝑙 = 𝑘 → ( ( lcm ‘ 𝑦 ) ∥ 𝑙 ↔ ( lcm ‘ 𝑦 ) ∥ 𝑘 ) )
100 98 99 imbi12d ⊢ ( 𝑙 = 𝑘 → ( ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → ( lcm ‘ 𝑦 ) ∥ 𝑙 ) ↔ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) )
101 100 rspcv ⊢ ( 𝑘 ∈ ℤ → ( ∀ 𝑙 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → ( lcm ‘ 𝑦 ) ∥ 𝑙 ) → ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) )
102 96 101 syl ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) ∧ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) ) → ( ∀ 𝑙 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → ( lcm ‘ 𝑦 ) ∥ 𝑙 ) → ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) )
103 94 102 biimtrid ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) ∧ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) → ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) )
104 89 103 mpid ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) ∧ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) )
105 104 exp31 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ) )
106 105 com24 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) → ( ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ) )
107 106 imp ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) → ( ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) )
108 107 impl ⊢ ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) )
109 108 imp ⊢ ( ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → ( lcm ‘ 𝑦 ) ∥ 𝑘 )
110 vsnid ⊢ 𝑧 ∈ { 𝑧 }
111 110 olci ⊢ ( 𝑧 ∈ 𝑦 ∨ 𝑧 ∈ { 𝑧 } )
112 elun ⊢ ( 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑧 ∈ 𝑦 ∨ 𝑧 ∈ { 𝑧 } ) )
113 111 112 mpbir ⊢ 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } )
114 113 orci ⊢ ( 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 𝑧 ∈ { 𝑛 } )
115 elun ⊢ ( 𝑧 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ↔ ( 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 𝑧 ∈ { 𝑛 } ) )
116 114 115 mpbir ⊢ 𝑧 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } )
117 breq1 ⊢ ( 𝑖 = 𝑧 → ( 𝑖 ∥ 𝑘 ↔ 𝑧 ∥ 𝑘 ) )
118 117 rspcv ⊢ ( 𝑧 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → 𝑧 ∥ 𝑘 ) )
119 116 118 mp1i ⊢ ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → 𝑧 ∥ 𝑘 ) )
120 119 imp ⊢ ( ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → 𝑧 ∥ 𝑘 )
121 109 120 jca ⊢ ( ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → ( ( lcm ‘ 𝑦 ) ∥ 𝑘 ∧ 𝑧 ∥ 𝑘 ) )
122 lcmdvds ⊢ ( ( 𝑘 ∈ ℤ ∧ ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( ( lcm ‘ 𝑦 ) ∥ 𝑘 ∧ 𝑧 ∥ 𝑘 ) → ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∥ 𝑘 ) )
123 78 121 122 sylc ⊢ ( ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∥ 𝑘 )
124 breq1 ⊢ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ↔ ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∥ 𝑘 ) )
125 123 124 imbitrrid ⊢ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → ( ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) )
126 125 expd ⊢ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → ( ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) )
127 126 exp5j ⊢ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) → ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) ) ) )
128 127 com12 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) → ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) ) ) )
129 68 128 syld ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) → ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) ) ) )
130 129 com23 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) ) ) )
131 130 imp32 ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) )
132 131 expd ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( 𝑛 ∈ ℤ → ( 𝑘 ∈ ℕ → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) ) )
133 132 com34 ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( 𝑛 ∈ ℤ → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( 𝑘 ∈ ℕ → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) ) )
134 133 com12 ⊢ ( 𝑛 ∈ ℤ → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( 𝑘 ∈ ℕ → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) ) )
135 134 imp ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( 𝑘 ∈ ℕ → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) )
136 135 com12 ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) → ( 𝑘 ∈ ℕ → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) ) )
137 136 imp ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ( 𝑘 ∈ ℕ → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) )
138 137 imp ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) )
139 138 imp ⊢ ( ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) ∧ 𝑘 ∈ ℕ ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 )
140 vsnid ⊢ 𝑛 ∈ { 𝑛 }
141 140 olci ⊢ ( 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 𝑛 ∈ { 𝑛 } )
142 elun ⊢ ( 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ↔ ( 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 𝑛 ∈ { 𝑛 } ) )
143 141 142 mpbir ⊢ 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } )
144 breq1 ⊢ ( 𝑖 = 𝑛 → ( 𝑖 ∥ 𝑘 ↔ 𝑛 ∥ 𝑘 ) )
145 144 rspcv ⊢ ( 𝑛 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → 𝑛 ∥ 𝑘 ) )
146 143 145 mp1i ⊢ ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → 𝑛 ∥ 𝑘 ) )
147 146 imp ⊢ ( ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) ∧ 𝑘 ∈ ℕ ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → 𝑛 ∥ 𝑘 )
148 139 147 jca ⊢ ( ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) ∧ 𝑘 ∈ ℕ ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ∧ 𝑛 ∥ 𝑘 ) )
149 lcmledvds ⊢ ( ( ( 𝑘 ∈ ℕ ∧ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) ) → ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ∧ 𝑛 ∥ 𝑘 ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ≤ 𝑘 ) )
150 61 148 149 sylc ⊢ ( ( ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) ∧ 𝑘 ∈ ℕ ) ∧ ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ≤ 𝑘 )
151 150 exp31 ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ( 𝑘 ∈ ℕ → ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ≤ 𝑘 ) ) )
152 9 151 ralrimi ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ∀ 𝑘 ∈ ℕ ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ≤ 𝑘 ) )