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 ⊢ Y ⊆ ℤ ∧ Y ∈ Fin → ∀ k ∈ ℤ ∀ m ∈ Y m ∥ k → lcm _ ⁡ Y ∥ k ∧ ∀ n ∈ ℤ lcm _ ⁡ Y ∪ n = lcm _ ⁡ Y lcm n

Proof

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