Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . 5
β’
β²ππ |
2 | | nfreu1 3384 |
. . . . 5
β’
β²πβ!π β (0..^π)π β ((πβπ)[,)(πβ(π + 1))) |
3 | | simpl 484 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β π) |
4 | | iccpartiun.m |
. . . . . . . . . . 11
β’ (π β π β β) |
5 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β β) |
6 | | iccpartiun.p |
. . . . . . . . . . 11
β’ (π β π β (RePartβπ)) |
7 | 6 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β (RePartβπ)) |
8 | | nnnn0 12428 |
. . . . . . . . . . . 12
β’ (π β β β π β
β0) |
9 | | 0elfz 13547 |
. . . . . . . . . . . 12
β’ (π β β0
β 0 β (0...π)) |
10 | 4, 8, 9 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β 0 β (0...π)) |
11 | 10 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β 0 β (0...π)) |
12 | 5, 7, 11 | iccpartxr 45701 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πβ0) β
β*) |
13 | | nn0fz0 13548 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β (0...π)) |
14 | 13 | biimpi 215 |
. . . . . . . . . . . 12
β’ (π β β0
β π β (0...π)) |
15 | 4, 8, 14 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β π β (0...π)) |
16 | 15 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
17 | 5, 7, 16 | iccpartxr 45701 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πβπ) β
β*) |
18 | 4, 6 | iccpartgel 45711 |
. . . . . . . . . . 11
β’ (π β βπ β (0...π)(πβ0) β€ (πβπ)) |
19 | | elfzofz 13597 |
. . . . . . . . . . . . . 14
β’ (π β (0..^π) β π β (0...π)) |
20 | 19 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
21 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
22 | 21 | breq2d 5121 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πβ0) β€ (πβπ) β (πβ0) β€ (πβπ))) |
23 | 22 | rspcv 3579 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β (βπ β (0...π)(πβ0) β€ (πβπ) β (πβ0) β€ (πβπ))) |
24 | 20, 23 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (βπ β (0...π)(πβ0) β€ (πβπ) β (πβ0) β€ (πβπ))) |
25 | 24 | ex 414 |
. . . . . . . . . . 11
β’ (π β (π β (0..^π) β (βπ β (0...π)(πβ0) β€ (πβπ) β (πβ0) β€ (πβπ)))) |
26 | 18, 25 | mpid 44 |
. . . . . . . . . 10
β’ (π β (π β (0..^π) β (πβ0) β€ (πβπ))) |
27 | 26 | imp 408 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πβ0) β€ (πβπ)) |
28 | 4, 6 | iccpartleu 45710 |
. . . . . . . . . . 11
β’ (π β βπ β (0...π)(πβπ) β€ (πβπ)) |
29 | | fzofzp1 13678 |
. . . . . . . . . . . . . 14
β’ (π β (0..^π) β (π + 1) β (0...π)) |
30 | 29 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
31 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
32 | 31 | breq1d 5119 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β ((πβπ) β€ (πβπ) β (πβ(π + 1)) β€ (πβπ))) |
33 | 32 | rspcv 3579 |
. . . . . . . . . . . . 13
β’ ((π + 1) β (0...π) β (βπ β (0...π)(πβπ) β€ (πβπ) β (πβ(π + 1)) β€ (πβπ))) |
34 | 30, 33 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (βπ β (0...π)(πβπ) β€ (πβπ) β (πβ(π + 1)) β€ (πβπ))) |
35 | 34 | ex 414 |
. . . . . . . . . . 11
β’ (π β (π β (0..^π) β (βπ β (0...π)(πβπ) β€ (πβπ) β (πβ(π + 1)) β€ (πβπ)))) |
36 | 28, 35 | mpid 44 |
. . . . . . . . . 10
β’ (π β (π β (0..^π) β (πβ(π + 1)) β€ (πβπ))) |
37 | 36 | imp 408 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β€ (πβπ)) |
38 | | icossico 13343 |
. . . . . . . . 9
β’ ((((πβ0) β
β* β§ (πβπ) β β*) β§ ((πβ0) β€ (πβπ) β§ (πβ(π + 1)) β€ (πβπ))) β ((πβπ)[,)(πβ(π + 1))) β ((πβ0)[,)(πβπ))) |
39 | 12, 17, 27, 37, 38 | syl22anc 838 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β ((πβπ)[,)(πβ(π + 1))) β ((πβ0)[,)(πβπ))) |
40 | 39 | sseld 3947 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)[,)(πβ(π + 1))) β π β ((πβ0)[,)(πβπ)))) |
41 | 4, 6 | icceuelpart 45718 |
. . . . . . 7
β’ ((π β§ π β ((πβ0)[,)(πβπ))) β β!π β (0..^π)π β ((πβπ)[,)(πβ(π + 1)))) |
42 | 3, 40, 41 | syl6an 683 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)[,)(πβ(π + 1))) β β!π β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) |
43 | 42 | ex 414 |
. . . . 5
β’ (π β (π β (0..^π) β (π β ((πβπ)[,)(πβ(π + 1))) β β!π β (0..^π)π β ((πβπ)[,)(πβ(π + 1)))))) |
44 | 1, 2, 43 | rexlimd 3248 |
. . . 4
β’ (π β (βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))) β β!π β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) |
45 | | rmo5 3372 |
. . . 4
β’
(β*π β
(0..^π)π β ((πβπ)[,)(πβ(π + 1))) β (βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))) β β!π β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) |
46 | 44, 45 | sylibr 233 |
. . 3
β’ (π β β*π β (0..^π)π β ((πβπ)[,)(πβ(π + 1)))) |
47 | 46 | alrimiv 1931 |
. 2
β’ (π β βπβ*π β (0..^π)π β ((πβπ)[,)(πβ(π + 1)))) |
48 | | df-disj 5075 |
. 2
β’
(Disj π
β (0..^π)((πβπ)[,)(πβ(π + 1))) β βπβ*π β (0..^π)π β ((πβπ)[,)(πβ(π + 1)))) |
49 | 47, 48 | sylibr 233 |
1
β’ (π β Disj π β (0..^π)((πβπ)[,)(πβ(π + 1)))) |