Step | Hyp | Ref
| Expression |
1 | | 1red 11215 |
. . . 4
β’ ((π β§ π‘ β π) β 1 β β) |
2 | | stoweidlem24.8 |
. . . . . 6
β’ (π β πΈ β
β+) |
3 | 2 | rpred 13016 |
. . . . 5
β’ (π β πΈ β β) |
4 | 3 | adantr 482 |
. . . 4
β’ ((π β§ π‘ β π) β πΈ β β) |
5 | 1, 4 | resubcld 11642 |
. . 3
β’ ((π β§ π‘ β π) β (1 β πΈ) β β) |
6 | | stoweidlem24.5 |
. . . . . . . 8
β’ (π β πΎ β
β0) |
7 | 6 | nn0red 12533 |
. . . . . . 7
β’ (π β πΎ β β) |
8 | 7 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π) β πΎ β β) |
9 | | stoweidlem24.3 |
. . . . . . . 8
β’ (π β π:πβΆβ) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β π) β π:πβΆβ) |
11 | | stoweidlem24.1 |
. . . . . . . . . 10
β’ π = {π‘ β π β£ (πβπ‘) < (π· / 2)} |
12 | 11 | reqabi 3455 |
. . . . . . . . 9
β’ (π‘ β π β (π‘ β π β§ (πβπ‘) < (π· / 2))) |
13 | 12 | simplbi 499 |
. . . . . . . 8
β’ (π‘ β π β π‘ β π) |
14 | 13 | adantl 483 |
. . . . . . 7
β’ ((π β§ π‘ β π) β π‘ β π) |
15 | 10, 14 | ffvelcdmd 7088 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πβπ‘) β β) |
16 | 8, 15 | remulcld 11244 |
. . . . 5
β’ ((π β§ π‘ β π) β (πΎ Β· (πβπ‘)) β β) |
17 | | stoweidlem24.4 |
. . . . . 6
β’ (π β π β
β0) |
18 | 17 | adantr 482 |
. . . . 5
β’ ((π β§ π‘ β π) β π β
β0) |
19 | 16, 18 | reexpcld 14128 |
. . . 4
β’ ((π β§ π‘ β π) β ((πΎ Β· (πβπ‘))βπ) β β) |
20 | 1, 19 | resubcld 11642 |
. . 3
β’ ((π β§ π‘ β π) β (1 β ((πΎ Β· (πβπ‘))βπ)) β β) |
21 | 15, 18 | reexpcld 14128 |
. . . . 5
β’ ((π β§ π‘ β π) β ((πβπ‘)βπ) β β) |
22 | 1, 21 | resubcld 11642 |
. . . 4
β’ ((π β§ π‘ β π) β (1 β ((πβπ‘)βπ)) β β) |
23 | 6, 17 | jca 513 |
. . . . . 6
β’ (π β (πΎ β β0 β§ π β
β0)) |
24 | 23 | adantr 482 |
. . . . 5
β’ ((π β§ π‘ β π) β (πΎ β β0 β§ π β
β0)) |
25 | | nn0expcl 14041 |
. . . . 5
β’ ((πΎ β β0
β§ π β
β0) β (πΎβπ) β
β0) |
26 | 24, 25 | syl 17 |
. . . 4
β’ ((π β§ π‘ β π) β (πΎβπ) β
β0) |
27 | 22, 26 | reexpcld 14128 |
. . 3
β’ ((π β§ π‘ β π) β ((1 β ((πβπ‘)βπ))β(πΎβπ)) β β) |
28 | | 1red 11215 |
. . . . . 6
β’ (π β 1 β
β) |
29 | | stoweidlem24.6 |
. . . . . . . . . 10
β’ (π β π· β
β+) |
30 | 29 | rpred 13016 |
. . . . . . . . 9
β’ (π β π· β β) |
31 | 7, 30 | remulcld 11244 |
. . . . . . . 8
β’ (π β (πΎ Β· π·) β β) |
32 | 31 | rehalfcld 12459 |
. . . . . . 7
β’ (π β ((πΎ Β· π·) / 2) β β) |
33 | 32, 17 | reexpcld 14128 |
. . . . . 6
β’ (π β (((πΎ Β· π·) / 2)βπ) β β) |
34 | 28, 33 | resubcld 11642 |
. . . . 5
β’ (π β (1 β (((πΎ Β· π·) / 2)βπ)) β β) |
35 | 34 | adantr 482 |
. . . 4
β’ ((π β§ π‘ β π) β (1 β (((πΎ Β· π·) / 2)βπ)) β β) |
36 | | stoweidlem24.9 |
. . . . 5
β’ (π β (1 β πΈ) < (1 β (((πΎ Β· π·) / 2)βπ))) |
37 | 36 | adantr 482 |
. . . 4
β’ ((π β§ π‘ β π) β (1 β πΈ) < (1 β (((πΎ Β· π·) / 2)βπ))) |
38 | 33 | adantr 482 |
. . . . 5
β’ ((π β§ π‘ β π) β (((πΎ Β· π·) / 2)βπ) β β) |
39 | 32 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π) β ((πΎ Β· π·) / 2) β β) |
40 | 6 | nn0ge0d 12535 |
. . . . . . . . 9
β’ (π β 0 β€ πΎ) |
41 | 7, 40 | jca 513 |
. . . . . . . 8
β’ (π β (πΎ β β β§ 0 β€ πΎ)) |
42 | 41 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (πΎ β β β§ 0 β€ πΎ)) |
43 | | stoweidlem24.10 |
. . . . . . . . . 10
β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
44 | 43 | r19.21bi 3249 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
45 | 44 | simpld 496 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β 0 β€ (πβπ‘)) |
46 | 13, 45 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π‘ β π) β 0 β€ (πβπ‘)) |
47 | | mulge0 11732 |
. . . . . . 7
β’ (((πΎ β β β§ 0 β€
πΎ) β§ ((πβπ‘) β β β§ 0 β€ (πβπ‘))) β 0 β€ (πΎ Β· (πβπ‘))) |
48 | 42, 15, 46, 47 | syl12anc 836 |
. . . . . 6
β’ ((π β§ π‘ β π) β 0 β€ (πΎ Β· (πβπ‘))) |
49 | 30 | rehalfcld 12459 |
. . . . . . . . 9
β’ (π β (π· / 2) β β) |
50 | 49 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (π· / 2) β β) |
51 | 12 | simprbi 498 |
. . . . . . . . . 10
β’ (π‘ β π β (πβπ‘) < (π· / 2)) |
52 | 51 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (πβπ‘) < (π· / 2)) |
53 | 15, 50, 52 | ltled 11362 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (πβπ‘) β€ (π· / 2)) |
54 | | lemul2a 12069 |
. . . . . . . 8
β’ ((((πβπ‘) β β β§ (π· / 2) β β β§ (πΎ β β β§ 0 β€
πΎ)) β§ (πβπ‘) β€ (π· / 2)) β (πΎ Β· (πβπ‘)) β€ (πΎ Β· (π· / 2))) |
55 | 15, 50, 42, 53, 54 | syl31anc 1374 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (πΎ Β· (πβπ‘)) β€ (πΎ Β· (π· / 2))) |
56 | 6 | nn0cnd 12534 |
. . . . . . . . 9
β’ (π β πΎ β β) |
57 | 56 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β πΎ β β) |
58 | 29 | rpcnd 13018 |
. . . . . . . . 9
β’ (π β π· β β) |
59 | 58 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β π· β β) |
60 | | 2cnne0 12422 |
. . . . . . . . 9
β’ (2 β
β β§ 2 β 0) |
61 | 60 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (2 β β β§ 2 β
0)) |
62 | | divass 11890 |
. . . . . . . 8
β’ ((πΎ β β β§ π· β β β§ (2 β
β β§ 2 β 0)) β ((πΎ Β· π·) / 2) = (πΎ Β· (π· / 2))) |
63 | 57, 59, 61, 62 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π‘ β π) β ((πΎ Β· π·) / 2) = (πΎ Β· (π· / 2))) |
64 | 55, 63 | breqtrrd 5177 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πΎ Β· (πβπ‘)) β€ ((πΎ Β· π·) / 2)) |
65 | | leexp1a 14140 |
. . . . . 6
β’ ((((πΎ Β· (πβπ‘)) β β β§ ((πΎ Β· π·) / 2) β β β§ π β β0)
β§ (0 β€ (πΎ Β·
(πβπ‘)) β§ (πΎ Β· (πβπ‘)) β€ ((πΎ Β· π·) / 2))) β ((πΎ Β· (πβπ‘))βπ) β€ (((πΎ Β· π·) / 2)βπ)) |
66 | 16, 39, 18, 48, 64, 65 | syl32anc 1379 |
. . . . 5
β’ ((π β§ π‘ β π) β ((πΎ Β· (πβπ‘))βπ) β€ (((πΎ Β· π·) / 2)βπ)) |
67 | 19, 38, 1, 66 | lesub2dd 11831 |
. . . 4
β’ ((π β§ π‘ β π) β (1 β (((πΎ Β· π·) / 2)βπ)) β€ (1 β ((πΎ Β· (πβπ‘))βπ))) |
68 | 5, 35, 20, 37, 67 | ltletrd 11374 |
. . 3
β’ ((π β§ π‘ β π) β (1 β πΈ) < (1 β ((πΎ Β· (πβπ‘))βπ))) |
69 | 15 | recnd 11242 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (πβπ‘) β β) |
70 | 57, 69, 18 | mulexpd 14126 |
. . . . . 6
β’ ((π β§ π‘ β π) β ((πΎ Β· (πβπ‘))βπ) = ((πΎβπ) Β· ((πβπ‘)βπ))) |
71 | 70 | eqcomd 2739 |
. . . . 5
β’ ((π β§ π‘ β π) β ((πΎβπ) Β· ((πβπ‘)βπ)) = ((πΎ Β· (πβπ‘))βπ)) |
72 | 71 | oveq2d 7425 |
. . . 4
β’ ((π β§ π‘ β π) β (1 β ((πΎβπ) Β· ((πβπ‘)βπ))) = (1 β ((πΎ Β· (πβπ‘))βπ))) |
73 | 13, 44 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
74 | 73 | simprd 497 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πβπ‘) β€ 1) |
75 | | exple1 14141 |
. . . . . 6
β’ ((((πβπ‘) β β β§ 0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ π β β0) β ((πβπ‘)βπ) β€ 1) |
76 | 15, 46, 74, 18, 75 | syl31anc 1374 |
. . . . 5
β’ ((π β§ π‘ β π) β ((πβπ‘)βπ) β€ 1) |
77 | | stoweidlem10 44726 |
. . . . 5
β’ ((((πβπ‘)βπ) β β β§ (πΎβπ) β β0 β§ ((πβπ‘)βπ) β€ 1) β (1 β ((πΎβπ) Β· ((πβπ‘)βπ))) β€ ((1 β ((πβπ‘)βπ))β(πΎβπ))) |
78 | 21, 26, 76, 77 | syl3anc 1372 |
. . . 4
β’ ((π β§ π‘ β π) β (1 β ((πΎβπ) Β· ((πβπ‘)βπ))) β€ ((1 β ((πβπ‘)βπ))β(πΎβπ))) |
79 | 72, 78 | eqbrtrrd 5173 |
. . 3
β’ ((π β§ π‘ β π) β (1 β ((πΎ Β· (πβπ‘))βπ)) β€ ((1 β ((πβπ‘)βπ))β(πΎβπ))) |
80 | 5, 20, 27, 68, 79 | ltletrd 11374 |
. 2
β’ ((π β§ π‘ β π) β (1 β πΈ) < ((1 β ((πβπ‘)βπ))β(πΎβπ))) |
81 | | stoweidlem24.2 |
. . . 4
β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) |
82 | 81, 9, 17, 6 | stoweidlem12 44728 |
. . 3
β’ ((π β§ π‘ β π) β (πβπ‘) = ((1 β ((πβπ‘)βπ))β(πΎβπ))) |
83 | 13, 82 | sylan2 594 |
. 2
β’ ((π β§ π‘ β π) β (πβπ‘) = ((1 β ((πβπ‘)βπ))β(πΎβπ))) |
84 | 80, 83 | breqtrrd 5177 |
1
β’ ((π β§ π‘ β π) β (1 β πΈ) < (πβπ‘)) |