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∈Ym∥k→lcm_⁡Y∥k∧∀n∈ℤlcm_⁡Y∪n=lcm_⁡Ylcmn

Proof

Step Hyp Ref Expression
1 sseq1 ⊢x=∅→x⊆ℤ↔∅⊆ℤ
2 raleq ⊢x=∅→∀m∈xm∥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∈xm∥k→lcm_⁡x∥k↔∀m∈∅m∥k→lcm_⁡∅∥k
6 5 ralbidv ⊢x=∅→∀k∈ℤ∀m∈xm∥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_⁡xlcmn=lcm_⁡∅lcmn
10 8 9 eqeq12d ⊢x=∅→lcm_⁡x∪n=lcm_⁡xlcmn↔lcm_⁡∅∪n=lcm_⁡∅lcmn
11 10 ralbidv ⊢x=∅→∀n∈ℤlcm_⁡x∪n=lcm_⁡xlcmn↔∀n∈ℤlcm_⁡∅∪n=lcm_⁡∅lcmn
12 6 11 anbi12d ⊢x=∅→∀k∈ℤ∀m∈xm∥k→lcm_⁡x∥k∧∀n∈ℤlcm_⁡x∪n=lcm_⁡xlcmn↔∀k∈ℤ∀m∈∅m∥k→lcm_⁡∅∥k∧∀n∈ℤlcm_⁡∅∪n=lcm_⁡∅lcmn
13 1 12 imbi12d ⊢x=∅→x⊆ℤ→∀k∈ℤ∀m∈xm∥k→lcm_⁡x∥k∧∀n∈ℤlcm_⁡x∪n=lcm_⁡xlcmn↔∅⊆ℤ→∀k∈ℤ∀m∈∅m∥k→lcm_⁡∅∥k∧∀n∈ℤlcm_⁡∅∪n=lcm_⁡∅lcmn
14 sseq1 ⊢x=y→x⊆ℤ↔y⊆ℤ
15 raleq ⊢x=y→∀m∈xm∥k↔∀m∈ym∥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∈xm∥k→lcm_⁡x∥k↔∀m∈ym∥k→lcm_⁡y∥k
19 18 ralbidv ⊢x=y→∀k∈ℤ∀m∈xm∥k→lcm_⁡x∥k↔∀k∈ℤ∀m∈ym∥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_⁡xlcmn=lcm_⁡ylcmn
23 21 22 eqeq12d ⊢x=y→lcm_⁡x∪n=lcm_⁡xlcmn↔lcm_⁡y∪n=lcm_⁡ylcmn
24 23 ralbidv ⊢x=y→∀n∈ℤlcm_⁡x∪n=lcm_⁡xlcmn↔∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn
25 19 24 anbi12d ⊢x=y→∀k∈ℤ∀m∈xm∥k→lcm_⁡x∥k∧∀n∈ℤlcm_⁡x∪n=lcm_⁡xlcmn↔∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn
26 14 25 imbi12d ⊢x=y→x⊆ℤ→∀k∈ℤ∀m∈xm∥k→lcm_⁡x∥k∧∀n∈ℤlcm_⁡x∪n=lcm_⁡xlcmn↔y⊆ℤ→∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn
27 sseq1 ⊢x=y∪z→x⊆ℤ↔y∪z⊆ℤ
28 raleq ⊢x=y∪z→∀m∈xm∥k↔∀m∈y∪zm∥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∈xm∥k→lcm_⁡x∥k↔∀m∈y∪zm∥k→lcm_⁡y∪z∥k
32 31 ralbidv ⊢x=y∪z→∀k∈ℤ∀m∈xm∥k→lcm_⁡x∥k↔∀k∈ℤ∀m∈y∪zm∥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_⁡xlcmn=lcm_⁡y∪zlcmn
36 34 35 eqeq12d ⊢x=y∪z→lcm_⁡x∪n=lcm_⁡xlcmn↔lcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
37 36 ralbidv ⊢x=y∪z→∀n∈ℤlcm_⁡x∪n=lcm_⁡xlcmn↔∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
38 32 37 anbi12d ⊢x=y∪z→∀k∈ℤ∀m∈xm∥k→lcm_⁡x∥k∧∀n∈ℤlcm_⁡x∪n=lcm_⁡xlcmn↔∀k∈ℤ∀m∈y∪zm∥k→lcm_⁡y∪z∥k∧∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
39 27 38 imbi12d ⊢x=y∪z→x⊆ℤ→∀k∈ℤ∀m∈xm∥k→lcm_⁡x∥k∧∀n∈ℤlcm_⁡x∪n=lcm_⁡xlcmn↔y∪z⊆ℤ→∀k∈ℤ∀m∈y∪zm∥k→lcm_⁡y∪z∥k∧∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
40 sseq1 ⊢x=Y→x⊆ℤ↔Y⊆ℤ
41 raleq ⊢x=Y→∀m∈xm∥k↔∀m∈Ym∥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∈xm∥k→lcm_⁡x∥k↔∀m∈Ym∥k→lcm_⁡Y∥k
45 44 ralbidv ⊢x=Y→∀k∈ℤ∀m∈xm∥k→lcm_⁡x∥k↔∀k∈ℤ∀m∈Ym∥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_⁡xlcmn=lcm_⁡Ylcmn
49 47 48 eqeq12d ⊢x=Y→lcm_⁡x∪n=lcm_⁡xlcmn↔lcm_⁡Y∪n=lcm_⁡Ylcmn
50 49 ralbidv ⊢x=Y→∀n∈ℤlcm_⁡x∪n=lcm_⁡xlcmn↔∀n∈ℤlcm_⁡Y∪n=lcm_⁡Ylcmn
51 45 50 anbi12d ⊢x=Y→∀k∈ℤ∀m∈xm∥k→lcm_⁡x∥k∧∀n∈ℤlcm_⁡x∪n=lcm_⁡xlcmn↔∀k∈ℤ∀m∈Ym∥k→lcm_⁡Y∥k∧∀n∈ℤlcm_⁡Y∪n=lcm_⁡Ylcmn
52 40 51 imbi12d ⊢x=Y→x⊆ℤ→∀k∈ℤ∀m∈xm∥k→lcm_⁡x∥k∧∀n∈ℤlcm_⁡x∪n=lcm_⁡xlcmn↔Y⊆ℤ→∀k∈ℤ∀m∈Ym∥k→lcm_⁡Y∥k∧∀n∈ℤlcm_⁡Y∪n=lcm_⁡Ylcmn
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_⁡∅lcmn=1lcmn
67 1z ⊢1∈ℤ
68 lcmcom ⊢1∈ℤ∧n∈ℤ→1lcmn=nlcm1
69 67 68 mpan ⊢n∈ℤ→1lcmn=nlcm1
70 lcm1 ⊢n∈ℤ→nlcm1=n
71 66 69 70 3eqtrrd ⊢n∈ℤ→n=lcm_⁡∅lcmn
72 63 64 71 3eqtrd ⊢n∈ℤ→lcm_⁡∅∪n=lcm_⁡∅lcmn
73 72 adantl ⊢∅⊆ℤ∧n∈ℤ→lcm_⁡∅∪n=lcm_⁡∅lcmn
74 73 ralrimiva ⊢∅⊆ℤ→∀n∈ℤlcm_⁡∅∪n=lcm_⁡∅lcmn
75 58 74 jca ⊢∅⊆ℤ→∀k∈ℤ∀m∈∅m∥k→lcm_⁡∅∥k∧∀n∈ℤlcm_⁡∅∪n=lcm_⁡∅lcmn
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∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀k∈ℤ∀m∈y∪zm∥k→lcm_⁡y∪z∥k
83 lcmfunsnlem2 ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
84 82 83 jca ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀k∈ℤ∀m∈y∪zm∥k→lcm_⁡y∪z∥k∧∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
85 84 3exp1 ⊢z∈ℤ→y⊆ℤ→y∈Fin→∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀k∈ℤ∀m∈y∪zm∥k→lcm_⁡y∪z∥k∧∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
86 81 85 sylbir ⊢z⊆ℤ→y⊆ℤ→y∈Fin→∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀k∈ℤ∀m∈y∪zm∥k→lcm_⁡y∪z∥k∧∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
87 86 impcom ⊢y⊆ℤ∧z⊆ℤ→y∈Fin→∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀k∈ℤ∀m∈y∪zm∥k→lcm_⁡y∪z∥k∧∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
88 76 87 sylbir ⊢y∪z⊆ℤ→y∈Fin→∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀k∈ℤ∀m∈y∪zm∥k→lcm_⁡y∪z∥k∧∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
89 88 impcom ⊢y∈Fin∧y∪z⊆ℤ→∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀k∈ℤ∀m∈y∪zm∥k→lcm_⁡y∪z∥k∧∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
90 79 89 embantd ⊢y∈Fin∧y∪z⊆ℤ→y⊆ℤ→∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀k∈ℤ∀m∈y∪zm∥k→lcm_⁡y∪z∥k∧∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
91 90 ex ⊢y∈Fin→y∪z⊆ℤ→y⊆ℤ→∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀k∈ℤ∀m∈y∪zm∥k→lcm_⁡y∪z∥k∧∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
92 91 com23 ⊢y∈Fin→y⊆ℤ→∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→y∪z⊆ℤ→∀k∈ℤ∀m∈y∪zm∥k→lcm_⁡y∪z∥k∧∀n∈ℤlcm_⁡y∪z∪n=lcm_⁡y∪zlcmn
93 13 26 39 52 75 92 findcard2 ⊢Y∈Fin→Y⊆ℤ→∀k∈ℤ∀m∈Ym∥k→lcm_⁡Y∥k∧∀n∈ℤlcm_⁡Y∪n=lcm_⁡Ylcmn
94 93 impcom ⊢Y⊆ℤ∧Y∈Fin→∀k∈ℤ∀m∈Ym∥k→lcm_⁡Y∥k∧∀n∈ℤlcm_⁡Y∪n=lcm_⁡Ylcmn