Theorem plydivlem1

Description: Lemma for plydivalg . (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	plydiv.pl	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to x+y\in S$$
	plydiv.tm	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xy\in S$$
	plydiv.rc	$$⊢\left(\phi \wedge \left(x\in S\wedge x\ne 0\right)\right)\to \frac{1}{x}\in S$$
	plydiv.m1	$$⊢\phi \to -1\in S$$
Assertion	plydivlem1	$$⊢\phi \to 0\in S$$

Proof

Step	Hyp	Ref	Expression
1		plydiv.pl	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to x+y\in S$$
2		plydiv.tm	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xy\in S$$
3		plydiv.rc	$$⊢\left(\phi \wedge \left(x\in S\wedge x\ne 0\right)\right)\to \frac{1}{x}\in S$$
4		plydiv.m1	$$⊢\phi \to -1\in S$$
5		1pneg1e0	$$⊢1+-1=0$$
6		neg1mulneg1e1	$$⊢-1-1=1$$
7	2 4 4	caovcld	$$⊢\phi \to -1-1\in S$$
8	6 7	eqeltrrid	$$⊢\phi \to 1\in S$$
9	1 8 4	caovcld	$$⊢\phi \to 1+-1\in S$$
10	5 9	eqeltrrid	$$⊢\phi \to 0\in S$$