fprodfvdvdsd

Description: A finite product of integers is divisible by any of its factors being function values. (Contributed by AV, 1-Aug-2021)

	Ref	Expression
Hypotheses	fprodfvdvdsd.a	$⊢ φ \to A \in Fin$
	fprodfvdvdsd.b	$⊢ φ \to A \subseteq B$
	fprodfvdvdsd.f	$⊢ φ \to F : B ⟶ ℤ$
Assertion	fprodfvdvdsd	$⊢ φ \to \forall x \in A F (x) ∥ \prod_{k \in A} F (k)$

Proof

Step	Hyp	Ref	Expression
1		fprodfvdvdsd.a	$⊢ φ \to A \in Fin$
2		fprodfvdvdsd.b	$⊢ φ \to A \subseteq B$
3		fprodfvdvdsd.f	$⊢ φ \to F : B ⟶ ℤ$
4	1	adantr	$⊢ (φ \land x \in A) \to A \in Fin$
5		diffi	$⊢ A \in Fin \to A ∖ \{x\} \in Fin$
6	4 5	syl	$⊢ (φ \land x \in A) \to A ∖ \{x\} \in Fin$
7	3	adantr	$⊢ (φ \land k \in (A ∖ \{x\})) \to F : B ⟶ ℤ$
8	2	ssdifssd	$⊢ φ \to A ∖ \{x\} \subseteq B$
9	8	sselda	$⊢ (φ \land k \in (A ∖ \{x\})) \to k \in B$
10	7 9	ffvelcdmd	$⊢ (φ \land k \in (A ∖ \{x\})) \to F (k) \in ℤ$
11	10	adantlr	$⊢ ((φ \land x \in A) \land k \in (A ∖ \{x\})) \to F (k) \in ℤ$
12	6 11	fprodzcl	$⊢ (φ \land x \in A) \to \prod_{k \in A ∖ \{x\}} F (k) \in ℤ$
13	3	adantr	$⊢ (φ \land x \in A) \to F : B ⟶ ℤ$
14	2	sselda	$⊢ (φ \land x \in A) \to x \in B$
15	13 14	ffvelcdmd	$⊢ (φ \land x \in A) \to F (x) \in ℤ$
16		dvdsmul2	$⊢ (\prod_{k \in A ∖ \{x\}} F (k) \in ℤ \land F (x) \in ℤ) \to F (x) ∥ \prod_{k \in A ∖ \{x\}} F (k) F (x)$
17	12 15 16	syl2anc	$⊢ (φ \land x \in A) \to F (x) ∥ \prod_{k \in A ∖ \{x\}} F (k) F (x)$
18	17	ralrimiva	$⊢ φ \to \forall x \in A F (x) ∥ \prod_{k \in A ∖ \{x\}} F (k) F (x)$
19		neldifsnd	$⊢ (φ \land x \in A) \to \neg x \in (A ∖ \{x\})$
20		disjsn	$⊢ (A ∖ \{x\}) \cap \{x\} = \emptyset \leftrightarrow \neg x \in (A ∖ \{x\})$
21	19 20	sylibr	$⊢ (φ \land x \in A) \to (A ∖ \{x\}) \cap \{x\} = \emptyset$
22		difsnid	$⊢ x \in A \to (A ∖ \{x\}) \cup \{x\} = A$
23	22	eqcomd	$⊢ x \in A \to A = (A ∖ \{x\}) \cup \{x\}$
24	23	adantl	$⊢ (φ \land x \in A) \to A = (A ∖ \{x\}) \cup \{x\}$
25	13	adantr	$⊢ ((φ \land x \in A) \land k \in A) \to F : B ⟶ ℤ$
26	2	adantr	$⊢ (φ \land x \in A) \to A \subseteq B$
27	26	sselda	$⊢ ((φ \land x \in A) \land k \in A) \to k \in B$
28	25 27	ffvelcdmd	$⊢ ((φ \land x \in A) \land k \in A) \to F (k) \in ℤ$
29	28	zcnd	$⊢ ((φ \land x \in A) \land k \in A) \to F (k) \in ℂ$
30	21 24 4 29	fprodsplit	$⊢ (φ \land x \in A) \to \prod_{k \in A} F (k) = \prod_{k \in A ∖ \{x\}} F (k) \prod_{k \in \{x\}} F (k)$
31		simpr	$⊢ (φ \land x \in A) \to x \in A$
32	15	zcnd	$⊢ (φ \land x \in A) \to F (x) \in ℂ$
33		fveq2	$⊢ k = x \to F (k) = F (x)$
34	33	prodsn	$⊢ (x \in A \land F (x) \in ℂ) \to \prod_{k \in \{x\}} F (k) = F (x)$
35	31 32 34	syl2anc	$⊢ (φ \land x \in A) \to \prod_{k \in \{x\}} F (k) = F (x)$
36	35	oveq2d	$⊢ (φ \land x \in A) \to \prod_{k \in A ∖ \{x\}} F (k) \prod_{k \in \{x\}} F (k) = \prod_{k \in A ∖ \{x\}} F (k) F (x)$
37	30 36	eqtrd	$⊢ (φ \land x \in A) \to \prod_{k \in A} F (k) = \prod_{k \in A ∖ \{x\}} F (k) F (x)$
38	37	breq2d	$⊢ (φ \land x \in A) \to (F (x) ∥ \prod_{k \in A} F (k) \leftrightarrow F (x) ∥ \prod_{k \in A ∖ \{x\}} F (k) F (x))$
39	38	ralbidva	$⊢ φ \to (\forall x \in A F (x) ∥ \prod_{k \in A} F (k) \leftrightarrow \forall x \in A F (x) ∥ \prod_{k \in A ∖ \{x\}} F (k) F (x))$
40	18 39	mpbird	$⊢ φ \to \forall x \in A F (x) ∥ \prod_{k \in A} F (k)$

Metamath Proof Explorer

Theorem fprodfvdvdsd

Proof