Metamath Proof Explorer

Theorem quotdgr

Description: Remainder property of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014)

		Ref	Expression
	Hypothesis	quotdgr.1	$⊢ R = F -_{f} (G \times_{f} (F quot G))$
	Assertion	quotdgr	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to (R = 0_{𝑝} \lor \deg (R) < \deg (G))$

Proof

Step	Hyp	Ref	Expression
1		quotdgr.1	$⊢ R = F -_{f} (G \times_{f} (F quot G))$
2		addcl	$⊢ (x \in ℂ \land y \in ℂ) \to x + y \in ℂ$
3	2	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \land (x \in ℂ \land y \in ℂ)) \to x + y \in ℂ$
4		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
5	4	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \land (x \in ℂ \land y \in ℂ)) \to x y \in ℂ$
6		reccl	$⊢ (x \in ℂ \land x \neq 0) \to \frac{1}{x} \in ℂ$
7	6	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \land (x \in ℂ \land x \neq 0)) \to \frac{1}{x} \in ℂ$
8		neg1cn	$⊢ - 1 \in ℂ$
9	8	a1i	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to - 1 \in ℂ$
10		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
11		simp1	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to F \in Poly (S)$
12	10 11	sselid	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to F \in Poly (ℂ)$
13		simp2	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to G \in Poly (S)$
14	10 13	sselid	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to G \in Poly (ℂ)$
15		simp3	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to G \neq 0_{𝑝}$
16	3 5 7 9 12 14 15 1	quotlem	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to (F quot G \in Poly (ℂ) \land (R = 0_{𝑝} \lor \deg (R) < \deg (G)))$
17	16	simprd	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to (R = 0_{𝑝} \lor \deg (R) < \deg (G))$