Step | Hyp | Ref
| Expression |
1 | | breq2 5113 |
. . . . 5
β’ (π = π β ((1 / π·) < π β (1 / π·) < π)) |
2 | 1 | cbvrabv 3416 |
. . . 4
β’ {π β β β£ (1 /
π·) < π} = {π β β β£ (1 / π·) < π} |
3 | | stoweidlem49.4 |
. . . 4
β’ (π β π· β
β+) |
4 | | stoweidlem49.5 |
. . . 4
β’ (π β π· < 1) |
5 | 2, 3, 4 | stoweidlem14 44345 |
. . 3
β’ (π β βπ β β (1 < (π Β· π·) β§ ((π Β· π·) / 2) < 1)) |
6 | | eqid 2733 |
. . . . . 6
β’ (π β β0
β¦ ((1 / (π Β·
π·))βπ)) = (π β β0 β¦ ((1 /
(π Β· π·))βπ)) |
7 | | eqid 2733 |
. . . . . 6
β’ (π β β0
β¦ (((π Β· π·) / 2)βπ)) = (π β β0 β¦ (((π Β· π·) / 2)βπ)) |
8 | | nnre 12168 |
. . . . . . . . 9
β’ (π β β β π β
β) |
9 | 8 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
10 | 3 | rpred 12965 |
. . . . . . . . 9
β’ (π β π· β β) |
11 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π· β β) |
12 | 9, 11 | remulcld 11193 |
. . . . . . 7
β’ ((π β§ π β β) β (π Β· π·) β β) |
13 | 12 | adantr 482 |
. . . . . 6
β’ (((π β§ π β β) β§ (1 < (π Β· π·) β§ ((π Β· π·) / 2) < 1)) β (π Β· π·) β β) |
14 | | simprl 770 |
. . . . . 6
β’ (((π β§ π β β) β§ (1 < (π Β· π·) β§ ((π Β· π·) / 2) < 1)) β 1 < (π Β· π·)) |
15 | 12 | rehalfcld 12408 |
. . . . . . . 8
β’ ((π β§ π β β) β ((π Β· π·) / 2) β β) |
16 | | nngt0 12192 |
. . . . . . . . . . 11
β’ (π β β β 0 <
π) |
17 | 16 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β) β 0 < π) |
18 | 3 | rpgt0d 12968 |
. . . . . . . . . . 11
β’ (π β 0 < π·) |
19 | 18 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β 0 < π·) |
20 | 9, 11, 17, 19 | mulgt0d 11318 |
. . . . . . . . 9
β’ ((π β§ π β β) β 0 < (π Β· π·)) |
21 | | 2re 12235 |
. . . . . . . . . . 11
β’ 2 β
β |
22 | | 2pos 12264 |
. . . . . . . . . . 11
β’ 0 <
2 |
23 | 21, 22 | pm3.2i 472 |
. . . . . . . . . 10
β’ (2 β
β β§ 0 < 2) |
24 | 23 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β β) β (2 β β
β§ 0 < 2)) |
25 | | divgt0 12031 |
. . . . . . . . 9
β’ ((((π Β· π·) β β β§ 0 < (π Β· π·)) β§ (2 β β β§ 0 < 2))
β 0 < ((π Β·
π·) / 2)) |
26 | 12, 20, 24, 25 | syl21anc 837 |
. . . . . . . 8
β’ ((π β§ π β β) β 0 < ((π Β· π·) / 2)) |
27 | 15, 26 | elrpd 12962 |
. . . . . . 7
β’ ((π β§ π β β) β ((π Β· π·) / 2) β
β+) |
28 | 27 | adantr 482 |
. . . . . 6
β’ (((π β§ π β β) β§ (1 < (π Β· π·) β§ ((π Β· π·) / 2) < 1)) β ((π Β· π·) / 2) β
β+) |
29 | | simprr 772 |
. . . . . 6
β’ (((π β§ π β β) β§ (1 < (π Β· π·) β§ ((π Β· π·) / 2) < 1)) β ((π Β· π·) / 2) < 1) |
30 | | stoweidlem49.14 |
. . . . . . 7
β’ (π β πΈ β
β+) |
31 | 30 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ (1 < (π Β· π·) β§ ((π Β· π·) / 2) < 1)) β πΈ β
β+) |
32 | 6, 7, 13, 14, 28, 29, 31 | stoweidlem7 44338 |
. . . . 5
β’ (((π β§ π β β) β§ (1 < (π Β· π·) β§ ((π Β· π·) / 2) < 1)) β βπ β β ((1 β
πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) |
33 | 32 | ex 414 |
. . . 4
β’ ((π β§ π β β) β ((1 < (π Β· π·) β§ ((π Β· π·) / 2) < 1) β βπ β β ((1 β
πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ))) |
34 | 33 | reximdva 3162 |
. . 3
β’ (π β (βπ β β (1 < (π Β· π·) β§ ((π Β· π·) / 2) < 1) β βπ β β βπ β β ((1 β
πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ))) |
35 | 5, 34 | mpd 15 |
. 2
β’ (π β βπ β β βπ β β ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) |
36 | | stoweidlem49.1 |
. . . . 5
β’
β²π‘π |
37 | | stoweidlem49.2 |
. . . . . . 7
β’
β²π‘π |
38 | | nfv 1918 |
. . . . . . 7
β’
β²π‘(π β β β§ π β
β) |
39 | 37, 38 | nfan 1903 |
. . . . . 6
β’
β²π‘(π β§ (π β β β§ π β β)) |
40 | | nfv 1918 |
. . . . . 6
β’
β²π‘((1 β
πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ) |
41 | 39, 40 | nfan 1903 |
. . . . 5
β’
β²π‘((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) |
42 | | stoweidlem49.3 |
. . . . 5
β’ π = {π‘ β π β£ (πβπ‘) < (π· / 2)} |
43 | | eqid 2733 |
. . . . 5
β’ (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πβπ))) = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πβπ))) |
44 | | simplrr 777 |
. . . . 5
β’ (((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β π β β) |
45 | | simplrl 776 |
. . . . 5
β’ (((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β π β β) |
46 | 3 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β π· β
β+) |
47 | 4 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β π· < 1) |
48 | | stoweidlem49.6 |
. . . . . 6
β’ (π β π β π΄) |
49 | 48 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β π β π΄) |
50 | | stoweidlem49.7 |
. . . . . 6
β’ (π β π:πβΆβ) |
51 | 50 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β π:πβΆβ) |
52 | | stoweidlem49.8 |
. . . . . 6
β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
53 | 52 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
54 | | stoweidlem49.9 |
. . . . . 6
β’ (π β βπ‘ β (π β π)π· β€ (πβπ‘)) |
55 | 54 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β βπ‘ β (π β π)π· β€ (πβπ‘)) |
56 | | stoweidlem49.10 |
. . . . . 6
β’ ((π β§ π β π΄) β π:πβΆβ) |
57 | 56 | ad4ant14 751 |
. . . . 5
β’ ((((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β§ π β π΄) β π:πβΆβ) |
58 | | simp1ll 1237 |
. . . . . 6
β’ ((((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β§ π β π΄ β§ π β π΄) β π) |
59 | | stoweidlem49.11 |
. . . . . 6
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
60 | 58, 59 | syld3an1 1411 |
. . . . 5
β’ ((((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
61 | | stoweidlem49.12 |
. . . . . 6
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
62 | 58, 61 | syld3an1 1411 |
. . . . 5
β’ ((((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
63 | | stoweidlem49.13 |
. . . . . 6
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
64 | 63 | ad4ant14 751 |
. . . . 5
β’ ((((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
65 | 30 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β πΈ β
β+) |
66 | | simprl 770 |
. . . . 5
β’ (((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β (1 β πΈ) < (1 β (((π Β· π·) / 2)βπ))) |
67 | | simprr 772 |
. . . . 5
β’ (((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β (1 / ((π Β· π·)βπ)) < πΈ) |
68 | 36, 41, 42, 43, 44, 45, 46, 47, 49, 51, 53, 55, 57, 60, 62, 64, 65, 66, 67 | stoweidlem45 44376 |
. . . 4
β’ (((π β§ (π β β β§ π β β)) β§ ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ)) β βπ¦ β π΄ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < πΈ)) |
69 | 68 | ex 414 |
. . 3
β’ ((π β§ (π β β β§ π β β)) β (((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ) β βπ¦ β π΄ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < πΈ))) |
70 | 69 | rexlimdvva 3202 |
. 2
β’ (π β (βπ β β βπ β β ((1 β πΈ) < (1 β (((π Β· π·) / 2)βπ)) β§ (1 / ((π Β· π·)βπ)) < πΈ) β βπ¦ β π΄ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < πΈ))) |
71 | 35, 70 | mpd 15 |
1
β’ (π β βπ¦ β π΄ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < πΈ)) |