Step | Hyp | Ref
| Expression |
1 | | oveq2 5885 |
. . . . . . . . 9
β’ (π = (πΏ β (πΉβπΎ)) β (πΏ + π) = (πΏ + (πΏ β (πΉβπΎ)))) |
2 | 1 | breq2d 4017 |
. . . . . . . 8
β’ (π = (πΏ β (πΉβπΎ)) β ((πΉβπ) < (πΏ + π) β (πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))))) |
3 | | oveq2 5885 |
. . . . . . . . 9
β’ (π = (πΏ β (πΉβπΎ)) β ((πΉβπ) + π) = ((πΉβπ) + (πΏ β (πΉβπΎ)))) |
4 | 3 | breq2d 4017 |
. . . . . . . 8
β’ (π = (πΏ β (πΉβπΎ)) β (πΏ < ((πΉβπ) + π) β πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ))))) |
5 | 2, 4 | anbi12d 473 |
. . . . . . 7
β’ (π = (πΏ β (πΉβπΎ)) β (((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β ((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) |
6 | 5 | rexralbidv 2503 |
. . . . . 6
β’ (π = (πΏ β (πΉβπΎ)) β (βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) |
7 | | resqrexlemgt0.lim |
. . . . . . 7
β’ (π β βπ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
8 | 7 | adantr 276 |
. . . . . 6
β’ ((π β§ (πΉβπΎ) < πΏ) β βπ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
9 | | resqrexlemex.seq |
. . . . . . . . . . 11
β’ πΉ = seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) |
10 | | resqrexlemex.a |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
11 | | resqrexlemex.agt0 |
. . . . . . . . . . 11
β’ (π β 0 β€ π΄) |
12 | 9, 10, 11 | resqrexlemf 11018 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ+) |
13 | | resqrexlemoverl.k |
. . . . . . . . . 10
β’ (π β πΎ β β) |
14 | 12, 13 | ffvelcdmd 5654 |
. . . . . . . . 9
β’ (π β (πΉβπΎ) β
β+) |
15 | 14 | rpred 9698 |
. . . . . . . 8
β’ (π β (πΉβπΎ) β β) |
16 | | resqrexlemgt0.rr |
. . . . . . . 8
β’ (π β πΏ β β) |
17 | | difrp 9694 |
. . . . . . . 8
β’ (((πΉβπΎ) β β β§ πΏ β β) β ((πΉβπΎ) < πΏ β (πΏ β (πΉβπΎ)) β
β+)) |
18 | 15, 16, 17 | syl2anc 411 |
. . . . . . 7
β’ (π β ((πΉβπΎ) < πΏ β (πΏ β (πΉβπΎ)) β
β+)) |
19 | 18 | biimpa 296 |
. . . . . 6
β’ ((π β§ (πΉβπΎ) < πΏ) β (πΏ β (πΉβπΎ)) β
β+) |
20 | 6, 8, 19 | rspcdva 2848 |
. . . . 5
β’ ((π β§ (πΉβπΎ) < πΏ) β βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ))))) |
21 | | fveq2 5517 |
. . . . . . 7
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
22 | 21 | raleqdv 2679 |
. . . . . 6
β’ (π = π β (βπ β (β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))) β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) |
23 | 22 | cbvrexv 2706 |
. . . . 5
β’
(βπ β
β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))) β βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ))))) |
24 | 20, 23 | sylib 122 |
. . . 4
β’ ((π β§ (πΉβπΎ) < πΏ) β βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ))))) |
25 | | fveq2 5517 |
. . . . . . . . . . 11
β’ (π = πΎ β (πΉβπ) = (πΉβπΎ)) |
26 | 25 | breq1d 4015 |
. . . . . . . . . 10
β’ (π = πΎ β ((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β (πΉβπΎ) < (πΏ + (πΏ β (πΉβπΎ))))) |
27 | 25 | oveq1d 5892 |
. . . . . . . . . . 11
β’ (π = πΎ β ((πΉβπ) + (πΏ β (πΉβπΎ))) = ((πΉβπΎ) + (πΏ β (πΉβπΎ)))) |
28 | 27 | breq2d 4017 |
. . . . . . . . . 10
β’ (π = πΎ β (πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ))) β πΏ < ((πΉβπΎ) + (πΏ β (πΉβπΎ))))) |
29 | 26, 28 | anbi12d 473 |
. . . . . . . . 9
β’ (π = πΎ β (((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))) β ((πΉβπΎ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπΎ) + (πΏ β (πΉβπΎ)))))) |
30 | | simprr 531 |
. . . . . . . . . 10
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ))))) |
31 | 30 | adantr 276 |
. . . . . . . . 9
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ))))) |
32 | | simprl 529 |
. . . . . . . . . . . 12
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β π β β) |
33 | 32 | nnzd 9376 |
. . . . . . . . . . 11
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β π β β€) |
34 | 33 | adantr 276 |
. . . . . . . . . 10
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β π β β€) |
35 | 13 | ad2antrr 488 |
. . . . . . . . . . . 12
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β πΎ β β) |
36 | 35 | nnzd 9376 |
. . . . . . . . . . 11
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β πΎ β β€) |
37 | 36 | adantr 276 |
. . . . . . . . . 10
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β πΎ β β€) |
38 | | simpr 110 |
. . . . . . . . . 10
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β π β€ πΎ) |
39 | | eluz2 9536 |
. . . . . . . . . 10
β’ (πΎ β
(β€β₯βπ) β (π β β€ β§ πΎ β β€ β§ π β€ πΎ)) |
40 | 34, 37, 38, 39 | syl3anbrc 1181 |
. . . . . . . . 9
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β πΎ β (β€β₯βπ)) |
41 | 29, 31, 40 | rspcdva 2848 |
. . . . . . . 8
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β ((πΉβπΎ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπΎ) + (πΏ β (πΉβπΎ))))) |
42 | 41 | simprd 114 |
. . . . . . 7
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β πΏ < ((πΉβπΎ) + (πΏ β (πΉβπΎ)))) |
43 | 14 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β (πΉβπΎ) β
β+) |
44 | 43 | rpcnd 9700 |
. . . . . . . . 9
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β (πΉβπΎ) β β) |
45 | 44 | adantr 276 |
. . . . . . . 8
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β (πΉβπΎ) β β) |
46 | 16 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β πΏ β β) |
47 | 46 | recnd 7988 |
. . . . . . . . 9
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β πΏ β β) |
48 | 47 | adantr 276 |
. . . . . . . 8
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β πΏ β β) |
49 | 45, 48 | pncan3d 8273 |
. . . . . . 7
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β ((πΉβπΎ) + (πΏ β (πΉβπΎ))) = πΏ) |
50 | 42, 49 | breqtrd 4031 |
. . . . . 6
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β πΏ < πΏ) |
51 | 16 | ad3antrrr 492 |
. . . . . . 7
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β πΏ β β) |
52 | 51 | ltnrd 8071 |
. . . . . 6
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β Β¬ πΏ < πΏ) |
53 | 50, 52 | pm2.21fal 1373 |
. . . . 5
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ π β€ πΎ) β β₯) |
54 | 10 | ad3antrrr 492 |
. . . . . . 7
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ πΎ < π) β π΄ β β) |
55 | 11 | ad3antrrr 492 |
. . . . . . 7
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ πΎ < π) β 0 β€ π΄) |
56 | 13 | ad3antrrr 492 |
. . . . . . 7
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ πΎ < π) β πΎ β β) |
57 | 32 | adantr 276 |
. . . . . . 7
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ πΎ < π) β π β β) |
58 | | simpr 110 |
. . . . . . 7
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ πΎ < π) β πΎ < π) |
59 | 9, 54, 55, 56, 57, 58 | resqrexlemdecn 11023 |
. . . . . 6
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ πΎ < π) β (πΉβπ) < (πΉβπΎ)) |
60 | 15 | ad3antrrr 492 |
. . . . . . 7
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ πΎ < π) β (πΉβπΎ) β β) |
61 | 12 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β πΉ:ββΆβ+) |
62 | 61, 32 | ffvelcdmd 5654 |
. . . . . . . . 9
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β (πΉβπ) β
β+) |
63 | 62 | rpred 9698 |
. . . . . . . 8
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β (πΉβπ) β β) |
64 | 63 | adantr 276 |
. . . . . . 7
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ πΎ < π) β (πΉβπ) β β) |
65 | | fveq2 5517 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΉβπ) = (πΉβπ)) |
66 | 65 | breq1d 4015 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β (πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))))) |
67 | 65 | oveq1d 5892 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΉβπ) + (πΏ β (πΉβπΎ))) = ((πΉβπ) + (πΏ β (πΉβπΎ)))) |
68 | 67 | breq2d 4017 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ))) β πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ))))) |
69 | 66, 68 | anbi12d 473 |
. . . . . . . . . . . . 13
β’ (π = π β (((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))) β ((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) |
70 | | uzid 9544 |
. . . . . . . . . . . . . 14
β’ (π β β€ β π β
(β€β₯βπ)) |
71 | 33, 70 | syl 14 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β π β (β€β₯βπ)) |
72 | 69, 30, 71 | rspcdva 2848 |
. . . . . . . . . . . 12
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β ((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ))))) |
73 | 72 | simprd 114 |
. . . . . . . . . . 11
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))) |
74 | 62 | rpcnd 9700 |
. . . . . . . . . . . 12
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β (πΉβπ) β β) |
75 | 74, 47, 44 | addsubassd 8290 |
. . . . . . . . . . 11
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β (((πΉβπ) + πΏ) β (πΉβπΎ)) = ((πΉβπ) + (πΏ β (πΉβπΎ)))) |
76 | 73, 75 | breqtrrd 4033 |
. . . . . . . . . 10
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β πΏ < (((πΉβπ) + πΏ) β (πΉβπΎ))) |
77 | 15 | ad2antrr 488 |
. . . . . . . . . . 11
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β (πΉβπΎ) β β) |
78 | 63, 46 | readdcld 7989 |
. . . . . . . . . . 11
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β ((πΉβπ) + πΏ) β β) |
79 | 77, 46, 78 | ltaddsub2d 8505 |
. . . . . . . . . 10
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β (((πΉβπΎ) + πΏ) < ((πΉβπ) + πΏ) β πΏ < (((πΉβπ) + πΏ) β (πΉβπΎ)))) |
80 | 76, 79 | mpbird 167 |
. . . . . . . . 9
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β ((πΉβπΎ) + πΏ) < ((πΉβπ) + πΏ)) |
81 | 77, 63, 46 | ltadd1d 8497 |
. . . . . . . . 9
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β ((πΉβπΎ) < (πΉβπ) β ((πΉβπΎ) + πΏ) < ((πΉβπ) + πΏ))) |
82 | 80, 81 | mpbird 167 |
. . . . . . . 8
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β (πΉβπΎ) < (πΉβπ)) |
83 | 82 | adantr 276 |
. . . . . . 7
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ πΎ < π) β (πΉβπΎ) < (πΉβπ)) |
84 | 60, 64, 83 | ltnsymd 8079 |
. . . . . 6
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ πΎ < π) β Β¬ (πΉβπ) < (πΉβπΎ)) |
85 | 59, 84 | pm2.21fal 1373 |
. . . . 5
β’ ((((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β§ πΎ < π) β β₯) |
86 | | zlelttric 9300 |
. . . . . 6
β’ ((π β β€ β§ πΎ β β€) β (π β€ πΎ β¨ πΎ < π)) |
87 | 33, 36, 86 | syl2anc 411 |
. . . . 5
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β (π β€ πΎ β¨ πΎ < π)) |
88 | 53, 85, 87 | mpjaodan 798 |
. . . 4
β’ (((π β§ (πΉβπΎ) < πΏ) β§ (π β β β§ βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + (πΏ β (πΉβπΎ))) β§ πΏ < ((πΉβπ) + (πΏ β (πΉβπΎ)))))) β β₯) |
89 | 24, 88 | rexlimddv 2599 |
. . 3
β’ ((π β§ (πΉβπΎ) < πΏ) β β₯) |
90 | 89 | inegd 1372 |
. 2
β’ (π β Β¬ (πΉβπΎ) < πΏ) |
91 | 16, 15 | lenltd 8077 |
. 2
β’ (π β (πΏ β€ (πΉβπΎ) β Β¬ (πΉβπΎ) < πΏ)) |
92 | 90, 91 | mpbird 167 |
1
β’ (π β πΏ β€ (πΉβπΎ)) |