Step | Hyp | Ref
| Expression |
1 | | iccpartgtprec.m |
. . . . . . 7
β’ (π β π β β) |
2 | | nnnn0 12428 |
. . . . . . . 8
β’ (π β β β π β
β0) |
3 | | elnn0uz 12816 |
. . . . . . . 8
β’ (π β β0
β π β
(β€β₯β0)) |
4 | 2, 3 | sylib 217 |
. . . . . . 7
β’ (π β β β π β
(β€β₯β0)) |
5 | 1, 4 | syl 17 |
. . . . . 6
β’ (π β π β
(β€β₯β0)) |
6 | | fzisfzounsn 13693 |
. . . . . 6
β’ (π β
(β€β₯β0) β (0...π) = ((0..^π) βͺ {π})) |
7 | 5, 6 | syl 17 |
. . . . 5
β’ (π β (0...π) = ((0..^π) βͺ {π})) |
8 | 7 | eleq2d 2820 |
. . . 4
β’ (π β (π β (0...π) β π β ((0..^π) βͺ {π}))) |
9 | | elun 4112 |
. . . . 5
β’ (π β ((0..^π) βͺ {π}) β (π β (0..^π) β¨ π β {π})) |
10 | 9 | a1i 11 |
. . . 4
β’ (π β (π β ((0..^π) βͺ {π}) β (π β (0..^π) β¨ π β {π}))) |
11 | | velsn 4606 |
. . . . . 6
β’ (π β {π} β π = π) |
12 | 11 | a1i 11 |
. . . . 5
β’ (π β (π β {π} β π = π)) |
13 | 12 | orbi2d 915 |
. . . 4
β’ (π β ((π β (0..^π) β¨ π β {π}) β (π β (0..^π) β¨ π = π))) |
14 | 8, 10, 13 | 3bitrd 305 |
. . 3
β’ (π β (π β (0...π) β (π β (0..^π) β¨ π = π))) |
15 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π β β) |
16 | | iccpartgtprec.p |
. . . . . . . . 9
β’ (π β π β (RePartβπ)) |
17 | 16 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π β (RePartβπ)) |
18 | | fzossfz 13600 |
. . . . . . . . . 10
β’
(0..^π) β
(0...π) |
19 | 18 | a1i 11 |
. . . . . . . . 9
β’ (π β (0..^π) β (0...π)) |
20 | 19 | sselda 3948 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
21 | 15, 17, 20 | iccpartxr 45701 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (πβπ) β
β*) |
22 | | nn0fz0 13548 |
. . . . . . . . . . 11
β’ (π β β0
β π β (0...π)) |
23 | 2, 22 | sylib 217 |
. . . . . . . . . 10
β’ (π β β β π β (0...π)) |
24 | 1, 23 | syl 17 |
. . . . . . . . 9
β’ (π β π β (0...π)) |
25 | 1, 16, 24 | iccpartxr 45701 |
. . . . . . . 8
β’ (π β (πβπ) β
β*) |
26 | 25 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (πβπ) β
β*) |
27 | 1, 16 | iccpartltu 45707 |
. . . . . . . . 9
β’ (π β βπ β (0..^π)(πβπ) < (πβπ)) |
28 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = π β (πβπ) = (πβπ)) |
29 | 28 | breq1d 5119 |
. . . . . . . . . 10
β’ (π = π β ((πβπ) < (πβπ) β (πβπ) < (πβπ))) |
30 | 29 | rspccv 3580 |
. . . . . . . . 9
β’
(βπ β
(0..^π)(πβπ) < (πβπ) β (π β (0..^π) β (πβπ) < (πβπ))) |
31 | 27, 30 | syl 17 |
. . . . . . . 8
β’ (π β (π β (0..^π) β (πβπ) < (πβπ))) |
32 | 31 | imp 408 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβπ)) |
33 | 21, 26, 32 | xrltled 13078 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (πβπ) β€ (πβπ)) |
34 | 33 | expcom 415 |
. . . . 5
β’ (π β (0..^π) β (π β (πβπ) β€ (πβπ))) |
35 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π β (πβπ) = (πβπ)) |
36 | 35 | adantr 482 |
. . . . . . 7
β’ ((π = π β§ π) β (πβπ) = (πβπ)) |
37 | 25 | xrleidd 13080 |
. . . . . . . 8
β’ (π β (πβπ) β€ (πβπ)) |
38 | 37 | adantl 483 |
. . . . . . 7
β’ ((π = π β§ π) β (πβπ) β€ (πβπ)) |
39 | 36, 38 | eqbrtrd 5131 |
. . . . . 6
β’ ((π = π β§ π) β (πβπ) β€ (πβπ)) |
40 | 39 | ex 414 |
. . . . 5
β’ (π = π β (π β (πβπ) β€ (πβπ))) |
41 | 34, 40 | jaoi 856 |
. . . 4
β’ ((π β (0..^π) β¨ π = π) β (π β (πβπ) β€ (πβπ))) |
42 | 41 | com12 32 |
. . 3
β’ (π β ((π β (0..^π) β¨ π = π) β (πβπ) β€ (πβπ))) |
43 | 14, 42 | sylbid 239 |
. 2
β’ (π β (π β (0...π) β (πβπ) β€ (πβπ))) |
44 | 43 | ralrimiv 3139 |
1
β’ (π β βπ β (0...π)(πβπ) β€ (πβπ)) |