Step | Hyp | Ref
| Expression |
1 | | iccpartgtprec.p |
. . . . 5
β’ (π β π β (RePartβπ)) |
2 | | iccpartgtprec.m |
. . . . . . 7
β’ (π β π β β) |
3 | | iccpart 45698 |
. . . . . . 7
β’ (π β β β (π β (RePartβπ) β (π β (β*
βm (0...π))
β§ βπ β
(0..^π)(πβπ) < (πβ(π + 1))))) |
4 | 2, 3 | syl 17 |
. . . . . 6
β’ (π β (π β (RePartβπ) β (π β (β*
βm (0...π))
β§ βπ β
(0..^π)(πβπ) < (πβ(π + 1))))) |
5 | | elmapfn 8809 |
. . . . . . 7
β’ (π β (β*
βm (0...π))
β π Fn (0...π)) |
6 | 5 | adantr 482 |
. . . . . 6
β’ ((π β (β*
βm (0...π))
β§ βπ β
(0..^π)(πβπ) < (πβ(π + 1))) β π Fn (0...π)) |
7 | 4, 6 | syl6bi 253 |
. . . . 5
β’ (π β (π β (RePartβπ) β π Fn (0...π))) |
8 | 1, 7 | mpd 15 |
. . . 4
β’ (π β π Fn (0...π)) |
9 | | fvelrnb 6907 |
. . . 4
β’ (π Fn (0...π) β (π β ran π β βπ β (0...π)(πβπ) = π)) |
10 | 8, 9 | syl 17 |
. . 3
β’ (π β (π β ran π β βπ β (0...π)(πβπ) = π)) |
11 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β π β β) |
12 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β π β (RePartβπ)) |
13 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β π β (0...π)) |
14 | 11, 12, 13 | iccpartxr 45701 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (πβπ) β
β*) |
15 | 2, 1 | iccpartgel 45711 |
. . . . . . . 8
β’ (π β βπ β (0...π)(πβ0) β€ (πβπ)) |
16 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = π β (πβπ) = (πβπ)) |
17 | 16 | breq2d 5121 |
. . . . . . . . . 10
β’ (π = π β ((πβ0) β€ (πβπ) β (πβ0) β€ (πβπ))) |
18 | 17 | rspcva 3581 |
. . . . . . . . 9
β’ ((π β (0...π) β§ βπ β (0...π)(πβ0) β€ (πβπ)) β (πβ0) β€ (πβπ)) |
19 | 18 | expcom 415 |
. . . . . . . 8
β’
(βπ β
(0...π)(πβ0) β€ (πβπ) β (π β (0...π) β (πβ0) β€ (πβπ))) |
20 | 15, 19 | syl 17 |
. . . . . . 7
β’ (π β (π β (0...π) β (πβ0) β€ (πβπ))) |
21 | 20 | imp 408 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (πβ0) β€ (πβπ)) |
22 | 2, 1 | iccpartleu 45710 |
. . . . . . . 8
β’ (π β βπ β (0...π)(πβπ) β€ (πβπ)) |
23 | 16 | breq1d 5119 |
. . . . . . . . . 10
β’ (π = π β ((πβπ) β€ (πβπ) β (πβπ) β€ (πβπ))) |
24 | 23 | rspcva 3581 |
. . . . . . . . 9
β’ ((π β (0...π) β§ βπ β (0...π)(πβπ) β€ (πβπ)) β (πβπ) β€ (πβπ)) |
25 | 24 | expcom 415 |
. . . . . . . 8
β’
(βπ β
(0...π)(πβπ) β€ (πβπ) β (π β (0...π) β (πβπ) β€ (πβπ))) |
26 | 22, 25 | syl 17 |
. . . . . . 7
β’ (π β (π β (0...π) β (πβπ) β€ (πβπ))) |
27 | 26 | imp 408 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (πβπ) β€ (πβπ)) |
28 | | nnnn0 12428 |
. . . . . . . . . . 11
β’ (π β β β π β
β0) |
29 | | 0elfz 13547 |
. . . . . . . . . . 11
β’ (π β β0
β 0 β (0...π)) |
30 | 2, 28, 29 | 3syl 18 |
. . . . . . . . . 10
β’ (π β 0 β (0...π)) |
31 | 2, 1, 30 | iccpartxr 45701 |
. . . . . . . . 9
β’ (π β (πβ0) β
β*) |
32 | | nn0fz0 13548 |
. . . . . . . . . . . 12
β’ (π β β0
β π β (0...π)) |
33 | 28, 32 | sylib 217 |
. . . . . . . . . . 11
β’ (π β β β π β (0...π)) |
34 | 2, 33 | syl 17 |
. . . . . . . . . 10
β’ (π β π β (0...π)) |
35 | 2, 1, 34 | iccpartxr 45701 |
. . . . . . . . 9
β’ (π β (πβπ) β
β*) |
36 | 31, 35 | jca 513 |
. . . . . . . 8
β’ (π β ((πβ0) β β* β§
(πβπ) β
β*)) |
37 | 36 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β ((πβ0) β β* β§
(πβπ) β
β*)) |
38 | | elicc1 13317 |
. . . . . . 7
β’ (((πβ0) β
β* β§ (πβπ) β β*) β ((πβπ) β ((πβ0)[,](πβπ)) β ((πβπ) β β* β§ (πβ0) β€ (πβπ) β§ (πβπ) β€ (πβπ)))) |
39 | 37, 38 | syl 17 |
. . . . . 6
β’ ((π β§ π β (0...π)) β ((πβπ) β ((πβ0)[,](πβπ)) β ((πβπ) β β* β§ (πβ0) β€ (πβπ) β§ (πβπ) β€ (πβπ)))) |
40 | 14, 21, 27, 39 | mpbir3and 1343 |
. . . . 5
β’ ((π β§ π β (0...π)) β (πβπ) β ((πβ0)[,](πβπ))) |
41 | | eleq1 2822 |
. . . . 5
β’ ((πβπ) = π β ((πβπ) β ((πβ0)[,](πβπ)) β π β ((πβ0)[,](πβπ)))) |
42 | 40, 41 | syl5ibcom 244 |
. . . 4
β’ ((π β§ π β (0...π)) β ((πβπ) = π β π β ((πβ0)[,](πβπ)))) |
43 | 42 | rexlimdva 3149 |
. . 3
β’ (π β (βπ β (0...π)(πβπ) = π β π β ((πβ0)[,](πβπ)))) |
44 | 10, 43 | sylbid 239 |
. 2
β’ (π β (π β ran π β π β ((πβ0)[,](πβπ)))) |
45 | 44 | ssrdv 3954 |
1
β’ (π β ran π β ((πβ0)[,](πβπ))) |