Metamath Proof Explorer

Theorem modfsummodslem1

Description: Lemma 1 for modfsummods . (Contributed by Alexander van der Vekens, 1-Sep-2018)

Ref Expression
Assertion modfsummodslem1 ⊢ ∀ k ∈ A ∪ z B ∈ ℤ → ⦋ z / k⦌ B ∈ ℤ

Proof

Step Hyp Ref Expression
1 vsnid ⊢ z ∈ z
2 elun2 ⊢ z ∈ z → z ∈ A ∪ z
3 1 2 ax-mp ⊢ z ∈ A ∪ z
4 rspcsbela ⊢ z ∈ A ∪ z ∧ ∀ k ∈ A ∪ z B ∈ ℤ → ⦋ z / k⦌ B ∈ ℤ
5 3 4 mpan ⊢ ∀ k ∈ A ∪ z B ∈ ℤ → ⦋ z / k⦌ B ∈ ℤ