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 biimpri ⊢ ( { 𝑧 } ⊆ ℤ → 𝑧 ∈ ℤ )
66 65 adantl ⊢ ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) → 𝑧 ∈ ℤ )
67 52 66 sylbir ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ → 𝑧 ∈ ℤ )
68 67 adantr ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → 𝑧 ∈ ℤ )
69 68 adantl ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → 𝑧 ∈ ℤ )
70 lcmfunsn ⊢ ( ( ( 𝑌 ∪ 𝑦 ) ⊆ ℤ ∧ ( 𝑌 ∪ 𝑦 ) ∈ Fin ∧ 𝑧 ∈ ℤ ) → ( lcm ‘ ( ( 𝑌 ∪ 𝑦 ) ∪ { 𝑧 } ) ) = ( ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) lcm 𝑧 ) )
71 57 62 69 70 syl3anc ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ ( ( 𝑌 ∪ 𝑦 ) ∪ { 𝑧 } ) ) = ( ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) lcm 𝑧 ) )
72 49 71 eqtrd ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) lcm 𝑧 ) )
73 72 adantr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) lcm 𝑧 ) )
74 54 anim1i ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) )
75 74 adantl ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) )
76 id ⊢ ( ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) → ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) )
77 75 76 mpan9 ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) )
78 77 oveq1d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) lcm 𝑧 ) = ( ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) lcm 𝑧 ) )
79 34 adantl ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ 𝑌 ) ∈ ℤ )
80 79 adantl ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ 𝑌 ) ∈ ℤ )
81 55 anim2i ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( 𝑦 ∈ Fin ∧ 𝑦 ⊆ ℤ ) )
82 81 ancomd ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) )
83 lcmfcl ⊢ ( ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ) → ( lcm ‘ 𝑦 ) ∈ ℕ0 )
84 82 83 syl ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ 𝑦 ) ∈ ℕ0 )
85 84 nn0zd ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ 𝑦 ) ∈ ℤ )
86 lcmass ⊢ ( ( ( lcm ‘ 𝑌 ) ∈ ℤ ∧ ( lcm ‘ 𝑦 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) lcm 𝑧 ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
87 80 85 69 86 syl3anc ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) lcm 𝑧 ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
88 87 adantr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) lcm 𝑧 ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
89 78 88 eqtrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) lcm 𝑧 ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
90 73 89 eqtrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
91 53 adantr ⊢ ( ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) ∧ 𝑦 ∈ Fin ) → 𝑦 ⊆ ℤ )
92 simpr ⊢ ( ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) ∧ 𝑦 ∈ Fin ) → 𝑦 ∈ Fin )
93 66 adantr ⊢ ( ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) ∧ 𝑦 ∈ Fin ) → 𝑧 ∈ ℤ )
94 91 92 93 3jca ⊢ ( ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) ∧ 𝑦 ∈ Fin ) → ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ ) )
95 94 ex ⊢ ( ( 𝑦 ⊆ ℤ ∧ { 𝑧 } ⊆ ℤ ) → ( 𝑦 ∈ Fin → ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ ) ) )
96 52 95 sylbir ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ → ( 𝑦 ∈ Fin → ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ ) ) )
97 96 adantr ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( 𝑦 ∈ Fin → ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ ) ) )
98 97 impcom ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ ) )
99 lcmfunsn ⊢ ( ( 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) )
100 98 99 syl ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) )
101 100 oveq2d ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) )
102 101 eqeq2d ⊢ ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) → ( ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ↔ ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) ) )
103 102 adantr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ↔ ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( ( lcm ‘ 𝑦 ) lcm 𝑧 ) ) ) )
104 90 103 mpbird ⊢ ( ( ( 𝑦 ∈ Fin ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) ) ∧ ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) )
105 104 exp31 ⊢ ( 𝑦 ∈ Fin → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) )
106 105 com23 ⊢ ( 𝑦 ∈ Fin → ( ( ( 𝑦 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑦 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑦 ) ) ) → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) )
107 11 18 25 32 45 106 findcard2 ⊢ ( 𝑍 ∈ Fin → ( ( 𝑍 ⊆ ℤ ∧ ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑍 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑍 ) ) ) )
108 107 expd ⊢ ( 𝑍 ∈ Fin → ( 𝑍 ⊆ ℤ → ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → ( lcm ‘ ( 𝑌 ∪ 𝑍 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑍 ) ) ) ) )
109 108 impcom ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) → ( lcm ‘ ( 𝑌 ∪ 𝑍 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑍 ) ) ) )
110 109 impcom ⊢ ( ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ) → ( lcm ‘ ( 𝑌 ∪ 𝑍 ) ) = ( ( lcm ‘ 𝑌 ) lcm ( lcm ‘ 𝑍 ) ) )