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

Metamath Proof Explorer

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