Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . . . 6
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅)) β π β β+) |
2 | | simpr 486 |
. . . . . 6
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅)) β βπ β β+ (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅)) |
3 | | rpxr 12931 |
. . . . . . . 8
β’ (π β β+
β π β
β*) |
4 | 3 | xrleidd 13078 |
. . . . . . 7
β’ (π β β+
β π β€ π) |
5 | 4 | ad2antlr 726 |
. . . . . 6
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅)) β π β€ π) |
6 | | id 22 |
. . . . . . 7
β’ (π β β+
β π β
β+) |
7 | | simpr 486 |
. . . . . . . . 9
β’ ((π β β+
β§ π = π) β π = π) |
8 | 7 | breq2d 5122 |
. . . . . . . 8
β’ ((π β β+
β§ π = π) β (π β€ π β π β€ π)) |
9 | 7 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β β+
β§ π = π) β (πΉβπ) = (πΉβπ)) |
10 | 7 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π β β+
β§ π = π) β (πβπ·) = (πβπ·)) |
11 | 9, 10 | oveq12d 7380 |
. . . . . . . . . 10
β’ ((π β β+
β§ π = π) β ((πΉβπ) / (πβπ·)) = ((πΉβπ) / (πβπ·))) |
12 | 11 | fvoveq1d 7384 |
. . . . . . . . 9
β’ ((π β β+
β§ π = π) β (absβ(((πΉβπ) / (πβπ·)) β π΅)) = (absβ(((πΉβπ) / (πβπ·)) β π΅))) |
13 | 12 | breq1d 5120 |
. . . . . . . 8
β’ ((π β β+
β§ π = π) β ((absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅ β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅)) |
14 | 8, 13 | imbi12d 345 |
. . . . . . 7
β’ ((π β β+
β§ π = π) β ((π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅) β (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅))) |
15 | 6, 14 | rspcdv 3576 |
. . . . . 6
β’ (π β β+
β (βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅) β (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅))) |
16 | 1, 2, 5, 15 | syl3c 66 |
. . . . 5
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅)) β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅) |
17 | | signsply0.1 |
. . . . . . . . . . . 12
β’ (π β πΉ β
(Polyββ)) |
18 | 17 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ -π΅ β β+) β§ π β β+)
β πΉ β
(Polyββ)) |
19 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ -π΅ β β+) β§ π β β+)
β π β
β+) |
20 | 19 | rpred 12964 |
. . . . . . . . . . 11
β’ (((π β§ -π΅ β β+) β§ π β β+)
β π β
β) |
21 | 18, 20 | plyrecld 33201 |
. . . . . . . . . 10
β’ (((π β§ -π΅ β β+) β§ π β β+)
β (πΉβπ) β
β) |
22 | | signsply0.d |
. . . . . . . . . . . . 13
β’ π· = (degβπΉ) |
23 | | dgrcl 25610 |
. . . . . . . . . . . . . 14
β’ (πΉ β (Polyββ)
β (degβπΉ) β
β0) |
24 | 17, 23 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (degβπΉ) β
β0) |
25 | 22, 24 | eqeltrid 2842 |
. . . . . . . . . . . 12
β’ (π β π· β
β0) |
26 | 25 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ -π΅ β β+) β§ π β β+)
β π· β
β0) |
27 | 20, 26 | reexpcld 14075 |
. . . . . . . . . 10
β’ (((π β§ -π΅ β β+) β§ π β β+)
β (πβπ·) β
β) |
28 | 19 | rpcnd 12966 |
. . . . . . . . . . 11
β’ (((π β§ -π΅ β β+) β§ π β β+)
β π β
β) |
29 | 19 | rpne0d 12969 |
. . . . . . . . . . 11
β’ (((π β§ -π΅ β β+) β§ π β β+)
β π β
0) |
30 | 25 | nn0zd 12532 |
. . . . . . . . . . . 12
β’ (π β π· β β€) |
31 | 30 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ -π΅ β β+) β§ π β β+)
β π· β
β€) |
32 | 28, 29, 31 | expne0d 14064 |
. . . . . . . . . 10
β’ (((π β§ -π΅ β β+) β§ π β β+)
β (πβπ·) β 0) |
33 | 21, 27, 32 | redivcld 11990 |
. . . . . . . . 9
β’ (((π β§ -π΅ β β+) β§ π β β+)
β ((πΉβπ) / (πβπ·)) β β) |
34 | | signsply0.b |
. . . . . . . . . . . 12
β’ π΅ = (πΆβπ·) |
35 | | 0re 11164 |
. . . . . . . . . . . . . 14
β’ 0 β
β |
36 | | signsply0.c |
. . . . . . . . . . . . . . 15
β’ πΆ = (coeffβπΉ) |
37 | 36 | coef2 25608 |
. . . . . . . . . . . . . 14
β’ ((πΉ β (Polyββ)
β§ 0 β β) β πΆ:β0βΆβ) |
38 | 35, 37 | mpan2 690 |
. . . . . . . . . . . . 13
β’ (πΉ β (Polyββ)
β πΆ:β0βΆβ) |
39 | 38 | ffvelcdmda 7040 |
. . . . . . . . . . . 12
β’ ((πΉ β (Polyββ)
β§ π· β
β0) β (πΆβπ·) β β) |
40 | 34, 39 | eqeltrid 2842 |
. . . . . . . . . . 11
β’ ((πΉ β (Polyββ)
β§ π· β
β0) β π΅ β β) |
41 | 17, 25, 40 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β π΅ β β) |
42 | 41 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ -π΅ β β+) β§ π β β+)
β π΅ β
β) |
43 | 42 | renegcld 11589 |
. . . . . . . . 9
β’ (((π β§ -π΅ β β+) β§ π β β+)
β -π΅ β
β) |
44 | 33, 42, 43 | absdifltd 15325 |
. . . . . . . 8
β’ (((π β§ -π΅ β β+) β§ π β β+)
β ((absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅ β ((π΅ β -π΅) < ((πΉβπ) / (πβπ·)) β§ ((πΉβπ) / (πβπ·)) < (π΅ + -π΅)))) |
45 | 44 | simplbda 501 |
. . . . . . 7
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅) β ((πΉβπ) / (πβπ·)) < (π΅ + -π΅)) |
46 | 41 | recnd 11190 |
. . . . . . . . . 10
β’ (π β π΅ β β) |
47 | 46 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ -π΅ β β+) β§ π β β+)
β π΅ β
β) |
48 | 47 | negidd 11509 |
. . . . . . . 8
β’ (((π β§ -π΅ β β+) β§ π β β+)
β (π΅ + -π΅) = 0) |
49 | 48 | adantr 482 |
. . . . . . 7
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅) β (π΅ + -π΅) = 0) |
50 | 45, 49 | breqtrd 5136 |
. . . . . 6
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅) β ((πΉβπ) / (πβπ·)) < 0) |
51 | 19, 31 | rpexpcld 14157 |
. . . . . . . . . 10
β’ (((π β§ -π΅ β β+) β§ π β β+)
β (πβπ·) β
β+) |
52 | 21, 51 | ge0divd 13002 |
. . . . . . . . 9
β’ (((π β§ -π΅ β β+) β§ π β β+)
β (0 β€ (πΉβπ) β 0 β€ ((πΉβπ) / (πβπ·)))) |
53 | 52 | notbid 318 |
. . . . . . . 8
β’ (((π β§ -π΅ β β+) β§ π β β+)
β (Β¬ 0 β€ (πΉβπ) β Β¬ 0 β€ ((πΉβπ) / (πβπ·)))) |
54 | | 0red 11165 |
. . . . . . . . 9
β’ (((π β§ -π΅ β β+) β§ π β β+)
β 0 β β) |
55 | 21, 54 | ltnled 11309 |
. . . . . . . 8
β’ (((π β§ -π΅ β β+) β§ π β β+)
β ((πΉβπ) < 0 β Β¬ 0 β€
(πΉβπ))) |
56 | 33, 54 | ltnled 11309 |
. . . . . . . 8
β’ (((π β§ -π΅ β β+) β§ π β β+)
β (((πΉβπ) / (πβπ·)) < 0 β Β¬ 0 β€ ((πΉβπ) / (πβπ·)))) |
57 | 53, 55, 56 | 3bitr4d 311 |
. . . . . . 7
β’ (((π β§ -π΅ β β+) β§ π β β+)
β ((πΉβπ) < 0 β ((πΉβπ) / (πβπ·)) < 0)) |
58 | 57 | adantr 482 |
. . . . . 6
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅) β ((πΉβπ) < 0 β ((πΉβπ) / (πβπ·)) < 0)) |
59 | 50, 58 | mpbird 257 |
. . . . 5
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅) β (πΉβπ) < 0) |
60 | 16, 59 | syldan 592 |
. . . 4
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅)) β (πΉβπ) < 0) |
61 | | 0red 11165 |
. . . . . 6
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β 0 β
β) |
62 | | simplr 768 |
. . . . . . 7
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β π β
β+) |
63 | 62 | rpred 12964 |
. . . . . 6
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β π β
β) |
64 | 62 | rpgt0d 12967 |
. . . . . 6
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β 0 < π) |
65 | | iccssre 13353 |
. . . . . . . 8
β’ ((0
β β β§ π
β β) β (0[,]π) β β) |
66 | 35, 63, 65 | sylancr 588 |
. . . . . . 7
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β (0[,]π) β
β) |
67 | | ax-resscn 11115 |
. . . . . . 7
β’ β
β β |
68 | 66, 67 | sstrdi 3961 |
. . . . . 6
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β (0[,]π) β
β) |
69 | | plycn 25638 |
. . . . . . . 8
β’ (πΉ β (Polyββ)
β πΉ β
(ββcnββ)) |
70 | 17, 69 | syl 17 |
. . . . . . 7
β’ (π β πΉ β (ββcnββ)) |
71 | 70 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β πΉ β (ββcnββ)) |
72 | 17 | ad4antr 731 |
. . . . . . 7
β’
(((((π β§ -π΅ β β+)
β§ π β
β+) β§ (πΉβπ) < 0) β§ π₯ β (0[,]π)) β πΉ β
(Polyββ)) |
73 | 66 | sselda 3949 |
. . . . . . 7
β’
(((((π β§ -π΅ β β+)
β§ π β
β+) β§ (πΉβπ) < 0) β§ π₯ β (0[,]π)) β π₯ β β) |
74 | 72, 73 | plyrecld 33201 |
. . . . . 6
β’
(((((π β§ -π΅ β β+)
β§ π β
β+) β§ (πΉβπ) < 0) β§ π₯ β (0[,]π)) β (πΉβπ₯) β β) |
75 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β (πΉβπ) < 0) |
76 | | simplll 774 |
. . . . . . . . 9
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β π) |
77 | 76, 41 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β π΅ β
β) |
78 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ -π΅ β β+) β -π΅ β
β+) |
79 | 78 | ad2antrr 725 |
. . . . . . . . . 10
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β -π΅ β
β+) |
80 | | negelrp 12955 |
. . . . . . . . . . 11
β’ (π΅ β β β (-π΅ β β+
β π΅ <
0)) |
81 | 80 | biimpa 478 |
. . . . . . . . . 10
β’ ((π΅ β β β§ -π΅ β β+)
β π΅ <
0) |
82 | 77, 79, 81 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β π΅ < 0) |
83 | | signsply0.a |
. . . . . . . . . . . 12
β’ π΄ = (πΆβ0) |
84 | 17, 35, 37 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (π β πΆ:β0βΆβ) |
85 | | 0nn0 12435 |
. . . . . . . . . . . . . 14
β’ 0 β
β0 |
86 | 85 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 0 β
β0) |
87 | 84, 86 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ (π β (πΆβ0) β β) |
88 | 83, 87 | eqeltrid 2842 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
89 | | signsply0.3 |
. . . . . . . . . . 11
β’ (π β (π΄ Β· π΅) < 0) |
90 | 88, 41, 89 | mul2lt0rlt0 13024 |
. . . . . . . . . 10
β’ ((π β§ π΅ < 0) β 0 < π΄) |
91 | 90, 83 | breqtrdi 5151 |
. . . . . . . . 9
β’ ((π β§ π΅ < 0) β 0 < (πΆβ0)) |
92 | 76, 82, 91 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β 0 < (πΆβ0)) |
93 | 36 | coefv0 25625 |
. . . . . . . . . 10
β’ (πΉ β (Polyββ)
β (πΉβ0) = (πΆβ0)) |
94 | 17, 93 | syl 17 |
. . . . . . . . 9
β’ (π β (πΉβ0) = (πΆβ0)) |
95 | 94 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β (πΉβ0) = (πΆβ0)) |
96 | 92, 95 | breqtrrd 5138 |
. . . . . . 7
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β 0 < (πΉβ0)) |
97 | 75, 96 | jca 513 |
. . . . . 6
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β ((πΉβπ) < 0 β§ 0 < (πΉβ0))) |
98 | 61, 63, 61, 64, 68, 71, 74, 97 | ivth2 24835 |
. . . . 5
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β βπ§ β (0(,)π)(πΉβπ§) = 0) |
99 | | 0le0 12261 |
. . . . . . . 8
β’ 0 β€
0 |
100 | | pnfge 13058 |
. . . . . . . . 9
β’ (π β β*
β π β€
+β) |
101 | 3, 100 | syl 17 |
. . . . . . . 8
β’ (π β β+
β π β€
+β) |
102 | | 0xr 11209 |
. . . . . . . . 9
β’ 0 β
β* |
103 | | pnfxr 11216 |
. . . . . . . . 9
β’ +β
β β* |
104 | | ioossioo 13365 |
. . . . . . . . 9
β’ (((0
β β* β§ +β β β*) β§ (0
β€ 0 β§ π β€
+β)) β (0(,)π)
β (0(,)+β)) |
105 | 102, 103,
104 | mpanl12 701 |
. . . . . . . 8
β’ ((0 β€
0 β§ π β€ +β)
β (0(,)π) β
(0(,)+β)) |
106 | 99, 101, 105 | sylancr 588 |
. . . . . . 7
β’ (π β β+
β (0(,)π) β
(0(,)+β)) |
107 | | ioorp 13349 |
. . . . . . 7
β’
(0(,)+β) = β+ |
108 | 106, 107 | sseqtrdi 3999 |
. . . . . 6
β’ (π β β+
β (0(,)π) β
β+) |
109 | | ssrexv 4016 |
. . . . . 6
β’
((0(,)π) β
β+ β (βπ§ β (0(,)π)(πΉβπ§) = 0 β βπ§ β β+ (πΉβπ§) = 0)) |
110 | 62, 108, 109 | 3syl 18 |
. . . . 5
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β (βπ§ β (0(,)π)(πΉβπ§) = 0 β βπ§ β β+ (πΉβπ§) = 0)) |
111 | 98, 110 | mpd 15 |
. . . 4
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ (πΉβπ) < 0) β βπ§ β β+
(πΉβπ§) = 0) |
112 | 60, 111 | syldan 592 |
. . 3
β’ ((((π β§ -π΅ β β+) β§ π β β+)
β§ βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅)) β βπ§ β β+ (πΉβπ§) = 0) |
113 | | plyf 25575 |
. . . . . . . . . . 11
β’ (πΉ β (Polyββ)
β πΉ:ββΆβ) |
114 | 17, 113 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
115 | 114 | ffnd 6674 |
. . . . . . . . 9
β’ (π β πΉ Fn β) |
116 | | ovex 7395 |
. . . . . . . . . . 11
β’ (π₯βπ·) β V |
117 | 116 | rgenw 3069 |
. . . . . . . . . 10
β’
βπ₯ β
β+ (π₯βπ·) β V |
118 | | eqid 2737 |
. . . . . . . . . . 11
β’ (π₯ β β+
β¦ (π₯βπ·)) = (π₯ β β+ β¦ (π₯βπ·)) |
119 | 118 | fnmpt 6646 |
. . . . . . . . . 10
β’
(βπ₯ β
β+ (π₯βπ·) β V β (π₯ β β+ β¦ (π₯βπ·)) Fn β+) |
120 | 117, 119 | mp1i 13 |
. . . . . . . . 9
β’ (π β (π₯ β β+ β¦ (π₯βπ·)) Fn β+) |
121 | | cnex 11139 |
. . . . . . . . . 10
β’ β
β V |
122 | 121 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
V) |
123 | | rpssre 12929 |
. . . . . . . . . . . 12
β’
β+ β β |
124 | 123, 67 | sstri 3958 |
. . . . . . . . . . 11
β’
β+ β β |
125 | 121, 124 | ssexi 5284 |
. . . . . . . . . 10
β’
β+ β V |
126 | 125 | a1i 11 |
. . . . . . . . 9
β’ (π β β+ β
V) |
127 | | sseqin2 4180 |
. . . . . . . . . 10
β’
(β+ β β β (β β©
β+) = β+) |
128 | 124, 127 | mpbi 229 |
. . . . . . . . 9
β’ (β
β© β+) = β+ |
129 | | eqidd 2738 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβπ) = (πΉβπ)) |
130 | | eqidd 2738 |
. . . . . . . . . 10
β’ ((π β§ π β β+) β (π₯ β β+
β¦ (π₯βπ·)) = (π₯ β β+ β¦ (π₯βπ·))) |
131 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π₯ = π) β π₯ = π) |
132 | 131 | oveq1d 7377 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ π₯ = π) β (π₯βπ·) = (πβπ·)) |
133 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β β+) β π β
β+) |
134 | | ovexd 7397 |
. . . . . . . . . 10
β’ ((π β§ π β β+) β (πβπ·) β V) |
135 | 130, 132,
133, 134 | fvmptd 6960 |
. . . . . . . . 9
β’ ((π β§ π β β+) β ((π₯ β β+
β¦ (π₯βπ·))βπ) = (πβπ·)) |
136 | 115, 120,
122, 126, 128, 129, 135 | offval 7631 |
. . . . . . . 8
β’ (π β (πΉ βf / (π₯ β β+ β¦ (π₯βπ·))) = (π β β+ β¦ ((πΉβπ) / (πβπ·)))) |
137 | | oveq1 7369 |
. . . . . . . . . . 11
β’ (π₯ = π β (π₯βπ·) = (πβπ·)) |
138 | 137 | cbvmptv 5223 |
. . . . . . . . . 10
β’ (π₯ β β+
β¦ (π₯βπ·)) = (π β β+ β¦ (πβπ·)) |
139 | 22, 36, 34, 138 | signsplypnf 33202 |
. . . . . . . . 9
β’ (πΉ β (Polyββ)
β (πΉ
βf / (π₯
β β+ β¦ (π₯βπ·))) βπ π΅) |
140 | 17, 139 | syl 17 |
. . . . . . . 8
β’ (π β (πΉ βf / (π₯ β β+ β¦ (π₯βπ·))) βπ π΅) |
141 | 136, 140 | eqbrtrrd 5134 |
. . . . . . 7
β’ (π β (π β β+ β¦ ((πΉβπ) / (πβπ·))) βπ π΅) |
142 | 114 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β+) β πΉ:ββΆβ) |
143 | 133 | rpcnd 12966 |
. . . . . . . . . . 11
β’ ((π β§ π β β+) β π β
β) |
144 | 142, 143 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π β§ π β β+) β (πΉβπ) β β) |
145 | 25 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β+) β π· β
β0) |
146 | 143, 145 | expcld 14058 |
. . . . . . . . . 10
β’ ((π β§ π β β+) β (πβπ·) β β) |
147 | 133 | rpne0d 12969 |
. . . . . . . . . . 11
β’ ((π β§ π β β+) β π β 0) |
148 | 30 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β+) β π· β
β€) |
149 | 143, 147,
148 | expne0d 14064 |
. . . . . . . . . 10
β’ ((π β§ π β β+) β (πβπ·) β 0) |
150 | 144, 146,
149 | divcld 11938 |
. . . . . . . . 9
β’ ((π β§ π β β+) β ((πΉβπ) / (πβπ·)) β β) |
151 | 150 | ralrimiva 3144 |
. . . . . . . 8
β’ (π β βπ β β+ ((πΉβπ) / (πβπ·)) β β) |
152 | 123 | a1i 11 |
. . . . . . . 8
β’ (π β β+
β β) |
153 | | 1red 11163 |
. . . . . . . 8
β’ (π β 1 β
β) |
154 | 151, 152,
46, 153 | rlim3 15387 |
. . . . . . 7
β’ (π β ((π β β+ β¦ ((πΉβπ) / (πβπ·))) βπ π΅ β βπ β β+
βπ β
(1[,)+β)βπ
β β+ (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π))) |
155 | 141, 154 | mpbid 231 |
. . . . . 6
β’ (π β βπ β β+ βπ β
(1[,)+β)βπ
β β+ (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π)) |
156 | | 0lt1 11684 |
. . . . . . . . . 10
β’ 0 <
1 |
157 | | pnfge 13058 |
. . . . . . . . . . 11
β’ (+β
β β* β +β β€ +β) |
158 | 103, 157 | ax-mp 5 |
. . . . . . . . . 10
β’ +β
β€ +β |
159 | | icossioo 13364 |
. . . . . . . . . 10
β’ (((0
β β* β§ +β β β*) β§ (0
< 1 β§ +β β€ +β)) β (1[,)+β) β
(0(,)+β)) |
160 | 102, 103,
156, 158, 159 | mp4an 692 |
. . . . . . . . 9
β’
(1[,)+β) β (0(,)+β) |
161 | 160, 107 | sseqtri 3985 |
. . . . . . . 8
β’
(1[,)+β) β β+ |
162 | | ssrexv 4016 |
. . . . . . . 8
β’
((1[,)+β) β β+ β (βπ β
(1[,)+β)βπ
β β+ (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π) β βπ β β+ βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π))) |
163 | 161, 162 | ax-mp 5 |
. . . . . . 7
β’
(βπ β
(1[,)+β)βπ
β β+ (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π) β βπ β β+ βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π)) |
164 | 163 | ralimi 3087 |
. . . . . 6
β’
(βπ β
β+ βπ β (1[,)+β)βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π) β βπ β β+ βπ β β+
βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < π)) |
165 | 155, 164 | syl 17 |
. . . . 5
β’ (π β βπ β β+ βπ β β+
βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < π)) |
166 | 165 | adantr 482 |
. . . 4
β’ ((π β§ -π΅ β β+) β
βπ β
β+ βπ β β+ βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π)) |
167 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ -π΅ β β+) β§ π = -π΅) β π = -π΅) |
168 | 167 | breq2d 5122 |
. . . . . . 7
β’ (((π β§ -π΅ β β+) β§ π = -π΅) β ((absβ(((πΉβπ) / (πβπ·)) β π΅)) < π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅)) |
169 | 168 | imbi2d 341 |
. . . . . 6
β’ (((π β§ -π΅ β β+) β§ π = -π΅) β ((π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π) β (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅))) |
170 | 169 | rexralbidv 3215 |
. . . . 5
β’ (((π β§ -π΅ β β+) β§ π = -π΅) β (βπ β β+ βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π) β βπ β β+ βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅))) |
171 | 78, 170 | rspcdv 3576 |
. . . 4
β’ ((π β§ -π΅ β β+) β
(βπ β
β+ βπ β β+ βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π) β βπ β β+ βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅))) |
172 | 166, 171 | mpd 15 |
. . 3
β’ ((π β§ -π΅ β β+) β
βπ β
β+ βπ β β+ (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < -π΅)) |
173 | 112, 172 | r19.29a 3160 |
. 2
β’ ((π β§ -π΅ β β+) β
βπ§ β
β+ (πΉβπ§) = 0) |
174 | | simplr 768 |
. . . . . 6
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅)) β π β β+) |
175 | | simpr 486 |
. . . . . 6
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅)) β βπ β β+ (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅)) |
176 | 4 | ad2antlr 726 |
. . . . . 6
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅)) β π β€ π) |
177 | 12 | breq1d 5120 |
. . . . . . . 8
β’ ((π β β+
β§ π = π) β ((absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅ β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅)) |
178 | 8, 177 | imbi12d 345 |
. . . . . . 7
β’ ((π β β+
β§ π = π) β ((π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅) β (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅))) |
179 | 6, 178 | rspcdv 3576 |
. . . . . 6
β’ (π β β+
β (βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅) β (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅))) |
180 | 174, 175,
176, 179 | syl3c 66 |
. . . . 5
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅)) β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅) |
181 | 46 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π΅ β β+) β§ π β β+)
β π΅ β
β) |
182 | 181 | subidd 11507 |
. . . . . . . 8
β’ (((π β§ π΅ β β+) β§ π β β+)
β (π΅ β π΅) = 0) |
183 | 182 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅) β (π΅ β π΅) = 0) |
184 | 17 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π΅ β β+) β§ π β β+)
β πΉ β
(Polyββ)) |
185 | 123 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π΅ β β+) β
β+ β β) |
186 | 185 | sselda 3949 |
. . . . . . . . . . 11
β’ (((π β§ π΅ β β+) β§ π β β+)
β π β
β) |
187 | 184, 186 | plyrecld 33201 |
. . . . . . . . . 10
β’ (((π β§ π΅ β β+) β§ π β β+)
β (πΉβπ) β
β) |
188 | 25 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π΅ β β+) β§ π β β+)
β π· β
β0) |
189 | 186, 188 | reexpcld 14075 |
. . . . . . . . . 10
β’ (((π β§ π΅ β β+) β§ π β β+)
β (πβπ·) β
β) |
190 | 186 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π΅ β β+) β§ π β β+)
β π β
β) |
191 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ β β+) β§ π β β+)
β π β
β+) |
192 | 191 | rpne0d 12969 |
. . . . . . . . . . 11
β’ (((π β§ π΅ β β+) β§ π β β+)
β π β
0) |
193 | 30 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π΅ β β+) β§ π β β+)
β π· β
β€) |
194 | 190, 192,
193 | expne0d 14064 |
. . . . . . . . . 10
β’ (((π β§ π΅ β β+) β§ π β β+)
β (πβπ·) β 0) |
195 | 187, 189,
194 | redivcld 11990 |
. . . . . . . . 9
β’ (((π β§ π΅ β β+) β§ π β β+)
β ((πΉβπ) / (πβπ·)) β β) |
196 | 41 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π΅ β β+) β§ π β β+)
β π΅ β
β) |
197 | 195, 196,
196 | absdifltd 15325 |
. . . . . . . 8
β’ (((π β§ π΅ β β+) β§ π β β+)
β ((absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅ β ((π΅ β π΅) < ((πΉβπ) / (πβπ·)) β§ ((πΉβπ) / (πβπ·)) < (π΅ + π΅)))) |
198 | 197 | simprbda 500 |
. . . . . . 7
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅) β (π΅ β π΅) < ((πΉβπ) / (πβπ·))) |
199 | 183, 198 | eqbrtrrd 5134 |
. . . . . 6
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅) β 0 < ((πΉβπ) / (πβπ·))) |
200 | 191, 193 | rpexpcld 14157 |
. . . . . . . 8
β’ (((π β§ π΅ β β+) β§ π β β+)
β (πβπ·) β
β+) |
201 | 187, 200 | gt0divd 13001 |
. . . . . . 7
β’ (((π β§ π΅ β β+) β§ π β β+)
β (0 < (πΉβπ) β 0 < ((πΉβπ) / (πβπ·)))) |
202 | 201 | adantr 482 |
. . . . . 6
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅) β (0 < (πΉβπ) β 0 < ((πΉβπ) / (πβπ·)))) |
203 | 199, 202 | mpbird 257 |
. . . . 5
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅) β 0 < (πΉβπ)) |
204 | 180, 203 | syldan 592 |
. . . 4
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅)) β 0 < (πΉβπ)) |
205 | | 0red 11165 |
. . . . . 6
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β 0 β
β) |
206 | | simplr 768 |
. . . . . . 7
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β π β β+) |
207 | 206 | rpred 12964 |
. . . . . 6
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β π β β) |
208 | 206 | rpgt0d 12967 |
. . . . . 6
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β 0 < π) |
209 | 35, 207, 65 | sylancr 588 |
. . . . . . 7
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β (0[,]π) β
β) |
210 | 209, 67 | sstrdi 3961 |
. . . . . 6
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β (0[,]π) β
β) |
211 | 70 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β πΉ β (ββcnββ)) |
212 | 17 | ad4antr 731 |
. . . . . . 7
β’
(((((π β§ π΅ β β+)
β§ π β
β+) β§ 0 < (πΉβπ)) β§ π₯ β (0[,]π)) β πΉ β
(Polyββ)) |
213 | 209 | sselda 3949 |
. . . . . . 7
β’
(((((π β§ π΅ β β+)
β§ π β
β+) β§ 0 < (πΉβπ)) β§ π₯ β (0[,]π)) β π₯ β β) |
214 | 212, 213 | plyrecld 33201 |
. . . . . 6
β’
(((((π β§ π΅ β β+)
β§ π β
β+) β§ 0 < (πΉβπ)) β§ π₯ β (0[,]π)) β (πΉβπ₯) β β) |
215 | 94 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β (πΉβ0) = (πΆβ0)) |
216 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β π) |
217 | | simpr1 1195 |
. . . . . . . . . . . 12
β’ ((π β§ (π΅ β β+ β§ π β β+
β§ 0 < (πΉβπ))) β π΅ β
β+) |
218 | 217 | rpgt0d 12967 |
. . . . . . . . . . 11
β’ ((π β§ (π΅ β β+ β§ π β β+
β§ 0 < (πΉβπ))) β 0 < π΅) |
219 | 218 | 3anassrs 1361 |
. . . . . . . . . 10
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β 0 < π΅) |
220 | 88, 41, 89 | mul2lt0rgt0 13025 |
. . . . . . . . . 10
β’ ((π β§ 0 < π΅) β π΄ < 0) |
221 | 216, 219,
220 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β π΄ < 0) |
222 | 83, 221 | eqbrtrrid 5146 |
. . . . . . . 8
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β (πΆβ0) < 0) |
223 | 215, 222 | eqbrtrd 5132 |
. . . . . . 7
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β (πΉβ0) < 0) |
224 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β 0 < (πΉβπ)) |
225 | 223, 224 | jca 513 |
. . . . . 6
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β ((πΉβ0) < 0 β§ 0 < (πΉβπ))) |
226 | 205, 207,
205, 208, 210, 211, 214, 225 | ivth 24834 |
. . . . 5
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β βπ§ β (0(,)π)(πΉβπ§) = 0) |
227 | 206, 108,
109 | 3syl 18 |
. . . . 5
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β (βπ§ β (0(,)π)(πΉβπ§) = 0 β βπ§ β β+ (πΉβπ§) = 0)) |
228 | 226, 227 | mpd 15 |
. . . 4
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ 0 < (πΉβπ)) β βπ§ β β+
(πΉβπ§) = 0) |
229 | 204, 228 | syldan 592 |
. . 3
β’ ((((π β§ π΅ β β+) β§ π β β+)
β§ βπ β
β+ (π β€
π β
(absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅)) β βπ§ β β+ (πΉβπ§) = 0) |
230 | 165 | adantr 482 |
. . . 4
β’ ((π β§ π΅ β β+) β
βπ β
β+ βπ β β+ βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π)) |
231 | | simpr 486 |
. . . . 5
β’ ((π β§ π΅ β β+) β π΅ β
β+) |
232 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π΅ β β+) β§ π = π΅) β π = π΅) |
233 | 232 | breq2d 5122 |
. . . . . . 7
β’ (((π β§ π΅ β β+) β§ π = π΅) β ((absβ(((πΉβπ) / (πβπ·)) β π΅)) < π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅)) |
234 | 233 | imbi2d 341 |
. . . . . 6
β’ (((π β§ π΅ β β+) β§ π = π΅) β ((π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π) β (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅))) |
235 | 234 | rexralbidv 3215 |
. . . . 5
β’ (((π β§ π΅ β β+) β§ π = π΅) β (βπ β β+ βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π) β βπ β β+ βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅))) |
236 | 231, 235 | rspcdv 3576 |
. . . 4
β’ ((π β§ π΅ β β+) β
(βπ β
β+ βπ β β+ βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π) β βπ β β+ βπ β β+
(π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅))) |
237 | 230, 236 | mpd 15 |
. . 3
β’ ((π β§ π΅ β β+) β
βπ β
β+ βπ β β+ (π β€ π β (absβ(((πΉβπ) / (πβπ·)) β π΅)) < π΅)) |
238 | 229, 237 | r19.29a 3160 |
. 2
β’ ((π β§ π΅ β β+) β
βπ§ β
β+ (πΉβπ§) = 0) |
239 | | signsply0.2 |
. . . . 5
β’ (π β πΉ β
0π) |
240 | 22, 36 | dgreq0 25642 |
. . . . . . 7
β’ (πΉ β (Polyββ)
β (πΉ =
0π β (πΆβπ·) = 0)) |
241 | 17, 240 | syl 17 |
. . . . . 6
β’ (π β (πΉ = 0π β (πΆβπ·) = 0)) |
242 | 241 | necon3bid 2989 |
. . . . 5
β’ (π β (πΉ β 0π β (πΆβπ·) β 0)) |
243 | 239, 242 | mpbid 231 |
. . . 4
β’ (π β (πΆβπ·) β 0) |
244 | 34 | neeq1i 3009 |
. . . 4
β’ (π΅ β 0 β (πΆβπ·) β 0) |
245 | 243, 244 | sylibr 233 |
. . 3
β’ (π β π΅ β 0) |
246 | | rpneg 12954 |
. . . . 5
β’ ((π΅ β β β§ π΅ β 0) β (π΅ β β+
β Β¬ -π΅ β
β+)) |
247 | 246 | biimprd 248 |
. . . 4
β’ ((π΅ β β β§ π΅ β 0) β (Β¬ -π΅ β β+
β π΅ β
β+)) |
248 | 247 | orrd 862 |
. . 3
β’ ((π΅ β β β§ π΅ β 0) β (-π΅ β β+ β¨
π΅ β
β+)) |
249 | 41, 245, 248 | syl2anc 585 |
. 2
β’ (π β (-π΅ β β+ β¨ π΅ β
β+)) |
250 | 173, 238,
249 | mpjaodan 958 |
1
β’ (π β βπ§ β β+ (πΉβπ§) = 0) |