Step | Hyp | Ref
| Expression |
1 | | iccpartgtprec.m |
. . . . . . . 8
β’ (π β π β β) |
2 | 1 | nnnn0d 12478 |
. . . . . . 7
β’ (π β π β
β0) |
3 | | elnn0uz 12813 |
. . . . . . 7
β’ (π β β0
β π β
(β€β₯β0)) |
4 | 2, 3 | sylib 217 |
. . . . . 6
β’ (π β π β
(β€β₯β0)) |
5 | | fzpred 13495 |
. . . . . 6
β’ (π β
(β€β₯β0) β (0...π) = ({0} βͺ ((0 + 1)...π))) |
6 | 4, 5 | syl 17 |
. . . . 5
β’ (π β (0...π) = ({0} βͺ ((0 + 1)...π))) |
7 | 6 | eleq2d 2820 |
. . . 4
β’ (π β (π β (0...π) β π β ({0} βͺ ((0 + 1)...π)))) |
8 | | elun 4109 |
. . . . 5
β’ (π β ({0} βͺ ((0 +
1)...π)) β (π β {0} β¨ π β ((0 + 1)...π))) |
9 | 8 | a1i 11 |
. . . 4
β’ (π β (π β ({0} βͺ ((0 + 1)...π)) β (π β {0} β¨ π β ((0 + 1)...π)))) |
10 | | velsn 4603 |
. . . . . 6
β’ (π β {0} β π = 0) |
11 | 10 | a1i 11 |
. . . . 5
β’ (π β (π β {0} β π = 0)) |
12 | | 0p1e1 12280 |
. . . . . . . 8
β’ (0 + 1) =
1 |
13 | 12 | a1i 11 |
. . . . . . 7
β’ (π β (0 + 1) =
1) |
14 | 13 | oveq1d 7373 |
. . . . . 6
β’ (π β ((0 + 1)...π) = (1...π)) |
15 | 14 | eleq2d 2820 |
. . . . 5
β’ (π β (π β ((0 + 1)...π) β π β (1...π))) |
16 | 11, 15 | orbi12d 918 |
. . . 4
β’ (π β ((π β {0} β¨ π β ((0 + 1)...π)) β (π = 0 β¨ π β (1...π)))) |
17 | 7, 9, 16 | 3bitrd 305 |
. . 3
β’ (π β (π β (0...π) β (π = 0 β¨ π β (1...π)))) |
18 | | iccpartgtprec.p |
. . . . . . . 8
β’ (π β π β (RePartβπ)) |
19 | | 0elfz 13544 |
. . . . . . . . 9
β’ (π β β0
β 0 β (0...π)) |
20 | 2, 19 | syl 17 |
. . . . . . . 8
β’ (π β 0 β (0...π)) |
21 | 1, 18, 20 | iccpartxr 45697 |
. . . . . . 7
β’ (π β (πβ0) β
β*) |
22 | 21 | xrleidd 13077 |
. . . . . 6
β’ (π β (πβ0) β€ (πβ0)) |
23 | | fveq2 6843 |
. . . . . . 7
β’ (π = 0 β (πβπ) = (πβ0)) |
24 | 23 | breq2d 5118 |
. . . . . 6
β’ (π = 0 β ((πβ0) β€ (πβπ) β (πβ0) β€ (πβ0))) |
25 | 22, 24 | syl5ibr 246 |
. . . . 5
β’ (π = 0 β (π β (πβ0) β€ (πβπ))) |
26 | 21 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (πβ0) β
β*) |
27 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β β) |
28 | 18 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β (RePartβπ)) |
29 | | 1nn0 12434 |
. . . . . . . . . . . 12
β’ 1 β
β0 |
30 | 29 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 1 β
β0) |
31 | | elnn0uz 12813 |
. . . . . . . . . . 11
β’ (1 β
β0 β 1 β
(β€β₯β0)) |
32 | 30, 31 | sylib 217 |
. . . . . . . . . 10
β’ (π β 1 β
(β€β₯β0)) |
33 | | fzss1 13486 |
. . . . . . . . . 10
β’ (1 β
(β€β₯β0) β (1...π) β (0...π)) |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
β’ (π β (1...π) β (0...π)) |
35 | 34 | sselda 3945 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β (0...π)) |
36 | 27, 28, 35 | iccpartxr 45697 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (πβπ) β
β*) |
37 | 1, 18 | iccpartgtl 45704 |
. . . . . . . . 9
β’ (π β βπ β (1...π)(πβ0) < (πβπ)) |
38 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = π β (πβπ) = (πβπ)) |
39 | 38 | breq2d 5118 |
. . . . . . . . . 10
β’ (π = π β ((πβ0) < (πβπ) β (πβ0) < (πβπ))) |
40 | 39 | rspccv 3577 |
. . . . . . . . 9
β’
(βπ β
(1...π)(πβ0) < (πβπ) β (π β (1...π) β (πβ0) < (πβπ))) |
41 | 37, 40 | syl 17 |
. . . . . . . 8
β’ (π β (π β (1...π) β (πβ0) < (πβπ))) |
42 | 41 | imp 408 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (πβ0) < (πβπ)) |
43 | 26, 36, 42 | xrltled 13075 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (πβ0) β€ (πβπ)) |
44 | 43 | expcom 415 |
. . . . 5
β’ (π β (1...π) β (π β (πβ0) β€ (πβπ))) |
45 | 25, 44 | jaoi 856 |
. . . 4
β’ ((π = 0 β¨ π β (1...π)) β (π β (πβ0) β€ (πβπ))) |
46 | 45 | com12 32 |
. . 3
β’ (π β ((π = 0 β¨ π β (1...π)) β (πβ0) β€ (πβπ))) |
47 | 17, 46 | sylbid 239 |
. 2
β’ (π β (π β (0...π) β (πβ0) β€ (πβπ))) |
48 | 47 | ralrimiv 3139 |
1
β’ (π β βπ β (0...π)(πβ0) β€ (πβπ)) |