quotcl

Description: The quotient of two polynomials in a field S is also in the field. (Contributed by Mario Carneiro, 26-Jul-2014)

	Ref	Expression
Hypotheses	plydiv.pl	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
	plydiv.tm	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
	plydiv.rc	$⊢ (φ \land (x \in S \land x \neq 0)) \to \frac{1}{x} \in S$
	plydiv.m1	$⊢ φ \to - 1 \in S$
	plydiv.f	$⊢ φ \to F \in Poly (S)$
	plydiv.g	$⊢ φ \to G \in Poly (S)$
	plydiv.z	$⊢ φ \to G \neq 0_{𝑝}$
Assertion	quotcl	$⊢ φ \to F quot G \in Poly (S)$

Step	Hyp	Ref	Expression
1		plydiv.pl	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
2		plydiv.tm	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
3		plydiv.rc	$⊢ (φ \land (x \in S \land x \neq 0)) \to \frac{1}{x} \in S$
4		plydiv.m1	$⊢ φ \to - 1 \in S$
5		plydiv.f	$⊢ φ \to F \in Poly (S)$
6		plydiv.g	$⊢ φ \to G \in Poly (S)$
7		plydiv.z	$⊢ φ \to G \neq 0_{𝑝}$
8		eqid	$⊢ F -_{f} (G \times_{f} (F quot G)) = F -_{f} (G \times_{f} (F quot G))$
9	1 2 3 4 5 6 7 8	quotlem	$⊢ φ \to (F quot G \in Poly (S) \land (F -_{f} (G \times_{f} (F quot G)) = 0_{𝑝} \lor \deg (F -_{f} (G \times_{f} (F quot G))) < \deg (G)))$
10	9	simpld	$⊢ φ \to F quot G \in Poly (S)$

Metamath Proof Explorer