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	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	ply1divalg.d	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
	ply1divalg.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1divalg.m	⊢ − = ( -_g ‘ 𝑃 )
	ply1divalg.z	⊢ 0 = ( 0_g ‘ 𝑃 )
	ply1divalg.t	⊢ ∙ = ( ._r ‘ 𝑃 )
	ply1divalg.r1	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ply1divalg.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	ply1divalg.g1	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	ply1divalg.g2	⊢ ( 𝜑 → 𝐺 ≠ 0 )
	ply1divmo.g3	⊢ ( 𝜑 → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ 𝐸 )
	ply1divmo.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
Assertion	ply1divmo	⊢ ( 𝜑 → ∃* 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1divalg.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
2		ply1divalg.d	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
3		ply1divalg.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		ply1divalg.m	⊢ − = ( -_g ‘ 𝑃 )
5		ply1divalg.z	⊢ 0 = ( 0_g ‘ 𝑃 )
6		ply1divalg.t	⊢ ∙ = ( ._r ‘ 𝑃 )
7		ply1divalg.r1	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		ply1divalg.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9		ply1divalg.g1	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
10		ply1divalg.g2	⊢ ( 𝜑 → 𝐺 ≠ 0 )
11		ply1divmo.g3	⊢ ( 𝜑 → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ 𝐸 )
12		ply1divmo.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
13	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
14	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15	13 14	syl	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑃 ∈ Ring )
16		ringgrp	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
17	15 16	syl	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑃 ∈ Grp )
18	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝐹 ∈ 𝐵 )
19	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝐺 ∈ 𝐵 )
20		simprl	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑞 ∈ 𝐵 )
21	3 6	ringcl	⊢ ( ( 𝑃 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐺 ∙ 𝑞 ) ∈ 𝐵 )
22	15 19 20 21	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐺 ∙ 𝑞 ) ∈ 𝐵 )
23	3 4	grpsubcl	⊢ ( ( 𝑃 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ ( 𝐺 ∙ 𝑞 ) ∈ 𝐵 ) → ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ∈ 𝐵 )
24	17 18 22 23	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ∈ 𝐵 )
25		simprr	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑟 ∈ 𝐵 )
26	3 6	ringcl	⊢ ( ( 𝑃 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) → ( 𝐺 ∙ 𝑟 ) ∈ 𝐵 )
27	15 19 25 26	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐺 ∙ 𝑟 ) ∈ 𝐵 )
28	3 4	grpsubcl	⊢ ( ( 𝑃 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ ( 𝐺 ∙ 𝑟 ) ∈ 𝐵 ) → ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ∈ 𝐵 )
29	17 18 27 28	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ∈ 𝐵 )
30	3 4	grpsubcl	⊢ ( ( 𝑃 ∈ Grp ∧ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ∈ 𝐵 ∧ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ∈ 𝐵 ) → ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ∈ 𝐵 )
31	17 24 29 30	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ∈ 𝐵 )
32	2 1 3	deg1xrcl	⊢ ( ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ∈ 𝐵 → ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) ∈ ℝ^* )
33	31 32	syl	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) ∈ ℝ^* )
34	2 1 3	deg1xrcl	⊢ ( ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ∈ 𝐵 → ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ∈ ℝ^* )
35	29 34	syl	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ∈ ℝ^* )
36	2 1 3	deg1xrcl	⊢ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ∈ 𝐵 → ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ∈ ℝ^* )
37	24 36	syl	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ∈ ℝ^* )
38	35 37	ifcld	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) ∈ ℝ^* )
39	2 1 3	deg1xrcl	⊢ ( 𝐺 ∈ 𝐵 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ^* )
40	19 39	syl	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐷 ‘ 𝐺 ) ∈ ℝ^* )
41	33 38 40	3jca	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) ∈ ℝ^* ∧ if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) ∈ ℝ^* ∧ ( 𝐷 ‘ 𝐺 ) ∈ ℝ^* ) )
42	41	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) → ( ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) ∈ ℝ^* ∧ if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) ∈ ℝ^* ∧ ( 𝐷 ‘ 𝐺 ) ∈ ℝ^* ) )
43	1 2 13 3 4 24 29	deg1suble	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) ≤ if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) )
44	43	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) → ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) ≤ if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) )
45		xrmaxlt	⊢ ( ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ∈ ℝ^* ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ∈ ℝ^* ∧ ( 𝐷 ‘ 𝐺 ) ∈ ℝ^* ) → ( if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
46	37 35 40 45	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
47	46	biimpar	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) → if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) )
48	44 47	jca	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) → ( ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) ≤ if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) ∧ if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
49		xrlelttr	⊢ ( ( ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) ∈ ℝ^* ∧ if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) ∈ ℝ^* ∧ ( 𝐷 ‘ 𝐺 ) ∈ ℝ^* ) → ( ( ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) ≤ if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) ∧ if ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ≤ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) , ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ) → ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
50	42 48 49	sylc	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) → ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) )
51	50	ex	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) → ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
52	2 1 5 3	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝐺 ≠ 0 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℕ₀ )
53	7 9 10 52	syl3anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℕ₀ )
54	53	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℕ₀ )
55	54	nn0red	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℝ )
56	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → 𝑅 ∈ Ring )
57	3 4	grpsubcl	⊢ ( ( 𝑃 ∈ Grp ∧ 𝑟 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( 𝑟 − 𝑞 ) ∈ 𝐵 )
58	17 25 20 57	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑟 − 𝑞 ) ∈ 𝐵 )
59	58	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ( 𝑟 − 𝑞 ) ∈ 𝐵 )
60	3 5 4	grpsubeq0	⊢ ( ( 𝑃 ∈ Grp ∧ 𝑟 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝑟 − 𝑞 ) = 0 ↔ 𝑟 = 𝑞 ) )
61	17 25 20 60	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑟 − 𝑞 ) = 0 ↔ 𝑟 = 𝑞 ) )
62		equcom	⊢ ( 𝑟 = 𝑞 ↔ 𝑞 = 𝑟 )
63	61 62	bitrdi	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑟 − 𝑞 ) = 0 ↔ 𝑞 = 𝑟 ) )
64	63	necon3bid	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑟 − 𝑞 ) ≠ 0 ↔ 𝑞 ≠ 𝑟 ) )
65	64	biimpar	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ( 𝑟 − 𝑞 ) ≠ 0 )
66	2 1 5 3	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑟 − 𝑞 ) ∈ 𝐵 ∧ ( 𝑟 − 𝑞 ) ≠ 0 ) → ( 𝐷 ‘ ( 𝑟 − 𝑞 ) ) ∈ ℕ₀ )
67	56 59 65 66	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ( 𝐷 ‘ ( 𝑟 − 𝑞 ) ) ∈ ℕ₀ )
68		nn0addge1	⊢ ( ( ( 𝐷 ‘ 𝐺 ) ∈ ℝ ∧ ( 𝐷 ‘ ( 𝑟 − 𝑞 ) ) ∈ ℕ₀ ) → ( 𝐷 ‘ 𝐺 ) ≤ ( ( 𝐷 ‘ 𝐺 ) + ( 𝐷 ‘ ( 𝑟 − 𝑞 ) ) ) )
69	55 67 68	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ( 𝐷 ‘ 𝐺 ) ≤ ( ( 𝐷 ‘ 𝐺 ) + ( 𝐷 ‘ ( 𝑟 − 𝑞 ) ) ) )
70	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → 𝐺 ∈ 𝐵 )
71	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → 𝐺 ≠ 0 )
72	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ 𝐸 )
73	2 1 12 3 6 5 56 70 71 72 59 65	deg1mul2	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ( 𝐷 ‘ ( 𝐺 ∙ ( 𝑟 − 𝑞 ) ) ) = ( ( 𝐷 ‘ 𝐺 ) + ( 𝐷 ‘ ( 𝑟 − 𝑞 ) ) ) )
74	69 73	breqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ( 𝐷 ‘ 𝐺 ) ≤ ( 𝐷 ‘ ( 𝐺 ∙ ( 𝑟 − 𝑞 ) ) ) )
75		ringabl	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Abel )
76	15 75	syl	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑃 ∈ Abel )
77	3 4 76 18 22 27	ablnnncan1	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) = ( ( 𝐺 ∙ 𝑟 ) − ( 𝐺 ∙ 𝑞 ) ) )
78	3 6 4 15 19 25 20	ringsubdi	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐺 ∙ ( 𝑟 − 𝑞 ) ) = ( ( 𝐺 ∙ 𝑟 ) − ( 𝐺 ∙ 𝑞 ) ) )
79	77 78	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) = ( 𝐺 ∙ ( 𝑟 − 𝑞 ) ) )
80	79	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) = ( 𝐷 ‘ ( 𝐺 ∙ ( 𝑟 − 𝑞 ) ) ) )
81	80	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) = ( 𝐷 ‘ ( 𝐺 ∙ ( 𝑟 − 𝑞 ) ) ) )
82	74 81	breqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ( 𝐷 ‘ 𝐺 ) ≤ ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) )
83	40 33	xrlenltd	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝐷 ‘ 𝐺 ) ≤ ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) ↔ ¬ ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
84	83	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ( ( 𝐷 ‘ 𝐺 ) ≤ ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) ↔ ¬ ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
85	82 84	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝑞 ≠ 𝑟 ) → ¬ ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) )
86	85	ex	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑞 ≠ 𝑟 → ¬ ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
87	86	necon4ad	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝐷 ‘ ( ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) − ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) ) < ( 𝐷 ‘ 𝐺 ) → 𝑞 = 𝑟 ) )
88	51 87	syld	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) → 𝑞 = 𝑟 ) )
89	88	ralrimivva	⊢ ( 𝜑 → ∀ 𝑞 ∈ 𝐵 ∀ 𝑟 ∈ 𝐵 ( ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) → 𝑞 = 𝑟 ) )
90		oveq2	⊢ ( 𝑞 = 𝑟 → ( 𝐺 ∙ 𝑞 ) = ( 𝐺 ∙ 𝑟 ) )
91	90	oveq2d	⊢ ( 𝑞 = 𝑟 → ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) = ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) )
92	91	fveq2d	⊢ ( 𝑞 = 𝑟 → ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) = ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) )
93	92	breq1d	⊢ ( 𝑞 = 𝑟 → ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
94	93	rmo4	⊢ ( ∃* 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ∀ 𝑞 ∈ 𝐵 ∀ 𝑟 ∈ 𝐵 ( ( ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) → 𝑞 = 𝑟 ) )
95	89 94	sylibr	⊢ ( 𝜑 → ∃* 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )

Metamath Proof Explorer

Theorem ply1divmo

Proof