Step | Hyp | Ref
| Expression |
1 | | iccpartiun.p |
. . . 4
β’ (π β π β (RePartβπ)) |
2 | 1 | adantr 482 |
. . 3
β’ ((π β§ π β ((πβ0)[,)(πβπ))) β π β (RePartβπ)) |
3 | | iccpartiun.m |
. . . . 5
β’ (π β π β β) |
4 | | iccelpart 45715 |
. . . . 5
β’ (π β β β
βπ β
(RePartβπ)(π β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) |
5 | 3, 4 | syl 17 |
. . . 4
β’ (π β βπ β (RePartβπ)(π β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) |
6 | 5 | adantr 482 |
. . 3
β’ ((π β§ π β ((πβ0)[,)(πβπ))) β βπ β (RePartβπ)(π β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) |
7 | | fveq1 6845 |
. . . . . . . . 9
β’ (π = π β (πβ0) = (πβ0)) |
8 | | fveq1 6845 |
. . . . . . . . 9
β’ (π = π β (πβπ) = (πβπ)) |
9 | 7, 8 | oveq12d 7379 |
. . . . . . . 8
β’ (π = π β ((πβ0)[,)(πβπ)) = ((πβ0)[,)(πβπ))) |
10 | 9 | eleq2d 2820 |
. . . . . . 7
β’ (π = π β (π β ((πβ0)[,)(πβπ)) β π β ((πβ0)[,)(πβπ)))) |
11 | | fveq1 6845 |
. . . . . . . . . 10
β’ (π = π β (πβπ) = (πβπ)) |
12 | | fveq1 6845 |
. . . . . . . . . 10
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
13 | 11, 12 | oveq12d 7379 |
. . . . . . . . 9
β’ (π = π β ((πβπ)[,)(πβ(π + 1))) = ((πβπ)[,)(πβ(π + 1)))) |
14 | 13 | eleq2d 2820 |
. . . . . . . 8
β’ (π = π β (π β ((πβπ)[,)(πβ(π + 1))) β π β ((πβπ)[,)(πβ(π + 1))))) |
15 | 14 | rexbidv 3172 |
. . . . . . 7
β’ (π = π β (βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) |
16 | 10, 15 | imbi12d 345 |
. . . . . 6
β’ (π = π β ((π β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1)))) β (π β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1)))))) |
17 | 16 | rspcva 3581 |
. . . . 5
β’ ((π β (RePartβπ) β§ βπ β (RePartβπ)(π β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) β (π β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) |
18 | 17 | adantld 492 |
. . . 4
β’ ((π β (RePartβπ) β§ βπ β (RePartβπ)(π β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) β ((π β§ π β ((πβ0)[,)(πβπ))) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) |
19 | 18 | com12 32 |
. . 3
β’ ((π β§ π β ((πβ0)[,)(πβπ))) β ((π β (RePartβπ) β§ βπ β (RePartβπ)(π β ((πβ0)[,)(πβπ)) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))))) |
20 | 2, 6, 19 | mp2and 698 |
. 2
β’ ((π β§ π β ((πβ0)[,)(πβπ))) β βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1)))) |
21 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β β) |
22 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β (RePartβπ)) |
23 | | elfzofz 13597 |
. . . . . . . . . . 11
β’ (π β (0..^π) β π β (0...π)) |
24 | 23 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
25 | 21, 22, 24 | iccpartxr 45701 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πβπ) β
β*) |
26 | | fzofzp1 13678 |
. . . . . . . . . . 11
β’ (π β (0..^π) β (π + 1) β (0...π)) |
27 | 26 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
28 | 21, 22, 27 | iccpartxr 45701 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β
β*) |
29 | 25, 28 | jca 513 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β ((πβπ) β β* β§ (πβ(π + 1)) β
β*)) |
30 | 29 | adantrr 716 |
. . . . . . 7
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β ((πβπ) β β* β§ (πβ(π + 1)) β
β*)) |
31 | | elico1 13316 |
. . . . . . 7
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β*) β
(π β ((πβπ)[,)(πβ(π + 1))) β (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))))) |
32 | 30, 31 | syl 17 |
. . . . . 6
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β (π β ((πβπ)[,)(πβ(π + 1))) β (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))))) |
33 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β β) |
34 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β (RePartβπ)) |
35 | | elfzofz 13597 |
. . . . . . . . . . 11
β’ (π β (0..^π) β π β (0...π)) |
36 | 35 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
37 | 33, 34, 36 | iccpartxr 45701 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πβπ) β
β*) |
38 | | fzofzp1 13678 |
. . . . . . . . . . 11
β’ (π β (0..^π) β (π + 1) β (0...π)) |
39 | 38 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
40 | 33, 34, 39 | iccpartxr 45701 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β
β*) |
41 | 37, 40 | jca 513 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β ((πβπ) β β* β§ (πβ(π + 1)) β
β*)) |
42 | 41 | adantrl 715 |
. . . . . . 7
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β ((πβπ) β β* β§ (πβ(π + 1)) β
β*)) |
43 | | elico1 13316 |
. . . . . . 7
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β*) β
(π β ((πβπ)[,)(πβ(π + 1))) β (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))))) |
44 | 42, 43 | syl 17 |
. . . . . 6
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β (π β ((πβπ)[,)(πβ(π + 1))) β (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))))) |
45 | 32, 44 | anbi12d 632 |
. . . . 5
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β ((π β ((πβπ)[,)(πβ(π + 1))) β§ π β ((πβπ)[,)(πβ(π + 1)))) β ((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β§ (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1)))))) |
46 | | elfzoelz 13581 |
. . . . . . . . . 10
β’ (π β (0..^π) β π β β€) |
47 | 46 | zred 12615 |
. . . . . . . . 9
β’ (π β (0..^π) β π β β) |
48 | | elfzoelz 13581 |
. . . . . . . . . 10
β’ (π β (0..^π) β π β β€) |
49 | 48 | zred 12615 |
. . . . . . . . 9
β’ (π β (0..^π) β π β β) |
50 | 47, 49 | anim12i 614 |
. . . . . . . 8
β’ ((π β (0..^π) β§ π β (0..^π)) β (π β β β§ π β β)) |
51 | 50 | adantl 483 |
. . . . . . 7
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β (π β β β§ π β β)) |
52 | | lttri4 11247 |
. . . . . . 7
β’ ((π β β β§ π β β) β (π < π β¨ π = π β¨ π < π)) |
53 | 51, 52 | syl 17 |
. . . . . 6
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β (π < π β¨ π = π β¨ π < π)) |
54 | 3, 1 | icceuelpartlem 45717 |
. . . . . . . . . 10
β’ (π β ((π β (0..^π) β§ π β (0..^π)) β (π < π β (πβ(π + 1)) β€ (πβπ)))) |
55 | 54 | imp31 419 |
. . . . . . . . 9
β’ (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ π < π) β (πβ(π + 1)) β€ (πβπ)) |
56 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β*
β§ (π β§ (π β (0..^π) β§ π β (0..^π)))) β π β
β*) |
57 | 28 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β (πβ(π + 1)) β
β*) |
58 | 57 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β*
β§ (π β§ (π β (0..^π) β§ π β (0..^π)))) β (πβ(π + 1)) β
β*) |
59 | 37 | adantrl 715 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β (πβπ) β
β*) |
60 | 59 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β*
β§ (π β§ (π β (0..^π) β§ π β (0..^π)))) β (πβπ) β
β*) |
61 | | nltle2tri 45635 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β*
β§ (πβ(π + 1)) β
β* β§ (πβπ) β β*) β Β¬
(π < (πβ(π + 1)) β§ (πβ(π + 1)) β€ (πβπ) β§ (πβπ) β€ π)) |
62 | 56, 58, 60, 61 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β*
β§ (π β§ (π β (0..^π) β§ π β (0..^π)))) β Β¬ (π < (πβ(π + 1)) β§ (πβ(π + 1)) β€ (πβπ) β§ (πβπ) β€ π)) |
63 | 62 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β*
β§ (π β§ (π β (0..^π) β§ π β (0..^π)))) β ((π < (πβ(π + 1)) β§ (πβ(π + 1)) β€ (πβπ) β§ (πβπ) β€ π) β π = π)) |
64 | 63 | 3expd 1354 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β*
β§ (π β§ (π β (0..^π) β§ π β (0..^π)))) β (π < (πβ(π + 1)) β ((πβ(π + 1)) β€ (πβπ) β ((πβπ) β€ π β π = π)))) |
65 | 64 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β*
β ((π β§ (π β (0..^π) β§ π β (0..^π))) β (π < (πβ(π + 1)) β ((πβ(π + 1)) β€ (πβπ) β ((πβπ) β€ π β π = π))))) |
66 | 65 | com23 86 |
. . . . . . . . . . . . . . . . 17
β’ (π β β*
β (π < (πβ(π + 1)) β ((π β§ (π β (0..^π) β§ π β (0..^π))) β ((πβ(π + 1)) β€ (πβπ) β ((πβπ) β€ π β π = π))))) |
67 | 66 | com25 99 |
. . . . . . . . . . . . . . . 16
β’ (π β β*
β ((πβπ) β€ π β ((π β§ (π β (0..^π) β§ π β (0..^π))) β ((πβ(π + 1)) β€ (πβπ) β (π < (πβ(π + 1)) β π = π))))) |
68 | 67 | imp4b 423 |
. . . . . . . . . . . . . . 15
β’ ((π β β*
β§ (πβπ) β€ π) β (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β (π < (πβ(π + 1)) β π = π))) |
69 | 68 | com23 86 |
. . . . . . . . . . . . . 14
β’ ((π β β*
β§ (πβπ) β€ π) β (π < (πβ(π + 1)) β (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β π = π))) |
70 | 69 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((π β β*
β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β (π < (πβ(π + 1)) β (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β π = π))) |
71 | 70 | com12 32 |
. . . . . . . . . . . 12
β’ (π < (πβ(π + 1)) β ((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β π = π))) |
72 | 71 | 3ad2ant3 1136 |
. . . . . . . . . . 11
β’ ((π β β*
β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β ((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β π = π))) |
73 | 72 | imp 408 |
. . . . . . . . . 10
β’ (((π β β*
β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β§ (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1)))) β (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β π = π)) |
74 | 73 | com12 32 |
. . . . . . . . 9
β’ (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β (((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β§ (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1)))) β π = π)) |
75 | 55, 74 | syldan 592 |
. . . . . . . 8
β’ (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ π < π) β (((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β§ (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1)))) β π = π)) |
76 | 75 | expcom 415 |
. . . . . . 7
β’ (π < π β ((π β§ (π β (0..^π) β§ π β (0..^π))) β (((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β§ (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1)))) β π = π))) |
77 | | 2a1 28 |
. . . . . . 7
β’ (π = π β ((π β§ (π β (0..^π) β§ π β (0..^π))) β (((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β§ (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1)))) β π = π))) |
78 | 3, 1 | icceuelpartlem 45717 |
. . . . . . . . . . 11
β’ (π β ((π β (0..^π) β§ π β (0..^π)) β (π < π β (πβ(π + 1)) β€ (πβπ)))) |
79 | 78 | ancomsd 467 |
. . . . . . . . . 10
β’ (π β ((π β (0..^π) β§ π β (0..^π)) β (π < π β (πβ(π + 1)) β€ (πβπ)))) |
80 | 79 | imp31 419 |
. . . . . . . . 9
β’ (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ π < π) β (πβ(π + 1)) β€ (πβπ)) |
81 | 40 | adantrl 715 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β (πβ(π + 1)) β
β*) |
82 | 81 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β*
β§ (π β§ (π β (0..^π) β§ π β (0..^π)))) β (πβ(π + 1)) β
β*) |
83 | 25 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β (πβπ) β
β*) |
84 | 83 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β*
β§ (π β§ (π β (0..^π) β§ π β (0..^π)))) β (πβπ) β
β*) |
85 | | nltle2tri 45635 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β*
β§ (πβ(π + 1)) β
β* β§ (πβπ) β β*) β Β¬
(π < (πβ(π + 1)) β§ (πβ(π + 1)) β€ (πβπ) β§ (πβπ) β€ π)) |
86 | 56, 82, 84, 85 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β*
β§ (π β§ (π β (0..^π) β§ π β (0..^π)))) β Β¬ (π < (πβ(π + 1)) β§ (πβ(π + 1)) β€ (πβπ) β§ (πβπ) β€ π)) |
87 | 86 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β*
β§ (π β§ (π β (0..^π) β§ π β (0..^π)))) β ((π < (πβ(π + 1)) β§ (πβ(π + 1)) β€ (πβπ) β§ (πβπ) β€ π) β π = π)) |
88 | 87 | 3expd 1354 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β*
β§ (π β§ (π β (0..^π) β§ π β (0..^π)))) β (π < (πβ(π + 1)) β ((πβ(π + 1)) β€ (πβπ) β ((πβπ) β€ π β π = π)))) |
89 | 88 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (π β β*
β ((π β§ (π β (0..^π) β§ π β (0..^π))) β (π < (πβ(π + 1)) β ((πβ(π + 1)) β€ (πβπ) β ((πβπ) β€ π β π = π))))) |
90 | 89 | com23 86 |
. . . . . . . . . . . . . . . 16
β’ (π β β*
β (π < (πβ(π + 1)) β ((π β§ (π β (0..^π) β§ π β (0..^π))) β ((πβ(π + 1)) β€ (πβπ) β ((πβπ) β€ π β π = π))))) |
91 | 90 | imp4b 423 |
. . . . . . . . . . . . . . 15
β’ ((π β β*
β§ π < (πβ(π + 1))) β (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β ((πβπ) β€ π β π = π))) |
92 | 91 | com23 86 |
. . . . . . . . . . . . . 14
β’ ((π β β*
β§ π < (πβ(π + 1))) β ((πβπ) β€ π β (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β π = π))) |
93 | 92 | 3adant2 1132 |
. . . . . . . . . . . . 13
β’ ((π β β*
β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β ((πβπ) β€ π β (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β π = π))) |
94 | 93 | com12 32 |
. . . . . . . . . . . 12
β’ ((πβπ) β€ π β ((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β π = π))) |
95 | 94 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π β β*
β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β ((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β π = π))) |
96 | 95 | imp 408 |
. . . . . . . . . 10
β’ (((π β β*
β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β§ (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1)))) β (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β π = π)) |
97 | 96 | com12 32 |
. . . . . . . . 9
β’ (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ (πβ(π + 1)) β€ (πβπ)) β (((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β§ (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1)))) β π = π)) |
98 | 80, 97 | syldan 592 |
. . . . . . . 8
β’ (((π β§ (π β (0..^π) β§ π β (0..^π))) β§ π < π) β (((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β§ (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1)))) β π = π)) |
99 | 98 | expcom 415 |
. . . . . . 7
β’ (π < π β ((π β§ (π β (0..^π) β§ π β (0..^π))) β (((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β§ (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1)))) β π = π))) |
100 | 76, 77, 99 | 3jaoi 1428 |
. . . . . 6
β’ ((π < π β¨ π = π β¨ π < π) β ((π β§ (π β (0..^π) β§ π β (0..^π))) β (((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β§ (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1)))) β π = π))) |
101 | 53, 100 | mpcom 38 |
. . . . 5
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β (((π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1))) β§ (π β β* β§ (πβπ) β€ π β§ π < (πβ(π + 1)))) β π = π)) |
102 | 45, 101 | sylbid 239 |
. . . 4
β’ ((π β§ (π β (0..^π) β§ π β (0..^π))) β ((π β ((πβπ)[,)(πβ(π + 1))) β§ π β ((πβπ)[,)(πβ(π + 1)))) β π = π)) |
103 | 102 | ralrimivva 3194 |
. . 3
β’ (π β βπ β (0..^π)βπ β (0..^π)((π β ((πβπ)[,)(πβ(π + 1))) β§ π β ((πβπ)[,)(πβ(π + 1)))) β π = π)) |
104 | 103 | adantr 482 |
. 2
β’ ((π β§ π β ((πβ0)[,)(πβπ))) β βπ β (0..^π)βπ β (0..^π)((π β ((πβπ)[,)(πβ(π + 1))) β§ π β ((πβπ)[,)(πβ(π + 1)))) β π = π)) |
105 | | fveq2 6846 |
. . . . 5
β’ (π = π β (πβπ) = (πβπ)) |
106 | | fvoveq1 7384 |
. . . . 5
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
107 | 105, 106 | oveq12d 7379 |
. . . 4
β’ (π = π β ((πβπ)[,)(πβ(π + 1))) = ((πβπ)[,)(πβ(π + 1)))) |
108 | 107 | eleq2d 2820 |
. . 3
β’ (π = π β (π β ((πβπ)[,)(πβ(π + 1))) β π β ((πβπ)[,)(πβ(π + 1))))) |
109 | 108 | reu4 3693 |
. 2
β’
(β!π β
(0..^π)π β ((πβπ)[,)(πβ(π + 1))) β (βπ β (0..^π)π β ((πβπ)[,)(πβ(π + 1))) β§ βπ β (0..^π)βπ β (0..^π)((π β ((πβπ)[,)(πβ(π + 1))) β§ π β ((πβπ)[,)(πβ(π + 1)))) β π = π))) |
110 | 20, 104, 109 | sylanbrc 584 |
1
β’ ((π β§ π β ((πβ0)[,)(πβπ))) β β!π β (0..^π)π β ((πβπ)[,)(πβ(π + 1)))) |