Metamath Proof Explorer

Theorem lcmfunsnlem1

Description: Lemma for lcmfdvds and lcmfunsnlem (Induction step part 1). (Contributed by AV, 25-Aug-2020)

Ref Expression
Assertion 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

Proof

Step Hyp Ref Expression
1 nfv ⊢Ⅎkz∈ℤ∧y⊆ℤ∧y∈Fin
2 nfra1 ⊢Ⅎk∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k
3 nfv ⊢Ⅎk∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn
4 2 3 nfan ⊢Ⅎk∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn
5 1 4 nfan ⊢Ⅎkz∈ℤ∧y⊆ℤ∧y∈Fin∧∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn
6 breq2 ⊢k=l→m∥k↔m∥l
7 6 ralbidv ⊢k=l→∀m∈ym∥k↔∀m∈ym∥l
8 breq2 ⊢k=l→lcm_⁡y∥k↔lcm_⁡y∥l
9 7 8 imbi12d ⊢k=l→∀m∈ym∥k→lcm_⁡y∥k↔∀m∈ym∥l→lcm_⁡y∥l
10 9 cbvralvw ⊢∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k↔∀l∈ℤ∀m∈ym∥l→lcm_⁡y∥l
11 breq2 ⊢l=k→m∥l↔m∥k
12 11 ralbidv ⊢l=k→∀m∈ym∥l↔∀m∈ym∥k
13 breq2 ⊢l=k→lcm_⁡y∥l↔lcm_⁡y∥k
14 12 13 imbi12d ⊢l=k→∀m∈ym∥l→lcm_⁡y∥l↔∀m∈ym∥k→lcm_⁡y∥k
15 14 rspcv ⊢k∈ℤ→∀l∈ℤ∀m∈ym∥l→lcm_⁡y∥l→∀m∈ym∥k→lcm_⁡y∥k
16 15 adantl ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→∀l∈ℤ∀m∈ym∥l→lcm_⁡y∥l→∀m∈ym∥k→lcm_⁡y∥k
17 sneq ⊢n=z→n=z
18 17 uneq2d ⊢n=z→y∪n=y∪z
19 18 fveq2d ⊢n=z→lcm_⁡y∪n=lcm_⁡y∪z
20 oveq2 ⊢n=z→lcm_⁡ylcmn=lcm_⁡ylcmz
21 19 20 eqeq12d ⊢n=z→lcm_⁡y∪n=lcm_⁡ylcmn↔lcm_⁡y∪z=lcm_⁡ylcmz
22 21 rspcv ⊢z∈ℤ→∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→lcm_⁡y∪z=lcm_⁡ylcmz
23 22 3ad2ant1 ⊢z∈ℤ∧y⊆ℤ∧y∈Fin→∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→lcm_⁡y∪z=lcm_⁡ylcmz
24 23 adantr ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→lcm_⁡y∪z=lcm_⁡ylcmz
25 simpr ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→k∈ℤ
26 lcmfcl ⊢y⊆ℤ∧y∈Fin→lcm_⁡y∈ℕ0
27 26 nn0zd ⊢y⊆ℤ∧y∈Fin→lcm_⁡y∈ℤ
28 27 3adant1 ⊢z∈ℤ∧y⊆ℤ∧y∈Fin→lcm_⁡y∈ℤ
29 28 adantr ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→lcm_⁡y∈ℤ
30 simpl1 ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→z∈ℤ
31 25 29 30 3jca ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→k∈ℤ∧lcm_⁡y∈ℤ∧z∈ℤ
32 31 adantr ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ∧∀m∈ym∥k→lcm_⁡y∥k→k∈ℤ∧lcm_⁡y∈ℤ∧z∈ℤ
33 32 adantr ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ∧∀m∈ym∥k→lcm_⁡y∥k∧∀m∈y∪zm∥k→k∈ℤ∧lcm_⁡y∈ℤ∧z∈ℤ
34 ssun1 ⊢y⊆y∪z
35 ssralv ⊢y⊆y∪z→∀m∈y∪zm∥k→∀m∈ym∥k
36 34 35 mp1i ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→∀m∈y∪zm∥k→∀m∈ym∥k
37 36 imim1d ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→∀m∈ym∥k→lcm_⁡y∥k→∀m∈y∪zm∥k→lcm_⁡y∥k
38 37 imp31 ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ∧∀m∈ym∥k→lcm_⁡y∥k∧∀m∈y∪zm∥k→lcm_⁡y∥k
39 snidg ⊢z∈ℤ→z∈z
40 39 olcd ⊢z∈ℤ→z∈y∨z∈z
41 elun ⊢z∈y∪z↔z∈y∨z∈z
42 40 41 sylibr ⊢z∈ℤ→z∈y∪z
43 breq1 ⊢m=z→m∥k↔z∥k
44 43 rspcv ⊢z∈y∪z→∀m∈y∪zm∥k→z∥k
45 42 44 syl ⊢z∈ℤ→∀m∈y∪zm∥k→z∥k
46 45 3ad2ant1 ⊢z∈ℤ∧y⊆ℤ∧y∈Fin→∀m∈y∪zm∥k→z∥k
47 46 adantr ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→∀m∈y∪zm∥k→z∥k
48 47 adantr ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ∧∀m∈ym∥k→lcm_⁡y∥k→∀m∈y∪zm∥k→z∥k
49 48 imp ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ∧∀m∈ym∥k→lcm_⁡y∥k∧∀m∈y∪zm∥k→z∥k
50 38 49 jca ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ∧∀m∈ym∥k→lcm_⁡y∥k∧∀m∈y∪zm∥k→lcm_⁡y∥k∧z∥k
51 lcmdvds ⊢k∈ℤ∧lcm_⁡y∈ℤ∧z∈ℤ→lcm_⁡y∥k∧z∥k→lcm_⁡ylcmz∥k
52 33 50 51 sylc ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ∧∀m∈ym∥k→lcm_⁡y∥k∧∀m∈y∪zm∥k→lcm_⁡ylcmz∥k
53 breq1 ⊢lcm_⁡y∪z=lcm_⁡ylcmz→lcm_⁡y∪z∥k↔lcm_⁡ylcmz∥k
54 52 53 syl5ibrcom ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ∧∀m∈ym∥k→lcm_⁡y∥k∧∀m∈y∪zm∥k→lcm_⁡y∪z=lcm_⁡ylcmz→lcm_⁡y∪z∥k
55 54 ex ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ∧∀m∈ym∥k→lcm_⁡y∥k→∀m∈y∪zm∥k→lcm_⁡y∪z=lcm_⁡ylcmz→lcm_⁡y∪z∥k
56 55 com23 ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ∧∀m∈ym∥k→lcm_⁡y∥k→lcm_⁡y∪z=lcm_⁡ylcmz→∀m∈y∪zm∥k→lcm_⁡y∪z∥k
57 56 ex ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→∀m∈ym∥k→lcm_⁡y∥k→lcm_⁡y∪z=lcm_⁡ylcmz→∀m∈y∪zm∥k→lcm_⁡y∪z∥k
58 24 57 syl5d ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→∀m∈ym∥k→lcm_⁡y∥k→∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀m∈y∪zm∥k→lcm_⁡y∪z∥k
59 16 58 syld ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→∀l∈ℤ∀m∈ym∥l→lcm_⁡y∥l→∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀m∈y∪zm∥k→lcm_⁡y∪z∥k
60 10 59 biimtrid ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k→∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀m∈y∪zm∥k→lcm_⁡y∪z∥k
61 60 impd ⊢z∈ℤ∧y⊆ℤ∧y∈Fin∧k∈ℤ→∀k∈ℤ∀m∈ym∥k→lcm_⁡y∥k∧∀n∈ℤlcm_⁡y∪n=lcm_⁡ylcmn→∀m∈y∪zm∥k→lcm_⁡y∪z∥k
62 61 impancom ⊢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
63 5 62 ralrimi ⊢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