signsplypnf

Description: The quotient of a polynomial F by a monic monomial of same degree G converges to the highest coefficient of F . (Contributed by Thierry Arnoux, 18-Sep-2018)

	Ref	Expression
Hypotheses	signsply0.d	$⊢ D = \deg (F)$
	signsply0.c	$⊢ C = coeff (F)$
	signsply0.b	$⊢ B = C (D)$
	signsplypnf.g	$⊢ G = (x \in ℝ^{+} ⟼ x^{D})$
Assertion	signsplypnf	$⊢ F \in Poly (ℝ) \to (F \div_{f} G) \underset{ℝ}{⇝} B$

Proof

Step	Hyp	Ref	Expression
1		signsply0.d	$⊢ D = \deg (F)$
2		signsply0.c	$⊢ C = coeff (F)$
3		signsply0.b	$⊢ B = C (D)$
4		signsplypnf.g	$⊢ G = (x \in ℝ^{+} ⟼ x^{D})$
5		plyf	$⊢ F \in Poly (ℝ) \to F : ℂ ⟶ ℂ$
6	5	ffnd	$⊢ F \in Poly (ℝ) \to F Fn ℂ$
7		ovex	$⊢ x^{D} \in V$
8	7	rgenw	$⊢ \forall x \in ℝ^{+} x^{D} \in V$
9	4	fnmpt	$⊢ \forall x \in ℝ^{+} x^{D} \in V \to G Fn ℝ^{+}$
10	8 9	mp1i	$⊢ F \in Poly (ℝ) \to G Fn ℝ^{+}$
11		cnex	$⊢ ℂ \in V$
12	11	a1i	$⊢ F \in Poly (ℝ) \to ℂ \in V$
13		reex	$⊢ ℝ \in V$
14		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
15	13 14	ssexi	$⊢ ℝ^{+} \in V$
16	15	a1i	$⊢ F \in Poly (ℝ) \to ℝ^{+} \in V$
17		ax-resscn	$⊢ ℝ \subseteq ℂ$
18	14 17	sstri	$⊢ ℝ^{+} \subseteq ℂ$
19		sseqin2	$⊢ ℝ^{+} \subseteq ℂ \leftrightarrow ℂ \cap ℝ^{+} = ℝ^{+}$
20	18 19	mpbi	$⊢ ℂ \cap ℝ^{+} = ℝ^{+}$
21	2 1	coeid2	$⊢ (F \in Poly (ℝ) \land x \in ℂ) \to F (x) = \sum_{k = 0}^{D} C (k) x^{k}$
22	4	fvmpt2	$⊢ (x \in ℝ^{+} \land x^{D} \in V) \to G (x) = x^{D}$
23	7 22	mpan2	$⊢ x \in ℝ^{+} \to G (x) = x^{D}$
24	23	adantl	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to G (x) = x^{D}$
25	6 10 12 16 20 21 24	offval	$⊢ F \in Poly (ℝ) \to F \div_{f} G = (x \in ℝ^{+} ⟼ \frac{\sum_{k = 0}^{D} C (k) x^{k}}{x^{D}})$
26		fzfid	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to (0 \dots D) \in Fin$
27	18	a1i	$⊢ F \in Poly (ℝ) \to ℝ^{+} \subseteq ℂ$
28	27	sselda	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to x \in ℂ$
29		dgrcl	$⊢ F \in Poly (ℝ) \to \deg (F) \in ℕ_{0}$
30	1 29	eqeltrid	$⊢ F \in Poly (ℝ) \to D \in ℕ_{0}$
31	30	adantr	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to D \in ℕ_{0}$
32	28 31	expcld	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to x^{D} \in ℂ$
33	2	coef3	$⊢ F \in Poly (ℝ) \to C : ℕ_{0} ⟶ ℂ$
34	33	ad2antrr	$⊢ ((F \in Poly (ℝ) \land x \in ℝ^{+}) \land k \in (0 \dots D)) \to C : ℕ_{0} ⟶ ℂ$
35		elfznn0	$⊢ k \in (0 \dots D) \to k \in ℕ_{0}$
36	35	adantl	$⊢ ((F \in Poly (ℝ) \land x \in ℝ^{+}) \land k \in (0 \dots D)) \to k \in ℕ_{0}$
37	34 36	ffvelcdmd	$⊢ ((F \in Poly (ℝ) \land x \in ℝ^{+}) \land k \in (0 \dots D)) \to C (k) \in ℂ$
38	28	adantr	$⊢ ((F \in Poly (ℝ) \land x \in ℝ^{+}) \land k \in (0 \dots D)) \to x \in ℂ$
39	38 36	expcld	$⊢ ((F \in Poly (ℝ) \land x \in ℝ^{+}) \land k \in (0 \dots D)) \to x^{k} \in ℂ$
40	37 39	mulcld	$⊢ ((F \in Poly (ℝ) \land x \in ℝ^{+}) \land k \in (0 \dots D)) \to C (k) x^{k} \in ℂ$
41		rpne0	$⊢ x \in ℝ^{+} \to x \neq 0$
42	41	adantl	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to x \neq 0$
43	30	nn0zd	$⊢ F \in Poly (ℝ) \to D \in ℤ$
44	43	adantr	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to D \in ℤ$
45	28 42 44	expne0d	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to x^{D} \neq 0$
46	26 32 40 45	fsumdivc	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to \frac{\sum_{k = 0}^{D} C (k) x^{k}}{x^{D}} = \sum_{k = 0}^{D} (\frac{C (k) x^{k}}{x^{D}})$
47		fzosn	$⊢ D \in ℤ \to (D ..^D + 1) = \{D\}$
48	47	ineq2d	$⊢ D \in ℤ \to (0 ..^D) \cap (D ..^D + 1) = (0 ..^D) \cap \{D\}$
49		fzodisj	$⊢ (0 ..^D) \cap (D ..^D + 1) = \emptyset$
50	48 49	eqtr3di	$⊢ D \in ℤ \to (0 ..^D) \cap \{D\} = \emptyset$
51	44 50	syl	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to (0 ..^D) \cap \{D\} = \emptyset$
52		fzval3	$⊢ D \in ℤ \to (0 \dots D) = (0 ..^D + 1)$
53	43 52	syl	$⊢ F \in Poly (ℝ) \to (0 \dots D) = (0 ..^D + 1)$
54		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
55	30 54	eleqtrdi	$⊢ F \in Poly (ℝ) \to D \in ℤ_{\geq 0}$
56		fzosplitsn	$⊢ D \in ℤ_{\geq 0} \to (0 ..^D + 1) = (0 ..^D) \cup \{D\}$
57	55 56	syl	$⊢ F \in Poly (ℝ) \to (0 ..^D + 1) = (0 ..^D) \cup \{D\}$
58	53 57	eqtrd	$⊢ F \in Poly (ℝ) \to (0 \dots D) = (0 ..^D) \cup \{D\}$
59	58	adantr	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to (0 \dots D) = (0 ..^D) \cup \{D\}$
60	32	adantr	$⊢ ((F \in Poly (ℝ) \land x \in ℝ^{+}) \land k \in (0 \dots D)) \to x^{D} \in ℂ$
61	42	adantr	$⊢ ((F \in Poly (ℝ) \land x \in ℝ^{+}) \land k \in (0 \dots D)) \to x \neq 0$
62	44	adantr	$⊢ ((F \in Poly (ℝ) \land x \in ℝ^{+}) \land k \in (0 \dots D)) \to D \in ℤ$
63	38 61 62	expne0d	$⊢ ((F \in Poly (ℝ) \land x \in ℝ^{+}) \land k \in (0 \dots D)) \to x^{D} \neq 0$
64	40 60 63	divcld	$⊢ ((F \in Poly (ℝ) \land x \in ℝ^{+}) \land k \in (0 \dots D)) \to \frac{C (k) x^{k}}{x^{D}} \in ℂ$
65	51 59 26 64	fsumsplit	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to \sum_{k = 0}^{D} (\frac{C (k) x^{k}}{x^{D}}) = \sum_{k \in (0 ..^D)} (\frac{C (k) x^{k}}{x^{D}}) + \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}})$
66	46 65	eqtrd	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to \frac{\sum_{k = 0}^{D} C (k) x^{k}}{x^{D}} = \sum_{k \in (0 ..^D)} (\frac{C (k) x^{k}}{x^{D}}) + \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}})$
67	66	mpteq2dva	$⊢ F \in Poly (ℝ) \to (x \in ℝ^{+} ⟼ \frac{\sum_{k = 0}^{D} C (k) x^{k}}{x^{D}}) = (x \in ℝ^{+} ⟼ \sum_{k \in (0 ..^D)} (\frac{C (k) x^{k}}{x^{D}}) + \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}}))$
68	25 67	eqtrd	$⊢ F \in Poly (ℝ) \to F \div_{f} G = (x \in ℝ^{+} ⟼ \sum_{k \in (0 ..^D)} (\frac{C (k) x^{k}}{x^{D}}) + \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}}))$
69		sumex	$⊢ \sum_{k \in (0 ..^D)} (\frac{C (k) x^{k}}{x^{D}}) \in V$
70	69	a1i	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to \sum_{k \in (0 ..^D)} (\frac{C (k) x^{k}}{x^{D}}) \in V$
71		sumex	$⊢ \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}}) \in V$
72	71	a1i	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}}) \in V$
73	14	a1i	$⊢ F \in Poly (ℝ) \to ℝ^{+} \subseteq ℝ$
74		fzofi	$⊢ (0 ..^D) \in Fin$
75	74	a1i	$⊢ F \in Poly (ℝ) \to (0 ..^D) \in Fin$
76		ovexd	$⊢ (F \in Poly (ℝ) \land (x \in ℝ^{+} \land k \in (0 ..^D))) \to \frac{C (k) x^{k}}{x^{D}} \in V$
77	33	ad2antrr	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to C : ℕ_{0} ⟶ ℂ$
78		elfzonn0	$⊢ k \in (0 ..^D) \to k \in ℕ_{0}$
79	78	ad2antlr	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to k \in ℕ_{0}$
80	77 79	ffvelcdmd	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to C (k) \in ℂ$
81	28	adantlr	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to x \in ℂ$
82	81 79	expcld	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to x^{k} \in ℂ$
83	32	adantlr	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to x^{D} \in ℂ$
84	41	adantl	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to x \neq 0$
85	44	adantlr	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to D \in ℤ$
86	81 84 85	expne0d	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to x^{D} \neq 0$
87	80 82 83 86	divassd	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to \frac{C (k) x^{k}}{x^{D}} = C (k) (\frac{x^{k}}{x^{D}})$
88	87	mpteq2dva	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to (x \in ℝ^{+} ⟼ \frac{C (k) x^{k}}{x^{D}}) = (x \in ℝ^{+} ⟼ C (k) (\frac{x^{k}}{x^{D}}))$
89		fvexd	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to C (k) \in V$
90		ovexd	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to \frac{x^{k}}{x^{D}} \in V$
91	33	adantr	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to C : ℕ_{0} ⟶ ℂ$
92	78	adantl	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to k \in ℕ_{0}$
93	91 92	ffvelcdmd	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to C (k) \in ℂ$
94		rlimconst	$⊢ (ℝ^{+} \subseteq ℝ \land C (k) \in ℂ) \to (x \in ℝ^{+} ⟼ C (k)) \underset{ℝ}{⇝} C (k)$
95	14 93 94	sylancr	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to (x \in ℝ^{+} ⟼ C (k)) \underset{ℝ}{⇝} C (k)$
96	79	nn0zd	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to k \in ℤ$
97	85 96	zsubcld	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to D - k \in ℤ$
98	81 84 97	cxpexpzd	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to x^{D - k} = x^{D - k}$
99	98	oveq2d	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to \frac{1}{x^{D - k}} = \frac{1}{x^{D - k}}$
100	81 84 97	expnegd	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to x^{- (D - k)} = \frac{1}{x^{D - k}}$
101	85	zcnd	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to D \in ℂ$
102	79	nn0cnd	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to k \in ℂ$
103	101 102	negsubdi2d	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to - (D - k) = k - D$
104	103	oveq2d	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to x^{- (D - k)} = x^{k - D}$
105	99 100 104	3eqtr2d	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to \frac{1}{x^{D - k}} = x^{k - D}$
106	81 84 85 96	expsubd	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to x^{k - D} = \frac{x^{k}}{x^{D}}$
107	105 106	eqtrd	$⊢ ((F \in Poly (ℝ) \land k \in (0 ..^D)) \land x \in ℝ^{+}) \to \frac{1}{x^{D - k}} = \frac{x^{k}}{x^{D}}$
108	107	mpteq2dva	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to (x \in ℝ^{+} ⟼ \frac{1}{x^{D - k}}) = (x \in ℝ^{+} ⟼ \frac{x^{k}}{x^{D}})$
109	92	nn0red	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to k \in ℝ$
110	30	adantr	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to D \in ℕ_{0}$
111	110	nn0red	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to D \in ℝ$
112		elfzolt2	$⊢ k \in (0 ..^D) \to k < D$
113	112	adantl	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to k < D$
114		difrp	$⊢ (k \in ℝ \land D \in ℝ) \to (k < D \leftrightarrow D - k \in ℝ^{+})$
115	114	biimpa	$⊢ ((k \in ℝ \land D \in ℝ) \land k < D) \to D - k \in ℝ^{+}$
116	109 111 113 115	syl21anc	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to D - k \in ℝ^{+}$
117		cxplim	$⊢ D - k \in ℝ^{+} \to (x \in ℝ^{+} ⟼ \frac{1}{x^{D - k}}) \underset{ℝ}{⇝} 0$
118	116 117	syl	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to (x \in ℝ^{+} ⟼ \frac{1}{x^{D - k}}) \underset{ℝ}{⇝} 0$
119	108 118	eqbrtrrd	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to (x \in ℝ^{+} ⟼ \frac{x^{k}}{x^{D}}) \underset{ℝ}{⇝} 0$
120	89 90 95 119	rlimmul	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to (x \in ℝ^{+} ⟼ C (k) (\frac{x^{k}}{x^{D}})) \underset{ℝ}{⇝} C (k) \cdot 0$
121	93	mul01d	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to C (k) \cdot 0 = 0$
122	120 121	breqtrd	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to (x \in ℝ^{+} ⟼ C (k) (\frac{x^{k}}{x^{D}})) \underset{ℝ}{⇝} 0$
123	88 122	eqbrtrd	$⊢ (F \in Poly (ℝ) \land k \in (0 ..^D)) \to (x \in ℝ^{+} ⟼ \frac{C (k) x^{k}}{x^{D}}) \underset{ℝ}{⇝} 0$
124	73 75 76 123	fsumrlim	$⊢ F \in Poly (ℝ) \to (x \in ℝ^{+} ⟼ \sum_{k \in (0 ..^D)} (\frac{C (k) x^{k}}{x^{D}})) \underset{ℝ}{⇝} \sum_{k \in (0 ..^D)} 0$
125	75	olcd	$⊢ F \in Poly (ℝ) \to ((0 ..^D) \subseteq ℤ_{\geq 0} \lor (0 ..^D) \in Fin)$
126		sumz	$⊢ ((0 ..^D) \subseteq ℤ_{\geq 0} \lor (0 ..^D) \in Fin) \to \sum_{k \in (0 ..^D)} 0 = 0$
127	125 126	syl	$⊢ F \in Poly (ℝ) \to \sum_{k \in (0 ..^D)} 0 = 0$
128	124 127	breqtrd	$⊢ F \in Poly (ℝ) \to (x \in ℝ^{+} ⟼ \sum_{k \in (0 ..^D)} (\frac{C (k) x^{k}}{x^{D}})) \underset{ℝ}{⇝} 0$
129	33 30	ffvelcdmd	$⊢ F \in Poly (ℝ) \to C (D) \in ℂ$
130	129	adantr	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to C (D) \in ℂ$
131	130 32	mulcld	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to C (D) x^{D} \in ℂ$
132	131 32 45	divcld	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to \frac{C (D) x^{D}}{x^{D}} \in ℂ$
133		fveq2	$⊢ k = D \to C (k) = C (D)$
134		oveq2	$⊢ k = D \to x^{k} = x^{D}$
135	133 134	oveq12d	$⊢ k = D \to C (k) x^{k} = C (D) x^{D}$
136	135	oveq1d	$⊢ k = D \to \frac{C (k) x^{k}}{x^{D}} = \frac{C (D) x^{D}}{x^{D}}$
137	136	sumsn	$⊢ (D \in ℕ_{0} \land \frac{C (D) x^{D}}{x^{D}} \in ℂ) \to \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}}) = \frac{C (D) x^{D}}{x^{D}}$
138	31 132 137	syl2anc	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}}) = \frac{C (D) x^{D}}{x^{D}}$
139	130 32 45	divcan4d	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to \frac{C (D) x^{D}}{x^{D}} = C (D)$
140	138 139	eqtrd	$⊢ (F \in Poly (ℝ) \land x \in ℝ^{+}) \to \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}}) = C (D)$
141	140	mpteq2dva	$⊢ F \in Poly (ℝ) \to (x \in ℝ^{+} ⟼ \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}})) = (x \in ℝ^{+} ⟼ C (D))$
142		rlimconst	$⊢ (ℝ^{+} \subseteq ℝ \land C (D) \in ℂ) \to (x \in ℝ^{+} ⟼ C (D)) \underset{ℝ}{⇝} C (D)$
143	14 129 142	sylancr	$⊢ F \in Poly (ℝ) \to (x \in ℝ^{+} ⟼ C (D)) \underset{ℝ}{⇝} C (D)$
144	141 143	eqbrtrd	$⊢ F \in Poly (ℝ) \to (x \in ℝ^{+} ⟼ \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}})) \underset{ℝ}{⇝} C (D)$
145	70 72 128 144	rlimadd	$⊢ F \in Poly (ℝ) \to (x \in ℝ^{+} ⟼ \sum_{k \in (0 ..^D)} (\frac{C (k) x^{k}}{x^{D}}) + \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}})) \underset{ℝ}{⇝} (0 + C (D))$
146	129	addlidd	$⊢ F \in Poly (ℝ) \to 0 + C (D) = C (D)$
147	146 3	eqtr4di	$⊢ F \in Poly (ℝ) \to 0 + C (D) = B$
148	145 147	breqtrd	$⊢ F \in Poly (ℝ) \to (x \in ℝ^{+} ⟼ \sum_{k \in (0 ..^D)} (\frac{C (k) x^{k}}{x^{D}}) + \sum_{k \in \{D\}} (\frac{C (k) x^{k}}{x^{D}})) \underset{ℝ}{⇝} B$
149	68 148	eqbrtrd	$⊢ F \in Poly (ℝ) \to (F \div_{f} G) \underset{ℝ}{⇝} B$

Metamath Proof Explorer

Theorem signsplypnf

Proof