Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  signsply0 Structured version   Visualization version   GIF version

Theorem signsply0 31236
 Description: Lemma for the rule of signs, based on Bolzano's intermediate value theorem for polynomials : If the lowest and highest coefficient 𝐴 and 𝐵 are of opposite signs, the polynomial admits a positive root. (Contributed by Thierry Arnoux, 19-Sep-2018.)
Hypotheses
Ref Expression
signsply0.d 𝐷 = (deg‘𝐹)
signsply0.c 𝐶 = (coeff‘𝐹)
signsply0.b 𝐵 = (𝐶𝐷)
signsply0.a 𝐴 = (𝐶‘0)
signsply0.1 (𝜑𝐹 ∈ (Poly‘ℝ))
signsply0.2 (𝜑𝐹 ≠ 0𝑝)
signsply0.3 (𝜑 → (𝐴 · 𝐵) < 0)
Assertion
Ref Expression
signsply0 (𝜑 → ∃𝑧 ∈ ℝ+ (𝐹𝑧) = 0)
Distinct variable groups:   𝑧,𝐵   𝑧,𝐹   𝜑,𝑧
Allowed substitution hints:   𝐴(𝑧)   𝐶(𝑧)   𝐷(𝑧)

Proof of Theorem signsply0
Dummy variables 𝑒 𝑑 𝑓 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 759 . . . . . 6 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵)) → 𝑑 ∈ ℝ+)
2 simpr 479 . . . . . 6 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵)) → ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵))
3 rpxr 12153 . . . . . . . 8 (𝑑 ∈ ℝ+𝑑 ∈ ℝ*)
43xrleidd 12300 . . . . . . 7 (𝑑 ∈ ℝ+𝑑𝑑)
54ad2antlr 717 . . . . . 6 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵)) → 𝑑𝑑)
6 id 22 . . . . . . 7 (𝑑 ∈ ℝ+𝑑 ∈ ℝ+)
7 simpr 479 . . . . . . . . 9 ((𝑑 ∈ ℝ+𝑓 = 𝑑) → 𝑓 = 𝑑)
87breq2d 4900 . . . . . . . 8 ((𝑑 ∈ ℝ+𝑓 = 𝑑) → (𝑑𝑓𝑑𝑑))
97fveq2d 6452 . . . . . . . . . . 11 ((𝑑 ∈ ℝ+𝑓 = 𝑑) → (𝐹𝑓) = (𝐹𝑑))
107oveq1d 6939 . . . . . . . . . . 11 ((𝑑 ∈ ℝ+𝑓 = 𝑑) → (𝑓𝐷) = (𝑑𝐷))
119, 10oveq12d 6942 . . . . . . . . . 10 ((𝑑 ∈ ℝ+𝑓 = 𝑑) → ((𝐹𝑓) / (𝑓𝐷)) = ((𝐹𝑑) / (𝑑𝐷)))
1211fvoveq1d 6946 . . . . . . . . 9 ((𝑑 ∈ ℝ+𝑓 = 𝑑) → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) = (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)))
1312breq1d 4898 . . . . . . . 8 ((𝑑 ∈ ℝ+𝑓 = 𝑑) → ((abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵 ↔ (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < -𝐵))
148, 13imbi12d 336 . . . . . . 7 ((𝑑 ∈ ℝ+𝑓 = 𝑑) → ((𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵) ↔ (𝑑𝑑 → (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < -𝐵)))
156, 14rspcdv 3514 . . . . . 6 (𝑑 ∈ ℝ+ → (∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵) → (𝑑𝑑 → (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < -𝐵)))
161, 2, 5, 15syl3c 66 . . . . 5 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵)) → (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < -𝐵)
17 signsply0.1 . . . . . . . . . . . 12 (𝜑𝐹 ∈ (Poly‘ℝ))
1817ad2antrr 716 . . . . . . . . . . 11 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝐹 ∈ (Poly‘ℝ))
19 simpr 479 . . . . . . . . . . . 12 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝑑 ∈ ℝ+)
2019rpred 12186 . . . . . . . . . . 11 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝑑 ∈ ℝ)
2118, 20plyrecld 31234 . . . . . . . . . 10 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝐹𝑑) ∈ ℝ)
22 signsply0.d . . . . . . . . . . . . 13 𝐷 = (deg‘𝐹)
23 dgrcl 24437 . . . . . . . . . . . . . 14 (𝐹 ∈ (Poly‘ℝ) → (deg‘𝐹) ∈ ℕ0)
2417, 23syl 17 . . . . . . . . . . . . 13 (𝜑 → (deg‘𝐹) ∈ ℕ0)
2522, 24syl5eqel 2863 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℕ0)
2625ad2antrr 716 . . . . . . . . . . 11 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝐷 ∈ ℕ0)
2720, 26reexpcld 13349 . . . . . . . . . 10 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝑑𝐷) ∈ ℝ)
2819rpcnd 12188 . . . . . . . . . . 11 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝑑 ∈ ℂ)
2919rpne0d 12191 . . . . . . . . . . 11 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝑑 ≠ 0)
3025nn0zd 11837 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℤ)
3130ad2antrr 716 . . . . . . . . . . 11 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝐷 ∈ ℤ)
3228, 29, 31expne0d 13338 . . . . . . . . . 10 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝑑𝐷) ≠ 0)
3321, 27, 32redivcld 11206 . . . . . . . . 9 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → ((𝐹𝑑) / (𝑑𝐷)) ∈ ℝ)
34 signsply0.b . . . . . . . . . . . 12 𝐵 = (𝐶𝐷)
35 0re 10380 . . . . . . . . . . . . . 14 0 ∈ ℝ
36 signsply0.c . . . . . . . . . . . . . . 15 𝐶 = (coeff‘𝐹)
3736coef2 24435 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Poly‘ℝ) ∧ 0 ∈ ℝ) → 𝐶:ℕ0⟶ℝ)
3835, 37mpan2 681 . . . . . . . . . . . . 13 (𝐹 ∈ (Poly‘ℝ) → 𝐶:ℕ0⟶ℝ)
3938ffvelrnda 6625 . . . . . . . . . . . 12 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝐷 ∈ ℕ0) → (𝐶𝐷) ∈ ℝ)
4034, 39syl5eqel 2863 . . . . . . . . . . 11 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝐷 ∈ ℕ0) → 𝐵 ∈ ℝ)
4117, 25, 40syl2anc 579 . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
4241ad2antrr 716 . . . . . . . . 9 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝐵 ∈ ℝ)
4342renegcld 10805 . . . . . . . . 9 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → -𝐵 ∈ ℝ)
4433, 42, 43absdifltd 14587 . . . . . . . 8 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → ((abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < -𝐵 ↔ ((𝐵 − -𝐵) < ((𝐹𝑑) / (𝑑𝐷)) ∧ ((𝐹𝑑) / (𝑑𝐷)) < (𝐵 + -𝐵))))
4544simplbda 495 . . . . . . 7 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < -𝐵) → ((𝐹𝑑) / (𝑑𝐷)) < (𝐵 + -𝐵))
4641recnd 10407 . . . . . . . . . 10 (𝜑𝐵 ∈ ℂ)
4746ad2antrr 716 . . . . . . . . 9 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝐵 ∈ ℂ)
4847negidd 10726 . . . . . . . 8 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝐵 + -𝐵) = 0)
4948adantr 474 . . . . . . 7 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < -𝐵) → (𝐵 + -𝐵) = 0)
5045, 49breqtrd 4914 . . . . . 6 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < -𝐵) → ((𝐹𝑑) / (𝑑𝐷)) < 0)
5119, 31rpexpcld 13359 . . . . . . . . . 10 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝑑𝐷) ∈ ℝ+)
5221, 51ge0divd 12224 . . . . . . . . 9 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (0 ≤ (𝐹𝑑) ↔ 0 ≤ ((𝐹𝑑) / (𝑑𝐷))))
5352notbid 310 . . . . . . . 8 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (¬ 0 ≤ (𝐹𝑑) ↔ ¬ 0 ≤ ((𝐹𝑑) / (𝑑𝐷))))
54 0red 10382 . . . . . . . . 9 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 0 ∈ ℝ)
5521, 54ltnled 10525 . . . . . . . 8 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → ((𝐹𝑑) < 0 ↔ ¬ 0 ≤ (𝐹𝑑)))
5633, 54ltnled 10525 . . . . . . . 8 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (((𝐹𝑑) / (𝑑𝐷)) < 0 ↔ ¬ 0 ≤ ((𝐹𝑑) / (𝑑𝐷))))
5753, 55, 563bitr4d 303 . . . . . . 7 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → ((𝐹𝑑) < 0 ↔ ((𝐹𝑑) / (𝑑𝐷)) < 0))
5857adantr 474 . . . . . 6 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < -𝐵) → ((𝐹𝑑) < 0 ↔ ((𝐹𝑑) / (𝑑𝐷)) < 0))
5950, 58mpbird 249 . . . . 5 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < -𝐵) → (𝐹𝑑) < 0)
6016, 59syldan 585 . . . 4 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵)) → (𝐹𝑑) < 0)
61 0red 10382 . . . . . 6 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → 0 ∈ ℝ)
62 simplr 759 . . . . . . 7 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → 𝑑 ∈ ℝ+)
6362rpred 12186 . . . . . 6 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → 𝑑 ∈ ℝ)
6462rpgt0d 12189 . . . . . 6 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → 0 < 𝑑)
65 iccssre 12572 . . . . . . . 8 ((0 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (0[,]𝑑) ⊆ ℝ)
6635, 63, 65sylancr 581 . . . . . . 7 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → (0[,]𝑑) ⊆ ℝ)
67 ax-resscn 10331 . . . . . . 7 ℝ ⊆ ℂ
6866, 67syl6ss 3833 . . . . . 6 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → (0[,]𝑑) ⊆ ℂ)
69 plycn 24465 . . . . . . . 8 (𝐹 ∈ (Poly‘ℝ) → 𝐹 ∈ (ℂ–cn→ℂ))
7017, 69syl 17 . . . . . . 7 (𝜑𝐹 ∈ (ℂ–cn→ℂ))
7170ad3antrrr 720 . . . . . 6 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → 𝐹 ∈ (ℂ–cn→ℂ))
7217ad4antr 722 . . . . . . 7 (((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝐹 ∈ (Poly‘ℝ))
7366sselda 3821 . . . . . . 7 (((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝑥 ∈ ℝ)
7472, 73plyrecld 31234 . . . . . 6 (((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) ∧ 𝑥 ∈ (0[,]𝑑)) → (𝐹𝑥) ∈ ℝ)
75 simpr 479 . . . . . . 7 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → (𝐹𝑑) < 0)
76 simplll 765 . . . . . . . . 9 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → 𝜑)
7776, 41syl 17 . . . . . . . . . 10 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → 𝐵 ∈ ℝ)
78 simpr 479 . . . . . . . . . . 11 ((𝜑 ∧ -𝐵 ∈ ℝ+) → -𝐵 ∈ ℝ+)
7978ad2antrr 716 . . . . . . . . . 10 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → -𝐵 ∈ ℝ+)
80 negelrp 12177 . . . . . . . . . . 11 (𝐵 ∈ ℝ → (-𝐵 ∈ ℝ+𝐵 < 0))
8180biimpa 470 . . . . . . . . . 10 ((𝐵 ∈ ℝ ∧ -𝐵 ∈ ℝ+) → 𝐵 < 0)
8277, 79, 81syl2anc 579 . . . . . . . . 9 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → 𝐵 < 0)
83 signsply0.a . . . . . . . . . . . 12 𝐴 = (𝐶‘0)
8417, 35, 37sylancl 580 . . . . . . . . . . . . 13 (𝜑𝐶:ℕ0⟶ℝ)
85 0nn0 11664 . . . . . . . . . . . . . 14 0 ∈ ℕ0
8685a1i 11 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℕ0)
8784, 86ffvelrnd 6626 . . . . . . . . . . . 12 (𝜑 → (𝐶‘0) ∈ ℝ)
8883, 87syl5eqel 2863 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
89 signsply0.3 . . . . . . . . . . 11 (𝜑 → (𝐴 · 𝐵) < 0)
9088, 41, 89mul2lt0rlt0 12246 . . . . . . . . . 10 ((𝜑𝐵 < 0) → 0 < 𝐴)
9190, 83syl6breq 4929 . . . . . . . . 9 ((𝜑𝐵 < 0) → 0 < (𝐶‘0))
9276, 82, 91syl2anc 579 . . . . . . . 8 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → 0 < (𝐶‘0))
9336coefv0 24452 . . . . . . . . . 10 (𝐹 ∈ (Poly‘ℝ) → (𝐹‘0) = (𝐶‘0))
9417, 93syl 17 . . . . . . . . 9 (𝜑 → (𝐹‘0) = (𝐶‘0))
9594ad3antrrr 720 . . . . . . . 8 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → (𝐹‘0) = (𝐶‘0))
9692, 95breqtrrd 4916 . . . . . . 7 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → 0 < (𝐹‘0))
9775, 96jca 507 . . . . . 6 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → ((𝐹𝑑) < 0 ∧ 0 < (𝐹‘0)))
9861, 63, 61, 64, 68, 71, 74, 97ivth2 23670 . . . . 5 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → ∃𝑧 ∈ (0(,)𝑑)(𝐹𝑧) = 0)
99 0le0 11488 . . . . . . . 8 0 ≤ 0
100 pnfge 12280 . . . . . . . . 9 (𝑑 ∈ ℝ*𝑑 ≤ +∞)
1013, 100syl 17 . . . . . . . 8 (𝑑 ∈ ℝ+𝑑 ≤ +∞)
102 0xr 10425 . . . . . . . . 9 0 ∈ ℝ*
103 pnfxr 10432 . . . . . . . . 9 +∞ ∈ ℝ*
104 ioossioo 12583 . . . . . . . . 9 (((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0 ≤ 0 ∧ 𝑑 ≤ +∞)) → (0(,)𝑑) ⊆ (0(,)+∞))
105102, 103, 104mpanl12 692 . . . . . . . 8 ((0 ≤ 0 ∧ 𝑑 ≤ +∞) → (0(,)𝑑) ⊆ (0(,)+∞))
10699, 101, 105sylancr 581 . . . . . . 7 (𝑑 ∈ ℝ+ → (0(,)𝑑) ⊆ (0(,)+∞))
107 ioorp 12568 . . . . . . 7 (0(,)+∞) = ℝ+
108106, 107syl6sseq 3870 . . . . . 6 (𝑑 ∈ ℝ+ → (0(,)𝑑) ⊆ ℝ+)
109 ssrexv 3886 . . . . . 6 ((0(,)𝑑) ⊆ ℝ+ → (∃𝑧 ∈ (0(,)𝑑)(𝐹𝑧) = 0 → ∃𝑧 ∈ ℝ+ (𝐹𝑧) = 0))
11062, 108, 1093syl 18 . . . . 5 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → (∃𝑧 ∈ (0(,)𝑑)(𝐹𝑧) = 0 → ∃𝑧 ∈ ℝ+ (𝐹𝑧) = 0))
11198, 110mpd 15 . . . 4 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (𝐹𝑑) < 0) → ∃𝑧 ∈ ℝ+ (𝐹𝑧) = 0)
11260, 111syldan 585 . . 3 ((((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵)) → ∃𝑧 ∈ ℝ+ (𝐹𝑧) = 0)
113 plyf 24402 . . . . . . . . . . 11 (𝐹 ∈ (Poly‘ℝ) → 𝐹:ℂ⟶ℂ)
11417, 113syl 17 . . . . . . . . . 10 (𝜑𝐹:ℂ⟶ℂ)
115114ffnd 6294 . . . . . . . . 9 (𝜑𝐹 Fn ℂ)
116 ovex 6956 . . . . . . . . . . 11 (𝑥𝐷) ∈ V
117116rgenw 3106 . . . . . . . . . 10 𝑥 ∈ ℝ+ (𝑥𝐷) ∈ V
118 eqid 2778 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ ↦ (𝑥𝐷)) = (𝑥 ∈ ℝ+ ↦ (𝑥𝐷))
119118fnmpt 6268 . . . . . . . . . 10 (∀𝑥 ∈ ℝ+ (𝑥𝐷) ∈ V → (𝑥 ∈ ℝ+ ↦ (𝑥𝐷)) Fn ℝ+)
120117, 119mp1i 13 . . . . . . . . 9 (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑥𝐷)) Fn ℝ+)
121 cnex 10355 . . . . . . . . . 10 ℂ ∈ V
122121a1i 11 . . . . . . . . 9 (𝜑 → ℂ ∈ V)
123 rpssre 12149 . . . . . . . . . . . 12 + ⊆ ℝ
124123, 67sstri 3830 . . . . . . . . . . 11 + ⊆ ℂ
125121, 124ssexi 5042 . . . . . . . . . 10 + ∈ V
126125a1i 11 . . . . . . . . 9 (𝜑 → ℝ+ ∈ V)
127 sseqin2 4040 . . . . . . . . . 10 (ℝ+ ⊆ ℂ ↔ (ℂ ∩ ℝ+) = ℝ+)
128124, 127mpbi 222 . . . . . . . . 9 (ℂ ∩ ℝ+) = ℝ+
129 eqidd 2779 . . . . . . . . 9 ((𝜑𝑓 ∈ ℂ) → (𝐹𝑓) = (𝐹𝑓))
130 eqidd 2779 . . . . . . . . . 10 ((𝜑𝑓 ∈ ℝ+) → (𝑥 ∈ ℝ+ ↦ (𝑥𝐷)) = (𝑥 ∈ ℝ+ ↦ (𝑥𝐷)))
131 simpr 479 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ℝ+) ∧ 𝑥 = 𝑓) → 𝑥 = 𝑓)
132131oveq1d 6939 . . . . . . . . . 10 (((𝜑𝑓 ∈ ℝ+) ∧ 𝑥 = 𝑓) → (𝑥𝐷) = (𝑓𝐷))
133 simpr 479 . . . . . . . . . 10 ((𝜑𝑓 ∈ ℝ+) → 𝑓 ∈ ℝ+)
134 ovexd 6958 . . . . . . . . . 10 ((𝜑𝑓 ∈ ℝ+) → (𝑓𝐷) ∈ V)
135130, 132, 133, 134fvmptd 6550 . . . . . . . . 9 ((𝜑𝑓 ∈ ℝ+) → ((𝑥 ∈ ℝ+ ↦ (𝑥𝐷))‘𝑓) = (𝑓𝐷))
136115, 120, 122, 126, 128, 129, 135offval 7183 . . . . . . . 8 (𝜑 → (𝐹𝑓 / (𝑥 ∈ ℝ+ ↦ (𝑥𝐷))) = (𝑓 ∈ ℝ+ ↦ ((𝐹𝑓) / (𝑓𝐷))))
137 oveq1 6931 . . . . . . . . . . 11 (𝑥 = 𝑓 → (𝑥𝐷) = (𝑓𝐷))
138137cbvmptv 4987 . . . . . . . . . 10 (𝑥 ∈ ℝ+ ↦ (𝑥𝐷)) = (𝑓 ∈ ℝ+ ↦ (𝑓𝐷))
13922, 36, 34, 138signsplypnf 31235 . . . . . . . . 9 (𝐹 ∈ (Poly‘ℝ) → (𝐹𝑓 / (𝑥 ∈ ℝ+ ↦ (𝑥𝐷))) ⇝𝑟 𝐵)
14017, 139syl 17 . . . . . . . 8 (𝜑 → (𝐹𝑓 / (𝑥 ∈ ℝ+ ↦ (𝑥𝐷))) ⇝𝑟 𝐵)
141136, 140eqbrtrrd 4912 . . . . . . 7 (𝜑 → (𝑓 ∈ ℝ+ ↦ ((𝐹𝑓) / (𝑓𝐷))) ⇝𝑟 𝐵)
142114adantr 474 . . . . . . . . . . 11 ((𝜑𝑓 ∈ ℝ+) → 𝐹:ℂ⟶ℂ)
143133rpcnd 12188 . . . . . . . . . . 11 ((𝜑𝑓 ∈ ℝ+) → 𝑓 ∈ ℂ)
144142, 143ffvelrnd 6626 . . . . . . . . . 10 ((𝜑𝑓 ∈ ℝ+) → (𝐹𝑓) ∈ ℂ)
14525adantr 474 . . . . . . . . . . 11 ((𝜑𝑓 ∈ ℝ+) → 𝐷 ∈ ℕ0)
146143, 145expcld 13332 . . . . . . . . . 10 ((𝜑𝑓 ∈ ℝ+) → (𝑓𝐷) ∈ ℂ)
147133rpne0d 12191 . . . . . . . . . . 11 ((𝜑𝑓 ∈ ℝ+) → 𝑓 ≠ 0)
14830adantr 474 . . . . . . . . . . 11 ((𝜑𝑓 ∈ ℝ+) → 𝐷 ∈ ℤ)
149143, 147, 148expne0d 13338 . . . . . . . . . 10 ((𝜑𝑓 ∈ ℝ+) → (𝑓𝐷) ≠ 0)
150144, 146, 149divcld 11154 . . . . . . . . 9 ((𝜑𝑓 ∈ ℝ+) → ((𝐹𝑓) / (𝑓𝐷)) ∈ ℂ)
151150ralrimiva 3148 . . . . . . . 8 (𝜑 → ∀𝑓 ∈ ℝ+ ((𝐹𝑓) / (𝑓𝐷)) ∈ ℂ)
152123a1i 11 . . . . . . . 8 (𝜑 → ℝ+ ⊆ ℝ)
153 1red 10379 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
154151, 152, 46, 153rlim3 14646 . . . . . . 7 (𝜑 → ((𝑓 ∈ ℝ+ ↦ ((𝐹𝑓) / (𝑓𝐷))) ⇝𝑟 𝐵 ↔ ∀𝑒 ∈ ℝ+𝑑 ∈ (1[,)+∞)∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒)))
155141, 154mpbid 224 . . . . . 6 (𝜑 → ∀𝑒 ∈ ℝ+𝑑 ∈ (1[,)+∞)∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒))
156 0lt1 10900 . . . . . . . . . 10 0 < 1
157 pnfge 12280 . . . . . . . . . . 11 (+∞ ∈ ℝ* → +∞ ≤ +∞)
158103, 157ax-mp 5 . . . . . . . . . 10 +∞ ≤ +∞
159 icossioo 12582 . . . . . . . . . 10 (((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0 < 1 ∧ +∞ ≤ +∞)) → (1[,)+∞) ⊆ (0(,)+∞))
160102, 103, 156, 158, 159mp4an 683 . . . . . . . . 9 (1[,)+∞) ⊆ (0(,)+∞)
161160, 107sseqtri 3856 . . . . . . . 8 (1[,)+∞) ⊆ ℝ+
162 ssrexv 3886 . . . . . . . 8 ((1[,)+∞) ⊆ ℝ+ → (∃𝑑 ∈ (1[,)+∞)∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒)))
163161, 162ax-mp 5 . . . . . . 7 (∃𝑑 ∈ (1[,)+∞)∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒))
164163ralimi 3134 . . . . . 6 (∀𝑒 ∈ ℝ+𝑑 ∈ (1[,)+∞)∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒) → ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒))
165155, 164syl 17 . . . . 5 (𝜑 → ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒))
166165adantr 474 . . . 4 ((𝜑 ∧ -𝐵 ∈ ℝ+) → ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒))
167 simpr 479 . . . . . . . 8 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → 𝑒 = -𝐵)
168167breq2d 4900 . . . . . . 7 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → ((abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒 ↔ (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵))
169168imbi2d 332 . . . . . 6 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → ((𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒) ↔ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵)))
170169rexralbidv 3243 . . . . 5 (((𝜑 ∧ -𝐵 ∈ ℝ+) ∧ 𝑒 = -𝐵) → (∃𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵)))
17178, 170rspcdv 3514 . . . 4 ((𝜑 ∧ -𝐵 ∈ ℝ+) → (∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵)))
172166, 171mpd 15 . . 3 ((𝜑 ∧ -𝐵 ∈ ℝ+) → ∃𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < -𝐵))
173112, 172r19.29a 3264 . 2 ((𝜑 ∧ -𝐵 ∈ ℝ+) → ∃𝑧 ∈ ℝ+ (𝐹𝑧) = 0)
174 simplr 759 . . . . . 6 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵)) → 𝑑 ∈ ℝ+)
175 simpr 479 . . . . . 6 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵)) → ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵))
1764ad2antlr 717 . . . . . 6 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵)) → 𝑑𝑑)
17712breq1d 4898 . . . . . . . 8 ((𝑑 ∈ ℝ+𝑓 = 𝑑) → ((abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵 ↔ (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < 𝐵))
1788, 177imbi12d 336 . . . . . . 7 ((𝑑 ∈ ℝ+𝑓 = 𝑑) → ((𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵) ↔ (𝑑𝑑 → (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < 𝐵)))
1796, 178rspcdv 3514 . . . . . 6 (𝑑 ∈ ℝ+ → (∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵) → (𝑑𝑑 → (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < 𝐵)))
180174, 175, 176, 179syl3c 66 . . . . 5 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵)) → (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < 𝐵)
18146ad2antrr 716 . . . . . . . . 9 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝐵 ∈ ℂ)
182181subidd 10724 . . . . . . . 8 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝐵𝐵) = 0)
183182adantr 474 . . . . . . 7 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < 𝐵) → (𝐵𝐵) = 0)
18417ad2antrr 716 . . . . . . . . . . 11 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝐹 ∈ (Poly‘ℝ))
185123a1i 11 . . . . . . . . . . . 12 ((𝜑𝐵 ∈ ℝ+) → ℝ+ ⊆ ℝ)
186185sselda 3821 . . . . . . . . . . 11 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝑑 ∈ ℝ)
187184, 186plyrecld 31234 . . . . . . . . . 10 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝐹𝑑) ∈ ℝ)
18825ad2antrr 716 . . . . . . . . . . 11 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝐷 ∈ ℕ0)
189186, 188reexpcld 13349 . . . . . . . . . 10 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝑑𝐷) ∈ ℝ)
190186recnd 10407 . . . . . . . . . . 11 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝑑 ∈ ℂ)
191 simpr 479 . . . . . . . . . . . 12 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝑑 ∈ ℝ+)
192191rpne0d 12191 . . . . . . . . . . 11 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝑑 ≠ 0)
19330ad2antrr 716 . . . . . . . . . . 11 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝐷 ∈ ℤ)
194190, 192, 193expne0d 13338 . . . . . . . . . 10 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝑑𝐷) ≠ 0)
195187, 189, 194redivcld 11206 . . . . . . . . 9 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → ((𝐹𝑑) / (𝑑𝐷)) ∈ ℝ)
19641ad2antrr 716 . . . . . . . . 9 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝐵 ∈ ℝ)
197195, 196, 196absdifltd 14587 . . . . . . . 8 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → ((abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < 𝐵 ↔ ((𝐵𝐵) < ((𝐹𝑑) / (𝑑𝐷)) ∧ ((𝐹𝑑) / (𝑑𝐷)) < (𝐵 + 𝐵))))
198197simprbda 494 . . . . . . 7 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < 𝐵) → (𝐵𝐵) < ((𝐹𝑑) / (𝑑𝐷)))
199183, 198eqbrtrrd 4912 . . . . . 6 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < 𝐵) → 0 < ((𝐹𝑑) / (𝑑𝐷)))
200191, 193rpexpcld 13359 . . . . . . . 8 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝑑𝐷) ∈ ℝ+)
201187, 200gt0divd 12223 . . . . . . 7 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (0 < (𝐹𝑑) ↔ 0 < ((𝐹𝑑) / (𝑑𝐷))))
202201adantr 474 . . . . . 6 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < 𝐵) → (0 < (𝐹𝑑) ↔ 0 < ((𝐹𝑑) / (𝑑𝐷))))
203199, 202mpbird 249 . . . . 5 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ (abs‘(((𝐹𝑑) / (𝑑𝐷)) − 𝐵)) < 𝐵) → 0 < (𝐹𝑑))
204180, 203syldan 585 . . . 4 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵)) → 0 < (𝐹𝑑))
205 0red 10382 . . . . . 6 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → 0 ∈ ℝ)
206 simplr 759 . . . . . . 7 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → 𝑑 ∈ ℝ+)
207206rpred 12186 . . . . . 6 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → 𝑑 ∈ ℝ)
208206rpgt0d 12189 . . . . . 6 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → 0 < 𝑑)
20935, 207, 65sylancr 581 . . . . . . 7 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → (0[,]𝑑) ⊆ ℝ)
210209, 67syl6ss 3833 . . . . . 6 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → (0[,]𝑑) ⊆ ℂ)
21170ad3antrrr 720 . . . . . 6 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → 𝐹 ∈ (ℂ–cn→ℂ))
21217ad4antr 722 . . . . . . 7 (((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝐹 ∈ (Poly‘ℝ))
213209sselda 3821 . . . . . . 7 (((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) ∧ 𝑥 ∈ (0[,]𝑑)) → 𝑥 ∈ ℝ)
214212, 213plyrecld 31234 . . . . . 6 (((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) ∧ 𝑥 ∈ (0[,]𝑑)) → (𝐹𝑥) ∈ ℝ)
21594ad3antrrr 720 . . . . . . . 8 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → (𝐹‘0) = (𝐶‘0))
216 simplll 765 . . . . . . . . . 10 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → 𝜑)
217 simpr1 1205 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 ∈ ℝ+𝑑 ∈ ℝ+ ∧ 0 < (𝐹𝑑))) → 𝐵 ∈ ℝ+)
218217rpgt0d 12189 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 ∈ ℝ+𝑑 ∈ ℝ+ ∧ 0 < (𝐹𝑑))) → 0 < 𝐵)
2192183anassrs 1422 . . . . . . . . . 10 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → 0 < 𝐵)
22088, 41, 89mul2lt0rgt0 12247 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝐵) → 𝐴 < 0)
221216, 219, 220syl2anc 579 . . . . . . . . 9 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → 𝐴 < 0)
22283, 221syl5eqbrr 4924 . . . . . . . 8 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → (𝐶‘0) < 0)
223215, 222eqbrtrd 4910 . . . . . . 7 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → (𝐹‘0) < 0)
224 simpr 479 . . . . . . 7 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → 0 < (𝐹𝑑))
225223, 224jca 507 . . . . . 6 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → ((𝐹‘0) < 0 ∧ 0 < (𝐹𝑑)))
226205, 207, 205, 208, 210, 211, 214, 225ivth 23669 . . . . 5 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → ∃𝑧 ∈ (0(,)𝑑)(𝐹𝑧) = 0)
227206, 108, 1093syl 18 . . . . 5 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → (∃𝑧 ∈ (0(,)𝑑)(𝐹𝑧) = 0 → ∃𝑧 ∈ ℝ+ (𝐹𝑧) = 0))
228226, 227mpd 15 . . . 4 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 0 < (𝐹𝑑)) → ∃𝑧 ∈ ℝ+ (𝐹𝑧) = 0)
229204, 228syldan 585 . . 3 ((((𝜑𝐵 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵)) → ∃𝑧 ∈ ℝ+ (𝐹𝑧) = 0)
230165adantr 474 . . . 4 ((𝜑𝐵 ∈ ℝ+) → ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒))
231 simpr 479 . . . . 5 ((𝜑𝐵 ∈ ℝ+) → 𝐵 ∈ ℝ+)
232 simpr 479 . . . . . . . 8 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
233232breq2d 4900 . . . . . . 7 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → ((abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒 ↔ (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵))
234233imbi2d 332 . . . . . 6 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → ((𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒) ↔ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵)))
235234rexralbidv 3243 . . . . 5 (((𝜑𝐵 ∈ ℝ+) ∧ 𝑒 = 𝐵) → (∃𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵)))
236231, 235rspcdv 3514 . . . 4 ((𝜑𝐵 ∈ ℝ+) → (∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝑒) → ∃𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵)))
237230, 236mpd 15 . . 3 ((𝜑𝐵 ∈ ℝ+) → ∃𝑑 ∈ ℝ+𝑓 ∈ ℝ+ (𝑑𝑓 → (abs‘(((𝐹𝑓) / (𝑓𝐷)) − 𝐵)) < 𝐵))
238229, 237r19.29a 3264 . 2 ((𝜑𝐵 ∈ ℝ+) → ∃𝑧 ∈ ℝ+ (𝐹𝑧) = 0)
239 signsply0.2 . . . . 5 (𝜑𝐹 ≠ 0𝑝)
24022, 36dgreq0 24469 . . . . . . 7 (𝐹 ∈ (Poly‘ℝ) → (𝐹 = 0𝑝 ↔ (𝐶𝐷) = 0))
24117, 240syl 17 . . . . . 6 (𝜑 → (𝐹 = 0𝑝 ↔ (𝐶𝐷) = 0))
242241necon3bid 3013 . . . . 5 (𝜑 → (𝐹 ≠ 0𝑝 ↔ (𝐶𝐷) ≠ 0))
243239, 242mpbid 224 . . . 4 (𝜑 → (𝐶𝐷) ≠ 0)
24434neeq1i 3033 . . . 4 (𝐵 ≠ 0 ↔ (𝐶𝐷) ≠ 0)
245243, 244sylibr 226 . . 3 (𝜑𝐵 ≠ 0)
246 rpneg 12176 . . . . 5 ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐵 ∈ ℝ+ ↔ ¬ -𝐵 ∈ ℝ+))
247246biimprd 240 . . . 4 ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (¬ -𝐵 ∈ ℝ+𝐵 ∈ ℝ+))
248247orrd 852 . . 3 ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (-𝐵 ∈ ℝ+𝐵 ∈ ℝ+))
24941, 245, 248syl2anc 579 . 2 (𝜑 → (-𝐵 ∈ ℝ+𝐵 ∈ ℝ+))
250173, 238, 249mpjaodan 944 1 (𝜑 → ∃𝑧 ∈ ℝ+ (𝐹𝑧) = 0)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 836   ∧ w3a 1071   = wceq 1601   ∈ wcel 2107   ≠ wne 2969  ∀wral 3090  ∃wrex 3091  Vcvv 3398   ∩ cin 3791   ⊆ wss 3792   class class class wbr 4888   ↦ cmpt 4967   Fn wfn 6132  ⟶wf 6133  ‘cfv 6137  (class class class)co 6924   ∘𝑓 cof 7174  ℂcc 10272  ℝcr 10273  0cc0 10274  1c1 10275   + caddc 10277   · cmul 10279  +∞cpnf 10410  ℝ*cxr 10412   < clt 10413   ≤ cle 10414   − cmin 10608  -cneg 10609   / cdiv 11035  ℕ0cn0 11647  ℤcz 11733  ℝ+crp 12142  (,)cioo 12492  [,)cico 12494  [,]cicc 12495  ↑cexp 13183  abscabs 14387   ⇝𝑟 crli 14633  –cn→ccncf 23098  0𝑝c0p 23884  Polycply 24388  coeffccoe 24390  degcdgr 24391 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352  ax-addf 10353  ax-mulf 10354 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-iin 4758  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-of 7176  df-om 7346  df-1st 7447  df-2nd 7448  df-supp 7579  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-2o 7846  df-oadd 7849  df-er 8028  df-map 8144  df-pm 8145  df-ixp 8197  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-fsupp 8566  df-fi 8607  df-sup 8638  df-inf 8639  df-oi 8706  df-card 9100  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11036  df-nn 11380  df-2 11443  df-3 11444  df-4 11445  df-5 11446  df-6 11447  df-7 11448  df-8 11449  df-9 11450  df-n0 11648  df-z 11734  df-dec 11851  df-uz 11998  df-q 12101  df-rp 12143  df-xneg 12262  df-xadd 12263  df-xmul 12264  df-ioo 12496  df-ioc 12497  df-ico 12498  df-icc 12499  df-fz 12649  df-fzo 12790  df-fl 12917  df-mod 12993  df-seq 13125  df-exp 13184  df-fac 13385  df-bc 13414  df-hash 13442  df-shft 14220  df-cj 14252  df-re 14253  df-im 14254  df-sqrt 14388  df-abs 14389  df-limsup 14619  df-clim 14636  df-rlim 14637  df-sum 14834  df-ef 15209  df-sin 15211  df-cos 15212  df-pi 15214  df-struct 16268  df-ndx 16269  df-slot 16270  df-base 16272  df-sets 16273  df-ress 16274  df-plusg 16362  df-mulr 16363  df-starv 16364  df-sca 16365  df-vsca 16366  df-ip 16367  df-tset 16368  df-ple 16369  df-ds 16371  df-unif 16372  df-hom 16373  df-cco 16374  df-rest 16480  df-topn 16481  df-0g 16499  df-gsum 16500  df-topgen 16501  df-pt 16502  df-prds 16505  df-xrs 16559  df-qtop 16564  df-imas 16565  df-xps 16567  df-mre 16643  df-mrc 16644  df-acs 16646  df-mgm 17639  df-sgrp 17681  df-mnd 17692  df-submnd 17733  df-mulg 17939  df-cntz 18144  df-cmn 18592  df-psmet 20145  df-xmet 20146  df-met 20147  df-bl 20148  df-mopn 20149  df-fbas 20150  df-fg 20151  df-cnfld 20154  df-top 21117  df-topon 21134  df-topsp 21156  df-bases 21169  df-cld 21242  df-ntr 21243  df-cls 21244  df-nei 21321  df-lp 21359  df-perf 21360  df-cn 21450  df-cnp 21451  df-haus 21538  df-tx 21785  df-hmeo 21978  df-fil 22069  df-fm 22161  df-flim 22162  df-flf 22163  df-xms 22544  df-ms 22545  df-tms 22546  df-cncf 23100  df-0p 23885  df-limc 24078  df-dv 24079  df-ply 24392  df-coe 24394  df-dgr 24395  df-log 24751  df-cxp 24752 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator