Metamath Proof Explorer

Theorem lcmfun

Description: The _lcm function for a union of sets of integers. (Contributed by AV, 27-Aug-2020)

Ref Expression
Assertion lcmfun ( ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑍 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 cleq1lem ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ↔ ( ∅ ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) )
2 uneq2 ⊢ ( 𝑥 = ∅ → ( 𝑌 ∪ 𝑥 ) = ( 𝑌 ∪ ∅ ) )
3 un0 ⊢ ( 𝑌 ∪ ∅ ) = 𝑌
4 2 3 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝑌 ∪ 𝑥 ) = 𝑌 )
5 4 fveq2d ⊢ ( 𝑥 = ∅ → ( lcm ‘ ( 𝑌 ∪ 𝑥 ) ) = ( lcm ‘ 𝑌 ) )
6 fveq2 ⊢ ( 𝑥 = ∅ → ( lcm ‘ 𝑥 ) = ( lcm ‘ ∅ ) )
7 lcmf0 ⊢ ( lcm ‘ ∅ ) = 1
8 6 7 eqtrdi ⊢ ( 𝑥 = ∅ → ( lcm ‘ 𝑥 ) = 1 )
9 8 oveq2d ⊢ ( 𝑥 = ∅ → ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑥 ) ) = ( ( lcm ‘ 𝑌 ) lcm 1 ) )
10 5 9 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( lcm ‘ ( 𝑌 ∪ 𝑥 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑥 ) ) ↔ ( lcm ‘ 𝑌 ) = ( ( lcm ‘ 𝑌 ) lcm 1 ) ) )
11 1 10 imbi12d ⊢ ( 𝑥 = ∅ → ( ( ( 𝑥 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑥 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑥 ) ) ) ↔ ( ( ∅ ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ 𝑌 ) = ( ( lcm ‘ 𝑌 ) lcm 1 ) ) ) )
12 cleq1lem ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ↔ ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) )
13 uneq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑌 ∪ 𝑥 ) = ( 𝑌 ∪ 𝑦 ) )
14 13 fveq2d ⊢ ( 𝑥 = 𝑦 → ( lcm ‘ ( 𝑌 ∪ 𝑥 ) ) = ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) )
15 fveq2 ⊢ ( 𝑥 = 𝑦 → ( lcm ‘ 𝑥 ) = ( lcm ‘ 𝑦 ) )
16 15 oveq2d ⊢ ( 𝑥 = 𝑦 → ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑥 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) )
17 14 16 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( lcm ‘ ( 𝑌 ∪ 𝑥 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑥 ) ) ↔ ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) )
18 12 17 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑥 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑥 ) ) ) ↔ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) )
19 cleq1lem ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑥 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ↔ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) )
20 uneq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑌 ∪ 𝑥 ) = ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) )
21 20 fveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( lcm ‘ ( 𝑌 ∪ 𝑥 ) ) = ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) )
22 fveq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( lcm ‘ 𝑥 ) = ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) )
23 22 oveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑥 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) )
24 21 23 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( lcm ‘ ( 𝑌 ∪ 𝑥 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑥 ) ) ↔ ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) )
25 19 24 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ( 𝑥 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑥 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑥 ) ) ) ↔ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) )
26 cleq1lem ⊢ ( 𝑥 = 𝑍 → ( ( 𝑥 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ↔ ( 𝑍 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) )
27 uneq2 ⊢ ( 𝑥 = 𝑍 → ( 𝑌 ∪ 𝑥 ) = ( 𝑌 ∪ 𝑍 ) )
28 27 fveq2d ⊢ ( 𝑥 = 𝑍 → ( lcm ‘ ( 𝑌 ∪ 𝑥 ) ) = ( lcm ‘ ( 𝑌 ∪ 𝑍 ) ) )
29 fveq2 ⊢ ( 𝑥 = 𝑍 → ( lcm ‘ 𝑥 ) = ( lcm ‘ 𝑍 ) )
30 29 oveq2d ⊢ ( 𝑥 = 𝑍 → ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑥 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑍 ) ) )
31 28 30 eqeq12d ⊢ ( 𝑥 = 𝑍 → ( ( lcm ‘ ( 𝑌 ∪ 𝑥 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑥 ) ) ↔ ( lcm ‘ ( 𝑌 ∪ 𝑍 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑍 ) ) ) )
32 26 31 imbi12d ⊢ ( 𝑥 = 𝑍 → ( ( ( 𝑥 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑥 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑥 ) ) ) ↔ ( ( 𝑍 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑍 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑍 ) ) ) ) )
33 lcmfcl ⊢ ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → ( lcm ‘ 𝑌 ) ∈ ℕ0 )
34 33 nn0zd ⊢ ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → ( lcm ‘ 𝑌 ) ∈ ℤ )
35 lcm1 ⊢ ( ( lcm ‘ 𝑌 ) ∈ ℤ → ( ( lcm ‘ 𝑌 ) lcm 1 ) = ( abs ‘ ( lcm ‘ 𝑌 ) ) )
36 34 35 syl ⊢ ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → ( ( lcm ‘ 𝑌 ) lcm 1 ) = ( abs ‘ ( lcm ‘ 𝑌 ) ) )
37 nn0re ⊢ ( ( lcm ‘ 𝑌 ) ∈ ℕ0 → ( lcm ‘ 𝑌 ) ∈ ℝ )
38 nn0ge0 ⊢ ( ( lcm ‘ 𝑌 ) ∈ ℕ0 → 0 ≤ ( lcm ‘ 𝑌 ) )
39 37 38 jca ⊢ ( ( lcm ‘ 𝑌 ) ∈ ℕ0 → ( ( lcm ‘ 𝑌 ) ∈ ℝ ∧ 0 ≤ ( lcm ‘ 𝑌 ) ) )
40 33 39 syl ⊢ ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → ( ( lcm ‘ 𝑌 ) ∈ ℝ ∧ 0 ≤ ( lcm ‘ 𝑌 ) ) )
41 absid ⊢ ( ( ( lcm ‘ 𝑌 ) ∈ ℝ ∧ 0 ≤ ( lcm ‘ 𝑌 ) ) → ( abs ‘ ( lcm ‘ 𝑌 ) ) = ( lcm ‘ 𝑌 ) )
42 40 41 syl ⊢ ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → ( abs ‘ ( lcm ‘ 𝑌 ) ) = ( lcm ‘ 𝑌 ) )
43 36 42 eqtrd ⊢ ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → ( ( lcm ‘ 𝑌 ) lcm 1 ) = ( lcm ‘ 𝑌 ) )
44 43 adantl ⊢ ( ( ∅ ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( ( lcm ‘ 𝑌 ) lcm 1 ) = ( lcm ‘ 𝑌 ) )
45 44 eqcomd ⊢ ( ( ∅ ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ 𝑌 ) = ( ( lcm ‘ 𝑌 ) lcm 1 ) )
46 unass ⊢ ( ( 𝑌 ∪ 𝑦 ) ∪ { 𝑧 } ) = ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) )
47 46 eqcomi ⊢ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( 𝑌 ∪ 𝑦 ) ∪ { 𝑧 } )
48 47 a1i ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( 𝑌 ∪ 𝑦 ) ∪ { 𝑧 } ) )
49 48 fveq2d ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( lcm ‘ ( ( 𝑌 ∪ 𝑦 ) ∪ { 𝑧 } ) ) )
50 simpl ⊢ ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → 𝑌 ⊆ ℤ )
51 50 adantl ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → 𝑌 ⊆ ℤ )
52 unss ⊢ ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) ↔ ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ )
53 simpl ⊢ ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) → 𝑦 ⊆ ℤ )
54 52 53 sylbir ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ → 𝑦 ⊆ ℤ )
55 54 adantr ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → 𝑦 ⊆ ℤ )
56 51 55 unssd ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( 𝑌 ∪ 𝑦 ) ⊆ ℤ )
57 56 adantl ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( 𝑌 ∪ 𝑦 ) ⊆ ℤ )
58 unfi ⊢ ( ( 𝑌 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( 𝑌 ∪ 𝑦 ) ∈ Fin )
59 58 ex ⊢ ( 𝑌 ∈ Fin → ( 𝑦 ∈ Fin → ( 𝑌 ∪ 𝑦 ) ∈ Fin ) )
60 59 adantl ⊢ ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → ( 𝑦 ∈ Fin → ( 𝑌 ∪ 𝑦 ) ∈ Fin ) )
61 60 adantl ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( 𝑦 ∈ Fin → ( 𝑌 ∪ 𝑦 ) ∈ Fin ) )
62 61 impcom ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( 𝑌 ∪ 𝑦 ) ∈ Fin )
63 vex ⊢ 𝑧 ∈ V
64 63 snss ⊢ ( 𝑧 ∈ ℤ ↔ { 𝑧 } ⊆ ℤ )
65 64 bilanri ⊢ ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) → 𝑧 ∈ ℤ )
66 52 65 sylbir ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ → 𝑧 ∈ ℤ )
67 66 adantr ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → 𝑧 ∈ ℤ )
68 67 adantl ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → 𝑧 ∈ ℤ )
69 lcmfunsn ⊢ ( ( ( 𝑌 ∪ 𝑦 ) ⊆ ℤ ∧ ( 𝑌 ∪ 𝑦 ) ∈ Fin ∧ 𝑧 ∈ ℤ ) → ( lcm ‘ ( ( 𝑌 ∪ 𝑦 ) ∪ { 𝑧 } ) ) = ( ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) lcm 𝑧 ) )
70 57 62 68 69 syl3anc ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ ( ( 𝑌 ∪ 𝑦 ) ∪ { 𝑧 } ) ) = ( ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) lcm 𝑧 ) )
71 49 70 eqtrd ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) lcm 𝑧 ) )
72 71 adantr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) lcm 𝑧 ) )
73 54 anim1i ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) )
74 73 adantl ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) )
75 id ⊢ ( ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) → ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) )
76 74 75 mpan9 ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) )
77 76 oveq1d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) lcm 𝑧 ) = ( ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) lcm 𝑧 ) )
78 34 adantl ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ 𝑌 ) ∈ ℤ )
79 78 adantl ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ 𝑌 ) ∈ ℤ )
80 55 anim2i ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( 𝑦 ∈ Fin ∧ 𝑦 ⊆ ℤ ) )
81 80 ancomd ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) )
82 lcmfcl ⊢ ( ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℕ0 )
83 81 82 syl ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ 𝑦 ) ∈ ℕ0 )
84 83 nn0zd ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ 𝑦 ) ∈ ℤ )
85 lcmass ⊢ ( ( ( lcm ‘ 𝑌 ) ∈ ℤ ∧ ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) lcm 𝑧 ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
86 79 84 68 85 syl3anc ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) lcm 𝑧 ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
87 86 adantr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) lcm 𝑧 ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
88 77 87 eqtrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) lcm 𝑧 ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
89 72 88 eqtrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
90 53 adantr ⊢ ( ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) ∧ 𝑦 ∈ Fin ) → 𝑦 ⊆ ℤ )
91 simpr ⊢ ( ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) ∧ 𝑦 ∈ Fin ) → 𝑦 ∈ Fin )
92 65 adantr ⊢ ( ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) ∧ 𝑦 ∈ Fin ) → 𝑧 ∈ ℤ )
93 90 91 92 3jca ⊢ ( ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) ∧ 𝑦 ∈ Fin ) → ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ ) )
94 93 ex ⊢ ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) → ( 𝑦 ∈ Fin → ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ ) ) )
95 52 94 sylbir ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ → ( 𝑦 ∈ Fin → ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ ) ) )
96 95 adantr ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( 𝑦 ∈ Fin → ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ ) ) )
97 96 impcom ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ ) )
98 lcmfunsn ⊢ ( ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) )
99 97 98 syl ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) )
100 99 oveq2d ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
101 100 eqeq2d ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ↔ ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) ) )
102 101 adantr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ↔ ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) ) )
103 89 102 mpbird ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) )
104 103 exp31 ⊢ ( 𝑦 ∈ Fin → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) )
105 104 com23 ⊢ ( 𝑦 ∈ Fin → ( ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) )
106 11 18 25 32 45 105 findcard2 ⊢ ( 𝑍 ∈ Fin → ( ( 𝑍 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑍 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑍 ) ) ) )
107 106 expd ⊢ ( 𝑍 ∈ Fin → ( 𝑍 ⊆ ℤ → ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → ( lcm ‘ ( 𝑌 ∪ 𝑍 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑍 ) ) ) ) )
108 107 impcom ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → ( lcm ‘ ( 𝑌 ∪ 𝑍 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑍 ) ) ) )
109 108 impcom ⊢ ( ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑍 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑍 ) ) )