Step | Hyp | Ref
| Expression |
1 | | stoweidlem5.2 |
. . 3
β’ π· = if(πΆ β€ (1 / 2), πΆ, (1 / 2)) |
2 | | stoweidlem5.5 |
. . . 4
β’ (π β πΆ β
β+) |
3 | | halfre 12375 |
. . . . 5
β’ (1 / 2)
β β |
4 | | halfgt0 12377 |
. . . . 5
β’ 0 < (1
/ 2) |
5 | 3, 4 | elrpii 12926 |
. . . 4
β’ (1 / 2)
β β+ |
6 | | ifcl 4535 |
. . . 4
β’ ((πΆ β β+
β§ (1 / 2) β β+) β if(πΆ β€ (1 / 2), πΆ, (1 / 2)) β
β+) |
7 | 2, 5, 6 | sylancl 587 |
. . 3
β’ (π β if(πΆ β€ (1 / 2), πΆ, (1 / 2)) β
β+) |
8 | 1, 7 | eqeltrid 2838 |
. 2
β’ (π β π· β
β+) |
9 | 8 | rpred 12965 |
. . 3
β’ (π β π· β β) |
10 | 3 | a1i 11 |
. . 3
β’ (π β (1 / 2) β
β) |
11 | | 1red 11164 |
. . 3
β’ (π β 1 β
β) |
12 | 2 | rpred 12965 |
. . . . 5
β’ (π β πΆ β β) |
13 | | min2 13118 |
. . . . 5
β’ ((πΆ β β β§ (1 / 2)
β β) β if(πΆ
β€ (1 / 2), πΆ, (1 / 2))
β€ (1 / 2)) |
14 | 12, 3, 13 | sylancl 587 |
. . . 4
β’ (π β if(πΆ β€ (1 / 2), πΆ, (1 / 2)) β€ (1 / 2)) |
15 | 1, 14 | eqbrtrid 5144 |
. . 3
β’ (π β π· β€ (1 / 2)) |
16 | | halflt1 12379 |
. . . 4
β’ (1 / 2)
< 1 |
17 | 16 | a1i 11 |
. . 3
β’ (π β (1 / 2) <
1) |
18 | 9, 10, 11, 15, 17 | lelttrd 11321 |
. 2
β’ (π β π· < 1) |
19 | | stoweidlem5.1 |
. . 3
β’
β²π‘π |
20 | 7 | rpred 12965 |
. . . . . . 7
β’ (π β if(πΆ β€ (1 / 2), πΆ, (1 / 2)) β β) |
21 | 20 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π) β if(πΆ β€ (1 / 2), πΆ, (1 / 2)) β β) |
22 | 12 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π) β πΆ β β) |
23 | | stoweidlem5.3 |
. . . . . . . 8
β’ (π β π:πβΆβ) |
24 | 23 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β π) β π:πβΆβ) |
25 | | stoweidlem5.4 |
. . . . . . . 8
β’ (π β π β π) |
26 | 25 | sselda 3948 |
. . . . . . 7
β’ ((π β§ π‘ β π) β π‘ β π) |
27 | 24, 26 | ffvelcdmd 7040 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πβπ‘) β β) |
28 | | min1 13117 |
. . . . . . . 8
β’ ((πΆ β β β§ (1 / 2)
β β) β if(πΆ
β€ (1 / 2), πΆ, (1 / 2))
β€ πΆ) |
29 | 12, 3, 28 | sylancl 587 |
. . . . . . 7
β’ (π β if(πΆ β€ (1 / 2), πΆ, (1 / 2)) β€ πΆ) |
30 | 29 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π) β if(πΆ β€ (1 / 2), πΆ, (1 / 2)) β€ πΆ) |
31 | | stoweidlem5.6 |
. . . . . . 7
β’ (π β βπ‘ β π πΆ β€ (πβπ‘)) |
32 | 31 | r19.21bi 3233 |
. . . . . 6
β’ ((π β§ π‘ β π) β πΆ β€ (πβπ‘)) |
33 | 21, 22, 27, 30, 32 | letrd 11320 |
. . . . 5
β’ ((π β§ π‘ β π) β if(πΆ β€ (1 / 2), πΆ, (1 / 2)) β€ (πβπ‘)) |
34 | 1, 33 | eqbrtrid 5144 |
. . . 4
β’ ((π β§ π‘ β π) β π· β€ (πβπ‘)) |
35 | 34 | ex 414 |
. . 3
β’ (π β (π‘ β π β π· β€ (πβπ‘))) |
36 | 19, 35 | ralrimi 3239 |
. 2
β’ (π β βπ‘ β π π· β€ (πβπ‘)) |
37 | | eleq1 2822 |
. . . . 5
β’ (π = π· β (π β β+ β π· β
β+)) |
38 | | breq1 5112 |
. . . . 5
β’ (π = π· β (π < 1 β π· < 1)) |
39 | | breq1 5112 |
. . . . . 6
β’ (π = π· β (π β€ (πβπ‘) β π· β€ (πβπ‘))) |
40 | 39 | ralbidv 3171 |
. . . . 5
β’ (π = π· β (βπ‘ β π π β€ (πβπ‘) β βπ‘ β π π· β€ (πβπ‘))) |
41 | 37, 38, 40 | 3anbi123d 1437 |
. . . 4
β’ (π = π· β ((π β β+ β§ π < 1 β§ βπ‘ β π π β€ (πβπ‘)) β (π· β β+ β§ π· < 1 β§ βπ‘ β π π· β€ (πβπ‘)))) |
42 | 41 | spcegv 3558 |
. . 3
β’ (π· β β+
β ((π· β
β+ β§ π·
< 1 β§ βπ‘
β π π· β€ (πβπ‘)) β βπ(π β β+ β§ π < 1 β§ βπ‘ β π π β€ (πβπ‘)))) |
43 | 8, 42 | syl 17 |
. 2
β’ (π β ((π· β β+ β§ π· < 1 β§ βπ‘ β π π· β€ (πβπ‘)) β βπ(π β β+ β§ π < 1 β§ βπ‘ β π π β€ (πβπ‘)))) |
44 | 8, 18, 36, 43 | mp3and 1465 |
1
β’ (π β βπ(π β β+ β§ π < 1 β§ βπ‘ β π π β€ (πβπ‘))) |