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

Metamath Proof Explorer

Theorem lcmfunsnlem2lem2

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

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

Proof

Step Hyp Ref Expression
1 elun ⊢ ( 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ↔ ( 𝑖 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 𝑖 ∈ { 𝑛 } ) )
2 elun ⊢ ( 𝑖 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑖 ∈ 𝑦 ∨ 𝑖 ∈ { 𝑧 } ) )
3 simp1 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → 𝑧 ∈ ℤ )
4 3 adantr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → 𝑧 ∈ ℤ )
5 4 adantl ⊢ ( ( ( 𝑖 ∈ 𝑦 ∨ 𝑖 ∈ { 𝑧 } ) ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → 𝑧 ∈ ℤ )
6 sneq ⊢ ( 𝑛 = 𝑧 → { 𝑛 } = { 𝑧 } )
7 6 uneq2d ⊢ ( 𝑛 = 𝑧 → ( 𝑦 ∪ { 𝑛 } ) = ( 𝑦 ∪ { 𝑧 } ) )
8 7 fveq2d ⊢ ( 𝑛 = 𝑧 → ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) )
9 oveq2 ⊢ ( 𝑛 = 𝑧 → ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) )
10 8 9 eqeq12d ⊢ ( 𝑛 = 𝑧 → ( ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ↔ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
11 10 rspcv ⊢ ( 𝑧 ∈ ℤ → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
12 5 11 syl ⊢ ( ( ( 𝑖 ∈ 𝑦 ∨ 𝑖 ∈ { 𝑧 } ) ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
13 ssel ⊢ ( 𝑦 ⊆ ℤ → ( 𝑖 ∈ 𝑦 → 𝑖 ∈ ℤ ) )
14 13 3ad2ant2 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑖 ∈ 𝑦 → 𝑖 ∈ ℤ ) )
15 14 adantr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( 𝑖 ∈ 𝑦 → 𝑖 ∈ ℤ ) )
16 15 impcom ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → 𝑖 ∈ ℤ )
17 lcmfcl ⊢ ( ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℕ0 )
18 17 nn0zd ⊢ ( ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℤ )
19 18 3adant1 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℤ )
20 19 adantr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( lcm ‘ 𝑦 ) ∈ ℤ )
21 20 adantl ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → ( lcm ‘ 𝑦 ) ∈ ℤ )
22 lcmcl ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑧 lcm 𝑛 ) ∈ ℕ0 )
23 3 22 sylan ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( 𝑧 lcm 𝑛 ) ∈ ℕ0 )
24 23 nn0zd ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( 𝑧 lcm 𝑛 ) ∈ ℤ )
25 24 adantl ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → ( 𝑧 lcm 𝑛 ) ∈ ℤ )
26 lcmcl ⊢ ( ( ( lcm ‘ 𝑦 ) ∈ ℤ ∧ ( 𝑧 lcm 𝑛 ) ∈ ℤ ) → ( ( lcm ‘ 𝑦 ) lcm ( 𝑧 lcm 𝑛 ) ) ∈ ℕ0 )
27 21 25 26 syl2anc ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → ( ( lcm ‘ 𝑦 ) lcm ( 𝑧 lcm 𝑛 ) ) ∈ ℕ0 )
28 27 nn0zd ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → ( ( lcm ‘ 𝑦 ) lcm ( 𝑧 lcm 𝑛 ) ) ∈ ℤ )
29 breq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 ∥ ( lcm ‘ 𝑦 ) ↔ 𝑖 ∥ ( lcm ‘ 𝑦 ) ) )
30 29 rspcv ⊢ ( 𝑖 ∈ 𝑦 → ( ∀ 𝑘 ∈ 𝑦 𝑘 ∥ ( lcm ‘ 𝑦 ) → 𝑖 ∥ ( lcm ‘ 𝑦 ) ) )
31 dvdslcmf ⊢ ( ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ∀ 𝑘 ∈ 𝑦 𝑘 ∥ ( lcm ‘ 𝑦 ) )
32 31 3adant1 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ∀ 𝑘 ∈ 𝑦 𝑘 ∥ ( lcm ‘ 𝑦 ) )
33 32 adantr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ∀ 𝑘 ∈ 𝑦 𝑘 ∥ ( lcm ‘ 𝑦 ) )
34 30 33 impel ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → 𝑖 ∥ ( lcm ‘ 𝑦 ) )
35 20 24 jca ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ( lcm ‘ 𝑦 ) ∈ ℤ ∧ ( 𝑧 lcm 𝑛 ) ∈ ℤ ) )
36 35 adantl ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → ( ( lcm ‘ 𝑦 ) ∈ ℤ ∧ ( 𝑧 lcm 𝑛 ) ∈ ℤ ) )
37 dvdslcm ⊢ ( ( ( lcm ‘ 𝑦 ) ∈ ℤ ∧ ( 𝑧 lcm 𝑛 ) ∈ ℤ ) → ( ( lcm ‘ 𝑦 ) ∥ ( ( lcm ‘ 𝑦 ) lcm ( 𝑧 lcm 𝑛 ) ) ∧ ( 𝑧 lcm 𝑛 ) ∥ ( ( lcm ‘ 𝑦 ) lcm ( 𝑧 lcm 𝑛 ) ) ) )
38 37 simpld ⊢ ( ( ( lcm ‘ 𝑦 ) ∈ ℤ ∧ ( 𝑧 lcm 𝑛 ) ∈ ℤ ) → ( lcm ‘ 𝑦 ) ∥ ( ( lcm ‘ 𝑦 ) lcm ( 𝑧 lcm 𝑛 ) ) )
39 36 38 syl ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → ( lcm ‘ 𝑦 ) ∥ ( ( lcm ‘ 𝑦 ) lcm ( 𝑧 lcm 𝑛 ) ) )
40 16 21 28 34 39 dvdstrd ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → 𝑖 ∥ ( ( lcm ‘ 𝑦 ) lcm ( 𝑧 lcm 𝑛 ) ) )
41 4 adantl ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → 𝑧 ∈ ℤ )
42 simprr ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → 𝑛 ∈ ℤ )
43 lcmass ⊢ ( ( ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) = ( ( lcm ‘ 𝑦 ) lcm ( 𝑧 lcm 𝑛 ) ) )
44 21 41 42 43 syl3anc ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) = ( ( lcm ‘ 𝑦 ) lcm ( 𝑧 lcm 𝑛 ) ) )
45 40 44 breqtrrd ⊢ ( ( 𝑖 ∈ 𝑦 ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → 𝑖 ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) )
46 45 ex ⊢ ( 𝑖 ∈ 𝑦 → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → 𝑖 ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) ) )
47 elsni ⊢ ( 𝑖 ∈ { 𝑧 } → 𝑖 = 𝑧 )
48 17 3adant1 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℕ0 )
49 48 nn0zd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℤ )
50 lcmcl ⊢ ( ( ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∈ ℕ0 )
51 49 3 50 syl2anc ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∈ ℕ0 )
52 51 nn0zd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∈ ℤ )
53 52 adantr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∈ ℤ )
54 lcmcl ⊢ ( ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) ∈ ℕ0 )
55 52 54 sylan ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) ∈ ℕ0 )
56 55 nn0zd ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) ∈ ℤ )
57 19 3 jca ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) )
58 57 adantr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) )
59 dvdslcm ⊢ ( ( ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( lcm ‘ 𝑦 ) ∥ ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∧ 𝑧 ∥ ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
60 59 simprd ⊢ ( ( ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) → 𝑧 ∥ ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) )
61 58 60 syl ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → 𝑧 ∥ ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) )
62 dvdslcm ⊢ ( ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) ∧ 𝑛 ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) ) )
63 62 simpld ⊢ ( ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) )
64 52 63 sylan ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) )
65 4 53 56 61 64 dvdstrd ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → 𝑧 ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) )
66 breq1 ⊢ ( 𝑖 = 𝑧 → ( 𝑖 ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) ↔ 𝑧 ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) ) )
67 65 66 imbitrrid ⊢ ( 𝑖 = 𝑧 → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → 𝑖 ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) ) )
68 47 67 syl ⊢ ( 𝑖 ∈ { 𝑧 } → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → 𝑖 ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) ) )
69 46 68 jaoi ⊢ ( ( 𝑖 ∈ 𝑦 ∨ 𝑖 ∈ { 𝑧 } ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → 𝑖 ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) ) )
70 69 imp ⊢ ( ( ( 𝑖 ∈ 𝑦 ∨ 𝑖 ∈ { 𝑧 } ) ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → 𝑖 ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) )
71 oveq1 ⊢ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) = ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) )
72 71 breq2d ⊢ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → ( 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ↔ 𝑖 ∥ ( ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) lcm 𝑛 ) ) )
73 70 72 syl5ibrcom ⊢ ( ( ( 𝑖 ∈ 𝑦 ∨ 𝑖 ∈ { 𝑧 } ) ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
74 12 73 syld ⊢ ( ( ( 𝑖 ∈ 𝑦 ∨ 𝑖 ∈ { 𝑧 } ) ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
75 74 ex ⊢ ( ( 𝑖 ∈ 𝑦 ∨ 𝑖 ∈ { 𝑧 } ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
76 2 75 sylbi ⊢ ( 𝑖 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
77 elsni ⊢ ( 𝑖 ∈ { 𝑛 } → 𝑖 = 𝑛 )
78 simp2 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → 𝑦 ⊆ ℤ )
79 snssi ⊢ ( 𝑧 ∈ ℤ → { 𝑧 } ⊆ ℤ )
80 79 3ad2ant1 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → { 𝑧 } ⊆ ℤ )
81 78 80 unssd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ )
82 simp3 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → 𝑦 ∈ Fin )
83 snfi ⊢ { 𝑧 } ∈ Fin
84 unfi ⊢ ( ( 𝑦 ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
85 82 83 84 sylancl ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
86 lcmfcl ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ0 )
87 81 85 86 syl2anc ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ0 )
88 87 nn0zd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ )
89 88 anim1i ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) )
90 89 adantr ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) )
91 dvdslcm ⊢ ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∧ 𝑛 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
92 90 91 syl ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∧ 𝑛 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
93 92 simprd ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → 𝑛 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) )
94 breq1 ⊢ ( 𝑖 = 𝑛 → ( 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ↔ 𝑛 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
95 93 94 imbitrrid ⊢ ( 𝑖 = 𝑛 → ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
96 95 expd ⊢ ( 𝑖 = 𝑛 → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
97 77 96 syl ⊢ ( 𝑖 ∈ { 𝑛 } → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
98 76 97 jaoi ⊢ ( ( 𝑖 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 𝑖 ∈ { 𝑛 } ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
99 1 98 sylbi ⊢ ( 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
100 99 com13 ⊢ ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
101 100 expd ⊢ ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) → ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑛 ∈ ℤ → ( 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) ) )
102 101 adantl ⊢ ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑛 ∈ ℤ → ( 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) ) )
103 102 impcom ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( 𝑛 ∈ ℤ → ( 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
104 103 impcom ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) → ( 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
105 104 adantl ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ( 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) → 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
106 105 ralrimiv ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) )
107 lcmfunsnlem2lem1 ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ∀ 𝑘 ∈ ℕ ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ≤ 𝑘 ) )
108 89 adantr ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) )
109 81 adantr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ )
110 85 adantr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
111 df-nel ⊢ ( 0 ∉ 𝑦 ↔ ¬ 0 ∈ 𝑦 )
112 111 biimpi ⊢ ( 0 ∉ 𝑦 → ¬ 0 ∈ 𝑦 )
113 112 3ad2ant1 ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ¬ 0 ∈ 𝑦 )
114 elsni ⊢ ( 0 ∈ { 𝑧 } → 0 = 𝑧 )
115 114 eqcomd ⊢ ( 0 ∈ { 𝑧 } → 𝑧 = 0 )
116 115 necon3ai ⊢ ( 𝑧 ≠ 0 → ¬ 0 ∈ { 𝑧 } )
117 116 3ad2ant2 ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ¬ 0 ∈ { 𝑧 } )
118 ioran ⊢ ( ¬ ( 0 ∈ 𝑦 ∨ 0 ∈ { 𝑧 } ) ↔ ( ¬ 0 ∈ 𝑦 ∧ ¬ 0 ∈ { 𝑧 } ) )
119 113 117 118 sylanbrc ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ¬ ( 0 ∈ 𝑦 ∨ 0 ∈ { 𝑧 } ) )
120 elun ⊢ ( 0 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 0 ∈ 𝑦 ∨ 0 ∈ { 𝑧 } ) )
121 119 120 sylnibr ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ¬ 0 ∈ ( 𝑦 ∪ { 𝑧 } ) )
122 df-nel ⊢ ( 0 ∉ ( 𝑦 ∪ { 𝑧 } ) ↔ ¬ 0 ∈ ( 𝑦 ∪ { 𝑧 } ) )
123 121 122 sylibr ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → 0 ∉ ( 𝑦 ∪ { 𝑧 } ) )
124 lcmfn0cl ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ∧ 0 ∉ ( 𝑦 ∪ { 𝑧 } ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ )
125 109 110 123 124 syl2an3an ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ )
126 125 nnne0d ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ≠ 0 )
127 126 neneqd ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ¬ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 )
128 neneq ⊢ ( 𝑛 ≠ 0 → ¬ 𝑛 = 0 )
129 128 3ad2ant3 ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ¬ 𝑛 = 0 )
130 129 adantl ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ¬ 𝑛 = 0 )
131 ioran ⊢ ( ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) ↔ ( ¬ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∧ ¬ 𝑛 = 0 ) )
132 127 130 131 sylanbrc ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) )
133 lcmn0cl ⊢ ( ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ¬ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = 0 ∨ 𝑛 = 0 ) ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∈ ℕ )
134 108 132 133 syl2anc ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∈ ℕ )
135 snssi ⊢ ( 𝑛 ∈ ℤ → { 𝑛 } ⊆ ℤ )
136 135 adantl ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → { 𝑛 } ⊆ ℤ )
137 109 136 unssd ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ )
138 137 adantr ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ )
139 83 84 mpan2 ⊢ ( 𝑦 ∈ Fin → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
140 snfi ⊢ { 𝑛 } ∈ Fin
141 unfi ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ∧ { 𝑛 } ∈ Fin ) → ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin )
142 139 140 141 sylancl ⊢ ( 𝑦 ∈ Fin → ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin )
143 142 3ad2ant3 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin )
144 143 adantr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin )
145 144 adantr ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin )
146 elun ⊢ ( 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ↔ ( 0 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 0 ∈ { 𝑛 } ) )
147 nnel ⊢ ( ¬ 0 ∉ 𝑦 ↔ 0 ∈ 𝑦 )
148 147 biimpri ⊢ ( 0 ∈ 𝑦 → ¬ 0 ∉ 𝑦 )
149 148 3mix1d ⊢ ( 0 ∈ 𝑦 → ( ¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0 ) )
150 nne ⊢ ( ¬ 𝑧 ≠ 0 ↔ 𝑧 = 0 )
151 115 150 sylibr ⊢ ( 0 ∈ { 𝑧 } → ¬ 𝑧 ≠ 0 )
152 151 3mix2d ⊢ ( 0 ∈ { 𝑧 } → ( ¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0 ) )
153 149 152 jaoi ⊢ ( ( 0 ∈ 𝑦 ∨ 0 ∈ { 𝑧 } ) → ( ¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0 ) )
154 120 153 sylbi ⊢ ( 0 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( ¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0 ) )
155 elsni ⊢ ( 0 ∈ { 𝑛 } → 0 = 𝑛 )
156 155 eqcomd ⊢ ( 0 ∈ { 𝑛 } → 𝑛 = 0 )
157 nne ⊢ ( ¬ 𝑛 ≠ 0 ↔ 𝑛 = 0 )
158 156 157 sylibr ⊢ ( 0 ∈ { 𝑛 } → ¬ 𝑛 ≠ 0 )
159 158 3mix3d ⊢ ( 0 ∈ { 𝑛 } → ( ¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0 ) )
160 154 159 jaoi ⊢ ( ( 0 ∈ ( 𝑦 ∪ { 𝑧 } ) ∨ 0 ∈ { 𝑛 } ) → ( ¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0 ) )
161 146 160 sylbi ⊢ ( 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) → ( ¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0 ) )
162 3ianor ⊢ ( ¬ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ↔ ( ¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0 ) )
163 161 162 sylibr ⊢ ( 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) → ¬ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) )
164 163 con2i ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ¬ 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) )
165 df-nel ⊢ ( 0 ∉ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ↔ ¬ 0 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) )
166 164 165 sylibr ⊢ ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → 0 ∉ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) )
167 166 adantl ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → 0 ∉ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) )
168 138 145 167 3jca ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ ∧ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin ∧ 0 ∉ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) )
169 134 168 jca ⊢ ( ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ) → ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∈ ℕ ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ ∧ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin ∧ 0 ∉ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) ) )
170 169 ex ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ 𝑛 ∈ ℤ ) → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∈ ℕ ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ ∧ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin ∧ 0 ∉ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) ) ) )
171 170 ex ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( 𝑛 ∈ ℤ → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∈ ℕ ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ ∧ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin ∧ 0 ∉ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) ) ) ) )
172 171 adantr ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( 𝑛 ∈ ℤ → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∈ ℕ ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ ∧ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin ∧ 0 ∉ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) ) ) ) )
173 172 impcom ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) → ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) → ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∈ ℕ ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ ∧ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin ∧ 0 ∉ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) ) ) )
174 173 impcom ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∈ ℕ ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ ∧ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin ∧ 0 ∉ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) ) )
175 lcmf ⊢ ( ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∈ ℕ ∧ ( ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ⊆ ℤ ∧ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ∈ Fin ∧ 0 ∉ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) ) → ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) = ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) ↔ ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ≤ 𝑘 ) ) ) )
176 174 175 syl ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ( ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) = ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) ↔ ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ∧ ∀ 𝑘 ∈ ℕ ( ∀ 𝑖 ∈ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) 𝑖 ∥ 𝑘 → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ≤ 𝑘 ) ) ) )
177 106 107 176 mpbir2and ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) = ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) )
178 177 eqcomd ⊢ ( ( ( 0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) ) → ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) )