Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodfvdvdsd.b	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	fprodfvdvdsd.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℤ )
Assertion	fprodfvdvdsd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∥ ∏ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) )

Proof

Step	Hyp	Ref	Expression
1		fprodfvdvdsd.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		fprodfvdvdsd.b	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
3		fprodfvdvdsd.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℤ )
4	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ∈ Fin )
5		diffi	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝑥 } ) ∈ Fin )
6	4 5	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑥 } ) ∈ Fin )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → 𝐹 : 𝐵 ⟶ ℤ )
8	2	ssdifssd	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝑥 } ) ⊆ 𝐵 )
9	8	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → 𝑘 ∈ 𝐵 )
10	7 9	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℤ )
11	10	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℤ )
12	6 11	fprodzcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑘 ) ∈ ℤ )
13	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝐵 ⟶ ℤ )
14	2	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
15	13 14	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
16		dvdsmul2	⊢ ( ( ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑘 ) ∈ ℤ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℤ ) → ( 𝐹 ‘ 𝑥 ) ∥ ( ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑥 ) ) )
17	12 15 16	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∥ ( ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑥 ) ) )
18	17	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∥ ( ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑥 ) ) )
19		neldifsnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 ∈ ( 𝐴 ∖ { 𝑥 } ) )
20		disjsn	⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 ∈ ( 𝐴 ∖ { 𝑥 } ) )
21	19 20	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ )
22		difsnid	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = 𝐴 )
23	22	eqcomd	⊢ ( 𝑥 ∈ 𝐴 → 𝐴 = ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
24	23	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 = ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
25	13	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐹 : 𝐵 ⟶ ℤ )
26	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ 𝐵 )
27	26	sselda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐵 )
28	25 27	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℤ )
29	28	zcnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
30	21 24 4 29	fprodsplit	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∏ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑘 ) · ∏ 𝑘 ∈ { 𝑥 } ( 𝐹 ‘ 𝑘 ) ) )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
32	15	zcnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
33		fveq2	⊢ ( 𝑘 = 𝑥 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑥 ) )
34	33	prodsn	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑥 } ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑥 ) )
35	31 32 34	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∏ 𝑘 ∈ { 𝑥 } ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑥 ) )
36	35	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑘 ) · ∏ 𝑘 ∈ { 𝑥 } ( 𝐹 ‘ 𝑘 ) ) = ( ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑥 ) ) )
37	30 36	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∏ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) = ( ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑥 ) ) )
38	37	breq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) ∥ ∏ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑥 ) ∥ ( ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑥 ) ) ) )
39	38	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∥ ∏ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∥ ( ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝑥 } ) ( 𝐹 ‘ 𝑘 ) · ( 𝐹 ‘ 𝑥 ) ) ) )
40	18 39	mpbird	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∥ ∏ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) )