Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fproddvdsd.s	⊢ ( 𝜑 → 𝐴 ⊆ ℤ )
Assertion	fproddvdsd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ∥ ∏ 𝑘 ∈ 𝐴 𝑘 )

Proof

Step	Hyp	Ref	Expression
1		fproddvdsd.f	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		fproddvdsd.s	⊢ ( 𝜑 → 𝐴 ⊆ ℤ )
3		f1oi	⊢ ( I ↾ ℤ ) : ℤ –1-1-onto→ ℤ
4		f1of	⊢ ( ( I ↾ ℤ ) : ℤ –1-1-onto→ ℤ → ( I ↾ ℤ ) : ℤ ⟶ ℤ )
5	3 4	mp1i	⊢ ( 𝜑 → ( I ↾ ℤ ) : ℤ ⟶ ℤ )
6	1 2 5	fprodfvdvdsd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( ( I ↾ ℤ ) ‘ 𝑥 ) ∥ ∏ 𝑘 ∈ 𝐴 ( ( I ↾ ℤ ) ‘ 𝑘 ) )
7	2	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℤ )
8		fvresi	⊢ ( 𝑥 ∈ ℤ → ( ( I ↾ ℤ ) ‘ 𝑥 ) = 𝑥 )
9	7 8	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( I ↾ ℤ ) ‘ 𝑥 ) = 𝑥 )
10	9	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = ( ( I ↾ ℤ ) ‘ 𝑥 ) )
11	2	sseld	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝑘 ∈ ℤ ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑘 ∈ 𝐴 → 𝑘 ∈ ℤ ) )
13	12	imp	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ℤ )
14		fvresi	⊢ ( 𝑘 ∈ ℤ → ( ( I ↾ ℤ ) ‘ 𝑘 ) = 𝑘 )
15	13 14	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐴 ) → ( ( I ↾ ℤ ) ‘ 𝑘 ) = 𝑘 )
16	15	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐴 ) → 𝑘 = ( ( I ↾ ℤ ) ‘ 𝑘 ) )
17	16	prodeq2dv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∏ 𝑘 ∈ 𝐴 𝑘 = ∏ 𝑘 ∈ 𝐴 ( ( I ↾ ℤ ) ‘ 𝑘 ) )
18	10 17	breq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∥ ∏ 𝑘 ∈ 𝐴 𝑘 ↔ ( ( I ↾ ℤ ) ‘ 𝑥 ) ∥ ∏ 𝑘 ∈ 𝐴 ( ( I ↾ ℤ ) ‘ 𝑘 ) ) )
19	18	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝑥 ∥ ∏ 𝑘 ∈ 𝐴 𝑘 ↔ ∀ 𝑥 ∈ 𝐴 ( ( I ↾ ℤ ) ‘ 𝑥 ) ∥ ∏ 𝑘 ∈ 𝐴 ( ( I ↾ ℤ ) ‘ 𝑘 ) ) )
20	6 19	mpbird	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ∥ ∏ 𝑘 ∈ 𝐴 𝑘 )