Step | Hyp | Ref
| Expression |
1 | | stoweidlem45.1 |
. . 3
β’
β²π‘π |
2 | | stoweidlem45.2 |
. . 3
β’
β²π‘π |
3 | | stoweidlem45.4 |
. . 3
β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) |
4 | | eqid 2733 |
. . 3
β’ (π‘ β π β¦ (1 β ((πβπ‘)βπ))) = (π‘ β π β¦ (1 β ((πβπ‘)βπ))) |
5 | | eqid 2733 |
. . 3
β’ (π‘ β π β¦ 1) = (π‘ β π β¦ 1) |
6 | | eqid 2733 |
. . 3
β’ (π‘ β π β¦ ((πβπ‘)βπ)) = (π‘ β π β¦ ((πβπ‘)βπ)) |
7 | | stoweidlem45.9 |
. . 3
β’ (π β π β π΄) |
8 | | stoweidlem45.10 |
. . 3
β’ (π β π:πβΆβ) |
9 | | stoweidlem45.13 |
. . 3
β’ ((π β§ π β π΄) β π:πβΆβ) |
10 | | stoweidlem45.14 |
. . 3
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
11 | | stoweidlem45.15 |
. . 3
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
12 | | stoweidlem45.16 |
. . 3
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
13 | | stoweidlem45.5 |
. . 3
β’ (π β π β β) |
14 | | stoweidlem45.6 |
. . . 4
β’ (π β πΎ β β) |
15 | 13 | nnnn0d 12532 |
. . . 4
β’ (π β π β
β0) |
16 | 14, 15 | nnexpcld 14208 |
. . 3
β’ (π β (πΎβπ) β β) |
17 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 16 | stoweidlem40 44756 |
. 2
β’ (π β π β π΄) |
18 | | 1red 11215 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β 1 β β) |
19 | 8 | ffvelcdmda 7087 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (πβπ‘) β β) |
20 | 15 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β π β
β0) |
21 | 19, 20 | reexpcld 14128 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β ((πβπ‘)βπ) β β) |
22 | 18, 21 | resubcld 11642 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (1 β ((πβπ‘)βπ)) β β) |
23 | 14 | nnnn0d 12532 |
. . . . . . . . 9
β’ (π β πΎ β
β0) |
24 | 23, 15 | nn0expcld 14209 |
. . . . . . . 8
β’ (π β (πΎβπ) β
β0) |
25 | 24 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (πΎβπ) β
β0) |
26 | | 1m1e0 12284 |
. . . . . . . 8
β’ (1
β 1) = 0 |
27 | | stoweidlem45.11 |
. . . . . . . . . . . 12
β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
28 | 27 | r19.21bi 3249 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
29 | 28 | simpld 496 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β 0 β€ (πβπ‘)) |
30 | 28 | simprd 497 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β (πβπ‘) β€ 1) |
31 | | exple1 14141 |
. . . . . . . . . 10
β’ ((((πβπ‘) β β β§ 0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ π β β0) β ((πβπ‘)βπ) β€ 1) |
32 | 19, 29, 30, 20, 31 | syl31anc 1374 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β ((πβπ‘)βπ) β€ 1) |
33 | 21, 18, 18, 32 | lesub2dd 11831 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (1 β 1) β€ (1 β
((πβπ‘)βπ))) |
34 | 26, 33 | eqbrtrrid 5185 |
. . . . . . 7
β’ ((π β§ π‘ β π) β 0 β€ (1 β ((πβπ‘)βπ))) |
35 | 22, 25, 34 | expge0d 14129 |
. . . . . 6
β’ ((π β§ π‘ β π) β 0 β€ ((1 β ((πβπ‘)βπ))β(πΎβπ))) |
36 | 3, 8, 15, 23 | stoweidlem12 44728 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πβπ‘) = ((1 β ((πβπ‘)βπ))β(πΎβπ))) |
37 | 35, 36 | breqtrrd 5177 |
. . . . 5
β’ ((π β§ π‘ β π) β 0 β€ (πβπ‘)) |
38 | | 0red 11217 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β 0 β β) |
39 | 19, 20, 29 | expge0d 14129 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β 0 β€ ((πβπ‘)βπ)) |
40 | 38, 21, 18, 39 | lesub2dd 11831 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (1 β ((πβπ‘)βπ)) β€ (1 β 0)) |
41 | | 1m0e1 12333 |
. . . . . . . 8
β’ (1
β 0) = 1 |
42 | 40, 41 | breqtrdi 5190 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (1 β ((πβπ‘)βπ)) β€ 1) |
43 | | exple1 14141 |
. . . . . . 7
β’ ((((1
β ((πβπ‘)βπ)) β β β§ 0 β€ (1 β
((πβπ‘)βπ)) β§ (1 β ((πβπ‘)βπ)) β€ 1) β§ (πΎβπ) β β0) β ((1
β ((πβπ‘)βπ))β(πΎβπ)) β€ 1) |
44 | 22, 34, 42, 25, 43 | syl31anc 1374 |
. . . . . 6
β’ ((π β§ π‘ β π) β ((1 β ((πβπ‘)βπ))β(πΎβπ)) β€ 1) |
45 | 36, 44 | eqbrtrd 5171 |
. . . . 5
β’ ((π β§ π‘ β π) β (πβπ‘) β€ 1) |
46 | 37, 45 | jca 513 |
. . . 4
β’ ((π β§ π‘ β π) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
47 | 46 | ex 414 |
. . 3
β’ (π β (π‘ β π β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
48 | 2, 47 | ralrimi 3255 |
. 2
β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
49 | | stoweidlem45.3 |
. . . . 5
β’ π = {π‘ β π β£ (πβπ‘) < (π· / 2)} |
50 | | stoweidlem45.7 |
. . . . 5
β’ (π β π· β
β+) |
51 | | stoweidlem45.17 |
. . . . 5
β’ (π β πΈ β
β+) |
52 | | stoweidlem45.18 |
. . . . 5
β’ (π β (1 β πΈ) < (1 β (((πΎ Β· π·) / 2)βπ))) |
53 | 49, 3, 8, 15, 23, 50, 51, 52, 27 | stoweidlem24 44740 |
. . . 4
β’ ((π β§ π‘ β π) β (1 β πΈ) < (πβπ‘)) |
54 | 53 | ex 414 |
. . 3
β’ (π β (π‘ β π β (1 β πΈ) < (πβπ‘))) |
55 | 2, 54 | ralrimi 3255 |
. 2
β’ (π β βπ‘ β π (1 β πΈ) < (πβπ‘)) |
56 | | stoweidlem45.12 |
. . . . 5
β’ (π β βπ‘ β (π β π)π· β€ (πβπ‘)) |
57 | | stoweidlem45.19 |
. . . . 5
β’ (π β (1 / ((πΎ Β· π·)βπ)) < πΈ) |
58 | 3, 13, 14, 50, 8, 27, 56, 51, 57 | stoweidlem25 44741 |
. . . 4
β’ ((π β§ π‘ β (π β π)) β (πβπ‘) < πΈ) |
59 | 58 | ex 414 |
. . 3
β’ (π β (π‘ β (π β π) β (πβπ‘) < πΈ)) |
60 | 2, 59 | ralrimi 3255 |
. 2
β’ (π β βπ‘ β (π β π)(πβπ‘) < πΈ) |
61 | | nfmpt1 5257 |
. . . . . . 7
β’
β²π‘(π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) |
62 | 3, 61 | nfcxfr 2902 |
. . . . . 6
β’
β²π‘π |
63 | 62 | nfeq2 2921 |
. . . . 5
β’
β²π‘ π¦ = π |
64 | | fveq1 6891 |
. . . . . . 7
β’ (π¦ = π β (π¦βπ‘) = (πβπ‘)) |
65 | 64 | breq2d 5161 |
. . . . . 6
β’ (π¦ = π β (0 β€ (π¦βπ‘) β 0 β€ (πβπ‘))) |
66 | 64 | breq1d 5159 |
. . . . . 6
β’ (π¦ = π β ((π¦βπ‘) β€ 1 β (πβπ‘) β€ 1)) |
67 | 65, 66 | anbi12d 632 |
. . . . 5
β’ (π¦ = π β ((0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
68 | 63, 67 | ralbid 3271 |
. . . 4
β’ (π¦ = π β (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
69 | 64 | breq2d 5161 |
. . . . 5
β’ (π¦ = π β ((1 β πΈ) < (π¦βπ‘) β (1 β πΈ) < (πβπ‘))) |
70 | 63, 69 | ralbid 3271 |
. . . 4
β’ (π¦ = π β (βπ‘ β π (1 β πΈ) < (π¦βπ‘) β βπ‘ β π (1 β πΈ) < (πβπ‘))) |
71 | 64 | breq1d 5159 |
. . . . 5
β’ (π¦ = π β ((π¦βπ‘) < πΈ β (πβπ‘) < πΈ)) |
72 | 63, 71 | ralbid 3271 |
. . . 4
β’ (π¦ = π β (βπ‘ β (π β π)(π¦βπ‘) < πΈ β βπ‘ β (π β π)(πβπ‘) < πΈ)) |
73 | 68, 70, 72 | 3anbi123d 1437 |
. . 3
β’ (π¦ = π β ((βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < πΈ) β (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (πβπ‘) β§ βπ‘ β (π β π)(πβπ‘) < πΈ))) |
74 | 73 | rspcev 3613 |
. 2
β’ ((π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (πβπ‘) β§ βπ‘ β (π β π)(πβπ‘) < πΈ)) β βπ¦ β π΄ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < πΈ)) |
75 | 17, 48, 55, 60, 74 | syl13anc 1373 |
1
β’ (π β βπ¦ β π΄ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < πΈ)) |