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

Metamath Proof Explorer

Theorem lcmfunsnlem

Description: Lemma for lcmfdvds and lcmfunsn . These two theorems must be proven simultaneously by induction on the cardinality of a finite set Y , because they depend on each other. This can be seen by the two parts lcmfunsnlem1 and lcmfunsnlem2 of the induction step, each of them using both induction hypotheses. (Contributed by AV, 26-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 sseq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ⊆ ℤ ↔ ∅ ⊆ ℤ ) )
2 raleq ⊢ ( 𝑥 = ∅ → ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 ↔ ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑘 ) )
3 fveq2 ⊢ ( 𝑥 = ∅ → ( lcm ‘ 𝑥 ) = ( lcm ‘ ∅ ) )
4 3 breq1d ⊢ ( 𝑥 = ∅ → ( ( lcm ‘ 𝑥 ) ∥ 𝑘 ↔ ( lcm ‘ ∅ ) ∥ 𝑘 ) )
5 2 4 imbi12d ⊢ ( 𝑥 = ∅ → ( ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ↔ ( ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑘 → ( lcm ‘ ∅ ) ∥ 𝑘 ) ) )
6 5 ralbidv ⊢ ( 𝑥 = ∅ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ↔ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑘 → ( lcm ‘ ∅ ) ∥ 𝑘 ) ) )
7 uneq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ∪ { 𝑛 } ) = ( ∅ ∪ { 𝑛 } ) )
8 7 fveq2d ⊢ ( 𝑥 = ∅ → ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( lcm ‘ ( ∅ ∪ { 𝑛 } ) ) )
9 3 oveq1d ⊢ ( 𝑥 = ∅ → ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) = ( ( lcm ‘ ∅ ) lcm 𝑛 ) )
10 8 9 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ↔ ( lcm ‘ ( ∅ ∪ { 𝑛 } ) ) = ( ( lcm ‘ ∅ ) lcm 𝑛 ) ) )
11 10 ralbidv ⊢ ( 𝑥 = ∅ → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ↔ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ∅ ∪ { 𝑛 } ) ) = ( ( lcm ‘ ∅ ) lcm 𝑛 ) ) )
12 6 11 anbi12d ⊢ ( 𝑥 = ∅ → ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ) ↔ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑘 → ( lcm ‘ ∅ ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ∅ ∪ { 𝑛 } ) ) = ( ( lcm ‘ ∅ ) lcm 𝑛 ) ) ) )
13 1 12 imbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ) ) ↔ ( ∅ ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑘 → ( lcm ‘ ∅ ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ∅ ∪ { 𝑛 } ) ) = ( ( lcm ‘ ∅ ) lcm 𝑛 ) ) ) ) )
14 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ ℤ ↔ 𝑦 ⊆ ℤ ) )
15 raleq ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 ↔ ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 ) )
16 fveq2 ⊢ ( 𝑥 = 𝑦 → ( lcm ‘ 𝑥 ) = ( lcm ‘ 𝑦 ) )
17 16 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( lcm ‘ 𝑥 ) ∥ 𝑘 ↔ ( lcm ‘ 𝑦 ) ∥ 𝑘 ) )
18 15 17 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ↔ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) )
19 18 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ↔ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ) )
20 uneq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∪ { 𝑛 } ) = ( 𝑦 ∪ { 𝑛 } ) )
21 20 fveq2d ⊢ ( 𝑥 = 𝑦 → ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) )
22 16 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) )
23 21 22 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ↔ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) )
24 23 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ↔ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) )
25 19 24 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ) ↔ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) )
26 14 25 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ) ) ↔ ( 𝑦 ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) ) )
27 sseq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ⊆ ℤ ↔ ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ) )
28 raleq ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 ↔ ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 ) )
29 fveq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( lcm ‘ 𝑥 ) = ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) )
30 29 breq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( lcm ‘ 𝑥 ) ∥ 𝑘 ↔ ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) )
31 28 30 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ↔ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) )
32 31 ralbidv ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ↔ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ) )
33 uneq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ∪ { 𝑛 } ) = ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) )
34 33 fveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) )
35 29 oveq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) )
36 34 35 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ↔ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
37 36 ralbidv ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ↔ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
38 32 37 anbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ) ↔ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
39 27 38 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑥 ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ) ) ↔ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) ) )
40 sseq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 ⊆ ℤ ↔ 𝑌 ⊆ ℤ ) )
41 raleq ⊢ ( 𝑥 = 𝑌 → ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 ↔ ∀ 𝑚 ∈ 𝑌 𝑚 ∥ 𝑘 ) )
42 fveq2 ⊢ ( 𝑥 = 𝑌 → ( lcm ‘ 𝑥 ) = ( lcm ‘ 𝑌 ) )
43 42 breq1d ⊢ ( 𝑥 = 𝑌 → ( ( lcm ‘ 𝑥 ) ∥ 𝑘 ↔ ( lcm ‘ 𝑌 ) ∥ 𝑘 ) )
44 41 43 imbi12d ⊢ ( 𝑥 = 𝑌 → ( ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ↔ ( ∀ 𝑚 ∈ 𝑌 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑌 ) ∥ 𝑘 ) ) )
45 44 ralbidv ⊢ ( 𝑥 = 𝑌 → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ↔ ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑌 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑌 ) ∥ 𝑘 ) ) )
46 uneq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 ∪ { 𝑛 } ) = ( 𝑌 ∪ { 𝑛 } ) )
47 46 fveq2d ⊢ ( 𝑥 = 𝑌 → ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( lcm ‘ ( 𝑌 ∪ { 𝑛 } ) ) )
48 42 oveq1d ⊢ ( 𝑥 = 𝑌 → ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) = ( ( lcm ‘ 𝑌 ) lcm 𝑛 ) )
49 47 48 eqeq12d ⊢ ( 𝑥 = 𝑌 → ( ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ↔ ( lcm ‘ ( 𝑌 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑌 ) lcm 𝑛 ) ) )
50 49 ralbidv ⊢ ( 𝑥 = 𝑌 → ( ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ↔ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑌 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑌 ) lcm 𝑛 ) ) )
51 45 50 anbi12d ⊢ ( 𝑥 = 𝑌 → ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ) ↔ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑌 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑌 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑌 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑌 ) lcm 𝑛 ) ) ) )
52 40 51 imbi12d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑥 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑥 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑥 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑥 ) lcm 𝑛 ) ) ) ↔ ( 𝑌 ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑌 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑌 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑌 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑌 ) lcm 𝑛 ) ) ) ) )
53 lcmf0 ⊢ ( lcm ‘ ∅ ) = 1
54 1dvds ⊢ ( 𝑘 ∈ ℤ → 1 ∥ 𝑘 )
55 53 54 eqbrtrid ⊢ ( 𝑘 ∈ ℤ → ( lcm ‘ ∅ ) ∥ 𝑘 )
56 55 a1d ⊢ ( 𝑘 ∈ ℤ → ( ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑘 → ( lcm ‘ ∅ ) ∥ 𝑘 ) )
57 56 adantl ⊢ ( ( ∅ ⊆ ℤ ∧ 𝑘 ∈ ℤ ) → ( ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑘 → ( lcm ‘ ∅ ) ∥ 𝑘 ) )
58 57 ralrimiva ⊢ ( ∅ ⊆ ℤ → ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑘 → ( lcm ‘ ∅ ) ∥ 𝑘 ) )
59 uncom ⊢ ( ∅ ∪ { 𝑛 } ) = ( { 𝑛 } ∪ ∅ )
60 un0 ⊢ ( { 𝑛 } ∪ ∅ ) = { 𝑛 }
61 59 60 eqtri ⊢ ( ∅ ∪ { 𝑛 } ) = { 𝑛 }
62 61 a1i ⊢ ( 𝑛 ∈ ℤ → ( ∅ ∪ { 𝑛 } ) = { 𝑛 } )
63 62 fveq2d ⊢ ( 𝑛 ∈ ℤ → ( lcm ‘ ( ∅ ∪ { 𝑛 } ) ) = ( lcm ‘ { 𝑛 } ) )
64 lcmfsn ⊢ ( 𝑛 ∈ ℤ → ( lcm ‘ { 𝑛 } ) = ( abs ‘ 𝑛 ) )
65 53 a1i ⊢ ( 𝑛 ∈ ℤ → ( lcm ‘ ∅ ) = 1 )
66 65 oveq1d ⊢ ( 𝑛 ∈ ℤ → ( ( lcm ‘ ∅ ) lcm 𝑛 ) = ( 1 lcm 𝑛 ) )
67 1z ⊢ 1 ∈ ℤ
68 lcmcom ⊢ ( ( 1 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 1 lcm 𝑛 ) = ( 𝑛 lcm 1 ) )
69 67 68 mpan ⊢ ( 𝑛 ∈ ℤ → ( 1 lcm 𝑛 ) = ( 𝑛 lcm 1 ) )
70 lcm1 ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 lcm 1 ) = ( abs ‘ 𝑛 ) )
71 66 69 70 3eqtrrd ⊢ ( 𝑛 ∈ ℤ → ( abs ‘ 𝑛 ) = ( ( lcm ‘ ∅ ) lcm 𝑛 ) )
72 63 64 71 3eqtrd ⊢ ( 𝑛 ∈ ℤ → ( lcm ‘ ( ∅ ∪ { 𝑛 } ) ) = ( ( lcm ‘ ∅ ) lcm 𝑛 ) )
73 72 adantl ⊢ ( ( ∅ ⊆ ℤ ∧ 𝑛 ∈ ℤ ) → ( lcm ‘ ( ∅ ∪ { 𝑛 } ) ) = ( ( lcm ‘ ∅ ) lcm 𝑛 ) )
74 73 ralrimiva ⊢ ( ∅ ⊆ ℤ → ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ∅ ∪ { 𝑛 } ) ) = ( ( lcm ‘ ∅ ) lcm 𝑛 ) )
75 58 74 jca ⊢ ( ∅ ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ∅ 𝑚 ∥ 𝑘 → ( lcm ‘ ∅ ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ∅ ∪ { 𝑛 } ) ) = ( ( lcm ‘ ∅ ) lcm 𝑛 ) ) )
76 unss ⊢ ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) ↔ ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ )
77 simpl ⊢ ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) → 𝑦 ⊆ ℤ )
78 76 77 sylbir ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ → 𝑦 ⊆ ℤ )
79 78 adantl ⊢ ( ( 𝑦 ∈ Fin ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ) → 𝑦 ⊆ ℤ )
80 vex ⊢ 𝑧 ∈ V
81 80 snss ⊢ ( 𝑧 ∈ ℤ ↔ { 𝑧 } ⊆ ℤ )
82 lcmfunsnlem1 ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) )
83 lcmfunsnlem2 ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) )
84 82 83 jca ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) ∧ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) )
85 84 3exp1 ⊢ ( 𝑧 ∈ ℤ → ( 𝑦 ⊆ ℤ → ( 𝑦 ∈ Fin → ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) ) ) )
86 81 85 sylbir ⊢ ( { 𝑧 } ⊆ ℤ → ( 𝑦 ⊆ ℤ → ( 𝑦 ∈ Fin → ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) ) ) )
87 86 impcom ⊢ ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) → ( 𝑦 ∈ Fin → ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) ) )
88 76 87 sylbir ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ → ( 𝑦 ∈ Fin → ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) ) )
89 88 impcom ⊢ ( ( 𝑦 ∈ Fin ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ) → ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
90 79 89 embantd ⊢ ( ( 𝑦 ∈ Fin ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ) → ( ( 𝑦 ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) )
91 90 ex ⊢ ( 𝑦 ∈ Fin → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ → ( ( 𝑦 ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) ) )
92 91 com23 ⊢ ( 𝑦 ∈ Fin → ( ( 𝑦 ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑦 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑦 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑛 ) ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝑚 ∥ 𝑘 → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( ( 𝑦 ∪ { 𝑧 } ) ∪ { 𝑛 } ) ) = ( ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) lcm 𝑛 ) ) ) ) )
93 13 26 39 52 75 92 findcard2 ⊢ ( 𝑌 ∈ Fin → ( 𝑌 ⊆ ℤ → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑌 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑌 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑌 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑌 ) lcm 𝑛 ) ) ) )
94 93 impcom ⊢ ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑌 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑌 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑌 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑌 ) lcm 𝑛 ) ) )