This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ∥ ∏ 𝑘 ∈ 𝐴 𝑘 )