Metamath Proof Explorer

Theorem coprmproddvds

Description: If a positive integer is divisible by each element of a set of pairwise coprime positive integers, then it is divisible by their product. (Contributed by AV, 19-Aug-2020)

Ref Expression
Assertion coprmproddvds ⊢ M ⊆ ℕ ∧ M ∈ Fin ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ M ∀ n ∈ M ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ M F ⁡ m ∥ K → ∏ m ∈ M F ⁡ m ∥ K

Proof

Step Hyp Ref Expression
1 cleq1lem ⊢ x = ∅ → x ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ↔ ∅ ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ
2 difeq1 ⊢ x = ∅ → x ∖ m = ∅ ∖ m
3 2 raleqdv ⊢ x = ∅ → ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ↔ ∀ n ∈ ∅ ∖ m F ⁡ m gcd F ⁡ n = 1
4 3 raleqbi1dv ⊢ x = ∅ → ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ↔ ∀ m ∈ ∅ ∀ n ∈ ∅ ∖ m F ⁡ m gcd F ⁡ n = 1
5 raleq ⊢ x = ∅ → ∀ m ∈ x F ⁡ m ∥ K ↔ ∀ m ∈ ∅ F ⁡ m ∥ K
6 4 5 anbi12d ⊢ x = ∅ → ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ x F ⁡ m ∥ K ↔ ∀ m ∈ ∅ ∀ n ∈ ∅ ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ ∅ F ⁡ m ∥ K
7 1 6 anbi12d ⊢ x = ∅ → x ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ x F ⁡ m ∥ K ↔ ∅ ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ ∅ ∀ n ∈ ∅ ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ ∅ F ⁡ m ∥ K
8 prodeq1 ⊢ x = ∅ → ∏ m ∈ x F ⁡ m = ∏ m ∈ ∅ F ⁡ m
9 8 breq1d ⊢ x = ∅ → ∏ m ∈ x F ⁡ m ∥ K ↔ ∏ m ∈ ∅ F ⁡ m ∥ K
10 7 9 imbi12d ⊢ x = ∅ → x ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ x F ⁡ m ∥ K → ∏ m ∈ x F ⁡ m ∥ K ↔ ∅ ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ ∅ ∀ n ∈ ∅ ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ ∅ F ⁡ m ∥ K → ∏ m ∈ ∅ F ⁡ m ∥ K
11 cleq1lem ⊢ x = y → x ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ↔ y ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ
12 difeq1 ⊢ x = y → x ∖ m = y ∖ m
13 12 raleqdv ⊢ x = y → ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ↔ ∀ n ∈ y ∖ m F ⁡ m gcd F ⁡ n = 1
14 13 raleqbi1dv ⊢ x = y → ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ↔ ∀ m ∈ y ∀ n ∈ y ∖ m F ⁡ m gcd F ⁡ n = 1
15 raleq ⊢ x = y → ∀ m ∈ x F ⁡ m ∥ K ↔ ∀ m ∈ y F ⁡ m ∥ K
16 14 15 anbi12d ⊢ x = y → ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ x F ⁡ m ∥ K ↔ ∀ m ∈ y ∀ n ∈ y ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ y F ⁡ m ∥ K
17 11 16 anbi12d ⊢ x = y → x ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ x F ⁡ m ∥ K ↔ y ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ y ∀ n ∈ y ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ y F ⁡ m ∥ K
18 prodeq1 ⊢ x = y → ∏ m ∈ x F ⁡ m = ∏ m ∈ y F ⁡ m
19 18 breq1d ⊢ x = y → ∏ m ∈ x F ⁡ m ∥ K ↔ ∏ m ∈ y F ⁡ m ∥ K
20 17 19 imbi12d ⊢ x = y → x ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ x F ⁡ m ∥ K → ∏ m ∈ x F ⁡ m ∥ K ↔ y ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ y ∀ n ∈ y ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ y F ⁡ m ∥ K → ∏ m ∈ y F ⁡ m ∥ K
21 cleq1lem ⊢ x = y ∪ z → x ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ↔ y ∪ z ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ
22 difeq1 ⊢ x = y ∪ z → x ∖ m = y ∪ z ∖ m
23 22 raleqdv ⊢ x = y ∪ z → ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ↔ ∀ n ∈ y ∪ z ∖ m F ⁡ m gcd F ⁡ n = 1
24 23 raleqbi1dv ⊢ x = y ∪ z → ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ↔ ∀ m ∈ y ∪ z ∀ n ∈ y ∪ z ∖ m F ⁡ m gcd F ⁡ n = 1
25 raleq ⊢ x = y ∪ z → ∀ m ∈ x F ⁡ m ∥ K ↔ ∀ m ∈ y ∪ z F ⁡ m ∥ K
26 24 25 anbi12d ⊢ x = y ∪ z → ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ x F ⁡ m ∥ K ↔ ∀ m ∈ y ∪ z ∀ n ∈ y ∪ z ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ y ∪ z F ⁡ m ∥ K
27 21 26 anbi12d ⊢ x = y ∪ z → x ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ x F ⁡ m ∥ K ↔ y ∪ z ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ y ∪ z ∀ n ∈ y ∪ z ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ y ∪ z F ⁡ m ∥ K
28 prodeq1 ⊢ x = y ∪ z → ∏ m ∈ x F ⁡ m = ∏ m ∈ y ∪ z F ⁡ m
29 28 breq1d ⊢ x = y ∪ z → ∏ m ∈ x F ⁡ m ∥ K ↔ ∏ m ∈ y ∪ z F ⁡ m ∥ K
30 27 29 imbi12d ⊢ x = y ∪ z → x ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ x F ⁡ m ∥ K → ∏ m ∈ x F ⁡ m ∥ K ↔ y ∪ z ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ y ∪ z ∀ n ∈ y ∪ z ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ y ∪ z F ⁡ m ∥ K → ∏ m ∈ y ∪ z F ⁡ m ∥ K
31 cleq1lem ⊢ x = M → x ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ↔ M ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ
32 difeq1 ⊢ x = M → x ∖ m = M ∖ m
33 32 raleqdv ⊢ x = M → ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ↔ ∀ n ∈ M ∖ m F ⁡ m gcd F ⁡ n = 1
34 33 raleqbi1dv ⊢ x = M → ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ↔ ∀ m ∈ M ∀ n ∈ M ∖ m F ⁡ m gcd F ⁡ n = 1
35 raleq ⊢ x = M → ∀ m ∈ x F ⁡ m ∥ K ↔ ∀ m ∈ M F ⁡ m ∥ K
36 34 35 anbi12d ⊢ x = M → ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ x F ⁡ m ∥ K ↔ ∀ m ∈ M ∀ n ∈ M ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ M F ⁡ m ∥ K
37 31 36 anbi12d ⊢ x = M → x ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ x F ⁡ m ∥ K ↔ M ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ M ∀ n ∈ M ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ M F ⁡ m ∥ K
38 prodeq1 ⊢ x = M → ∏ m ∈ x F ⁡ m = ∏ m ∈ M F ⁡ m
39 38 breq1d ⊢ x = M → ∏ m ∈ x F ⁡ m ∥ K ↔ ∏ m ∈ M F ⁡ m ∥ K
40 37 39 imbi12d ⊢ x = M → x ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ x ∀ n ∈ x ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ x F ⁡ m ∥ K → ∏ m ∈ x F ⁡ m ∥ K ↔ M ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ M ∀ n ∈ M ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ M F ⁡ m ∥ K → ∏ m ∈ M F ⁡ m ∥ K
41 prod0 ⊢ ∏ m ∈ ∅ F ⁡ m = 1
42 nnz ⊢ K ∈ ℕ → K ∈ ℤ
43 1dvds ⊢ K ∈ ℤ → 1 ∥ K
44 42 43 syl ⊢ K ∈ ℕ → 1 ∥ K
45 41 44 eqbrtrid ⊢ K ∈ ℕ → ∏ m ∈ ∅ F ⁡ m ∥ K
46 45 adantr ⊢ K ∈ ℕ ∧ F : ℕ ⟶ ℕ → ∏ m ∈ ∅ F ⁡ m ∥ K
47 46 ad2antlr ⊢ ∅ ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ ∅ ∀ n ∈ ∅ ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ ∅ F ⁡ m ∥ K → ∏ m ∈ ∅ F ⁡ m ∥ K
48 coprmproddvdslem ⊢ y ∈ Fin ∧ ¬ z ∈ y → y ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ y ∀ n ∈ y ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ y F ⁡ m ∥ K → ∏ m ∈ y F ⁡ m ∥ K → y ∪ z ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ y ∪ z ∀ n ∈ y ∪ z ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ y ∪ z F ⁡ m ∥ K → ∏ m ∈ y ∪ z F ⁡ m ∥ K
49 10 20 30 40 47 48 findcard2s ⊢ M ∈ Fin → M ⊆ ℕ ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ M ∀ n ∈ M ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ M F ⁡ m ∥ K → ∏ m ∈ M F ⁡ m ∥ K
50 49 exp4c ⊢ M ∈ Fin → M ⊆ ℕ → K ∈ ℕ ∧ F : ℕ ⟶ ℕ → ∀ m ∈ M ∀ n ∈ M ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ M F ⁡ m ∥ K → ∏ m ∈ M F ⁡ m ∥ K
51 50 impcom ⊢ M ⊆ ℕ ∧ M ∈ Fin → K ∈ ℕ ∧ F : ℕ ⟶ ℕ → ∀ m ∈ M ∀ n ∈ M ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ M F ⁡ m ∥ K → ∏ m ∈ M F ⁡ m ∥ K
52 51 3imp ⊢ M ⊆ ℕ ∧ M ∈ Fin ∧ K ∈ ℕ ∧ F : ℕ ⟶ ℕ ∧ ∀ m ∈ M ∀ n ∈ M ∖ m F ⁡ m gcd F ⁡ n = 1 ∧ ∀ m ∈ M F ⁡ m ∥ K → ∏ m ∈ M F ⁡ m ∥ K