Step | Hyp | Ref
| Expression |
1 | | iccpartgtprec.m |
. . . . . . 7
β’ (π β π β β) |
2 | | 0zd 12516 |
. . . . . . . 8
β’ (π β β β 0 β
β€) |
3 | | nnz 12525 |
. . . . . . . 8
β’ (π β β β π β
β€) |
4 | | nngt0 12189 |
. . . . . . . 8
β’ (π β β β 0 <
π) |
5 | 2, 3, 4 | 3jca 1129 |
. . . . . . 7
β’ (π β β β (0 β
β€ β§ π β
β€ β§ 0 < π)) |
6 | 1, 5 | syl 17 |
. . . . . 6
β’ (π β (0 β β€ β§
π β β€ β§ 0
< π)) |
7 | | fzopred 45640 |
. . . . . 6
β’ ((0
β β€ β§ π
β β€ β§ 0 < π) β (0..^π) = ({0} βͺ ((0 + 1)..^π))) |
8 | 6, 7 | syl 17 |
. . . . 5
β’ (π β (0..^π) = ({0} βͺ ((0 + 1)..^π))) |
9 | | 0p1e1 12280 |
. . . . . . . 8
β’ (0 + 1) =
1 |
10 | 9 | a1i 11 |
. . . . . . 7
β’ (π β (0 + 1) =
1) |
11 | 10 | oveq1d 7373 |
. . . . . 6
β’ (π β ((0 + 1)..^π) = (1..^π)) |
12 | 11 | uneq2d 4124 |
. . . . 5
β’ (π β ({0} βͺ ((0 +
1)..^π)) = ({0} βͺ
(1..^π))) |
13 | 8, 12 | eqtrd 2773 |
. . . 4
β’ (π β (0..^π) = ({0} βͺ (1..^π))) |
14 | 13 | eleq2d 2820 |
. . 3
β’ (π β (π β (0..^π) β π β ({0} βͺ (1..^π)))) |
15 | | elun 4109 |
. . . 4
β’ (π β ({0} βͺ (1..^π)) β (π β {0} β¨ π β (1..^π))) |
16 | | elsni 4604 |
. . . . . . 7
β’ (π β {0} β π = 0) |
17 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = 0 β (πβπ) = (πβ0)) |
18 | 17 | adantr 482 |
. . . . . . . . 9
β’ ((π = 0 β§ π) β (πβπ) = (πβ0)) |
19 | | iccpartgtprec.p |
. . . . . . . . . . 11
β’ (π β π β (RePartβπ)) |
20 | 1, 19 | iccpartlt 45702 |
. . . . . . . . . 10
β’ (π β (πβ0) < (πβπ)) |
21 | 20 | adantl 483 |
. . . . . . . . 9
β’ ((π = 0 β§ π) β (πβ0) < (πβπ)) |
22 | 18, 21 | eqbrtrd 5128 |
. . . . . . . 8
β’ ((π = 0 β§ π) β (πβπ) < (πβπ)) |
23 | 22 | ex 414 |
. . . . . . 7
β’ (π = 0 β (π β (πβπ) < (πβπ))) |
24 | 16, 23 | syl 17 |
. . . . . 6
β’ (π β {0} β (π β (πβπ) < (πβπ))) |
25 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π β (πβπ) = (πβπ)) |
26 | 25 | breq1d 5116 |
. . . . . . . 8
β’ (π = π β ((πβπ) < (πβπ) β (πβπ) < (πβπ))) |
27 | 26 | rspccv 3577 |
. . . . . . 7
β’
(βπ β
(1..^π)(πβπ) < (πβπ) β (π β (1..^π) β (πβπ) < (πβπ))) |
28 | 1, 19 | iccpartiltu 45700 |
. . . . . . 7
β’ (π β βπ β (1..^π)(πβπ) < (πβπ)) |
29 | 27, 28 | syl11 33 |
. . . . . 6
β’ (π β (1..^π) β (π β (πβπ) < (πβπ))) |
30 | 24, 29 | jaoi 856 |
. . . . 5
β’ ((π β {0} β¨ π β (1..^π)) β (π β (πβπ) < (πβπ))) |
31 | 30 | com12 32 |
. . . 4
β’ (π β ((π β {0} β¨ π β (1..^π)) β (πβπ) < (πβπ))) |
32 | 15, 31 | biimtrid 241 |
. . 3
β’ (π β (π β ({0} βͺ (1..^π)) β (πβπ) < (πβπ))) |
33 | 14, 32 | sylbid 239 |
. 2
β’ (π β (π β (0..^π) β (πβπ) < (πβπ))) |
34 | 33 | ralrimiv 3139 |
1
β’ (π β βπ β (0..^π)(πβπ) < (πβπ)) |