plydivlem4

Description: Lemma for plydivex . Induction step. (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_{𝑝}$
	plydiv.r	$⊢ R = F -_{f} (G \times_{f} q)$
	plydiv.d	$⊢ φ \to D \in ℕ_{0}$
	plydiv.e	$⊢ φ \to M - N = D$
	plydiv.fz	$⊢ φ \to F \neq 0_{𝑝}$
	plydiv.u	$⊢ U = f -_{f} (G \times_{f} p)$
	plydiv.h	$⊢ H = (z \in ℂ ⟼ (\frac{A (M)}{B (N)}) z^{D})$
	plydiv.al	$⊢ φ \to \forall f \in Poly (S) ((f = 0_{𝑝} \lor \deg (f) - N < D) \to \exists p \in Poly (S) (U = 0_{𝑝} \lor \deg (U) < N))$
	plydiv.a	$⊢ A = coeff (F)$
	plydiv.b	$⊢ B = coeff (G)$
	plydiv.m	$⊢ M = \deg (F)$
	plydiv.n	$⊢ N = \deg (G)$
Assertion	plydivlem4	$⊢ φ \to \exists q \in Poly (S) (R = 0_{𝑝} \lor \deg (R) < N)$

Proof

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		plydiv.r	$⊢ R = F -_{f} (G \times_{f} q)$
9		plydiv.d	$⊢ φ \to D \in ℕ_{0}$
10		plydiv.e	$⊢ φ \to M - N = D$
11		plydiv.fz	$⊢ φ \to F \neq 0_{𝑝}$
12		plydiv.u	$⊢ U = f -_{f} (G \times_{f} p)$
13		plydiv.h	$⊢ H = (z \in ℂ ⟼ (\frac{A (M)}{B (N)}) z^{D})$
14		plydiv.al	$⊢ φ \to \forall f \in Poly (S) ((f = 0_{𝑝} \lor \deg (f) - N < D) \to \exists p \in Poly (S) (U = 0_{𝑝} \lor \deg (U) < N))$
15		plydiv.a	$⊢ A = coeff (F)$
16		plydiv.b	$⊢ B = coeff (G)$
17		plydiv.m	$⊢ M = \deg (F)$
18		plydiv.n	$⊢ N = \deg (G)$
19		plybss	$⊢ F \in Poly (S) \to S \subseteq ℂ$
20	5 19	syl	$⊢ φ \to S \subseteq ℂ$
21	1 2 3 4	plydivlem1	$⊢ φ \to 0 \in S$
22	15	coef2	$⊢ (F \in Poly (S) \land 0 \in S) \to A : ℕ_{0} ⟶ S$
23	5 21 22	syl2anc	$⊢ φ \to A : ℕ_{0} ⟶ S$
24		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
25	5 24	syl	$⊢ φ \to \deg (F) \in ℕ_{0}$
26	17 25	eqeltrid	$⊢ φ \to M \in ℕ_{0}$
27	23 26	ffvelcdmd	$⊢ φ \to A (M) \in S$
28	20 27	sseldd	$⊢ φ \to A (M) \in ℂ$
29	16	coef2	$⊢ (G \in Poly (S) \land 0 \in S) \to B : ℕ_{0} ⟶ S$
30	6 21 29	syl2anc	$⊢ φ \to B : ℕ_{0} ⟶ S$
31		dgrcl	$⊢ G \in Poly (S) \to \deg (G) \in ℕ_{0}$
32	6 31	syl	$⊢ φ \to \deg (G) \in ℕ_{0}$
33	18 32	eqeltrid	$⊢ φ \to N \in ℕ_{0}$
34	30 33	ffvelcdmd	$⊢ φ \to B (N) \in S$
35	20 34	sseldd	$⊢ φ \to B (N) \in ℂ$
36	18 16	dgreq0	$⊢ G \in Poly (S) \to (G = 0_{𝑝} \leftrightarrow B (N) = 0)$
37	6 36	syl	$⊢ φ \to (G = 0_{𝑝} \leftrightarrow B (N) = 0)$
38	37	necon3bid	$⊢ φ \to (G \neq 0_{𝑝} \leftrightarrow B (N) \neq 0)$
39	7 38	mpbid	$⊢ φ \to B (N) \neq 0$
40	28 35 39	divrecd	$⊢ φ \to \frac{A (M)}{B (N)} = A (M) (\frac{1}{B (N)})$
41		fvex	$⊢ B (N) \in V$
42		eleq1	$⊢ x = B (N) \to (x \in S \leftrightarrow B (N) \in S)$
43		neeq1	$⊢ x = B (N) \to (x \neq 0 \leftrightarrow B (N) \neq 0)$
44	42 43	anbi12d	$⊢ x = B (N) \to ((x \in S \land x \neq 0) \leftrightarrow (B (N) \in S \land B (N) \neq 0))$
45	44	anbi2d	$⊢ x = B (N) \to ((φ \land (x \in S \land x \neq 0)) \leftrightarrow (φ \land (B (N) \in S \land B (N) \neq 0)))$
46		oveq2	$⊢ x = B (N) \to \frac{1}{x} = \frac{1}{B (N)}$
47	46	eleq1d	$⊢ x = B (N) \to (\frac{1}{x} \in S \leftrightarrow \frac{1}{B (N)} \in S)$
48	45 47	imbi12d	$⊢ x = B (N) \to (((φ \land (x \in S \land x \neq 0)) \to \frac{1}{x} \in S) \leftrightarrow ((φ \land (B (N) \in S \land B (N) \neq 0)) \to \frac{1}{B (N)} \in S))$
49	41 48 3	vtocl	$⊢ (φ \land (B (N) \in S \land B (N) \neq 0)) \to \frac{1}{B (N)} \in S$
50	49	ex	$⊢ φ \to ((B (N) \in S \land B (N) \neq 0) \to \frac{1}{B (N)} \in S)$
51	34 39 50	mp2and	$⊢ φ \to \frac{1}{B (N)} \in S$
52	2 27 51	caovcld	$⊢ φ \to A (M) (\frac{1}{B (N)}) \in S$
53	40 52	eqeltrd	$⊢ φ \to \frac{A (M)}{B (N)} \in S$
54	13	ply1term	$⊢ (S \subseteq ℂ \land \frac{A (M)}{B (N)} \in S \land D \in ℕ_{0}) \to H \in Poly (S)$
55	20 53 9 54	syl3anc	$⊢ φ \to H \in Poly (S)$
56	55	adantr	$⊢ (φ \land p \in Poly (S)) \to H \in Poly (S)$
57		simpr	$⊢ (φ \land p \in Poly (S)) \to p \in Poly (S)$
58	1	adantlr	$⊢ ((φ \land p \in Poly (S)) \land (x \in S \land y \in S)) \to x + y \in S$
59	56 57 58	plyadd	$⊢ (φ \land p \in Poly (S)) \to H +_{f} p \in Poly (S)$
60		cnex	$⊢ ℂ \in V$
61	60	a1i	$⊢ (φ \land p \in Poly (S)) \to ℂ \in V$
62	5	adantr	$⊢ (φ \land p \in Poly (S)) \to F \in Poly (S)$
63		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
64	62 63	syl	$⊢ (φ \land p \in Poly (S)) \to F : ℂ ⟶ ℂ$
65		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
66	65	adantl	$⊢ ((φ \land p \in Poly (S)) \land (x \in ℂ \land y \in ℂ)) \to x y \in ℂ$
67		plyf	$⊢ H \in Poly (S) \to H : ℂ ⟶ ℂ$
68	56 67	syl	$⊢ (φ \land p \in Poly (S)) \to H : ℂ ⟶ ℂ$
69	6	adantr	$⊢ (φ \land p \in Poly (S)) \to G \in Poly (S)$
70		plyf	$⊢ G \in Poly (S) \to G : ℂ ⟶ ℂ$
71	69 70	syl	$⊢ (φ \land p \in Poly (S)) \to G : ℂ ⟶ ℂ$
72		inidm	$⊢ ℂ \cap ℂ = ℂ$
73	66 68 71 61 61 72	off	$⊢ (φ \land p \in Poly (S)) \to (H \times_{f} G) : ℂ ⟶ ℂ$
74		plyf	$⊢ p \in Poly (S) \to p : ℂ ⟶ ℂ$
75	74	adantl	$⊢ (φ \land p \in Poly (S)) \to p : ℂ ⟶ ℂ$
76	66 71 75 61 61 72	off	$⊢ (φ \land p \in Poly (S)) \to (G \times_{f} p) : ℂ ⟶ ℂ$
77		subsub4	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x - y - z = x - (y + z)$
78	77	adantl	$⊢ ((φ \land p \in Poly (S)) \land (x \in ℂ \land y \in ℂ \land z \in ℂ)) \to x - y - z = x - (y + z)$
79	61 64 73 76 78	caofass	$⊢ (φ \land p \in Poly (S)) \to (F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p) = F -_{f} ((H \times_{f} G) +_{f} (G \times_{f} p))$
80		mulcom	$⊢ (x \in ℂ \land y \in ℂ) \to x y = y x$
81	80	adantl	$⊢ ((φ \land p \in Poly (S)) \land (x \in ℂ \land y \in ℂ)) \to x y = y x$
82	61 68 71 81	caofcom	$⊢ (φ \land p \in Poly (S)) \to H \times_{f} G = G \times_{f} H$
83	82	oveq1d	$⊢ (φ \land p \in Poly (S)) \to (H \times_{f} G) +_{f} (G \times_{f} p) = (G \times_{f} H) +_{f} (G \times_{f} p)$
84		adddi	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x (y + z) = x y + x z$
85	84	adantl	$⊢ ((φ \land p \in Poly (S)) \land (x \in ℂ \land y \in ℂ \land z \in ℂ)) \to x (y + z) = x y + x z$
86	61 71 68 75 85	caofdi	$⊢ (φ \land p \in Poly (S)) \to G \times_{f} (H +_{f} p) = (G \times_{f} H) +_{f} (G \times_{f} p)$
87	83 86	eqtr4d	$⊢ (φ \land p \in Poly (S)) \to (H \times_{f} G) +_{f} (G \times_{f} p) = G \times_{f} (H +_{f} p)$
88	87	oveq2d	$⊢ (φ \land p \in Poly (S)) \to F -_{f} ((H \times_{f} G) +_{f} (G \times_{f} p)) = F -_{f} (G \times_{f} (H +_{f} p))$
89	79 88	eqtrd	$⊢ (φ \land p \in Poly (S)) \to (F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p) = F -_{f} (G \times_{f} (H +_{f} p))$
90	89	eqeq1d	$⊢ (φ \land p \in Poly (S)) \to ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p) = 0_{𝑝} \leftrightarrow F -_{f} (G \times_{f} (H +_{f} p)) = 0_{𝑝})$
91	89	fveq2d	$⊢ (φ \land p \in Poly (S)) \to \deg ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)) = \deg (F -_{f} (G \times_{f} (H +_{f} p)))$
92	91	breq1d	$⊢ (φ \land p \in Poly (S)) \to (\deg ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)) < N \leftrightarrow \deg (F -_{f} (G \times_{f} (H +_{f} p))) < N)$
93	90 92	orbi12d	$⊢ (φ \land p \in Poly (S)) \to (((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p) = 0_{𝑝} \lor \deg ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)) < N) \leftrightarrow (F -_{f} (G \times_{f} (H +_{f} p)) = 0_{𝑝} \lor \deg (F -_{f} (G \times_{f} (H +_{f} p))) < N))$
94	93	biimpa	$⊢ ((φ \land p \in Poly (S)) \land ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p) = 0_{𝑝} \lor \deg ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)) < N)) \to (F -_{f} (G \times_{f} (H +_{f} p)) = 0_{𝑝} \lor \deg (F -_{f} (G \times_{f} (H +_{f} p))) < N)$
95		oveq2	$⊢ q = H +_{f} p \to G \times_{f} q = G \times_{f} (H +_{f} p)$
96	95	oveq2d	$⊢ q = H +_{f} p \to F -_{f} (G \times_{f} q) = F -_{f} (G \times_{f} (H +_{f} p))$
97	8 96	eqtrid	$⊢ q = H +_{f} p \to R = F -_{f} (G \times_{f} (H +_{f} p))$
98	97	eqeq1d	$⊢ q = H +_{f} p \to (R = 0_{𝑝} \leftrightarrow F -_{f} (G \times_{f} (H +_{f} p)) = 0_{𝑝})$
99	97	fveq2d	$⊢ q = H +_{f} p \to \deg (R) = \deg (F -_{f} (G \times_{f} (H +_{f} p)))$
100	99	breq1d	$⊢ q = H +_{f} p \to (\deg (R) < N \leftrightarrow \deg (F -_{f} (G \times_{f} (H +_{f} p))) < N)$
101	98 100	orbi12d	$⊢ q = H +_{f} p \to ((R = 0_{𝑝} \lor \deg (R) < N) \leftrightarrow (F -_{f} (G \times_{f} (H +_{f} p)) = 0_{𝑝} \lor \deg (F -_{f} (G \times_{f} (H +_{f} p))) < N))$
102	101	rspcev	$⊢ (H +_{f} p \in Poly (S) \land (F -_{f} (G \times_{f} (H +_{f} p)) = 0_{𝑝} \lor \deg (F -_{f} (G \times_{f} (H +_{f} p))) < N)) \to \exists q \in Poly (S) (R = 0_{𝑝} \lor \deg (R) < N)$
103	59 94 102	syl2an2r	$⊢ ((φ \land p \in Poly (S)) \land ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p) = 0_{𝑝} \lor \deg ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)) < N)) \to \exists q \in Poly (S) (R = 0_{𝑝} \lor \deg (R) < N)$
104	55 6 1 2	plymul	$⊢ φ \to H \times_{f} G \in Poly (S)$
105		eqid	$⊢ \deg (H \times_{f} G) = \deg (H \times_{f} G)$
106	17 105	dgrsub	$⊢ (F \in Poly (S) \land H \times_{f} G \in Poly (S)) \to \deg (F -_{f} (H \times_{f} G)) \leq if (M \leq \deg (H \times_{f} G), \deg (H \times_{f} G), M)$
107	5 104 106	syl2anc	$⊢ φ \to \deg (F -_{f} (H \times_{f} G)) \leq if (M \leq \deg (H \times_{f} G), \deg (H \times_{f} G), M)$
108	17 15	dgreq0	$⊢ F \in Poly (S) \to (F = 0_{𝑝} \leftrightarrow A (M) = 0)$
109	5 108	syl	$⊢ φ \to (F = 0_{𝑝} \leftrightarrow A (M) = 0)$
110	109	necon3bid	$⊢ φ \to (F \neq 0_{𝑝} \leftrightarrow A (M) \neq 0)$
111	11 110	mpbid	$⊢ φ \to A (M) \neq 0$
112	28 35 111 39	divne0d	$⊢ φ \to \frac{A (M)}{B (N)} \neq 0$
113	20 53	sseldd	$⊢ φ \to \frac{A (M)}{B (N)} \in ℂ$
114	13	coe1term	$⊢ (\frac{A (M)}{B (N)} \in ℂ \land D \in ℕ_{0} \land D \in ℕ_{0}) \to coeff (H) (D) = if (D = D, \frac{A (M)}{B (N)}, 0)$
115	113 9 9 114	syl3anc	$⊢ φ \to coeff (H) (D) = if (D = D, \frac{A (M)}{B (N)}, 0)$
116		eqid	$⊢ D = D$
117	116	iftruei	$⊢ if (D = D, \frac{A (M)}{B (N)}, 0) = \frac{A (M)}{B (N)}$
118	115 117	eqtrdi	$⊢ φ \to coeff (H) (D) = \frac{A (M)}{B (N)}$
119		c0ex	$⊢ 0 \in V$
120	119	fvconst2	$⊢ D \in ℕ_{0} \to (ℕ_{0} \times \{0\}) (D) = 0$
121	9 120	syl	$⊢ φ \to (ℕ_{0} \times \{0\}) (D) = 0$
122	112 118 121	3netr4d	$⊢ φ \to coeff (H) (D) \neq (ℕ_{0} \times \{0\}) (D)$
123		fveq2	$⊢ H = 0_{𝑝} \to coeff (H) = coeff (0_{𝑝})$
124		coe0	$⊢ coeff (0_{𝑝}) = ℕ_{0} \times \{0\}$
125	123 124	eqtrdi	$⊢ H = 0_{𝑝} \to coeff (H) = ℕ_{0} \times \{0\}$
126	125	fveq1d	$⊢ H = 0_{𝑝} \to coeff (H) (D) = (ℕ_{0} \times \{0\}) (D)$
127	126	necon3i	$⊢ coeff (H) (D) \neq (ℕ_{0} \times \{0\}) (D) \to H \neq 0_{𝑝}$
128	122 127	syl	$⊢ φ \to H \neq 0_{𝑝}$
129		eqid	$⊢ \deg (H) = \deg (H)$
130	129 18	dgrmul	$⊢ ((H \in Poly (S) \land H \neq 0_{𝑝}) \land (G \in Poly (S) \land G \neq 0_{𝑝})) \to \deg (H \times_{f} G) = \deg (H) + N$
131	55 128 6 7 130	syl22anc	$⊢ φ \to \deg (H \times_{f} G) = \deg (H) + N$
132	13	dgr1term	$⊢ (\frac{A (M)}{B (N)} \in ℂ \land \frac{A (M)}{B (N)} \neq 0 \land D \in ℕ_{0}) \to \deg (H) = D$
133	113 112 9 132	syl3anc	$⊢ φ \to \deg (H) = D$
134	133 10	eqtr4d	$⊢ φ \to \deg (H) = M - N$
135	134	oveq1d	$⊢ φ \to \deg (H) + N = M - N + N$
136	26	nn0cnd	$⊢ φ \to M \in ℂ$
137	33	nn0cnd	$⊢ φ \to N \in ℂ$
138	136 137	npcand	$⊢ φ \to M - N + N = M$
139	135 138	eqtrd	$⊢ φ \to \deg (H) + N = M$
140	131 139	eqtrd	$⊢ φ \to \deg (H \times_{f} G) = M$
141	140	ifeq1d	$⊢ φ \to if (M \leq \deg (H \times_{f} G), \deg (H \times_{f} G), M) = if (M \leq \deg (H \times_{f} G), M, M)$
142		ifid	$⊢ if (M \leq \deg (H \times_{f} G), M, M) = M$
143	141 142	eqtrdi	$⊢ φ \to if (M \leq \deg (H \times_{f} G), \deg (H \times_{f} G), M) = M$
144	107 143	breqtrd	$⊢ φ \to \deg (F -_{f} (H \times_{f} G)) \leq M$
145		eqid	$⊢ coeff (H \times_{f} G) = coeff (H \times_{f} G)$
146	15 145	coesub	$⊢ (F \in Poly (S) \land H \times_{f} G \in Poly (S)) \to coeff (F -_{f} (H \times_{f} G)) = A -_{f} coeff (H \times_{f} G)$
147	5 104 146	syl2anc	$⊢ φ \to coeff (F -_{f} (H \times_{f} G)) = A -_{f} coeff (H \times_{f} G)$
148	147	fveq1d	$⊢ φ \to coeff (F -_{f} (H \times_{f} G)) (M) = (A -_{f} coeff (H \times_{f} G)) (M)$
149	15	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
150		ffn	$⊢ A : ℕ_{0} ⟶ ℂ \to A Fn ℕ_{0}$
151	5 149 150	3syl	$⊢ φ \to A Fn ℕ_{0}$
152	145	coef3	$⊢ H \times_{f} G \in Poly (S) \to coeff (H \times_{f} G) : ℕ_{0} ⟶ ℂ$
153		ffn	$⊢ coeff (H \times_{f} G) : ℕ_{0} ⟶ ℂ \to coeff (H \times_{f} G) Fn ℕ_{0}$
154	104 152 153	3syl	$⊢ φ \to coeff (H \times_{f} G) Fn ℕ_{0}$
155		nn0ex	$⊢ ℕ_{0} \in V$
156	155	a1i	$⊢ φ \to ℕ_{0} \in V$
157		inidm	$⊢ ℕ_{0} \cap ℕ_{0} = ℕ_{0}$
158		eqidd	$⊢ (φ \land M \in ℕ_{0}) \to A (M) = A (M)$
159		eqid	$⊢ coeff (H) = coeff (H)$
160	159 16 129 18	coemulhi	$⊢ (H \in Poly (S) \land G \in Poly (S)) \to coeff (H \times_{f} G) (\deg (H) + N) = coeff (H) (\deg (H)) B (N)$
161	55 6 160	syl2anc	$⊢ φ \to coeff (H \times_{f} G) (\deg (H) + N) = coeff (H) (\deg (H)) B (N)$
162	139	fveq2d	$⊢ φ \to coeff (H \times_{f} G) (\deg (H) + N) = coeff (H \times_{f} G) (M)$
163	133	fveq2d	$⊢ φ \to coeff (H) (\deg (H)) = coeff (H) (D)$
164	163 118	eqtrd	$⊢ φ \to coeff (H) (\deg (H)) = \frac{A (M)}{B (N)}$
165	164	oveq1d	$⊢ φ \to coeff (H) (\deg (H)) B (N) = (\frac{A (M)}{B (N)}) B (N)$
166	28 35 39	divcan1d	$⊢ φ \to (\frac{A (M)}{B (N)}) B (N) = A (M)$
167	165 166	eqtrd	$⊢ φ \to coeff (H) (\deg (H)) B (N) = A (M)$
168	161 162 167	3eqtr3d	$⊢ φ \to coeff (H \times_{f} G) (M) = A (M)$
169	168	adantr	$⊢ (φ \land M \in ℕ_{0}) \to coeff (H \times_{f} G) (M) = A (M)$
170	151 154 156 156 157 158 169	ofval	$⊢ (φ \land M \in ℕ_{0}) \to (A -_{f} coeff (H \times_{f} G)) (M) = A (M) - A (M)$
171	26 170	mpdan	$⊢ φ \to (A -_{f} coeff (H \times_{f} G)) (M) = A (M) - A (M)$
172	28	subidd	$⊢ φ \to A (M) - A (M) = 0$
173	148 171 172	3eqtrd	$⊢ φ \to coeff (F -_{f} (H \times_{f} G)) (M) = 0$
174	5 104 1 2 4	plysub	$⊢ φ \to F -_{f} (H \times_{f} G) \in Poly (S)$
175		dgrcl	$⊢ F -_{f} (H \times_{f} G) \in Poly (S) \to \deg (F -_{f} (H \times_{f} G)) \in ℕ_{0}$
176	174 175	syl	$⊢ φ \to \deg (F -_{f} (H \times_{f} G)) \in ℕ_{0}$
177	176	nn0red	$⊢ φ \to \deg (F -_{f} (H \times_{f} G)) \in ℝ$
178	26	nn0red	$⊢ φ \to M \in ℝ$
179	33	nn0red	$⊢ φ \to N \in ℝ$
180	177 178 179	ltsub1d	$⊢ φ \to (\deg (F -_{f} (H \times_{f} G)) < M \leftrightarrow \deg (F -_{f} (H \times_{f} G)) - N < M - N)$
181	10	breq2d	$⊢ φ \to (\deg (F -_{f} (H \times_{f} G)) - N < M - N \leftrightarrow \deg (F -_{f} (H \times_{f} G)) - N < D)$
182	180 181	bitrd	$⊢ φ \to (\deg (F -_{f} (H \times_{f} G)) < M \leftrightarrow \deg (F -_{f} (H \times_{f} G)) - N < D)$
183	182	orbi2d	$⊢ φ \to ((F -_{f} (H \times_{f} G) = 0_{𝑝} \lor \deg (F -_{f} (H \times_{f} G)) < M) \leftrightarrow (F -_{f} (H \times_{f} G) = 0_{𝑝} \lor \deg (F -_{f} (H \times_{f} G)) - N < D))$
184		eqid	$⊢ \deg (F -_{f} (H \times_{f} G)) = \deg (F -_{f} (H \times_{f} G))$
185		eqid	$⊢ coeff (F -_{f} (H \times_{f} G)) = coeff (F -_{f} (H \times_{f} G))$
186	184 185	dgrlt	$⊢ (F -_{f} (H \times_{f} G) \in Poly (S) \land M \in ℕ_{0}) \to ((F -_{f} (H \times_{f} G) = 0_{𝑝} \lor \deg (F -_{f} (H \times_{f} G)) < M) \leftrightarrow (\deg (F -_{f} (H \times_{f} G)) \leq M \land coeff (F -_{f} (H \times_{f} G)) (M) = 0))$
187	174 26 186	syl2anc	$⊢ φ \to ((F -_{f} (H \times_{f} G) = 0_{𝑝} \lor \deg (F -_{f} (H \times_{f} G)) < M) \leftrightarrow (\deg (F -_{f} (H \times_{f} G)) \leq M \land coeff (F -_{f} (H \times_{f} G)) (M) = 0))$
188	183 187	bitr3d	$⊢ φ \to ((F -_{f} (H \times_{f} G) = 0_{𝑝} \lor \deg (F -_{f} (H \times_{f} G)) - N < D) \leftrightarrow (\deg (F -_{f} (H \times_{f} G)) \leq M \land coeff (F -_{f} (H \times_{f} G)) (M) = 0))$
189	144 173 188	mpbir2and	$⊢ φ \to (F -_{f} (H \times_{f} G) = 0_{𝑝} \lor \deg (F -_{f} (H \times_{f} G)) - N < D)$
190		eqeq1	$⊢ f = F -_{f} (H \times_{f} G) \to (f = 0_{𝑝} \leftrightarrow F -_{f} (H \times_{f} G) = 0_{𝑝})$
191		fveq2	$⊢ f = F -_{f} (H \times_{f} G) \to \deg (f) = \deg (F -_{f} (H \times_{f} G))$
192	191	oveq1d	$⊢ f = F -_{f} (H \times_{f} G) \to \deg (f) - N = \deg (F -_{f} (H \times_{f} G)) - N$
193	192	breq1d	$⊢ f = F -_{f} (H \times_{f} G) \to (\deg (f) - N < D \leftrightarrow \deg (F -_{f} (H \times_{f} G)) - N < D)$
194	190 193	orbi12d	$⊢ f = F -_{f} (H \times_{f} G) \to ((f = 0_{𝑝} \lor \deg (f) - N < D) \leftrightarrow (F -_{f} (H \times_{f} G) = 0_{𝑝} \lor \deg (F -_{f} (H \times_{f} G)) - N < D))$
195		oveq1	$⊢ f = F -_{f} (H \times_{f} G) \to f -_{f} (G \times_{f} p) = (F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)$
196	12 195	eqtrid	$⊢ f = F -_{f} (H \times_{f} G) \to U = (F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)$
197	196	eqeq1d	$⊢ f = F -_{f} (H \times_{f} G) \to (U = 0_{𝑝} \leftrightarrow (F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p) = 0_{𝑝})$
198	196	fveq2d	$⊢ f = F -_{f} (H \times_{f} G) \to \deg (U) = \deg ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p))$
199	198	breq1d	$⊢ f = F -_{f} (H \times_{f} G) \to (\deg (U) < N \leftrightarrow \deg ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)) < N)$
200	197 199	orbi12d	$⊢ f = F -_{f} (H \times_{f} G) \to ((U = 0_{𝑝} \lor \deg (U) < N) \leftrightarrow ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p) = 0_{𝑝} \lor \deg ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)) < N))$
201	200	rexbidv	$⊢ f = F -_{f} (H \times_{f} G) \to (\exists p \in Poly (S) (U = 0_{𝑝} \lor \deg (U) < N) \leftrightarrow \exists p \in Poly (S) ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p) = 0_{𝑝} \lor \deg ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)) < N))$
202	194 201	imbi12d	$⊢ f = F -_{f} (H \times_{f} G) \to (((f = 0_{𝑝} \lor \deg (f) - N < D) \to \exists p \in Poly (S) (U = 0_{𝑝} \lor \deg (U) < N)) \leftrightarrow ((F -_{f} (H \times_{f} G) = 0_{𝑝} \lor \deg (F -_{f} (H \times_{f} G)) - N < D) \to \exists p \in Poly (S) ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p) = 0_{𝑝} \lor \deg ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)) < N)))$
203	202 14 174	rspcdva	$⊢ φ \to ((F -_{f} (H \times_{f} G) = 0_{𝑝} \lor \deg (F -_{f} (H \times_{f} G)) - N < D) \to \exists p \in Poly (S) ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p) = 0_{𝑝} \lor \deg ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)) < N))$
204	189 203	mpd	$⊢ φ \to \exists p \in Poly (S) ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p) = 0_{𝑝} \lor \deg ((F -_{f} (H \times_{f} G)) -_{f} (G \times_{f} p)) < N)$
205	103 204	r19.29a	$⊢ φ \to \exists q \in Poly (S) (R = 0_{𝑝} \lor \deg (R) < N)$

Metamath Proof Explorer

Theorem plydivlem4

Proof