Step | Hyp | Ref
| Expression |
1 | | fveq2 6892 |
. . 3
β’ (π₯ = 1 β (RePartβπ₯) =
(RePartβ1)) |
2 | | fveq2 6892 |
. . . . . 6
β’ (π₯ = 1 β (πβπ₯) = (πβ1)) |
3 | 2 | oveq2d 7428 |
. . . . 5
β’ (π₯ = 1 β ((πβ0)[,)(πβπ₯)) = ((πβ0)[,)(πβ1))) |
4 | 3 | eleq2d 2818 |
. . . 4
β’ (π₯ = 1 β (π β ((πβ0)[,)(πβπ₯)) β π β ((πβ0)[,)(πβ1)))) |
5 | | oveq2 7420 |
. . . . . 6
β’ (π₯ = 1 β (0..^π₯) = (0..^1)) |
6 | | fzo01 13719 |
. . . . . 6
β’ (0..^1) =
{0} |
7 | 5, 6 | eqtrdi 2787 |
. . . . 5
β’ (π₯ = 1 β (0..^π₯) = {0}) |
8 | 7 | rexeqdv 3325 |
. . . 4
β’ (π₯ = 1 β (βπ β (0..^π₯)π β ((πβπ)[,)(πβ(π + 1))) β βπ β {0}π β ((πβπ)[,)(πβ(π + 1))))) |
9 | 4, 8 | imbi12d 343 |
. . 3
β’ (π₯ = 1 β ((π β ((πβ0)[,)(πβπ₯)) β βπ β (0..^π₯)π β ((πβπ)[,)(πβ(π + 1)))) β (π β ((πβ0)[,)(πβ1)) β βπ β {0}π β ((πβπ)[,)(πβ(π + 1)))))) |
10 | 1, 9 | raleqbidv 3341 |
. 2
β’ (π₯ = 1 β (βπ β (RePartβπ₯)(π β ((πβ0)[,)(πβπ₯)) β βπ β (0..^π₯)π β ((πβπ)[,)(πβ(π + 1)))) β βπ β (RePartβ1)(π β ((πβ0)[,)(πβ1)) β βπ β {0}π β ((πβπ)[,)(πβ(π + 1)))))) |
11 | | fveq2 6892 |
. . 3
β’ (π₯ = π¦ β (RePartβπ₯) = (RePartβπ¦)) |
12 | | fveq2 6892 |
. . . . . 6
β’ (π₯ = π¦ β (πβπ₯) = (πβπ¦)) |
13 | 12 | oveq2d 7428 |
. . . . 5
β’ (π₯ = π¦ β ((πβ0)[,)(πβπ₯)) = ((πβ0)[,)(πβπ¦))) |
14 | 13 | eleq2d 2818 |
. . . 4
β’ (π₯ = π¦ β (π β ((πβ0)[,)(πβπ₯)) β π β ((πβ0)[,)(πβπ¦)))) |
15 | | oveq2 7420 |
. . . . 5
β’ (π₯ = π¦ β (0..^π₯) = (0..^π¦)) |
16 | 15 | rexeqdv 3325 |
. . . 4
β’ (π₯ = π¦ β (βπ β (0..^π₯)π β ((πβπ)[,)(πβ(π + 1))) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))))) |
17 | 14, 16 | imbi12d 343 |
. . 3
β’ (π₯ = π¦ β ((π β ((πβ0)[,)(πβπ₯)) β βπ β (0..^π₯)π β ((πβπ)[,)(πβ(π + 1)))) β (π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))))) |
18 | 11, 17 | raleqbidv 3341 |
. 2
β’ (π₯ = π¦ β (βπ β (RePartβπ₯)(π β ((πβ0)[,)(πβπ₯)) β βπ β (0..^π₯)π β ((πβπ)[,)(πβ(π + 1)))) β βπ β (RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))))) |
19 | | fveq2 6892 |
. . 3
β’ (π₯ = (π¦ + 1) β (RePartβπ₯) = (RePartβ(π¦ + 1))) |
20 | | fveq2 6892 |
. . . . . 6
β’ (π₯ = (π¦ + 1) β (πβπ₯) = (πβ(π¦ + 1))) |
21 | 20 | oveq2d 7428 |
. . . . 5
β’ (π₯ = (π¦ + 1) β ((πβ0)[,)(πβπ₯)) = ((πβ0)[,)(πβ(π¦ + 1)))) |
22 | 21 | eleq2d 2818 |
. . . 4
β’ (π₯ = (π¦ + 1) β (π β ((πβ0)[,)(πβπ₯)) β π β ((πβ0)[,)(πβ(π¦ + 1))))) |
23 | | oveq2 7420 |
. . . . 5
β’ (π₯ = (π¦ + 1) β (0..^π₯) = (0..^(π¦ + 1))) |
24 | 23 | rexeqdv 3325 |
. . . 4
β’ (π₯ = (π¦ + 1) β (βπ β (0..^π₯)π β ((πβπ)[,)(πβ(π + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))) |
25 | 22, 24 | imbi12d 343 |
. . 3
β’ (π₯ = (π¦ + 1) β ((π β ((πβ0)[,)(πβπ₯)) β βπ β (0..^π₯)π β ((πβπ)[,)(πβ(π + 1)))) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1)))))) |
26 | 19, 25 | raleqbidv 3341 |
. 2
β’ (π₯ = (π¦ + 1) β (βπ β (RePartβπ₯)(π β ((πβ0)[,)(πβπ₯)) β βπ β (0..^π₯)π β ((πβπ)[,)(πβ(π + 1)))) β βπ β (RePartβ(π¦ + 1))(π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1)))))) |
27 | | fveq2 6892 |
. . 3
β’ (π₯ = π β (RePartβπ₯) = (RePartβπ)) |
28 | | fveq2 6892 |
. . . . . 6
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
29 | 28 | oveq2d 7428 |
. . . . 5
β’ (π₯ = π β ((πβ0)[,)(πβπ₯)) = ((πβ0)[,)(πβπ))) |
30 | 29 | eleq2d 2818 |
. . . 4
β’ (π₯ = π β (π β ((πβ0)[,)(πβπ₯)) β π β ((πβ0)[,)(πβπ)))) |
31 | | oveq2 7420 |
. . . . 5
β’ (π₯ = π β (0..^π₯) = (0..^π)) |
32 | 31 | rexeqdv 3325 |
. . . 4
β’ (π₯ = π β (βπ β (0..^π₯)π β ((πβπ)[,)(πβ(π + 1))) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) |
33 | 30, 32 | imbi12d 343 |
. . 3
β’ (π₯ = π β ((π β ((πβ0)[,)(πβπ₯)) β βπ β (0..^π₯)π β ((πβπ)[,)(πβ(π + 1)))) β (π β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1)))))) |
34 | 27, 33 | raleqbidv 3341 |
. 2
β’ (π₯ = π β (βπ β (RePartβπ₯)(π β ((πβ0)[,)(πβπ₯)) β βπ β (0..^π₯)π β ((πβπ)[,)(πβ(π + 1)))) β βπ β (RePartβπ)(π β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1)))))) |
35 | | 0nn0 12492 |
. . . . 5
β’ 0 β
β0 |
36 | | fveq2 6892 |
. . . . . . . 8
β’ (π = 0 β (πβπ) = (πβ0)) |
37 | | fv0p1e1 12340 |
. . . . . . . 8
β’ (π = 0 β (πβ(π + 1)) = (πβ1)) |
38 | 36, 37 | oveq12d 7430 |
. . . . . . 7
β’ (π = 0 β ((πβπ)[,)(πβ(π + 1))) = ((πβ0)[,)(πβ1))) |
39 | 38 | eleq2d 2818 |
. . . . . 6
β’ (π = 0 β (π β ((πβπ)[,)(πβ(π + 1))) β π β ((πβ0)[,)(πβ1)))) |
40 | 39 | rexsng 4679 |
. . . . 5
β’ (0 β
β0 β (βπ β {0}π β ((πβπ)[,)(πβ(π + 1))) β π β ((πβ0)[,)(πβ1)))) |
41 | 35, 40 | ax-mp 5 |
. . . 4
β’
(βπ β
{0}π β ((πβπ)[,)(πβ(π + 1))) β π β ((πβ0)[,)(πβ1))) |
42 | 41 | biimpri 227 |
. . 3
β’ (π β ((πβ0)[,)(πβ1)) β βπ β {0}π β ((πβπ)[,)(πβ(π + 1)))) |
43 | 42 | rgenw 3064 |
. 2
β’
βπ β
(RePartβ1)(π β
((πβ0)[,)(πβ1)) β βπ β {0}π β ((πβπ)[,)(πβ(π + 1)))) |
44 | | nfv 1916 |
. . . . 5
β’
β²π π¦ β β |
45 | | nfra1 3280 |
. . . . 5
β’
β²πβπ β (RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))) |
46 | 44, 45 | nfan 1901 |
. . . 4
β’
β²π(π¦ β β β§
βπ β
(RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))))) |
47 | | nnnn0 12484 |
. . . . . . . . . 10
β’ (π¦ β β β π¦ β
β0) |
48 | | fzonn0p1 13714 |
. . . . . . . . . 10
β’ (π¦ β β0
β π¦ β (0..^(π¦ + 1))) |
49 | 47, 48 | syl 17 |
. . . . . . . . 9
β’ (π¦ β β β π¦ β (0..^(π¦ + 1))) |
50 | 49 | ad2antrr 723 |
. . . . . . . 8
β’ (((π¦ β β β§ (πβπ¦) β€ π) β§ (π β (RePartβ(π¦ + 1)) β§ π β ((πβ0)[,)(πβ(π¦ + 1))))) β π¦ β (0..^(π¦ + 1))) |
51 | | fveq2 6892 |
. . . . . . . . . . 11
β’ (π = π¦ β (πβπ) = (πβπ¦)) |
52 | | fvoveq1 7435 |
. . . . . . . . . . 11
β’ (π = π¦ β (πβ(π + 1)) = (πβ(π¦ + 1))) |
53 | 51, 52 | oveq12d 7430 |
. . . . . . . . . 10
β’ (π = π¦ β ((πβπ)[,)(πβ(π + 1))) = ((πβπ¦)[,)(πβ(π¦ + 1)))) |
54 | 53 | eleq2d 2818 |
. . . . . . . . 9
β’ (π = π¦ β (π β ((πβπ)[,)(πβ(π + 1))) β π β ((πβπ¦)[,)(πβ(π¦ + 1))))) |
55 | 54 | adantl 481 |
. . . . . . . 8
β’ ((((π¦ β β β§ (πβπ¦) β€ π) β§ (π β (RePartβ(π¦ + 1)) β§ π β ((πβ0)[,)(πβ(π¦ + 1))))) β§ π = π¦) β (π β ((πβπ)[,)(πβ(π + 1))) β π β ((πβπ¦)[,)(πβ(π¦ + 1))))) |
56 | | peano2nn 12229 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β (π¦ + 1) β
β) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (π¦ + 1) β
β) |
58 | | simpr 484 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β π β (RePartβ(π¦ + 1))) |
59 | 56 | nnnn0d 12537 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β β β (π¦ + 1) β
β0) |
60 | | 0elfz 13603 |
. . . . . . . . . . . . . . . . 17
β’ ((π¦ + 1) β β0
β 0 β (0...(π¦ +
1))) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β 0 β
(0...(π¦ +
1))) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β 0 β
(0...(π¦ +
1))) |
63 | 57, 58, 62 | iccpartxr 46387 |
. . . . . . . . . . . . . 14
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (πβ0) β
β*) |
64 | | nn0fz0 13604 |
. . . . . . . . . . . . . . . . 17
β’ ((π¦ + 1) β β0
β (π¦ + 1) β
(0...(π¦ +
1))) |
65 | 59, 64 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β (π¦ + 1) β (0...(π¦ + 1))) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (π¦ + 1) β (0...(π¦ + 1))) |
67 | 57, 58, 66 | iccpartxr 46387 |
. . . . . . . . . . . . . 14
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (πβ(π¦ + 1)) β
β*) |
68 | 63, 67 | jca 511 |
. . . . . . . . . . . . 13
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β ((πβ0) β
β* β§ (πβ(π¦ + 1)) β
β*)) |
69 | 68 | adantlr 712 |
. . . . . . . . . . . 12
β’ (((π¦ β β β§ (πβπ¦) β€ π) β§ π β (RePartβ(π¦ + 1))) β ((πβ0) β β* β§
(πβ(π¦ + 1)) β
β*)) |
70 | | elico1 13372 |
. . . . . . . . . . . 12
β’ (((πβ0) β
β* β§ (πβ(π¦ + 1)) β β*) β
(π β ((πβ0)[,)(πβ(π¦ + 1))) β (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1))))) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . 11
β’ (((π¦ β β β§ (πβπ¦) β€ π) β§ π β (RePartβ(π¦ + 1))) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1))))) |
72 | | simp1 1135 |
. . . . . . . . . . . . . . . 16
β’ ((π β β*
β§ (πβ0) β€
π β§ π < (πβ(π¦ + 1))) β π β
β*) |
73 | 72 | adantl 481 |
. . . . . . . . . . . . . . 15
β’ (((πβπ¦) β€ π β§ (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1)))) β π β
β*) |
74 | | simpl 482 |
. . . . . . . . . . . . . . 15
β’ (((πβπ¦) β€ π β§ (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1)))) β (πβπ¦) β€ π) |
75 | | simpr3 1195 |
. . . . . . . . . . . . . . 15
β’ (((πβπ¦) β€ π β§ (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1)))) β π < (πβ(π¦ + 1))) |
76 | 73, 74, 75 | 3jca 1127 |
. . . . . . . . . . . . . 14
β’ (((πβπ¦) β€ π β§ (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1)))) β (π β β* β§ (πβπ¦) β€ π β§ π < (πβ(π¦ + 1)))) |
77 | 76 | ex 412 |
. . . . . . . . . . . . 13
β’ ((πβπ¦) β€ π β ((π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1))) β (π β β* β§ (πβπ¦) β€ π β§ π < (πβ(π¦ + 1))))) |
78 | 77 | adantl 481 |
. . . . . . . . . . . 12
β’ ((π¦ β β β§ (πβπ¦) β€ π) β ((π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1))) β (π β β* β§ (πβπ¦) β€ π β§ π < (πβ(π¦ + 1))))) |
79 | 78 | adantr 480 |
. . . . . . . . . . 11
β’ (((π¦ β β β§ (πβπ¦) β€ π) β§ π β (RePartβ(π¦ + 1))) β ((π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1))) β (π β β* β§ (πβπ¦) β€ π β§ π < (πβ(π¦ + 1))))) |
80 | 71, 79 | sylbid 239 |
. . . . . . . . . 10
β’ (((π¦ β β β§ (πβπ¦) β€ π) β§ π β (RePartβ(π¦ + 1))) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β (π β β* β§ (πβπ¦) β€ π β§ π < (πβ(π¦ + 1))))) |
81 | 80 | impr 454 |
. . . . . . . . 9
β’ (((π¦ β β β§ (πβπ¦) β€ π) β§ (π β (RePartβ(π¦ + 1)) β§ π β ((πβ0)[,)(πβ(π¦ + 1))))) β (π β β* β§ (πβπ¦) β€ π β§ π < (πβ(π¦ + 1)))) |
82 | | nn0fz0 13604 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β0
β π¦ β (0...π¦)) |
83 | 47, 82 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β π¦ β (0...π¦)) |
84 | | fzelp1 13558 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (0...π¦) β π¦ β (0...(π¦ + 1))) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β π¦ β (0...(π¦ + 1))) |
86 | 85 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β π¦ β (0...(π¦ + 1))) |
87 | 57, 58, 86 | iccpartxr 46387 |
. . . . . . . . . . . 12
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (πβπ¦) β
β*) |
88 | 87, 67 | jca 511 |
. . . . . . . . . . 11
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β ((πβπ¦) β β* β§ (πβ(π¦ + 1)) β
β*)) |
89 | 88 | ad2ant2r 744 |
. . . . . . . . . 10
β’ (((π¦ β β β§ (πβπ¦) β€ π) β§ (π β (RePartβ(π¦ + 1)) β§ π β ((πβ0)[,)(πβ(π¦ + 1))))) β ((πβπ¦) β β* β§ (πβ(π¦ + 1)) β
β*)) |
90 | | elico1 13372 |
. . . . . . . . . 10
β’ (((πβπ¦) β β* β§ (πβ(π¦ + 1)) β β*) β
(π β ((πβπ¦)[,)(πβ(π¦ + 1))) β (π β β* β§ (πβπ¦) β€ π β§ π < (πβ(π¦ + 1))))) |
91 | 89, 90 | syl 17 |
. . . . . . . . 9
β’ (((π¦ β β β§ (πβπ¦) β€ π) β§ (π β (RePartβ(π¦ + 1)) β§ π β ((πβ0)[,)(πβ(π¦ + 1))))) β (π β ((πβπ¦)[,)(πβ(π¦ + 1))) β (π β β* β§ (πβπ¦) β€ π β§ π < (πβ(π¦ + 1))))) |
92 | 81, 91 | mpbird 256 |
. . . . . . . 8
β’ (((π¦ β β β§ (πβπ¦) β€ π) β§ (π β (RePartβ(π¦ + 1)) β§ π β ((πβ0)[,)(πβ(π¦ + 1))))) β π β ((πβπ¦)[,)(πβ(π¦ + 1)))) |
93 | 50, 55, 92 | rspcedvd 3615 |
. . . . . . 7
β’ (((π¦ β β β§ (πβπ¦) β€ π) β§ (π β (RePartβ(π¦ + 1)) β§ π β ((πβ0)[,)(πβ(π¦ + 1))))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1)))) |
94 | 93 | exp43 436 |
. . . . . 6
β’ (π¦ β β β ((πβπ¦) β€ π β (π β (RePartβ(π¦ + 1)) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))))) |
95 | 94 | adantr 480 |
. . . . 5
β’ ((π¦ β β β§
βπ β
(RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))))) β ((πβπ¦) β€ π β (π β (RePartβ(π¦ + 1)) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))))) |
96 | | iccpartres 46386 |
. . . . . . . . 9
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (π βΎ (0...π¦)) β (RePartβπ¦)) |
97 | | rspsbca 3875 |
. . . . . . . . . . . 12
β’ (((π βΎ (0...π¦)) β (RePartβπ¦) β§ βπ β (RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))))) β [(π βΎ (0...π¦)) / π](π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))))) |
98 | | vex 3477 |
. . . . . . . . . . . . . . 15
β’ π β V |
99 | 98 | resex 6030 |
. . . . . . . . . . . . . 14
β’ (π βΎ (0...π¦)) β V |
100 | | sbcimg 3829 |
. . . . . . . . . . . . . . 15
β’ ((π βΎ (0...π¦)) β V β ([(π βΎ (0...π¦)) / π](π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))) β ([(π βΎ (0...π¦)) / π]π β ((πβ0)[,)(πβπ¦)) β [(π βΎ (0...π¦)) / π]βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))))) |
101 | | sbcel2 4416 |
. . . . . . . . . . . . . . . . 17
β’
([(π βΎ
(0...π¦)) / π]π β ((πβ0)[,)(πβπ¦)) β π β β¦(π βΎ (0...π¦)) / πβ¦((πβ0)[,)(πβπ¦))) |
102 | | csbov12g 7456 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦((πβ0)[,)(πβπ¦)) = (β¦(π βΎ (0...π¦)) / πβ¦(πβ0)[,)β¦(π βΎ (0...π¦)) / πβ¦(πβπ¦))) |
103 | | csbfv12 6940 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β¦(π
βΎ (0...π¦)) / πβ¦(πβ0) =
(β¦(π βΎ
(0...π¦)) / πβ¦πββ¦(π βΎ (0...π¦)) / πβ¦0) |
104 | | csbvarg 4432 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦π = (π βΎ (0...π¦))) |
105 | | csbconstg 3913 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦0 = 0) |
106 | 104, 105 | fveq12d 6899 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π βΎ (0...π¦)) β V β (β¦(π βΎ (0...π¦)) / πβ¦πββ¦(π βΎ (0...π¦)) / πβ¦0) = ((π βΎ (0...π¦))β0)) |
107 | 103, 106 | eqtrid 2783 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦(πβ0) = ((π βΎ (0...π¦))β0)) |
108 | | csbfv12 6940 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β¦(π
βΎ (0...π¦)) / πβ¦(πβπ¦) = (β¦(π βΎ (0...π¦)) / πβ¦πββ¦(π βΎ (0...π¦)) / πβ¦π¦) |
109 | | csbconstg 3913 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦π¦ = π¦) |
110 | 104, 109 | fveq12d 6899 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π βΎ (0...π¦)) β V β (β¦(π βΎ (0...π¦)) / πβ¦πββ¦(π βΎ (0...π¦)) / πβ¦π¦) = ((π βΎ (0...π¦))βπ¦)) |
111 | 108, 110 | eqtrid 2783 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦(πβπ¦) = ((π βΎ (0...π¦))βπ¦)) |
112 | 107, 111 | oveq12d 7430 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π βΎ (0...π¦)) β V β (β¦(π βΎ (0...π¦)) / πβ¦(πβ0)[,)β¦(π βΎ (0...π¦)) / πβ¦(πβπ¦)) = (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦))) |
113 | 102, 112 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . 18
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦((πβ0)[,)(πβπ¦)) = (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦))) |
114 | 113 | eleq2d 2818 |
. . . . . . . . . . . . . . . . 17
β’ ((π βΎ (0...π¦)) β V β (π β β¦(π βΎ (0...π¦)) / πβ¦((πβ0)[,)(πβπ¦)) β π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)))) |
115 | 101, 114 | bitrid 282 |
. . . . . . . . . . . . . . . 16
β’ ((π βΎ (0...π¦)) β V β ([(π βΎ (0...π¦)) / π]π β ((πβ0)[,)(πβπ¦)) β π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)))) |
116 | | sbcrex 3870 |
. . . . . . . . . . . . . . . . 17
β’
([(π βΎ
(0...π¦)) / π]βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))) β βπ β (0..^π¦)[(π βΎ (0...π¦)) / π]π β ((πβπ)[,)(πβ(π + 1)))) |
117 | | sbcel2 4416 |
. . . . . . . . . . . . . . . . . . 19
β’
([(π βΎ
(0...π¦)) / π]π β ((πβπ)[,)(πβ(π + 1))) β π β β¦(π βΎ (0...π¦)) / πβ¦((πβπ)[,)(πβ(π + 1)))) |
118 | | csbov12g 7456 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦((πβπ)[,)(πβ(π + 1))) = (β¦(π βΎ (0...π¦)) / πβ¦(πβπ)[,)β¦(π βΎ (0...π¦)) / πβ¦(πβ(π + 1)))) |
119 | | csbfv12 6940 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β¦(π
βΎ (0...π¦)) / πβ¦(πβπ) = (β¦(π βΎ (0...π¦)) / πβ¦πββ¦(π βΎ (0...π¦)) / πβ¦π) |
120 | | csbconstg 3913 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦π = π) |
121 | 104, 120 | fveq12d 6899 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π βΎ (0...π¦)) β V β (β¦(π βΎ (0...π¦)) / πβ¦πββ¦(π βΎ (0...π¦)) / πβ¦π) = ((π βΎ (0...π¦))βπ)) |
122 | 119, 121 | eqtrid 2783 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦(πβπ) = ((π βΎ (0...π¦))βπ)) |
123 | | csbfv12 6940 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β¦(π
βΎ (0...π¦)) / πβ¦(πβ(π + 1)) = (β¦(π βΎ (0...π¦)) / πβ¦πββ¦(π βΎ (0...π¦)) / πβ¦(π + 1)) |
124 | | csbconstg 3913 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦(π + 1) = (π + 1)) |
125 | 104, 124 | fveq12d 6899 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π βΎ (0...π¦)) β V β (β¦(π βΎ (0...π¦)) / πβ¦πββ¦(π βΎ (0...π¦)) / πβ¦(π + 1)) = ((π βΎ (0...π¦))β(π + 1))) |
126 | 123, 125 | eqtrid 2783 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦(πβ(π + 1)) = ((π βΎ (0...π¦))β(π + 1))) |
127 | 122, 126 | oveq12d 7430 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π βΎ (0...π¦)) β V β (β¦(π βΎ (0...π¦)) / πβ¦(πβπ)[,)β¦(π βΎ (0...π¦)) / πβ¦(πβ(π + 1))) = (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1)))) |
128 | 118, 127 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π βΎ (0...π¦)) β V β β¦(π βΎ (0...π¦)) / πβ¦((πβπ)[,)(πβ(π + 1))) = (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1)))) |
129 | 128 | eleq2d 2818 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π βΎ (0...π¦)) β V β (π β β¦(π βΎ (0...π¦)) / πβ¦((πβπ)[,)(πβ(π + 1))) β π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1))))) |
130 | 117, 129 | bitrid 282 |
. . . . . . . . . . . . . . . . . 18
β’ ((π βΎ (0...π¦)) β V β ([(π βΎ (0...π¦)) / π]π β ((πβπ)[,)(πβ(π + 1))) β π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1))))) |
131 | 130 | rexbidv 3177 |
. . . . . . . . . . . . . . . . 17
β’ ((π βΎ (0...π¦)) β V β (βπ β (0..^π¦)[(π βΎ (0...π¦)) / π]π β ((πβπ)[,)(πβ(π + 1))) β βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1))))) |
132 | 116, 131 | bitrid 282 |
. . . . . . . . . . . . . . . 16
β’ ((π βΎ (0...π¦)) β V β ([(π βΎ (0...π¦)) / π]βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))) β βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1))))) |
133 | 115, 132 | imbi12d 343 |
. . . . . . . . . . . . . . 15
β’ ((π βΎ (0...π¦)) β V β (([(π βΎ (0...π¦)) / π]π β ((πβ0)[,)(πβπ¦)) β [(π βΎ (0...π¦)) / π]βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))) β (π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)) β βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1)))))) |
134 | 100, 133 | bitrd 278 |
. . . . . . . . . . . . . 14
β’ ((π βΎ (0...π¦)) β V β ([(π βΎ (0...π¦)) / π](π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))) β (π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)) β βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1)))))) |
135 | 99, 134 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
([(π βΎ
(0...π¦)) / π](π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))) β (π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)) β βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1))))) |
136 | 68, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1))))) |
137 | 136 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ Β¬ (πβπ¦) β€ π) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1))))) |
138 | 72 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ Β¬ (πβπ¦) β€ π) β§ (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1)))) β π β
β*) |
139 | | simpr2 1194 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ Β¬ (πβπ¦) β€ π) β§ (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1)))) β (πβ0) β€ π) |
140 | | xrltnle 11286 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β*
β§ (πβπ¦) β β*)
β (π < (πβπ¦) β Β¬ (πβπ¦) β€ π)) |
141 | 72, 87, 140 | syl2anr 596 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1)))) β (π < (πβπ¦) β Β¬ (πβπ¦) β€ π)) |
142 | 141 | exbiri 808 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β ((π β β*
β§ (πβ0) β€
π β§ π < (πβ(π¦ + 1))) β (Β¬ (πβπ¦) β€ π β π < (πβπ¦)))) |
143 | 142 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (Β¬ (πβπ¦) β€ π β ((π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1))) β π < (πβπ¦)))) |
144 | 143 | imp31 417 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ Β¬ (πβπ¦) β€ π) β§ (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1)))) β π < (πβπ¦)) |
145 | 138, 139,
144 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ Β¬ (πβπ¦) β€ π) β§ (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1)))) β (π β β* β§ (πβ0) β€ π β§ π < (πβπ¦))) |
146 | 63, 87 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β ((πβ0) β
β* β§ (πβπ¦) β
β*)) |
147 | 146 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ Β¬ (πβπ¦) β€ π) β§ (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1)))) β ((πβ0) β β* β§
(πβπ¦) β
β*)) |
148 | | elico1 13372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πβ0) β
β* β§ (πβπ¦) β β*) β (π β ((πβ0)[,)(πβπ¦)) β (π β β* β§ (πβ0) β€ π β§ π < (πβπ¦)))) |
149 | 147, 148 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ Β¬ (πβπ¦) β€ π) β§ (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1)))) β (π β ((πβ0)[,)(πβπ¦)) β (π β β* β§ (πβ0) β€ π β§ π < (πβπ¦)))) |
150 | 145, 149 | mpbird 256 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ Β¬ (πβπ¦) β€ π) β§ (π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1)))) β π β ((πβ0)[,)(πβπ¦))) |
151 | 150 | ex 412 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ Β¬ (πβπ¦) β€ π) β ((π β β* β§ (πβ0) β€ π β§ π < (πβ(π¦ + 1))) β π β ((πβ0)[,)(πβπ¦)))) |
152 | 137, 151 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ Β¬ (πβπ¦) β€ π) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β π β ((πβ0)[,)(πβπ¦)))) |
153 | | 0elfz 13603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ β β0
β 0 β (0...π¦)) |
154 | 47, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β β β 0 β
(0...π¦)) |
155 | 154 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β 0 β
(0...π¦)) |
156 | | fvres 6911 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (0 β
(0...π¦) β ((π βΎ (0...π¦))β0) = (πβ0)) |
157 | 155, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β ((π βΎ (0...π¦))β0) = (πβ0)) |
158 | 157 | eqcomd 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (πβ0) = ((π βΎ (0...π¦))β0)) |
159 | 83 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β π¦ β (0...π¦)) |
160 | | fvres 6911 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ β (0...π¦) β ((π βΎ (0...π¦))βπ¦) = (πβπ¦)) |
161 | 159, 160 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β ((π βΎ (0...π¦))βπ¦) = (πβπ¦)) |
162 | 161 | eqcomd 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (πβπ¦) = ((π βΎ (0...π¦))βπ¦)) |
163 | 158, 162 | oveq12d 7430 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β ((πβ0)[,)(πβπ¦)) = (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦))) |
164 | 163 | eleq2d 2818 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (π β ((πβ0)[,)(πβπ¦)) β π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)))) |
165 | 164 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β ((πβ0)[,)(πβπ¦))) β π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦))) |
166 | | elfzofz 13653 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (0..^π¦) β π β (0...π¦)) |
167 | 166 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β ((πβ0)[,)(πβπ¦))) β§ π β (0..^π¦)) β π β (0...π¦)) |
168 | | fvres 6911 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0...π¦) β ((π βΎ (0...π¦))βπ) = (πβπ)) |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β ((πβ0)[,)(πβπ¦))) β§ π β (0..^π¦)) β ((π βΎ (0...π¦))βπ) = (πβπ)) |
170 | | fzofzp1 13734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (0..^π¦) β (π + 1) β (0...π¦)) |
171 | 170 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β (0..^π¦)) β (π + 1) β (0...π¦)) |
172 | | fvres 6911 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π + 1) β (0...π¦) β ((π βΎ (0...π¦))β(π + 1)) = (πβ(π + 1))) |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β (0..^π¦)) β ((π βΎ (0...π¦))β(π + 1)) = (πβ(π + 1))) |
174 | 173 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β ((πβ0)[,)(πβπ¦))) β§ π β (0..^π¦)) β ((π βΎ (0...π¦))β(π + 1)) = (πβ(π + 1))) |
175 | 169, 174 | oveq12d 7430 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β ((πβ0)[,)(πβπ¦))) β§ π β (0..^π¦)) β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1))) = ((πβπ)[,)(πβ(π + 1)))) |
176 | 175 | eleq2d 2818 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β ((πβ0)[,)(πβπ¦))) β§ π β (0..^π¦)) β (π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1))) β π β ((πβπ)[,)(πβ(π + 1))))) |
177 | 176 | rexbidva 3175 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β ((πβ0)[,)(πβπ¦))) β (βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1))) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))))) |
178 | | nnz 12584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ β β β π¦ β
β€) |
179 | | uzid 12842 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ β β€ β π¦ β
(β€β₯βπ¦)) |
180 | 178, 179 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ β β β π¦ β
(β€β₯βπ¦)) |
181 | | peano2uz 12890 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ β
(β€β₯βπ¦) β (π¦ + 1) β
(β€β₯βπ¦)) |
182 | | fzoss2 13665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π¦ + 1) β
(β€β₯βπ¦) β (0..^π¦) β (0..^(π¦ + 1))) |
183 | 180, 181,
182 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ β β β
(0..^π¦) β (0..^(π¦ + 1))) |
184 | 183 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β ((πβ0)[,)(πβπ¦))) β (0..^π¦) β (0..^(π¦ + 1))) |
185 | | ssrexv 4052 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((0..^π¦) β
(0..^(π¦ + 1)) β
(βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β ((πβ0)[,)(πβπ¦))) β (βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))) |
187 | 177, 186 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β ((πβ0)[,)(πβπ¦))) β (βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))) |
188 | 165, 187 | embantd 59 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ π β ((πβ0)[,)(πβπ¦))) β ((π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)) β βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1)))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))) |
189 | 188 | ex 412 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (π β ((πβ0)[,)(πβπ¦)) β ((π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)) β βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1)))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1)))))) |
190 | 189 | adantr 480 |
. . . . . . . . . . . . . . . . 17
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ Β¬ (πβπ¦) β€ π) β (π β ((πβ0)[,)(πβπ¦)) β ((π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)) β βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1)))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1)))))) |
191 | 152, 190 | syld 47 |
. . . . . . . . . . . . . . . 16
β’ (((π¦ β β β§ π β (RePartβ(π¦ + 1))) β§ Β¬ (πβπ¦) β€ π) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β ((π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)) β βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1)))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1)))))) |
192 | 191 | ex 412 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (Β¬ (πβπ¦) β€ π β (π β ((πβ0)[,)(πβ(π¦ + 1))) β ((π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)) β βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1)))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))))) |
193 | 192 | com34 91 |
. . . . . . . . . . . . . 14
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (Β¬ (πβπ¦) β€ π β ((π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)) β βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1)))) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))))) |
194 | 193 | com13 88 |
. . . . . . . . . . . . 13
β’ ((π β (((π βΎ (0...π¦))β0)[,)((π βΎ (0...π¦))βπ¦)) β βπ β (0..^π¦)π β (((π βΎ (0...π¦))βπ)[,)((π βΎ (0...π¦))β(π + 1)))) β (Β¬ (πβπ¦) β€ π β ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))))) |
195 | 135, 194 | sylbi 216 |
. . . . . . . . . . . 12
β’
([(π βΎ
(0...π¦)) / π](π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))) β (Β¬ (πβπ¦) β€ π β ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))))) |
196 | 97, 195 | syl 17 |
. . . . . . . . . . 11
β’ (((π βΎ (0...π¦)) β (RePartβπ¦) β§ βπ β (RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))))) β (Β¬ (πβπ¦) β€ π β ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))))) |
197 | 196 | ex 412 |
. . . . . . . . . 10
β’ ((π βΎ (0...π¦)) β (RePartβπ¦) β (βπ β (RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))) β (Β¬ (πβπ¦) β€ π β ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1)))))))) |
198 | 197 | com24 95 |
. . . . . . . . 9
β’ ((π βΎ (0...π¦)) β (RePartβπ¦) β ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (Β¬ (πβπ¦) β€ π β (βπ β (RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1)))))))) |
199 | 96, 198 | mpcom 38 |
. . . . . . . 8
β’ ((π¦ β β β§ π β (RePartβ(π¦ + 1))) β (Β¬ (πβπ¦) β€ π β (βπ β (RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))))) |
200 | 199 | ex 412 |
. . . . . . 7
β’ (π¦ β β β (π β (RePartβ(π¦ + 1)) β (Β¬ (πβπ¦) β€ π β (βπ β (RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1)))))))) |
201 | 200 | com24 95 |
. . . . . 6
β’ (π¦ β β β
(βπ β
(RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))) β (Β¬ (πβπ¦) β€ π β (π β (RePartβ(π¦ + 1)) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1)))))))) |
202 | 201 | imp 406 |
. . . . 5
β’ ((π¦ β β β§
βπ β
(RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))))) β (Β¬ (πβπ¦) β€ π β (π β (RePartβ(π¦ + 1)) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))))) |
203 | 95, 202 | pm2.61d 179 |
. . . 4
β’ ((π¦ β β β§
βπ β
(RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))))) β (π β (RePartβ(π¦ + 1)) β (π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1)))))) |
204 | 46, 203 | ralrimi 3253 |
. . 3
β’ ((π¦ β β β§
βπ β
(RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1))))) β βπ β (RePartβ(π¦ + 1))(π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1))))) |
205 | 204 | ex 412 |
. 2
β’ (π¦ β β β
(βπ β
(RePartβπ¦)(π β ((πβ0)[,)(πβπ¦)) β βπ β (0..^π¦)π β ((πβπ)[,)(πβ(π + 1)))) β βπ β (RePartβ(π¦ + 1))(π β ((πβ0)[,)(πβ(π¦ + 1))) β βπ β (0..^(π¦ + 1))π β ((πβπ)[,)(πβ(π + 1)))))) |
206 | 10, 18, 26, 34, 43, 205 | nnind 12235 |
1
β’ (π β β β
βπ β
(RePartβπ)(π β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) |