Theorem modfsummodslem1

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

	Ref	Expression
Assertion	modfsummodslem1	$$⊢\forall k\in \left(A\cup \left\{z\right\}\right)B\in \mathbb{Z}\to ⦋z/k⦌B\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		vsnid	$$⊢z\in \left\{z\right\}$$
2		elun2	$$⊢z\in \left\{z\right\}\to z\in \left(A\cup \left\{z\right\}\right)$$
3	1 2	ax-mp	$$⊢z\in \left(A\cup \left\{z\right\}\right)$$
4		rspcsbela	$$⊢\left(z\in \left(A\cup \left\{z\right\}\right)\wedge \forall k\in \left(A\cup \left\{z\right\}\right)B\in \mathbb{Z}\right)\to ⦋z/k⦌B\in \mathbb{Z}$$
5	3 4	mpan	$$⊢\forall k\in \left(A\cup \left\{z\right\}\right)B\in \mathbb{Z}\to ⦋z/k⦌B\in \mathbb{Z}$$