ply1divmo

Description: Uniqueness of a quotient in a polynomial division. For polynomials F , G such that G =/= 0 and the leading coefficient of G is not a zero divisor, there is at most one polynomial q which satisfies F = ( G x. q ) + r where the degree of r is less than the degree of G . (Contributed by Stefan O'Rear, 26-Mar-2015) (Revised by NM, 17-Jun-2017)

	Ref	Expression
Hypotheses	ply1divalg.p	$⊢ P = {Poly}_{1} (R)$
	ply1divalg.d	$⊢ D = \deg_{1} (R)$
	ply1divalg.b	$⊢ B = {Base}_{P}$
	ply1divalg.m	$⊢ \underset{˙}{-} = -_{P}$
	ply1divalg.z	$⊢ \underset{˙}{0} = 0_{P}$
	ply1divalg.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
	ply1divalg.r1	$⊢ φ \to R \in Ring$
	ply1divalg.f	$⊢ φ \to F \in B$
	ply1divalg.g1	$⊢ φ \to G \in B$
	ply1divalg.g2	$⊢ φ \to G \neq \underset{˙}{0}$
	ply1divmo.g3	$⊢ φ \to {coe}_{1} (G) (D (G)) \in E$
	ply1divmo.e	$⊢ E = RLReg (R)$
Assertion	ply1divmo	$⊢ φ \to \exists^{*} q \in B D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)$

Proof

Step	Hyp	Ref	Expression
1		ply1divalg.p	$⊢ P = {Poly}_{1} (R)$
2		ply1divalg.d	$⊢ D = \deg_{1} (R)$
3		ply1divalg.b	$⊢ B = {Base}_{P}$
4		ply1divalg.m	$⊢ \underset{˙}{-} = -_{P}$
5		ply1divalg.z	$⊢ \underset{˙}{0} = 0_{P}$
6		ply1divalg.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
7		ply1divalg.r1	$⊢ φ \to R \in Ring$
8		ply1divalg.f	$⊢ φ \to F \in B$
9		ply1divalg.g1	$⊢ φ \to G \in B$
10		ply1divalg.g2	$⊢ φ \to G \neq \underset{˙}{0}$
11		ply1divmo.g3	$⊢ φ \to {coe}_{1} (G) (D (G)) \in E$
12		ply1divmo.e	$⊢ E = RLReg (R)$
13	7	adantr	$⊢ (φ \land (q \in B \land r \in B)) \to R \in Ring$
14	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
15	13 14	syl	$⊢ (φ \land (q \in B \land r \in B)) \to P \in Ring$
16		ringgrp	$⊢ P \in Ring \to P \in Grp$
17	15 16	syl	$⊢ (φ \land (q \in B \land r \in B)) \to P \in Grp$
18	8	adantr	$⊢ (φ \land (q \in B \land r \in B)) \to F \in B$
19	9	adantr	$⊢ (φ \land (q \in B \land r \in B)) \to G \in B$
20		simprl	$⊢ (φ \land (q \in B \land r \in B)) \to q \in B$
21	3 6	ringcl	$⊢ (P \in Ring \land G \in B \land q \in B) \to G \underset{˙}{∙} q \in B$
22	15 19 20 21	syl3anc	$⊢ (φ \land (q \in B \land r \in B)) \to G \underset{˙}{∙} q \in B$
23	3 4	grpsubcl	$⊢ (P \in Grp \land F \in B \land G \underset{˙}{∙} q \in B) \to F \underset{˙}{-} (G \underset{˙}{∙} q) \in B$
24	17 18 22 23	syl3anc	$⊢ (φ \land (q \in B \land r \in B)) \to F \underset{˙}{-} (G \underset{˙}{∙} q) \in B$
25		simprr	$⊢ (φ \land (q \in B \land r \in B)) \to r \in B$
26	3 6	ringcl	$⊢ (P \in Ring \land G \in B \land r \in B) \to G \underset{˙}{∙} r \in B$
27	15 19 25 26	syl3anc	$⊢ (φ \land (q \in B \land r \in B)) \to G \underset{˙}{∙} r \in B$
28	3 4	grpsubcl	$⊢ (P \in Grp \land F \in B \land G \underset{˙}{∙} r \in B) \to F \underset{˙}{-} (G \underset{˙}{∙} r) \in B$
29	17 18 27 28	syl3anc	$⊢ (φ \land (q \in B \land r \in B)) \to F \underset{˙}{-} (G \underset{˙}{∙} r) \in B$
30	3 4	grpsubcl	$⊢ (P \in Grp \land F \underset{˙}{-} (G \underset{˙}{∙} q) \in B \land F \underset{˙}{-} (G \underset{˙}{∙} r) \in B) \to (F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r)) \in B$
31	17 24 29 30	syl3anc	$⊢ (φ \land (q \in B \land r \in B)) \to (F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r)) \in B$
32	2 1 3	deg1xrcl	$⊢ (F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r)) \in B \to D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) \in ℝ^{*}$
33	31 32	syl	$⊢ (φ \land (q \in B \land r \in B)) \to D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) \in ℝ^{*}$
34	2 1 3	deg1xrcl	$⊢ F \underset{˙}{-} (G \underset{˙}{∙} r) \in B \to D (F \underset{˙}{-} (G \underset{˙}{∙} r)) \in ℝ^{*}$
35	29 34	syl	$⊢ (φ \land (q \in B \land r \in B)) \to D (F \underset{˙}{-} (G \underset{˙}{∙} r)) \in ℝ^{*}$
36	2 1 3	deg1xrcl	$⊢ F \underset{˙}{-} (G \underset{˙}{∙} q) \in B \to D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \in ℝ^{*}$
37	24 36	syl	$⊢ (φ \land (q \in B \land r \in B)) \to D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \in ℝ^{*}$
38	35 37	ifcld	$⊢ (φ \land (q \in B \land r \in B)) \to if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q))) \in ℝ^{*}$
39	2 1 3	deg1xrcl	$⊢ G \in B \to D (G) \in ℝ^{*}$
40	19 39	syl	$⊢ (φ \land (q \in B \land r \in B)) \to D (G) \in ℝ^{*}$
41	33 38 40	3jca	$⊢ (φ \land (q \in B \land r \in B)) \to (D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) \in ℝ^{} \land if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q))) \in ℝ^{} \land D (G) \in ℝ^{*})$
42	41	adantr	$⊢ ((φ \land (q \in B \land r \in B)) \land (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \land D (F \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))) \to (D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) \in ℝ^{} \land if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q))) \in ℝ^{} \land D (G) \in ℝ^{*})$
43	1 2 13 3 4 24 29	deg1suble	$⊢ (φ \land (q \in B \land r \in B)) \to D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) \leq if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q)))$
44	43	adantr	$⊢ ((φ \land (q \in B \land r \in B)) \land (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \land D (F \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))) \to D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) \leq if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q)))$
45		xrmaxlt	$⊢ (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \in ℝ^{} \land D (F \underset{˙}{-} (G \underset{˙}{∙} r)) \in ℝ^{} \land D (G) \in ℝ^{*}) \to (if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q))) < D (G) \leftrightarrow (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \land D (F \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G)))$
46	37 35 40 45	syl3anc	$⊢ (φ \land (q \in B \land r \in B)) \to (if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q))) < D (G) \leftrightarrow (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \land D (F \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G)))$
47	46	biimpar	$⊢ ((φ \land (q \in B \land r \in B)) \land (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \land D (F \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))) \to if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q))) < D (G)$
48	44 47	jca	$⊢ ((φ \land (q \in B \land r \in B)) \land (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \land D (F \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))) \to (D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) \leq if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q))) \land if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q))) < D (G))$
49		xrlelttr	$⊢ (D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) \in ℝ^{} \land if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q))) \in ℝ^{} \land D (G) \in ℝ^{*}) \to ((D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) \leq if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q))) \land if (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) \leq D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} r)), D (F \underset{˙}{-} (G \underset{˙}{∙} q))) < D (G)) \to D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) < D (G))$
50	42 48 49	sylc	$⊢ ((φ \land (q \in B \land r \in B)) \land (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \land D (F \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))) \to D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) < D (G)$
51	50	ex	$⊢ (φ \land (q \in B \land r \in B)) \to ((D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \land D (F \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G)) \to D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) < D (G))$
52	2 1 5 3	deg1nn0cl	$⊢ (R \in Ring \land G \in B \land G \neq \underset{˙}{0}) \to D (G) \in ℕ_{0}$
53	7 9 10 52	syl3anc	$⊢ φ \to D (G) \in ℕ_{0}$
54	53	ad2antrr	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to D (G) \in ℕ_{0}$
55	54	nn0red	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to D (G) \in ℝ$
56	7	ad2antrr	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to R \in Ring$
57	3 4	grpsubcl	$⊢ (P \in Grp \land r \in B \land q \in B) \to r \underset{˙}{-} q \in B$
58	17 25 20 57	syl3anc	$⊢ (φ \land (q \in B \land r \in B)) \to r \underset{˙}{-} q \in B$
59	58	adantr	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to r \underset{˙}{-} q \in B$
60	3 5 4	grpsubeq0	$⊢ (P \in Grp \land r \in B \land q \in B) \to (r \underset{˙}{-} q = \underset{˙}{0} \leftrightarrow r = q)$
61	17 25 20 60	syl3anc	$⊢ (φ \land (q \in B \land r \in B)) \to (r \underset{˙}{-} q = \underset{˙}{0} \leftrightarrow r = q)$
62		equcom	$⊢ r = q \leftrightarrow q = r$
63	61 62	syl6bb	$⊢ (φ \land (q \in B \land r \in B)) \to (r \underset{˙}{-} q = \underset{˙}{0} \leftrightarrow q = r)$
64	63	necon3bid	$⊢ (φ \land (q \in B \land r \in B)) \to (r \underset{˙}{-} q \neq \underset{˙}{0} \leftrightarrow q \neq r)$
65	64	biimpar	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to r \underset{˙}{-} q \neq \underset{˙}{0}$
66	2 1 5 3	deg1nn0cl	$⊢ (R \in Ring \land r \underset{˙}{-} q \in B \land r \underset{˙}{-} q \neq \underset{˙}{0}) \to D (r \underset{˙}{-} q) \in ℕ_{0}$
67	56 59 65 66	syl3anc	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to D (r \underset{˙}{-} q) \in ℕ_{0}$
68		nn0addge1	$⊢ (D (G) \in ℝ \land D (r \underset{˙}{-} q) \in ℕ_{0}) \to D (G) \leq D (G) + D (r \underset{˙}{-} q)$
69	55 67 68	syl2anc	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to D (G) \leq D (G) + D (r \underset{˙}{-} q)$
70	9	ad2antrr	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to G \in B$
71	10	ad2antrr	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to G \neq \underset{˙}{0}$
72	11	ad2antrr	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to {coe}_{1} (G) (D (G)) \in E$
73	2 1 12 3 6 5 56 70 71 72 59 65	deg1mul2	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to D (G \underset{˙}{∙} (r \underset{˙}{-} q)) = D (G) + D (r \underset{˙}{-} q)$
74	69 73	breqtrrd	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to D (G) \leq D (G \underset{˙}{∙} (r \underset{˙}{-} q))$
75		ringabl	$⊢ P \in Ring \to P \in Abel$
76	15 75	syl	$⊢ (φ \land (q \in B \land r \in B)) \to P \in Abel$
77	3 4 76 18 22 27	ablnnncan1	$⊢ (φ \land (q \in B \land r \in B)) \to (F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r)) = (G \underset{˙}{∙} r) \underset{˙}{-} (G \underset{˙}{∙} q)$
78	3 6 4 15 19 25 20	ringsubdi	$⊢ (φ \land (q \in B \land r \in B)) \to G \underset{˙}{∙} (r \underset{˙}{-} q) = (G \underset{˙}{∙} r) \underset{˙}{-} (G \underset{˙}{∙} q)$
79	77 78	eqtr4d	$⊢ (φ \land (q \in B \land r \in B)) \to (F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r)) = G \underset{˙}{∙} (r \underset{˙}{-} q)$
80	79	fveq2d	$⊢ (φ \land (q \in B \land r \in B)) \to D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) = D (G \underset{˙}{∙} (r \underset{˙}{-} q))$
81	80	adantr	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) = D (G \underset{˙}{∙} (r \underset{˙}{-} q))$
82	74 81	breqtrrd	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to D (G) \leq D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r)))$
83	40 33	xrlenltd	$⊢ (φ \land (q \in B \land r \in B)) \to (D (G) \leq D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) \leftrightarrow \neg D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) < D (G))$
84	83	adantr	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to (D (G) \leq D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) \leftrightarrow \neg D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) < D (G))$
85	82 84	mpbid	$⊢ ((φ \land (q \in B \land r \in B)) \land q \neq r) \to \neg D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) < D (G)$
86	85	ex	$⊢ (φ \land (q \in B \land r \in B)) \to (q \neq r \to \neg D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) < D (G))$
87	86	necon4ad	$⊢ (φ \land (q \in B \land r \in B)) \to (D ((F \underset{˙}{-} (G \underset{˙}{∙} q)) \underset{˙}{-} (F \underset{˙}{-} (G \underset{˙}{∙} r))) < D (G) \to q = r)$
88	51 87	syld	$⊢ (φ \land (q \in B \land r \in B)) \to ((D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \land D (F \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G)) \to q = r)$
89	88	ralrimivva	$⊢ φ \to \forall q \in B \forall r \in B ((D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \land D (F \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G)) \to q = r)$
90		oveq2	$⊢ q = r \to G \underset{˙}{∙} q = G \underset{˙}{∙} r$
91	90	oveq2d	$⊢ q = r \to F \underset{˙}{-} (G \underset{˙}{∙} q) = F \underset{˙}{-} (G \underset{˙}{∙} r)$
92	91	fveq2d	$⊢ q = r \to D (F \underset{˙}{-} (G \underset{˙}{∙} q)) = D (F \underset{˙}{-} (G \underset{˙}{∙} r))$
93	92	breq1d	$⊢ q = r \to (D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \leftrightarrow D (F \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))$
94	93	rmo4	$⊢ \exists^{*} q \in B D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \leftrightarrow \forall q \in B \forall r \in B ((D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \land D (F \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G)) \to q = r)$
95	89 94	sylibr	$⊢ φ \to \exists^{*} q \in B D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)$

Metamath Proof Explorer

Theorem ply1divmo

Proof