Metamath Proof Explorer

Theorem 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 ⊢ 𝐷 = ( deg ‘ 𝐹 )
signsply0.c ⊢ 𝐶 = ( coeff ‘ 𝐹 )
signsply0.b ⊢ 𝐵 = ( 𝐶 ‘ 𝐷 )
signsply0.a ⊢ 𝐴 = ( 𝐶 ‘ 0 )
signsply0.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℝ ) )
signsply0.2 ⊢ ( 𝜑 → 𝐹 ≠ 0𝑝 )
signsply0.3 ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) < 0 )
Assertion signsply0 ( 𝜑 → ∃ 𝑧 ∈ ℝ+ ( 𝐹 ‘ 𝑧 ) = 0 )

Proof

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