Theorem modfsummodslem1

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

	Ref	Expression
Assertion	modfsummodslem1	⊢ ( ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		vsnid	⊢ 𝑧 ∈ { 𝑧 }
2		elun2	⊢ ( 𝑧 ∈ { 𝑧 } → 𝑧 ∈ ( 𝐴 ∪ { 𝑧 } ) )
3	1 2	ax-mp	⊢ 𝑧 ∈ ( 𝐴 ∪ { 𝑧 } )
4		rspcsbela	⊢ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝑧 } ) ∧ ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ )
5	3 4	mpan	⊢ ( ∀ 𝑘 ∈ ( 𝐴 ∪ { 𝑧 } ) 𝐵 ∈ ℤ → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℤ )