Step | Hyp | Ref
| Expression |
1 | | iccpartiun.p |
. . . . 5
β’ (π β π β (RePartβπ)) |
2 | | iccpartiun.m |
. . . . . 6
β’ (π β π β β) |
3 | | iccelpart 45715 |
. . . . . 6
β’ (π β β β
βπ β
(RePartβπ)(π₯ β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1))))) |
4 | | fveq1 6845 |
. . . . . . . . . . 11
β’ (π = π β (πβ0) = (πβ0)) |
5 | | fveq1 6845 |
. . . . . . . . . . 11
β’ (π = π β (πβπ) = (πβπ)) |
6 | 4, 5 | oveq12d 7379 |
. . . . . . . . . 10
β’ (π = π β ((πβ0)[,)(πβπ)) = ((πβ0)[,)(πβπ))) |
7 | 6 | eleq2d 2820 |
. . . . . . . . 9
β’ (π = π β (π₯ β ((πβ0)[,)(πβπ)) β π₯ β ((πβ0)[,)(πβπ)))) |
8 | | fveq1 6845 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ) = (πβπ)) |
9 | | fveq1 6845 |
. . . . . . . . . . . 12
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
10 | 8, 9 | oveq12d 7379 |
. . . . . . . . . . 11
β’ (π = π β ((πβπ)[,)(πβ(π + 1))) = ((πβπ)[,)(πβ(π + 1)))) |
11 | 10 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π = π β (π₯ β ((πβπ)[,)(πβ(π + 1))) β π₯ β ((πβπ)[,)(πβ(π + 1))))) |
12 | 11 | rexbidv 3172 |
. . . . . . . . 9
β’ (π = π β (βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1))) β βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1))))) |
13 | 7, 12 | imbi12d 345 |
. . . . . . . 8
β’ (π = π β ((π₯ β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1)))) β (π₯ β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1)))))) |
14 | 13 | rspcva 3581 |
. . . . . . 7
β’ ((π β (RePartβπ) β§ βπ β (RePartβπ)(π₯ β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1))))) β (π₯ β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1))))) |
15 | 14 | expcom 415 |
. . . . . 6
β’
(βπ β
(RePartβπ)(π₯ β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1)))) β (π β (RePartβπ) β (π₯ β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1)))))) |
16 | 2, 3, 15 | 3syl 18 |
. . . . 5
β’ (π β (π β (RePartβπ) β (π₯ β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1)))))) |
17 | 1, 16 | mpd 15 |
. . . 4
β’ (π β (π₯ β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1))))) |
18 | | nnnn0 12428 |
. . . . . . . . . . 11
β’ (π β β β π β
β0) |
19 | | 0elfz 13547 |
. . . . . . . . . . 11
β’ (π β β0
β 0 β (0...π)) |
20 | 2, 18, 19 | 3syl 18 |
. . . . . . . . . 10
β’ (π β 0 β (0...π)) |
21 | 2, 1, 20 | iccpartxr 45701 |
. . . . . . . . 9
β’ (π β (πβ0) β
β*) |
22 | | nn0fz0 13548 |
. . . . . . . . . . . 12
β’ (π β β0
β π β (0...π)) |
23 | 22 | biimpi 215 |
. . . . . . . . . . 11
β’ (π β β0
β π β (0...π)) |
24 | 2, 18, 23 | 3syl 18 |
. . . . . . . . . 10
β’ (π β π β (0...π)) |
25 | 2, 1, 24 | iccpartxr 45701 |
. . . . . . . . 9
β’ (π β (πβπ) β
β*) |
26 | 21, 25 | jca 513 |
. . . . . . . 8
β’ (π β ((πβ0) β β* β§
(πβπ) β
β*)) |
27 | 26 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β ((πβ0) β β* β§
(πβπ) β
β*)) |
28 | | elfzofz 13597 |
. . . . . . . 8
β’ (π β (0..^π) β π β (0...π)) |
29 | 2, 1 | iccpartgel 45711 |
. . . . . . . 8
β’ (π β βπ β (0...π)(πβ0) β€ (πβπ)) |
30 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = π β (πβπ) = (πβπ)) |
31 | 30 | breq2d 5121 |
. . . . . . . . 9
β’ (π = π β ((πβ0) β€ (πβπ) β (πβ0) β€ (πβπ))) |
32 | 31 | rspcva 3581 |
. . . . . . . 8
β’ ((π β (0...π) β§ βπ β (0...π)(πβ0) β€ (πβπ)) β (πβ0) β€ (πβπ)) |
33 | 28, 29, 32 | syl2anr 598 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (πβ0) β€ (πβπ)) |
34 | | fzofzp1 13678 |
. . . . . . . 8
β’ (π β (0..^π) β (π + 1) β (0...π)) |
35 | 2, 1 | iccpartleu 45710 |
. . . . . . . 8
β’ (π β βπ β (0...π)(πβπ) β€ (πβπ)) |
36 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
37 | 36 | breq1d 5119 |
. . . . . . . . 9
β’ (π = (π + 1) β ((πβπ) β€ (πβπ) β (πβ(π + 1)) β€ (πβπ))) |
38 | 37 | rspcva 3581 |
. . . . . . . 8
β’ (((π + 1) β (0...π) β§ βπ β (0...π)(πβπ) β€ (πβπ)) β (πβ(π + 1)) β€ (πβπ)) |
39 | 34, 35, 38 | syl2anr 598 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β€ (πβπ)) |
40 | | icossico 13343 |
. . . . . . 7
β’ ((((πβ0) β
β* β§ (πβπ) β β*) β§ ((πβ0) β€ (πβπ) β§ (πβ(π + 1)) β€ (πβπ))) β ((πβπ)[,)(πβ(π + 1))) β ((πβ0)[,)(πβπ))) |
41 | 27, 33, 39, 40 | syl12anc 836 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β ((πβπ)[,)(πβ(π + 1))) β ((πβ0)[,)(πβπ))) |
42 | 41 | sseld 3947 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (π₯ β ((πβπ)[,)(πβ(π + 1))) β π₯ β ((πβ0)[,)(πβπ)))) |
43 | 42 | rexlimdva 3149 |
. . . 4
β’ (π β (βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1))) β π₯ β ((πβ0)[,)(πβπ)))) |
44 | 17, 43 | impbid 211 |
. . 3
β’ (π β (π₯ β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1))))) |
45 | | eliun 4962 |
. . 3
β’ (π₯ β βͺ π β (0..^π)((πβπ)[,)(πβ(π + 1))) β βπ β (0..^π)π₯ β ((πβπ)[,)(πβ(π + 1)))) |
46 | 44, 45 | bitr4di 289 |
. 2
β’ (π β (π₯ β ((πβ0)[,)(πβπ)) β π₯ β βͺ
π β (0..^π)((πβπ)[,)(πβ(π + 1))))) |
47 | 46 | eqrdv 2731 |
1
β’ (π β ((πβ0)[,)(πβπ)) = βͺ
π β (0..^π)((πβπ)[,)(πβ(π + 1)))) |