signsply0

Description: Lemma for the rule of signs, based on Bolzano's intermediate value theorem for polynomials : If the lowest and highest coefficient A and B are of opposite signs, the polynomial admits a positive root. (Contributed by Thierry Arnoux, 19-Sep-2018)

	Ref	Expression
Hypotheses	signsply0.d	$⊢ D = \deg (F)$
	signsply0.c	$⊢ C = coeff (F)$
	signsply0.b	$⊢ B = C (D)$
	signsply0.a	$⊢ A = C (0)$
	signsply0.1	$⊢ φ \to F \in Poly (ℝ)$
	signsply0.2	$⊢ φ \to F \neq 0_{𝑝}$
	signsply0.3	$⊢ φ \to A B < 0$
Assertion	signsply0	$⊢ φ \to \exists z \in ℝ^{+} F (z) = 0$

Proof

Step	Hyp	Ref	Expression
1		signsply0.d	$⊢ D = \deg (F)$
2		signsply0.c	$⊢ C = coeff (F)$
3		signsply0.b	$⊢ B = C (D)$
4		signsply0.a	$⊢ A = C (0)$
5		signsply0.1	$⊢ φ \to F \in Poly (ℝ)$
6		signsply0.2	$⊢ φ \to F \neq 0_{𝑝}$
7		signsply0.3	$⊢ φ \to A B < 0$
8		simplr	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B)) \to d \in ℝ^{+}$
9		simpr	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B)) \to \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B)$
10		rpxr	$⊢ d \in ℝ^{+} \to d \in ℝ^{*}$
11	10	xrleidd	$⊢ d \in ℝ^{+} \to d \leq d$
12	11	ad2antlr	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B)) \to d \leq d$
13		id	$⊢ d \in ℝ^{+} \to d \in ℝ^{+}$
14		simpr	$⊢ (d \in ℝ^{+} \land f = d) \to f = d$
15	14	breq2d	$⊢ (d \in ℝ^{+} \land f = d) \to (d \leq f \leftrightarrow d \leq d)$
16	14	fveq2d	$⊢ (d \in ℝ^{+} \land f = d) \to F (f) = F (d)$
17	14	oveq1d	$⊢ (d \in ℝ^{+} \land f = d) \to f^{D} = d^{D}$
18	16 17	oveq12d	$⊢ (d \in ℝ^{+} \land f = d) \to \frac{F (f)}{f^{D}} = \frac{F (d)}{d^{D}}$
19	18	fvoveq1d	$⊢ (d \in ℝ^{+} \land f = d) \to \|(\frac{F (f)}{f^{D}}) - B\| = \|(\frac{F (d)}{d^{D}}) - B\|$
20	19	breq1d	$⊢ (d \in ℝ^{+} \land f = d) \to (\|(\frac{F (f)}{f^{D}}) - B\| < - B \leftrightarrow \|(\frac{F (d)}{d^{D}}) - B\| < - B)$
21	15 20	imbi12d	$⊢ (d \in ℝ^{+} \land f = d) \to ((d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B) \leftrightarrow (d \leq d \to \|(\frac{F (d)}{d^{D}}) - B\| < - B))$
22	13 21	rspcdv	$⊢ d \in ℝ^{+} \to (\forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B) \to (d \leq d \to \|(\frac{F (d)}{d^{D}}) - B\| < - B))$
23	8 9 12 22	syl3c	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B)) \to \|(\frac{F (d)}{d^{D}}) - B\| < - B$
24	5	ad2antrr	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to F \in Poly (ℝ)$
25		simpr	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to d \in ℝ^{+}$
26	25	rpred	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to d \in ℝ$
27	24 26	plyrecld	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to F (d) \in ℝ$
28		dgrcl	$⊢ F \in Poly (ℝ) \to \deg (F) \in ℕ_{0}$
29	5 28	syl	$⊢ φ \to \deg (F) \in ℕ_{0}$
30	1 29	eqeltrid	$⊢ φ \to D \in ℕ_{0}$
31	30	ad2antrr	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to D \in ℕ_{0}$
32	26 31	reexpcld	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to d^{D} \in ℝ$
33	25	rpcnd	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to d \in ℂ$
34	25	rpne0d	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to d \neq 0$
35	30	nn0zd	$⊢ φ \to D \in ℤ$
36	35	ad2antrr	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to D \in ℤ$
37	33 34 36	expne0d	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to d^{D} \neq 0$
38	27 32 37	redivcld	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to \frac{F (d)}{d^{D}} \in ℝ$
39		0re	$⊢ 0 \in ℝ$
40	2	coef2	$⊢ (F \in Poly (ℝ) \land 0 \in ℝ) \to C : ℕ_{0} ⟶ ℝ$
41	39 40	mpan2	$⊢ F \in Poly (ℝ) \to C : ℕ_{0} ⟶ ℝ$
42	41	ffvelrnda	$⊢ (F \in Poly (ℝ) \land D \in ℕ_{0}) \to C (D) \in ℝ$
43	3 42	eqeltrid	$⊢ (F \in Poly (ℝ) \land D \in ℕ_{0}) \to B \in ℝ$
44	5 30 43	syl2anc	$⊢ φ \to B \in ℝ$
45	44	ad2antrr	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to B \in ℝ$
46	45	renegcld	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to - B \in ℝ$
47	38 45 46	absdifltd	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to (\|(\frac{F (d)}{d^{D}}) - B\| < - B \leftrightarrow (B - (- B) < \frac{F (d)}{d^{D}} \land \frac{F (d)}{d^{D}} < B + (- B)))$
48	47	simplbda	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land \|(\frac{F (d)}{d^{D}}) - B\| < - B) \to \frac{F (d)}{d^{D}} < B + (- B)$
49	44	recnd	$⊢ φ \to B \in ℂ$
50	49	ad2antrr	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to B \in ℂ$
51	50	negidd	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to B + (- B) = 0$
52	51	adantr	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land \|(\frac{F (d)}{d^{D}}) - B\| < - B) \to B + (- B) = 0$
53	48 52	breqtrd	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land \|(\frac{F (d)}{d^{D}}) - B\| < - B) \to \frac{F (d)}{d^{D}} < 0$
54	25 36	rpexpcld	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to d^{D} \in ℝ^{+}$
55	27 54	ge0divd	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to (0 \leq F (d) \leftrightarrow 0 \leq \frac{F (d)}{d^{D}})$
56	55	notbid	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to (\neg 0 \leq F (d) \leftrightarrow \neg 0 \leq \frac{F (d)}{d^{D}})$
57		0red	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to 0 \in ℝ$
58	27 57	ltnled	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to (F (d) < 0 \leftrightarrow \neg 0 \leq F (d))$
59	38 57	ltnled	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to (\frac{F (d)}{d^{D}} < 0 \leftrightarrow \neg 0 \leq \frac{F (d)}{d^{D}})$
60	56 58 59	3bitr4d	$⊢ ((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \to (F (d) < 0 \leftrightarrow \frac{F (d)}{d^{D}} < 0)$
61	60	adantr	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land \|(\frac{F (d)}{d^{D}}) - B\| < - B) \to (F (d) < 0 \leftrightarrow \frac{F (d)}{d^{D}} < 0)$
62	53 61	mpbird	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land \|(\frac{F (d)}{d^{D}}) - B\| < - B) \to F (d) < 0$
63	23 62	syldan	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B)) \to F (d) < 0$
64		0red	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to 0 \in ℝ$
65		simplr	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to d \in ℝ^{+}$
66	65	rpred	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to d \in ℝ$
67	65	rpgt0d	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to 0 < d$
68		iccssre	$⊢ (0 \in ℝ \land d \in ℝ) \to [0, d] \subseteq ℝ$
69	39 66 68	sylancr	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to [0, d] \subseteq ℝ$
70		ax-resscn	$⊢ ℝ \subseteq ℂ$
71	69 70	sstrdi	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to [0, d] \subseteq ℂ$
72		plycn	$⊢ F \in Poly (ℝ) \to F : ℂ \underset{cn}{⟶} ℂ$
73	5 72	syl	$⊢ φ \to F : ℂ \underset{cn}{⟶} ℂ$
74	73	ad3antrrr	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to F : ℂ \underset{cn}{⟶} ℂ$
75	5	ad4antr	$⊢ ((((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \land x \in [0, d]) \to F \in Poly (ℝ)$
76	69	sselda	$⊢ ((((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \land x \in [0, d]) \to x \in ℝ$
77	75 76	plyrecld	$⊢ ((((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \land x \in [0, d]) \to F (x) \in ℝ$
78		simpr	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to F (d) < 0$
79		simplll	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to φ$
80	79 44	syl	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to B \in ℝ$
81		simpr	$⊢ (φ \land - B \in ℝ^{+}) \to - B \in ℝ^{+}$
82	81	ad2antrr	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to - B \in ℝ^{+}$
83		negelrp	$⊢ B \in ℝ \to (- B \in ℝ^{+} \leftrightarrow B < 0)$
84	83	biimpa	$⊢ (B \in ℝ \land - B \in ℝ^{+}) \to B < 0$
85	80 82 84	syl2anc	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to B < 0$
86	5 39 40	sylancl	$⊢ φ \to C : ℕ_{0} ⟶ ℝ$
87		0nn0	$⊢ 0 \in ℕ_{0}$
88	87	a1i	$⊢ φ \to 0 \in ℕ_{0}$
89	86 88	ffvelrnd	$⊢ φ \to C (0) \in ℝ$
90	4 89	eqeltrid	$⊢ φ \to A \in ℝ$
91	90 44 7	mul2lt0rlt0	$⊢ (φ \land B < 0) \to 0 < A$
92	91 4	breqtrdi	$⊢ (φ \land B < 0) \to 0 < C (0)$
93	79 85 92	syl2anc	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to 0 < C (0)$
94	2	coefv0	$⊢ F \in Poly (ℝ) \to F (0) = C (0)$
95	5 94	syl	$⊢ φ \to F (0) = C (0)$
96	95	ad3antrrr	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to F (0) = C (0)$
97	93 96	breqtrrd	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to 0 < F (0)$
98	78 97	jca	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to (F (d) < 0 \land 0 < F (0))$
99	64 66 64 67 71 74 77 98	ivth2	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to \exists z \in (0, d) F (z) = 0$
100		0le0	$⊢ 0 \leq 0$
101		pnfge	$⊢ d \in ℝ^{*} \to d \leq +∞$
102	10 101	syl	$⊢ d \in ℝ^{+} \to d \leq +∞$
103		0xr	$⊢ 0 \in ℝ^{*}$
104		pnfxr	$⊢ +∞ \in ℝ^{*}$
105		ioossioo	$⊢ ((0 \in ℝ^{} \land +∞ \in ℝ^{}) \land (0 \leq 0 \land d \leq +∞)) \to (0, d) \subseteq (0, +∞)$
106	103 104 105	mpanl12	$⊢ (0 \leq 0 \land d \leq +∞) \to (0, d) \subseteq (0, +∞)$
107	100 102 106	sylancr	$⊢ d \in ℝ^{+} \to (0, d) \subseteq (0, +∞)$
108		ioorp	$⊢ (0, +∞) = ℝ^{+}$
109	107 108	sseqtrdi	$⊢ d \in ℝ^{+} \to (0, d) \subseteq ℝ^{+}$
110		ssrexv	$⊢ (0, d) \subseteq ℝ^{+} \to (\exists z \in (0, d) F (z) = 0 \to \exists z \in ℝ^{+} F (z) = 0)$
111	65 109 110	3syl	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to (\exists z \in (0, d) F (z) = 0 \to \exists z \in ℝ^{+} F (z) = 0)$
112	99 111	mpd	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land F (d) < 0) \to \exists z \in ℝ^{+} F (z) = 0$
113	63 112	syldan	$⊢ (((φ \land - B \in ℝ^{+}) \land d \in ℝ^{+}) \land \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B)) \to \exists z \in ℝ^{+} F (z) = 0$
114		plyf	$⊢ F \in Poly (ℝ) \to F : ℂ ⟶ ℂ$
115	5 114	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
116	115	ffnd	$⊢ φ \to F Fn ℂ$
117		ovex	$⊢ x^{D} \in V$
118	117	rgenw	$⊢ \forall x \in ℝ^{+} x^{D} \in V$
119		eqid	$⊢ (x \in ℝ^{+} ⟼ x^{D}) = (x \in ℝ^{+} ⟼ x^{D})$
120	119	fnmpt	$⊢ \forall x \in ℝ^{+} x^{D} \in V \to (x \in ℝ^{+} ⟼ x^{D}) Fn ℝ^{+}$
121	118 120	mp1i	$⊢ φ \to (x \in ℝ^{+} ⟼ x^{D}) Fn ℝ^{+}$
122		cnex	$⊢ ℂ \in V$
123	122	a1i	$⊢ φ \to ℂ \in V$
124		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
125	124 70	sstri	$⊢ ℝ^{+} \subseteq ℂ$
126	122 125	ssexi	$⊢ ℝ^{+} \in V$
127	126	a1i	$⊢ φ \to ℝ^{+} \in V$
128		sseqin2	$⊢ ℝ^{+} \subseteq ℂ \leftrightarrow ℂ \cap ℝ^{+} = ℝ^{+}$
129	125 128	mpbi	$⊢ ℂ \cap ℝ^{+} = ℝ^{+}$
130		eqidd	$⊢ (φ \land f \in ℂ) \to F (f) = F (f)$
131		eqidd	$⊢ (φ \land f \in ℝ^{+}) \to (x \in ℝ^{+} ⟼ x^{D}) = (x \in ℝ^{+} ⟼ x^{D})$
132		simpr	$⊢ ((φ \land f \in ℝ^{+}) \land x = f) \to x = f$
133	132	oveq1d	$⊢ ((φ \land f \in ℝ^{+}) \land x = f) \to x^{D} = f^{D}$
134		simpr	$⊢ (φ \land f \in ℝ^{+}) \to f \in ℝ^{+}$
135		ovexd	$⊢ (φ \land f \in ℝ^{+}) \to f^{D} \in V$
136	131 133 134 135	fvmptd	$⊢ (φ \land f \in ℝ^{+}) \to (x \in ℝ^{+} ⟼ x^{D}) (f) = f^{D}$
137	116 121 123 127 129 130 136	offval	$⊢ φ \to F \div_{f} (x \in ℝ^{+} ⟼ x^{D}) = (f \in ℝ^{+} ⟼ \frac{F (f)}{f^{D}})$
138		oveq1	$⊢ x = f \to x^{D} = f^{D}$
139	138	cbvmptv	$⊢ (x \in ℝ^{+} ⟼ x^{D}) = (f \in ℝ^{+} ⟼ f^{D})$
140	1 2 3 139	signsplypnf	$⊢ F \in Poly (ℝ) \to (F \div_{f} (x \in ℝ^{+} ⟼ x^{D})) \underset{ℝ}{⇝} B$
141	5 140	syl	$⊢ φ \to (F \div_{f} (x \in ℝ^{+} ⟼ x^{D})) \underset{ℝ}{⇝} B$
142	137 141	eqbrtrrd	$⊢ φ \to (f \in ℝ^{+} ⟼ \frac{F (f)}{f^{D}}) \underset{ℝ}{⇝} B$
143	115	adantr	$⊢ (φ \land f \in ℝ^{+}) \to F : ℂ ⟶ ℂ$
144	134	rpcnd	$⊢ (φ \land f \in ℝ^{+}) \to f \in ℂ$
145	143 144	ffvelrnd	$⊢ (φ \land f \in ℝ^{+}) \to F (f) \in ℂ$
146	30	adantr	$⊢ (φ \land f \in ℝ^{+}) \to D \in ℕ_{0}$
147	144 146	expcld	$⊢ (φ \land f \in ℝ^{+}) \to f^{D} \in ℂ$
148	134	rpne0d	$⊢ (φ \land f \in ℝ^{+}) \to f \neq 0$
149	35	adantr	$⊢ (φ \land f \in ℝ^{+}) \to D \in ℤ$
150	144 148 149	expne0d	$⊢ (φ \land f \in ℝ^{+}) \to f^{D} \neq 0$
151	145 147 150	divcld	$⊢ (φ \land f \in ℝ^{+}) \to \frac{F (f)}{f^{D}} \in ℂ$
152	151	ralrimiva	$⊢ φ \to \forall f \in ℝ^{+} \frac{F (f)}{f^{D}} \in ℂ$
153	124	a1i	$⊢ φ \to ℝ^{+} \subseteq ℝ$
154		1red	$⊢ φ \to 1 \in ℝ$
155	152 153 49 154	rlim3	$⊢ φ \to ((f \in ℝ^{+} ⟼ \frac{F (f)}{f^{D}}) \underset{ℝ}{⇝} B \leftrightarrow \forall e \in ℝ^{+} \exists d \in [1, +∞) \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e))$
156	142 155	mpbid	$⊢ φ \to \forall e \in ℝ^{+} \exists d \in [1, +∞) \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e)$
157		0lt1	$⊢ 0 < 1$
158		pnfge	$⊢ +∞ \in ℝ^{*} \to +∞ \leq +∞$
159	104 158	ax-mp	$⊢ +∞ \leq +∞$
160		icossioo	$⊢ ((0 \in ℝ^{} \land +∞ \in ℝ^{}) \land (0 < 1 \land +∞ \leq +∞)) \to [1, +∞) \subseteq (0, +∞)$
161	103 104 157 159 160	mp4an	$⊢ [1, +∞) \subseteq (0, +∞)$
162	161 108	sseqtri	$⊢ [1, +∞) \subseteq ℝ^{+}$
163		ssrexv	$⊢ [1, +∞) \subseteq ℝ^{+} \to (\exists d \in [1, +∞) \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e) \to \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e))$
164	162 163	ax-mp	$⊢ \exists d \in [1, +∞) \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e) \to \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e)$
165	164	ralimi	$⊢ \forall e \in ℝ^{+} \exists d \in [1, +∞) \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e) \to \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e)$
166	156 165	syl	$⊢ φ \to \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e)$
167	166	adantr	$⊢ (φ \land - B \in ℝ^{+}) \to \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e)$
168		simpr	$⊢ ((φ \land - B \in ℝ^{+}) \land e = - B) \to e = - B$
169	168	breq2d	$⊢ ((φ \land - B \in ℝ^{+}) \land e = - B) \to (\|(\frac{F (f)}{f^{D}}) - B\| < e \leftrightarrow \|(\frac{F (f)}{f^{D}}) - B\| < - B)$
170	169	imbi2d	$⊢ ((φ \land - B \in ℝ^{+}) \land e = - B) \to ((d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e) \leftrightarrow (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B))$
171	170	rexralbidv	$⊢ ((φ \land - B \in ℝ^{+}) \land e = - B) \to (\exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e) \leftrightarrow \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B))$
172	81 171	rspcdv	$⊢ (φ \land - B \in ℝ^{+}) \to (\forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e) \to \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B))$
173	167 172	mpd	$⊢ (φ \land - B \in ℝ^{+}) \to \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < - B)$
174	113 173	r19.29a	$⊢ (φ \land - B \in ℝ^{+}) \to \exists z \in ℝ^{+} F (z) = 0$
175		simplr	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B)) \to d \in ℝ^{+}$
176		simpr	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B)) \to \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B)$
177	11	ad2antlr	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B)) \to d \leq d$
178	19	breq1d	$⊢ (d \in ℝ^{+} \land f = d) \to (\|(\frac{F (f)}{f^{D}}) - B\| < B \leftrightarrow \|(\frac{F (d)}{d^{D}}) - B\| < B)$
179	15 178	imbi12d	$⊢ (d \in ℝ^{+} \land f = d) \to ((d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B) \leftrightarrow (d \leq d \to \|(\frac{F (d)}{d^{D}}) - B\| < B))$
180	13 179	rspcdv	$⊢ d \in ℝ^{+} \to (\forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B) \to (d \leq d \to \|(\frac{F (d)}{d^{D}}) - B\| < B))$
181	175 176 177 180	syl3c	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B)) \to \|(\frac{F (d)}{d^{D}}) - B\| < B$
182	49	ad2antrr	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to B \in ℂ$
183	182	subidd	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to B - B = 0$
184	183	adantr	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land \|(\frac{F (d)}{d^{D}}) - B\| < B) \to B - B = 0$
185	5	ad2antrr	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to F \in Poly (ℝ)$
186	124	a1i	$⊢ (φ \land B \in ℝ^{+}) \to ℝ^{+} \subseteq ℝ$
187	186	sselda	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to d \in ℝ$
188	185 187	plyrecld	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to F (d) \in ℝ$
189	30	ad2antrr	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to D \in ℕ_{0}$
190	187 189	reexpcld	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to d^{D} \in ℝ$
191	187	recnd	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to d \in ℂ$
192		simpr	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to d \in ℝ^{+}$
193	192	rpne0d	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to d \neq 0$
194	35	ad2antrr	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to D \in ℤ$
195	191 193 194	expne0d	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to d^{D} \neq 0$
196	188 190 195	redivcld	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to \frac{F (d)}{d^{D}} \in ℝ$
197	44	ad2antrr	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to B \in ℝ$
198	196 197 197	absdifltd	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to (\|(\frac{F (d)}{d^{D}}) - B\| < B \leftrightarrow (B - B < \frac{F (d)}{d^{D}} \land \frac{F (d)}{d^{D}} < B + B))$
199	198	simprbda	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land \|(\frac{F (d)}{d^{D}}) - B\| < B) \to B - B < \frac{F (d)}{d^{D}}$
200	184 199	eqbrtrrd	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land \|(\frac{F (d)}{d^{D}}) - B\| < B) \to 0 < \frac{F (d)}{d^{D}}$
201	192 194	rpexpcld	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to d^{D} \in ℝ^{+}$
202	188 201	gt0divd	$⊢ ((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \to (0 < F (d) \leftrightarrow 0 < \frac{F (d)}{d^{D}})$
203	202	adantr	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land \|(\frac{F (d)}{d^{D}}) - B\| < B) \to (0 < F (d) \leftrightarrow 0 < \frac{F (d)}{d^{D}})$
204	200 203	mpbird	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land \|(\frac{F (d)}{d^{D}}) - B\| < B) \to 0 < F (d)$
205	181 204	syldan	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B)) \to 0 < F (d)$
206		0red	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to 0 \in ℝ$
207		simplr	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to d \in ℝ^{+}$
208	207	rpred	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to d \in ℝ$
209	207	rpgt0d	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to 0 < d$
210	39 208 68	sylancr	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to [0, d] \subseteq ℝ$
211	210 70	sstrdi	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to [0, d] \subseteq ℂ$
212	73	ad3antrrr	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to F : ℂ \underset{cn}{⟶} ℂ$
213	5	ad4antr	$⊢ ((((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \land x \in [0, d]) \to F \in Poly (ℝ)$
214	210	sselda	$⊢ ((((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \land x \in [0, d]) \to x \in ℝ$
215	213 214	plyrecld	$⊢ ((((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \land x \in [0, d]) \to F (x) \in ℝ$
216	95	ad3antrrr	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to F (0) = C (0)$
217		simplll	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to φ$
218		simpr1	$⊢ (φ \land (B \in ℝ^{+} \land d \in ℝ^{+} \land 0 < F (d))) \to B \in ℝ^{+}$
219	218	rpgt0d	$⊢ (φ \land (B \in ℝ^{+} \land d \in ℝ^{+} \land 0 < F (d))) \to 0 < B$
220	219	3anassrs	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to 0 < B$
221	90 44 7	mul2lt0rgt0	$⊢ (φ \land 0 < B) \to A < 0$
222	217 220 221	syl2anc	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to A < 0$
223	4 222	eqbrtrrid	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to C (0) < 0$
224	216 223	eqbrtrd	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to F (0) < 0$
225		simpr	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to 0 < F (d)$
226	224 225	jca	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to (F (0) < 0 \land 0 < F (d))$
227	206 208 206 209 211 212 215 226	ivth	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to \exists z \in (0, d) F (z) = 0$
228	207 109 110	3syl	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to (\exists z \in (0, d) F (z) = 0 \to \exists z \in ℝ^{+} F (z) = 0)$
229	227 228	mpd	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land 0 < F (d)) \to \exists z \in ℝ^{+} F (z) = 0$
230	205 229	syldan	$⊢ (((φ \land B \in ℝ^{+}) \land d \in ℝ^{+}) \land \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B)) \to \exists z \in ℝ^{+} F (z) = 0$
231	166	adantr	$⊢ (φ \land B \in ℝ^{+}) \to \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e)$
232		simpr	$⊢ (φ \land B \in ℝ^{+}) \to B \in ℝ^{+}$
233		simpr	$⊢ ((φ \land B \in ℝ^{+}) \land e = B) \to e = B$
234	233	breq2d	$⊢ ((φ \land B \in ℝ^{+}) \land e = B) \to (\|(\frac{F (f)}{f^{D}}) - B\| < e \leftrightarrow \|(\frac{F (f)}{f^{D}}) - B\| < B)$
235	234	imbi2d	$⊢ ((φ \land B \in ℝ^{+}) \land e = B) \to ((d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e) \leftrightarrow (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B))$
236	235	rexralbidv	$⊢ ((φ \land B \in ℝ^{+}) \land e = B) \to (\exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e) \leftrightarrow \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B))$
237	232 236	rspcdv	$⊢ (φ \land B \in ℝ^{+}) \to (\forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < e) \to \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B))$
238	231 237	mpd	$⊢ (φ \land B \in ℝ^{+}) \to \exists d \in ℝ^{+} \forall f \in ℝ^{+} (d \leq f \to \|(\frac{F (f)}{f^{D}}) - B\| < B)$
239	230 238	r19.29a	$⊢ (φ \land B \in ℝ^{+}) \to \exists z \in ℝ^{+} F (z) = 0$
240	1 2	dgreq0	$⊢ F \in Poly (ℝ) \to (F = 0_{𝑝} \leftrightarrow C (D) = 0)$
241	5 240	syl	$⊢ φ \to (F = 0_{𝑝} \leftrightarrow C (D) = 0)$
242	241	necon3bid	$⊢ φ \to (F \neq 0_{𝑝} \leftrightarrow C (D) \neq 0)$
243	6 242	mpbid	$⊢ φ \to C (D) \neq 0$
244	3	neeq1i	$⊢ B \neq 0 \leftrightarrow C (D) \neq 0$
245	243 244	sylibr	$⊢ φ \to B \neq 0$
246		rpneg	$⊢ (B \in ℝ \land B \neq 0) \to (B \in ℝ^{+} \leftrightarrow \neg - B \in ℝ^{+})$
247	246	biimprd	$⊢ (B \in ℝ \land B \neq 0) \to (\neg - B \in ℝ^{+} \to B \in ℝ^{+})$
248	247	orrd	$⊢ (B \in ℝ \land B \neq 0) \to (- B \in ℝ^{+} \lor B \in ℝ^{+})$
249	44 245 248	syl2anc	$⊢ φ \to (- B \in ℝ^{+} \lor B \in ℝ^{+})$
250	174 239 249	mpjaodan	$⊢ φ \to \exists z \in ℝ^{+} F (z) = 0$

Metamath Proof Explorer

Theorem signsply0

Proof