Theorem fissn0dvds

Description: For each finite subset of the integers not containing 0 there is a positive integer which is divisible by each element of this subset. (Contributed by AV, 21-Aug-2020)

	Ref	Expression
Assertion	fissn0dvds	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → 𝑍 ⊆ ℤ )
2		simp2	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → 𝑍 ∈ Fin )
3		eqid	⊢ ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) = ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 )
4		simp3	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → 0 ∉ 𝑍 )
5	1 2 3 4	absprodnn	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) ∈ ℕ )
6		breq2	⊢ ( 𝑛 = ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) → ( 𝑚 ∥ 𝑛 ↔ 𝑚 ∥ ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) ) )
7	6	ralbidv	⊢ ( 𝑛 = ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 ↔ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) ) )
8	7	adantl	⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ∧ 𝑛 = ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) ) → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 ↔ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) ) )
9	1 2 3	absproddvds	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ∀ 𝑚 ∈ 𝑍 𝑚 ∥ ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) )
10	5 8 9	rspcedvd	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 )