fproddvdsd

Description: A finite product of integers is divisible by any of its factors. (Contributed by AV, 14-Aug-2020) (Proof shortened by AV, 2-Aug-2021)

	Ref	Expression
Hypotheses	fproddvdsd.f	$⊢ φ \to A \in Fin$
	fproddvdsd.s	$⊢ φ \to A \subseteq ℤ$
Assertion	fproddvdsd	$⊢ φ \to \forall x \in A x ∥ \prod_{k \in A} k$

Proof

Step	Hyp	Ref	Expression
1		fproddvdsd.f	$⊢ φ \to A \in Fin$
2		fproddvdsd.s	$⊢ φ \to A \subseteq ℤ$
3		f1oi	$⊢ ({I ↾}_{ℤ}) : ℤ \underset{1-1 onto}{⟶} ℤ$
4		f1of	$⊢ ({I ↾}_{ℤ}) : ℤ \underset{1-1 onto}{⟶} ℤ \to ({I ↾}_{ℤ}) : ℤ ⟶ ℤ$
5	3 4	mp1i	$⊢ φ \to ({I ↾}_{ℤ}) : ℤ ⟶ ℤ$
6	1 2 5	fprodfvdvdsd	$⊢ φ \to \forall x \in A ({I ↾}_{ℤ}) (x) ∥ \prod_{k \in A} ({I ↾}_{ℤ}) (k)$
7	2	sselda	$⊢ (φ \land x \in A) \to x \in ℤ$
8		fvresi	$⊢ x \in ℤ \to ({I ↾}_{ℤ}) (x) = x$
9	7 8	syl	$⊢ (φ \land x \in A) \to ({I ↾}_{ℤ}) (x) = x$
10	9	eqcomd	$⊢ (φ \land x \in A) \to x = ({I ↾}_{ℤ}) (x)$
11	2	sseld	$⊢ φ \to (k \in A \to k \in ℤ)$
12	11	adantr	$⊢ (φ \land x \in A) \to (k \in A \to k \in ℤ)$
13	12	imp	$⊢ ((φ \land x \in A) \land k \in A) \to k \in ℤ$
14		fvresi	$⊢ k \in ℤ \to ({I ↾}_{ℤ}) (k) = k$
15	13 14	syl	$⊢ ((φ \land x \in A) \land k \in A) \to ({I ↾}_{ℤ}) (k) = k$
16	15	eqcomd	$⊢ ((φ \land x \in A) \land k \in A) \to k = ({I ↾}_{ℤ}) (k)$
17	16	prodeq2dv	$⊢ (φ \land x \in A) \to \prod_{k \in A} k = \prod_{k \in A} ({I ↾}_{ℤ}) (k)$
18	10 17	breq12d	$⊢ (φ \land x \in A) \to (x ∥ \prod_{k \in A} k \leftrightarrow ({I ↾}_{ℤ}) (x) ∥ \prod_{k \in A} ({I ↾}_{ℤ}) (k))$
19	18	ralbidva	$⊢ φ \to (\forall x \in A x ∥ \prod_{k \in A} k \leftrightarrow \forall x \in A ({I ↾}_{ℤ}) (x) ∥ \prod_{k \in A} ({I ↾}_{ℤ}) (k))$
20	6 19	mpbird	$⊢ φ \to \forall x \in A x ∥ \prod_{k \in A} k$

Metamath Proof Explorer

Theorem fproddvdsd

Proof