Theorem plydivlem1

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

	Ref	Expression
Hypotheses	plydiv.pl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
	plydiv.tm	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
	plydiv.rc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
	plydiv.m1	⊢ ( 𝜑 → - 1 ∈ 𝑆 )
Assertion	plydivlem1	⊢ ( 𝜑 → 0 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		plydiv.pl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2		plydiv.tm	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
3		plydiv.rc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
4		plydiv.m1	⊢ ( 𝜑 → - 1 ∈ 𝑆 )
5		1pneg1e0	⊢ ( 1 + - 1 ) = 0
6		neg1mulneg1e1	⊢ ( - 1 · - 1 ) = 1
7	2 4 4	caovcld	⊢ ( 𝜑 → ( - 1 · - 1 ) ∈ 𝑆 )
8	6 7	eqeltrrid	⊢ ( 𝜑 → 1 ∈ 𝑆 )
9	1 8 4	caovcld	⊢ ( 𝜑 → ( 1 + - 1 ) ∈ 𝑆 )
10	5 9	eqeltrrid	⊢ ( 𝜑 → 0 ∈ 𝑆 )