Step | Hyp | Ref
| Expression |
1 | | oveq2 5882 |
. . . . . . . . 9
β’ (π = -πΏ β (πΏ + π) = (πΏ + -πΏ)) |
2 | 1 | breq2d 4015 |
. . . . . . . 8
β’ (π = -πΏ β ((πΉβπ) < (πΏ + π) β (πΉβπ) < (πΏ + -πΏ))) |
3 | | oveq2 5882 |
. . . . . . . . 9
β’ (π = -πΏ β ((πΉβπ) + π) = ((πΉβπ) + -πΏ)) |
4 | 3 | breq2d 4015 |
. . . . . . . 8
β’ (π = -πΏ β (πΏ < ((πΉβπ) + π) β πΏ < ((πΉβπ) + -πΏ))) |
5 | 2, 4 | anbi12d 473 |
. . . . . . 7
β’ (π = -πΏ β (((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β ((πΉβπ) < (πΏ + -πΏ) β§ πΏ < ((πΉβπ) + -πΏ)))) |
6 | 5 | rexralbidv 2503 |
. . . . . 6
β’ (π = -πΏ β (βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + -πΏ) β§ πΏ < ((πΉβπ) + -πΏ)))) |
7 | | resqrexlemgt0.lim |
. . . . . . 7
β’ (π β βπ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
8 | 7 | adantr 276 |
. . . . . 6
β’ ((π β§ πΏ < 0) β βπ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
9 | | resqrexlemgt0.rr |
. . . . . . . . 9
β’ (π β πΏ β β) |
10 | 9 | adantr 276 |
. . . . . . . 8
β’ ((π β§ πΏ < 0) β πΏ β β) |
11 | 10 | renegcld 8336 |
. . . . . . 7
β’ ((π β§ πΏ < 0) β -πΏ β β) |
12 | 9 | lt0neg1d 8471 |
. . . . . . . 8
β’ (π β (πΏ < 0 β 0 < -πΏ)) |
13 | 12 | biimpa 296 |
. . . . . . 7
β’ ((π β§ πΏ < 0) β 0 < -πΏ) |
14 | 11, 13 | elrpd 9692 |
. . . . . 6
β’ ((π β§ πΏ < 0) β -πΏ β
β+) |
15 | 6, 8, 14 | rspcdva 2846 |
. . . . 5
β’ ((π β§ πΏ < 0) β βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + -πΏ) β§ πΏ < ((πΉβπ) + -πΏ))) |
16 | | simpl 109 |
. . . . . . . 8
β’ (((πΉβπ) < (πΏ + -πΏ) β§ πΏ < ((πΉβπ) + -πΏ)) β (πΉβπ) < (πΏ + -πΏ)) |
17 | 10 | recnd 7985 |
. . . . . . . . . 10
β’ ((π β§ πΏ < 0) β πΏ β β) |
18 | 17 | negidd 8257 |
. . . . . . . . 9
β’ ((π β§ πΏ < 0) β (πΏ + -πΏ) = 0) |
19 | 18 | breq2d 4015 |
. . . . . . . 8
β’ ((π β§ πΏ < 0) β ((πΉβπ) < (πΏ + -πΏ) β (πΉβπ) < 0)) |
20 | 16, 19 | imbitrid 154 |
. . . . . . 7
β’ ((π β§ πΏ < 0) β (((πΉβπ) < (πΏ + -πΏ) β§ πΏ < ((πΉβπ) + -πΏ)) β (πΉβπ) < 0)) |
21 | 20 | ralimdv 2545 |
. . . . . 6
β’ ((π β§ πΏ < 0) β (βπ β (β€β₯βπ)((πΉβπ) < (πΏ + -πΏ) β§ πΏ < ((πΉβπ) + -πΏ)) β βπ β (β€β₯βπ)(πΉβπ) < 0)) |
22 | 21 | reximdv 2578 |
. . . . 5
β’ ((π β§ πΏ < 0) β (βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + -πΏ) β§ πΏ < ((πΉβπ) + -πΏ)) β βπ β β βπ β (β€β₯βπ)(πΉβπ) < 0)) |
23 | 15, 22 | mpd 13 |
. . . 4
β’ ((π β§ πΏ < 0) β βπ β β βπ β (β€β₯βπ)(πΉβπ) < 0) |
24 | | 0red 7957 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β 0 β
β) |
25 | | eluznn 9599 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
26 | | resqrexlemex.seq |
. . . . . . . . . . . . . . 15
β’ πΉ = seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) |
27 | | resqrexlemex.a |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β β) |
28 | | resqrexlemex.agt0 |
. . . . . . . . . . . . . . 15
β’ (π β 0 β€ π΄) |
29 | 26, 27, 28 | resqrexlemf 11015 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:ββΆβ+) |
30 | 29 | ffvelcdmda 5651 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΉβπ) β
β+) |
31 | 25, 30 | sylan2 286 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (πΉβπ) β
β+) |
32 | 31 | rpred 9695 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β (πΉβπ) β β) |
33 | 31 | rpgt0d 9698 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β 0 < (πΉβπ)) |
34 | 24, 32, 33 | ltnsymd 8076 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β Β¬ (πΉβπ) < 0) |
35 | 34 | pm2.21d 619 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β ((πΉβπ) < 0 β β₯)) |
36 | 35 | anassrs 400 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ) < 0 β β₯)) |
37 | 36 | ralimdva 2544 |
. . . . . . 7
β’ ((π β§ π β β) β (βπ β
(β€β₯βπ)(πΉβπ) < 0 β βπ β (β€β₯βπ)β₯)) |
38 | | nnz 9271 |
. . . . . . . . 9
β’ (π β β β π β
β€) |
39 | | uzid 9541 |
. . . . . . . . . 10
β’ (π β β€ β π β
(β€β₯βπ)) |
40 | | elex2 2753 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β βπ§ π§ β (β€β₯βπ)) |
41 | | r19.3rmv 3513 |
. . . . . . . . . 10
β’
(βπ§ π§ β
(β€β₯βπ) β (β₯ β βπ β
(β€β₯βπ)β₯)) |
42 | 39, 40, 41 | 3syl 17 |
. . . . . . . . 9
β’ (π β β€ β (β₯
β βπ β
(β€β₯βπ)β₯)) |
43 | 38, 42 | syl 14 |
. . . . . . . 8
β’ (π β β β (β₯
β βπ β
(β€β₯βπ)β₯)) |
44 | 43 | adantl 277 |
. . . . . . 7
β’ ((π β§ π β β) β (β₯ β
βπ β
(β€β₯βπ)β₯)) |
45 | 37, 44 | sylibrd 169 |
. . . . . 6
β’ ((π β§ π β β) β (βπ β
(β€β₯βπ)(πΉβπ) < 0 β β₯)) |
46 | 45 | rexlimdva 2594 |
. . . . 5
β’ (π β (βπ β β βπ β (β€β₯βπ)(πΉβπ) < 0 β β₯)) |
47 | 46 | adantr 276 |
. . . 4
β’ ((π β§ πΏ < 0) β (βπ β β βπ β (β€β₯βπ)(πΉβπ) < 0 β β₯)) |
48 | 23, 47 | mpd 13 |
. . 3
β’ ((π β§ πΏ < 0) β β₯) |
49 | 48 | inegd 1372 |
. 2
β’ (π β Β¬ πΏ < 0) |
50 | | 0re 7956 |
. . 3
β’ 0 β
β |
51 | | lenlt 8032 |
. . 3
β’ ((0
β β β§ πΏ
β β) β (0 β€ πΏ β Β¬ πΏ < 0)) |
52 | 50, 9, 51 | sylancr 414 |
. 2
β’ (π β (0 β€ πΏ β Β¬ πΏ < 0)) |
53 | 49, 52 | mpbird 167 |
1
β’ (π β 0 β€ πΏ) |