Step | Hyp | Ref
| Expression |
1 | | peano2nn 12173 |
. . . 4
β’ (π β β β (π + 1) β
β) |
2 | | iccpart 45698 |
. . . 4
β’ ((π + 1) β β β
(π β
(RePartβ(π + 1))
β (π β
(β* βm (0...(π + 1))) β§ βπ β (0..^(π + 1))(πβπ) < (πβ(π + 1))))) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β β β (π β (RePartβ(π + 1)) β (π β (β*
βm (0...(π
+ 1))) β§ βπ
β (0..^(π + 1))(πβπ) < (πβ(π + 1))))) |
4 | | simpl 484 |
. . . . . 6
β’ ((π β (β*
βm (0...(π
+ 1))) β§ βπ
β (0..^(π + 1))(πβπ) < (πβ(π + 1))) β π β (β*
βm (0...(π
+ 1)))) |
5 | | nnz 12528 |
. . . . . . . . 9
β’ (π β β β π β
β€) |
6 | | uzid 12786 |
. . . . . . . . 9
β’ (π β β€ β π β
(β€β₯βπ)) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
β’ (π β β β π β
(β€β₯βπ)) |
8 | | peano2uz 12834 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
9 | 7, 8 | syl 17 |
. . . . . . 7
β’ (π β β β (π + 1) β
(β€β₯βπ)) |
10 | | fzss2 13490 |
. . . . . . 7
β’ ((π + 1) β
(β€β₯βπ) β (0...π) β (0...(π + 1))) |
11 | 9, 10 | syl 17 |
. . . . . 6
β’ (π β β β
(0...π) β (0...(π + 1))) |
12 | | elmapssres 8811 |
. . . . . 6
β’ ((π β (β*
βm (0...(π
+ 1))) β§ (0...π)
β (0...(π + 1)))
β (π βΎ
(0...π)) β
(β* βm (0...π))) |
13 | 4, 11, 12 | syl2anr 598 |
. . . . 5
β’ ((π β β β§ (π β (β*
βm (0...(π
+ 1))) β§ βπ
β (0..^(π + 1))(πβπ) < (πβ(π + 1)))) β (π βΎ (0...π)) β (β*
βm (0...π))) |
14 | | fzoss2 13609 |
. . . . . . . . . 10
β’ ((π + 1) β
(β€β₯βπ) β (0..^π) β (0..^(π + 1))) |
15 | 9, 14 | syl 17 |
. . . . . . . . 9
β’ (π β β β
(0..^π) β (0..^(π + 1))) |
16 | | ssralv 4014 |
. . . . . . . . 9
β’
((0..^π) β
(0..^(π + 1)) β
(βπ β
(0..^(π + 1))(πβπ) < (πβ(π + 1)) β βπ β (0..^π)(πβπ) < (πβ(π + 1)))) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
β’ (π β β β
(βπ β
(0..^(π + 1))(πβπ) < (πβ(π + 1)) β βπ β (0..^π)(πβπ) < (πβ(π + 1)))) |
18 | 17 | adantld 492 |
. . . . . . 7
β’ (π β β β ((π β (β*
βm (0...(π
+ 1))) β§ βπ
β (0..^(π + 1))(πβπ) < (πβ(π + 1))) β βπ β (0..^π)(πβπ) < (πβ(π + 1)))) |
19 | 18 | imp 408 |
. . . . . 6
β’ ((π β β β§ (π β (β*
βm (0...(π
+ 1))) β§ βπ
β (0..^(π + 1))(πβπ) < (πβ(π + 1)))) β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
20 | | fzossfz 13600 |
. . . . . . . . . . . . . . 15
β’
(0..^π) β
(0...π) |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β (β*
βm (0...(π
+ 1))) β§ π β
β) β (0..^π)
β (0...π)) |
22 | 21 | sselda 3948 |
. . . . . . . . . . . . 13
β’ (((π β (β*
βm (0...(π
+ 1))) β§ π β
β) β§ π β
(0..^π)) β π β (0...π)) |
23 | | fvres 6865 |
. . . . . . . . . . . . . 14
β’ (π β (0...π) β ((π βΎ (0...π))βπ) = (πβπ)) |
24 | 23 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β (πβπ) = ((π βΎ (0...π))βπ)) |
25 | 22, 24 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β (β*
βm (0...(π
+ 1))) β§ π β
β) β§ π β
(0..^π)) β (πβπ) = ((π βΎ (0...π))βπ)) |
26 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π β (β*
βm (0...(π
+ 1))) β§ π β
β) β§ π β
(0..^π)) β π β (0..^π)) |
27 | | elfzouz 13585 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^π) β π β
(β€β₯β0)) |
28 | 27 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β (β*
βm (0...(π
+ 1))) β§ π β
β) β§ π β
(0..^π)) β π β
(β€β₯β0)) |
29 | | fzofzp1b 13679 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β0) β (π β (0..^π) β (π + 1) β (0...π))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β (β*
βm (0...(π
+ 1))) β§ π β
β) β§ π β
(0..^π)) β (π β (0..^π) β (π + 1) β (0...π))) |
31 | 26, 30 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π β (β*
βm (0...(π
+ 1))) β§ π β
β) β§ π β
(0..^π)) β (π + 1) β (0...π)) |
32 | | fvres 6865 |
. . . . . . . . . . . . . 14
β’ ((π + 1) β (0...π) β ((π βΎ (0...π))β(π + 1)) = (πβ(π + 1))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β (β*
βm (0...(π
+ 1))) β§ π β
β) β§ π β
(0..^π)) β ((π βΎ (0...π))β(π + 1)) = (πβ(π + 1))) |
34 | 33 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ (((π β (β*
βm (0...(π
+ 1))) β§ π β
β) β§ π β
(0..^π)) β (πβ(π + 1)) = ((π βΎ (0...π))β(π + 1))) |
35 | 25, 34 | breq12d 5122 |
. . . . . . . . . . 11
β’ (((π β (β*
βm (0...(π
+ 1))) β§ π β
β) β§ π β
(0..^π)) β ((πβπ) < (πβ(π + 1)) β ((π βΎ (0...π))βπ) < ((π βΎ (0...π))β(π + 1)))) |
36 | 35 | biimpd 228 |
. . . . . . . . . 10
β’ (((π β (β*
βm (0...(π
+ 1))) β§ π β
β) β§ π β
(0..^π)) β ((πβπ) < (πβ(π + 1)) β ((π βΎ (0...π))βπ) < ((π βΎ (0...π))β(π + 1)))) |
37 | 36 | ralimdva 3161 |
. . . . . . . . 9
β’ ((π β (β*
βm (0...(π
+ 1))) β§ π β
β) β (βπ
β (0..^π)(πβπ) < (πβ(π + 1)) β βπ β (0..^π)((π βΎ (0...π))βπ) < ((π βΎ (0...π))β(π + 1)))) |
38 | 37 | ex 414 |
. . . . . . . 8
β’ (π β (β*
βm (0...(π
+ 1))) β (π β
β β (βπ
β (0..^π)(πβπ) < (πβ(π + 1)) β βπ β (0..^π)((π βΎ (0...π))βπ) < ((π βΎ (0...π))β(π + 1))))) |
39 | 38 | adantr 482 |
. . . . . . 7
β’ ((π β (β*
βm (0...(π
+ 1))) β§ βπ
β (0..^(π + 1))(πβπ) < (πβ(π + 1))) β (π β β β (βπ β (0..^π)(πβπ) < (πβ(π + 1)) β βπ β (0..^π)((π βΎ (0...π))βπ) < ((π βΎ (0...π))β(π + 1))))) |
40 | 39 | impcom 409 |
. . . . . 6
β’ ((π β β β§ (π β (β*
βm (0...(π
+ 1))) β§ βπ
β (0..^(π + 1))(πβπ) < (πβ(π + 1)))) β (βπ β (0..^π)(πβπ) < (πβ(π + 1)) β βπ β (0..^π)((π βΎ (0...π))βπ) < ((π βΎ (0...π))β(π + 1)))) |
41 | 19, 40 | mpd 15 |
. . . . 5
β’ ((π β β β§ (π β (β*
βm (0...(π
+ 1))) β§ βπ
β (0..^(π + 1))(πβπ) < (πβ(π + 1)))) β βπ β (0..^π)((π βΎ (0...π))βπ) < ((π βΎ (0...π))β(π + 1))) |
42 | | iccpart 45698 |
. . . . . 6
β’ (π β β β ((π βΎ (0...π)) β (RePartβπ) β ((π βΎ (0...π)) β (β*
βm (0...π))
β§ βπ β
(0..^π)((π βΎ (0...π))βπ) < ((π βΎ (0...π))β(π + 1))))) |
43 | 42 | adantr 482 |
. . . . 5
β’ ((π β β β§ (π β (β*
βm (0...(π
+ 1))) β§ βπ
β (0..^(π + 1))(πβπ) < (πβ(π + 1)))) β ((π βΎ (0...π)) β (RePartβπ) β ((π βΎ (0...π)) β (β*
βm (0...π))
β§ βπ β
(0..^π)((π βΎ (0...π))βπ) < ((π βΎ (0...π))β(π + 1))))) |
44 | 13, 41, 43 | mpbir2and 712 |
. . . 4
β’ ((π β β β§ (π β (β*
βm (0...(π
+ 1))) β§ βπ
β (0..^(π + 1))(πβπ) < (πβ(π + 1)))) β (π βΎ (0...π)) β (RePartβπ)) |
45 | 44 | ex 414 |
. . 3
β’ (π β β β ((π β (β*
βm (0...(π
+ 1))) β§ βπ
β (0..^(π + 1))(πβπ) < (πβ(π + 1))) β (π βΎ (0...π)) β (RePartβπ))) |
46 | 3, 45 | sylbid 239 |
. 2
β’ (π β β β (π β (RePartβ(π + 1)) β (π βΎ (0...π)) β (RePartβπ))) |
47 | 46 | imp 408 |
1
β’ ((π β β β§ π β (RePartβ(π + 1))) β (π βΎ (0...π)) β (RePartβπ)) |