Step | Hyp | Ref
| Expression |
1 | | nfcv 2904 |
. . 3
β’
β²π‘(π· / 2) |
2 | | stoweidlem52.3 |
. . 3
β’
β²π‘π |
3 | | stoweidlem52.2 |
. . 3
β’
β²π‘π |
4 | | stoweidlem52.4 |
. . 3
β’ πΎ = (topGenβran
(,)) |
5 | | stoweidlem52.7 |
. . 3
β’ π = βͺ
π½ |
6 | | stoweidlem52.5 |
. . 3
β’ π = {π‘ β π β£ (πβπ‘) < (π· / 2)} |
7 | | stoweidlem52.13 |
. . . . . 6
β’ (π β π· β
β+) |
8 | 7 | rpred 12962 |
. . . . 5
β’ (π β π· β β) |
9 | 8 | rehalfcld 12405 |
. . . 4
β’ (π β (π· / 2) β β) |
10 | 9 | rexrd 11210 |
. . 3
β’ (π β (π· / 2) β
β*) |
11 | | stoweidlem52.9 |
. . . . 5
β’ (π β π΄ β πΆ) |
12 | | stoweidlem52.8 |
. . . . 5
β’ πΆ = (π½ Cn πΎ) |
13 | 11, 12 | sseqtrdi 3995 |
. . . 4
β’ (π β π΄ β (π½ Cn πΎ)) |
14 | | stoweidlem52.17 |
. . . 4
β’ (π β π β π΄) |
15 | 13, 14 | sseldd 3946 |
. . 3
β’ (π β π β (π½ Cn πΎ)) |
16 | 1, 2, 3, 4, 5, 6, 10, 15 | rfcnpre2 43324 |
. 2
β’ (π β π β π½) |
17 | | stoweidlem52.15 |
. . . . . . . 8
β’ (π β π β π½) |
18 | | elssuni 4899 |
. . . . . . . 8
β’ (π β π½ β π β βͺ π½) |
19 | 17, 18 | syl 17 |
. . . . . . 7
β’ (π β π β βͺ π½) |
20 | 19, 5 | sseqtrrdi 3996 |
. . . . . 6
β’ (π β π β π) |
21 | | stoweidlem52.16 |
. . . . . 6
β’ (π β π β π) |
22 | 20, 21 | sseldd 3946 |
. . . . 5
β’ (π β π β π) |
23 | | stoweidlem52.19 |
. . . . . 6
β’ (π β (πβπ) = 0) |
24 | | 2re 12232 |
. . . . . . . 8
β’ 2 β
β |
25 | 24 | a1i 11 |
. . . . . . 7
β’ (π β 2 β
β) |
26 | 7 | rpgt0d 12965 |
. . . . . . 7
β’ (π β 0 < π·) |
27 | | 2pos 12261 |
. . . . . . . 8
β’ 0 <
2 |
28 | 27 | a1i 11 |
. . . . . . 7
β’ (π β 0 < 2) |
29 | 8, 25, 26, 28 | divgt0d 12095 |
. . . . . 6
β’ (π β 0 < (π· / 2)) |
30 | 23, 29 | eqbrtrd 5128 |
. . . . 5
β’ (π β (πβπ) < (π· / 2)) |
31 | | nfcv 2904 |
. . . . . 6
β’
β²π‘π |
32 | | nfcv 2904 |
. . . . . 6
β’
β²π‘π |
33 | 2, 31 | nffv 6853 |
. . . . . . 7
β’
β²π‘(πβπ) |
34 | | nfcv 2904 |
. . . . . . 7
β’
β²π‘
< |
35 | 33, 34, 1 | nfbr 5153 |
. . . . . 6
β’
β²π‘(πβπ) < (π· / 2) |
36 | | fveq2 6843 |
. . . . . . 7
β’ (π‘ = π β (πβπ‘) = (πβπ)) |
37 | 36 | breq1d 5116 |
. . . . . 6
β’ (π‘ = π β ((πβπ‘) < (π· / 2) β (πβπ) < (π· / 2))) |
38 | 31, 32, 35, 37 | elrabf 3642 |
. . . . 5
β’ (π β {π‘ β π β£ (πβπ‘) < (π· / 2)} β (π β π β§ (πβπ) < (π· / 2))) |
39 | 22, 30, 38 | sylanbrc 584 |
. . . 4
β’ (π β π β {π‘ β π β£ (πβπ‘) < (π· / 2)}) |
40 | 39, 6 | eleqtrrdi 2845 |
. . 3
β’ (π β π β π) |
41 | | nfrab1 3425 |
. . . . 5
β’
β²π‘{π‘ β π β£ (πβπ‘) < (π· / 2)} |
42 | 6, 41 | nfcxfr 2902 |
. . . 4
β’
β²π‘π |
43 | | stoweidlem52.1 |
. . . 4
β’
β²π‘π |
44 | 11, 14 | sseldd 3946 |
. . . . . . . . . . 11
β’ (π β π β πΆ) |
45 | 4, 5, 12, 44 | fcnre 43318 |
. . . . . . . . . 10
β’ (π β π:πβΆβ) |
46 | 45 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β π:πβΆβ) |
47 | 6 | reqabi 3428 |
. . . . . . . . . . . 12
β’ (π‘ β π β (π‘ β π β§ (πβπ‘) < (π· / 2))) |
48 | 47 | biimpi 215 |
. . . . . . . . . . 11
β’ (π‘ β π β (π‘ β π β§ (πβπ‘) < (π· / 2))) |
49 | 48 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β (π‘ β π β§ (πβπ‘) < (π· / 2))) |
50 | 49 | simpld 496 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β π‘ β π) |
51 | 46, 50 | ffvelcdmd 7037 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (πβπ‘) β β) |
52 | 9 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (π· / 2) β β) |
53 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β π· β β) |
54 | 49 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (πβπ‘) < (π· / 2)) |
55 | | halfpos 12388 |
. . . . . . . . . . 11
β’ (π· β β β (0 <
π· β (π· / 2) < π·)) |
56 | 8, 55 | syl 17 |
. . . . . . . . . 10
β’ (π β (0 < π· β (π· / 2) < π·)) |
57 | 26, 56 | mpbid 231 |
. . . . . . . . 9
β’ (π β (π· / 2) < π·) |
58 | 57 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (π· / 2) < π·) |
59 | 51, 52, 53, 54, 58 | lttrd 11321 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (πβπ‘) < π·) |
60 | 59 | adantr 482 |
. . . . . 6
β’ (((π β§ π‘ β π) β§ Β¬ π‘ β π) β (πβπ‘) < π·) |
61 | 8 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π‘ β π) β§ Β¬ π‘ β π) β π· β β) |
62 | 51 | adantr 482 |
. . . . . . 7
β’ (((π β§ π‘ β π) β§ Β¬ π‘ β π) β (πβπ‘) β β) |
63 | | stoweidlem52.20 |
. . . . . . . . 9
β’ (π β βπ‘ β (π β π)π· β€ (πβπ‘)) |
64 | 63 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π‘ β π) β§ Β¬ π‘ β π) β βπ‘ β (π β π)π· β€ (πβπ‘)) |
65 | 50 | anim1i 616 |
. . . . . . . . 9
β’ (((π β§ π‘ β π) β§ Β¬ π‘ β π) β (π‘ β π β§ Β¬ π‘ β π)) |
66 | | eldif 3921 |
. . . . . . . . 9
β’ (π‘ β (π β π) β (π‘ β π β§ Β¬ π‘ β π)) |
67 | 65, 66 | sylibr 233 |
. . . . . . . 8
β’ (((π β§ π‘ β π) β§ Β¬ π‘ β π) β π‘ β (π β π)) |
68 | | rsp 3229 |
. . . . . . . 8
β’
(βπ‘ β
(π β π)π· β€ (πβπ‘) β (π‘ β (π β π) β π· β€ (πβπ‘))) |
69 | 64, 67, 68 | sylc 65 |
. . . . . . 7
β’ (((π β§ π‘ β π) β§ Β¬ π‘ β π) β π· β€ (πβπ‘)) |
70 | 61, 62, 69 | lensymd 11311 |
. . . . . 6
β’ (((π β§ π‘ β π) β§ Β¬ π‘ β π) β Β¬ (πβπ‘) < π·) |
71 | 60, 70 | condan 817 |
. . . . 5
β’ ((π β§ π‘ β π) β π‘ β π) |
72 | 71 | ex 414 |
. . . 4
β’ (π β (π‘ β π β π‘ β π)) |
73 | 3, 42, 43, 72 | ssrd 3950 |
. . 3
β’ (π β π β π) |
74 | | nfv 1918 |
. . . . . . . . 9
β’
β²π‘ π β
β+ |
75 | 3, 74 | nfan 1903 |
. . . . . . . 8
β’
β²π‘(π β§ π β β+) |
76 | | nfv 1918 |
. . . . . . . 8
β’
β²π‘ π¦ β π΄ |
77 | 75, 76 | nfan 1903 |
. . . . . . 7
β’
β²π‘((π β§ π β β+) β§ π¦ β π΄) |
78 | | nfra1 3266 |
. . . . . . . 8
β’
β²π‘βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) |
79 | | nfra1 3266 |
. . . . . . . 8
β’
β²π‘βπ‘ β π (1 β π) < (π¦βπ‘) |
80 | | nfra1 3266 |
. . . . . . . 8
β’
β²π‘βπ‘ β (π β π)(π¦βπ‘) < π |
81 | 78, 79, 80 | nf3an 1905 |
. . . . . . 7
β’
β²π‘(βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π) |
82 | 77, 81 | nfan 1903 |
. . . . . 6
β’
β²π‘(((π β§ π β β+) β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) |
83 | | eqid 2733 |
. . . . . 6
β’ (π‘ β π β¦ (1 β (π¦βπ‘))) = (π‘ β π β¦ (1 β (π¦βπ‘))) |
84 | | eqid 2733 |
. . . . . 6
β’ (π‘ β π β¦ 1) = (π‘ β π β¦ 1) |
85 | | ssrab2 4038 |
. . . . . . 7
β’ {π‘ β π β£ (πβπ‘) < (π· / 2)} β π |
86 | 6, 85 | eqsstri 3979 |
. . . . . 6
β’ π β π |
87 | | simplr 768 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) β π¦ β π΄) |
88 | | simplll 774 |
. . . . . . 7
β’ ((((π β§ π β β+) β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) β π) |
89 | 11 | sselda 3945 |
. . . . . . . 8
β’ ((π β§ π¦ β π΄) β π¦ β πΆ) |
90 | 4, 5, 12, 89 | fcnre 43318 |
. . . . . . 7
β’ ((π β§ π¦ β π΄) β π¦:πβΆβ) |
91 | 88, 87, 90 | syl2anc 585 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) β π¦:πβΆβ) |
92 | 11 | sselda 3945 |
. . . . . . . 8
β’ ((π β§ π β π΄) β π β πΆ) |
93 | 4, 5, 12, 92 | fcnre 43318 |
. . . . . . 7
β’ ((π β§ π β π΄) β π:πβΆβ) |
94 | 88, 93 | sylan 581 |
. . . . . 6
β’
(((((π β§ π β β+)
β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) β§ π β π΄) β π:πβΆβ) |
95 | | stoweidlem52.10 |
. . . . . . 7
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
96 | 88, 95 | syl3an1 1164 |
. . . . . 6
β’
(((((π β§ π β β+)
β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
97 | | stoweidlem52.11 |
. . . . . . 7
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
98 | 88, 97 | syl3an1 1164 |
. . . . . 6
β’
(((((π β§ π β β+)
β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
99 | | stoweidlem52.12 |
. . . . . . 7
β’ ((π β§ π β β) β (π‘ β π β¦ π) β π΄) |
100 | 88, 99 | sylan 581 |
. . . . . 6
β’
(((((π β§ π β β+)
β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) β§ π β β) β (π‘ β π β¦ π) β π΄) |
101 | | simpllr 775 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) β π β β+) |
102 | | simpr1 1195 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) β βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)) |
103 | | simpr2 1196 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) β βπ‘ β π (1 β π) < (π¦βπ‘)) |
104 | | simpr3 1197 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) β βπ‘ β (π β π)(π¦βπ‘) < π) |
105 | 82, 83, 84, 86, 87, 91, 94, 96, 98, 100, 101, 102, 103, 104 | stoweidlem41 44368 |
. . . . 5
β’ ((((π β§ π β β+) β§ π¦ β π΄) β§ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘))) |
106 | 7 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β+) β π· β
β+) |
107 | | stoweidlem52.14 |
. . . . . . 7
β’ (π β π· < 1) |
108 | 107 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β+) β π· < 1) |
109 | 14 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β+) β π β π΄) |
110 | 45 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β+) β π:πβΆβ) |
111 | | stoweidlem52.18 |
. . . . . . 7
β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
112 | 111 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β+) β
βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
113 | 63 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β+) β
βπ‘ β (π β π)π· β€ (πβπ‘)) |
114 | 93 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β+) β§ π β π΄) β π:πβΆβ) |
115 | 95 | 3adant1r 1178 |
. . . . . 6
β’ (((π β§ π β β+) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
116 | 97 | 3adant1r 1178 |
. . . . . 6
β’ (((π β§ π β β+) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
117 | 99 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β+) β§ π β β) β (π‘ β π β¦ π) β π΄) |
118 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β β+) β π β
β+) |
119 | 2, 75, 6, 106, 108, 109, 110, 112, 113, 114, 115, 116, 117, 118 | stoweidlem49 44376 |
. . . . 5
β’ ((π β§ π β β+) β
βπ¦ β π΄ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β π) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < π)) |
120 | 105, 119 | r19.29a 3156 |
. . . 4
β’ ((π β§ π β β+) β
βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘))) |
121 | 120 | ralrimiva 3140 |
. . 3
β’ (π β βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘))) |
122 | 40, 73, 121 | jca31 516 |
. 2
β’ (π β ((π β π β§ π β π) β§ βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)))) |
123 | | eleq2 2823 |
. . . . 5
β’ (π£ = π β (π β π£ β π β π)) |
124 | | sseq1 3970 |
. . . . 5
β’ (π£ = π β (π£ β π β π β π)) |
125 | 123, 124 | anbi12d 632 |
. . . 4
β’ (π£ = π β ((π β π£ β§ π£ β π) β (π β π β§ π β π))) |
126 | | nfcv 2904 |
. . . . . . . 8
β’
β²π‘π£ |
127 | 126, 42 | raleqf 3327 |
. . . . . . 7
β’ (π£ = π β (βπ‘ β π£ (π₯βπ‘) < π β βπ‘ β π (π₯βπ‘) < π)) |
128 | 127 | 3anbi2d 1442 |
. . . . . 6
β’ (π£ = π β ((βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π£ (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)) β (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)))) |
129 | 128 | rexbidv 3172 |
. . . . 5
β’ (π£ = π β (βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π£ (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)) β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)))) |
130 | 129 | ralbidv 3171 |
. . . 4
β’ (π£ = π β (βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π£ (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)) β βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)))) |
131 | 125, 130 | anbi12d 632 |
. . 3
β’ (π£ = π β (((π β π£ β§ π£ β π) β§ βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π£ (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘))) β ((π β π β§ π β π) β§ βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘))))) |
132 | 131 | rspcev 3580 |
. 2
β’ ((π β π½ β§ ((π β π β§ π β π) β§ βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)))) β βπ£ β π½ ((π β π£ β§ π£ β π) β§ βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π£ (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)))) |
133 | 16, 122, 132 | syl2anc 585 |
1
β’ (π β βπ£ β π½ ((π β π£ β§ π£ β π) β§ βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π£ (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)))) |