Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β ((πΉβπΆ)βπ) = ((πΉβπΆ)βπ)) |
2 | 1 | breq1d 5120 |
. . . . . 6
β’ (π = π β (((πΉβπΆ)βπ) β€ 0 β ((πΉβπΆ)βπ) β€ 0)) |
3 | 2 | elrab 3650 |
. . . . 5
β’ (π β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) |
4 | 3 | anbi1i 625 |
. . . 4
β’ ((π β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π) β ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) |
5 | | simprlr 779 |
. . . . 5
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β ((πΉβπΆ)βπ) β€ 0) |
6 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β π β (1...π½)) |
7 | 6 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β π β (1...π½)) |
8 | | fzssuz 13489 |
. . . . . . . . . . . . . 14
β’
(1...π½) β
(β€β₯β1) |
9 | | uzssz 12791 |
. . . . . . . . . . . . . 14
β’
(β€β₯β1) β β€ |
10 | 8, 9 | sstri 3958 |
. . . . . . . . . . . . 13
β’
(1...π½) β
β€ |
11 | | zssre 12513 |
. . . . . . . . . . . . 13
β’ β€
β β |
12 | 10, 11 | sstri 3958 |
. . . . . . . . . . . 12
β’
(1...π½) β
β |
13 | 12 | sseli 3945 |
. . . . . . . . . . 11
β’ (π β (1...π½) β π β β) |
14 | 13 | ltp1d 12092 |
. . . . . . . . . 10
β’ (π β (1...π½) β π < (π + 1)) |
15 | | 1red 11163 |
. . . . . . . . . . . 12
β’ (π β (1...π½) β 1 β β) |
16 | 13, 15 | readdcld 11191 |
. . . . . . . . . . 11
β’ (π β (1...π½) β (π + 1) β β) |
17 | 13, 16 | ltnled 11309 |
. . . . . . . . . 10
β’ (π β (1...π½) β (π < (π + 1) β Β¬ (π + 1) β€ π)) |
18 | 14, 17 | mpbid 231 |
. . . . . . . . 9
β’ (π β (1...π½) β Β¬ (π + 1) β€ π) |
19 | 7, 18 | syl 17 |
. . . . . . . 8
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β Β¬ (π + 1) β€ π) |
20 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π) |
21 | | ballotlemfc0.4 |
. . . . . . . . . . . . . . . 16
β’ (π β 0 < ((πΉβπΆ)βπ½)) |
22 | 21 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π = π½) β 0 < ((πΉβπΆ)βπ½)) |
23 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π = π½) β π = π½) |
24 | 23 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π = π½) β ((πΉβπΆ)βπ) = ((πΉβπΆ)βπ½)) |
25 | 24 | breq2d 5122 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π = π½) β (0 < ((πΉβπΆ)βπ) β 0 < ((πΉβπΆ)βπ½))) |
26 | | ballotlemfp1.j |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π½ β β) |
27 | | elnnuz 12814 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π½ β β β π½ β
(β€β₯β1)) |
28 | 26, 27 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π½ β
(β€β₯β1)) |
29 | | eluzfz2 13456 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π½ β
(β€β₯β1) β π½ β (1...π½)) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π½ β (1...π½)) |
31 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π½ β (π β (1...π½) β π½ β (1...π½))) |
32 | 30, 31 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π = π½ β π β (1...π½))) |
33 | 32 | anc2li 557 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π = π½ β (π β§ π β (1...π½)))) |
34 | | 1eluzge0 12824 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 β
(β€β₯β0) |
35 | | fzss1 13487 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1 β
(β€β₯β0) β (1...π½) β (0...π½)) |
36 | 35 | sseld 3948 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1 β
(β€β₯β0) β (π β (1...π½) β π β (0...π½))) |
37 | 34, 36 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π½) β π β (0...π½)) |
38 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0...π½)) β 0 β β) |
39 | | ballotth.m |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π β β |
40 | | ballotth.n |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π β β |
41 | | ballotth.o |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} |
42 | | ballotth.p |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) |
43 | | ballotth.f |
. . . . . . . . . . . . . . . . . . . . . 22
β’ πΉ = (π β π β¦ (π β β€ β¦
((β―β((1...π)
β© π)) β
(β―β((1...π)
β π))))) |
44 | | ballotlemfp1.c |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΆ β π) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (0...π½)) β πΆ β π) |
46 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0...π½) β π β β€) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (0...π½)) β π β β€) |
48 | 39, 40, 41, 42, 43, 45, 47 | ballotlemfelz 33130 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (0...π½)) β ((πΉβπΆ)βπ) β β€) |
49 | 48 | zred 12614 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0...π½)) β ((πΉβπΆ)βπ) β β) |
50 | 38, 49 | ltnled 11309 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0...π½)) β (0 < ((πΉβπΆ)βπ) β Β¬ ((πΉβπΆ)βπ) β€ 0)) |
51 | 37, 50 | sylan2 594 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π½)) β (0 < ((πΉβπΆ)βπ) β Β¬ ((πΉβπΆ)βπ) β€ 0)) |
52 | 33, 51 | syl6 35 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π = π½ β (0 < ((πΉβπΆ)βπ) β Β¬ ((πΉβπΆ)βπ) β€ 0))) |
53 | 52 | imp 408 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π = π½) β (0 < ((πΉβπΆ)βπ) β Β¬ ((πΉβπΆ)βπ) β€ 0)) |
54 | 25, 53 | bitr3d 281 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π = π½) β (0 < ((πΉβπΆ)βπ½) β Β¬ ((πΉβπΆ)βπ) β€ 0)) |
55 | 22, 54 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β§ π = π½) β Β¬ ((πΉβπΆ)βπ) β€ 0) |
56 | 55 | ex 414 |
. . . . . . . . . . . . 13
β’ (π β (π = π½ β Β¬ ((πΉβπΆ)βπ) β€ 0)) |
57 | 56 | con2d 134 |
. . . . . . . . . . . 12
β’ (π β (((πΉβπΆ)βπ) β€ 0 β Β¬ π = π½)) |
58 | | nn1m1nn 12181 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π½ β β β (π½ = 1 β¨ (π½ β 1) β
β)) |
59 | 26, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π½ = 1 β¨ (π½ β 1) β
β)) |
60 | | ballotlemfc0.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β βπ β (1...π½)((πΉβπΆ)βπ) β€ 0) |
61 | 60 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π½ = 1) β βπ β (1...π½)((πΉβπΆ)βπ) β€ 0) |
62 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π½ = 1 β (π½...π½) = (1...π½)) |
63 | 62 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π½ = 1) β (π½...π½) = (1...π½)) |
64 | 26 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π½ β β€) |
65 | | fzsn 13490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π½ β β€ β (π½...π½) = {π½}) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π½...π½) = {π½}) |
67 | 66 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π½ = 1) β (π½...π½) = {π½}) |
68 | 63, 67 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π½ = 1) β (1...π½) = {π½}) |
69 | 68 | rexeqdv 3317 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π½ = 1) β (βπ β (1...π½)((πΉβπΆ)βπ) β€ 0 β βπ β {π½} ((πΉβπΆ)βπ) β€ 0)) |
70 | 61, 69 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π½ = 1) β βπ β {π½} ((πΉβπΆ)βπ) β€ 0) |
71 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π½ β ((πΉβπΆ)βπ) = ((πΉβπΆ)βπ½)) |
72 | 71 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π½ β (((πΉβπΆ)βπ) β€ 0 β ((πΉβπΆ)βπ½) β€ 0)) |
73 | 72 | rexsng 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π½ β β β
(βπ β {π½} ((πΉβπΆ)βπ) β€ 0 β ((πΉβπΆ)βπ½) β€ 0)) |
74 | 26, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (βπ β {π½} ((πΉβπΆ)βπ) β€ 0 β ((πΉβπΆ)βπ½) β€ 0)) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π½ = 1) β (βπ β {π½} ((πΉβπΆ)βπ) β€ 0 β ((πΉβπΆ)βπ½) β€ 0)) |
76 | 70, 75 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π½ = 1) β ((πΉβπΆ)βπ½) β€ 0) |
77 | 21 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π½ = 1) β 0 < ((πΉβπΆ)βπ½)) |
78 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β 0 β
β) |
79 | 39, 40, 41, 42, 43, 44, 64 | ballotlemfelz 33130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((πΉβπΆ)βπ½) β β€) |
80 | 79 | zred 12614 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((πΉβπΆ)βπ½) β β) |
81 | 78, 80 | ltnled 11309 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0 < ((πΉβπΆ)βπ½) β Β¬ ((πΉβπΆ)βπ½) β€ 0)) |
82 | 81 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π½ = 1) β (0 < ((πΉβπΆ)βπ½) β Β¬ ((πΉβπΆ)βπ½) β€ 0)) |
83 | 77, 82 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π½ = 1) β Β¬ ((πΉβπΆ)βπ½) β€ 0) |
84 | 76, 83 | pm2.65da 816 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β Β¬ π½ = 1) |
85 | | biortn 937 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (Β¬
π½ = 1 β ((π½ β 1) β β
β (Β¬ Β¬ π½ = 1
β¨ (π½ β 1) β
β))) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((π½ β 1) β β β (Β¬
Β¬ π½ = 1 β¨ (π½ β 1) β
β))) |
87 | | notnotb 315 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π½ = 1 β Β¬ Β¬ π½ = 1) |
88 | 87 | orbi1i 913 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π½ = 1 β¨ (π½ β 1) β β) β (Β¬
Β¬ π½ = 1 β¨ (π½ β 1) β
β)) |
89 | 86, 88 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π½ β 1) β β β (π½ = 1 β¨ (π½ β 1) β
β))) |
90 | 59, 89 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π½ β 1) β β) |
91 | | elnnuz 12814 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π½ β 1) β β
β (π½ β 1) β
(β€β₯β1)) |
92 | 90, 91 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π½ β 1) β
(β€β₯β1)) |
93 | | elfzp1 13498 |
. . . . . . . . . . . . . . . . . 18
β’ ((π½ β 1) β
(β€β₯β1) β (π β (1...((π½ β 1) + 1)) β (π β (1...(π½ β 1)) β¨ π = ((π½ β 1) + 1)))) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β (1...((π½ β 1) + 1)) β (π β (1...(π½ β 1)) β¨ π = ((π½ β 1) + 1)))) |
95 | 26 | nncnd 12176 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π½ β β) |
96 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β 1 β
β) |
97 | 95, 96 | npcand 11523 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π½ β 1) + 1) = π½) |
98 | 97 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...((π½ β 1) + 1)) = (1...π½)) |
99 | 98 | eleq2d 2824 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β (1...((π½ β 1) + 1)) β π β (1...π½))) |
100 | 97 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π = ((π½ β 1) + 1) β π = π½)) |
101 | 100 | orbi2d 915 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π β (1...(π½ β 1)) β¨ π = ((π½ β 1) + 1)) β (π β (1...(π½ β 1)) β¨ π = π½))) |
102 | 94, 99, 101 | 3bitr3d 309 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β (1...π½) β (π β (1...(π½ β 1)) β¨ π = π½))) |
103 | | orcom 869 |
. . . . . . . . . . . . . . . 16
β’ ((π β (1...(π½ β 1)) β¨ π = π½) β (π = π½ β¨ π β (1...(π½ β 1)))) |
104 | 102, 103 | bitrdi 287 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (1...π½) β (π = π½ β¨ π β (1...(π½ β 1))))) |
105 | 104 | biimpd 228 |
. . . . . . . . . . . . . 14
β’ (π β (π β (1...π½) β (π = π½ β¨ π β (1...(π½ β 1))))) |
106 | | pm5.6 1001 |
. . . . . . . . . . . . . 14
β’ (((π β (1...π½) β§ Β¬ π = π½) β π β (1...(π½ β 1))) β (π β (1...π½) β (π = π½ β¨ π β (1...(π½ β 1))))) |
107 | 105, 106 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (π β ((π β (1...π½) β§ Β¬ π = π½) β π β (1...(π½ β 1)))) |
108 | 90 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π½ β 1) β β€) |
109 | | 1z 12540 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β
β€ |
110 | 108, 109 | jctil 521 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1 β β€ β§
(π½ β 1) β
β€)) |
111 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...(π½ β 1)) β π β β€) |
112 | 111, 109 | jctir 522 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...(π½ β 1)) β (π β β€ β§ 1 β
β€)) |
113 | | fzaddel 13482 |
. . . . . . . . . . . . . . . . . 18
β’ (((1
β β€ β§ (π½
β 1) β β€) β§ (π β β€ β§ 1 β β€))
β (π β
(1...(π½ β 1)) β
(π + 1) β ((1 +
1)...((π½ β 1) +
1)))) |
114 | 110, 112,
113 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...(π½ β 1))) β (π β (1...(π½ β 1)) β (π + 1) β ((1 + 1)...((π½ β 1) + 1)))) |
115 | 114 | biimp3a 1470 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...(π½ β 1)) β§ π β (1...(π½ β 1))) β (π + 1) β ((1 + 1)...((π½ β 1) + 1))) |
116 | 115 | 3anidm23 1422 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...(π½ β 1))) β (π + 1) β ((1 + 1)...((π½ β 1) + 1))) |
117 | | 1p1e2 12285 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1 + 1) =
2 |
118 | 117 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1 + 1) =
2) |
119 | 118, 97 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((1 + 1)...((π½ β 1) + 1)) = (2...π½)) |
120 | 119 | eleq2d 2824 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π + 1) β ((1 + 1)...((π½ β 1) + 1)) β (π + 1) β (2...π½))) |
121 | | 2eluzge1 12826 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 β
(β€β₯β1) |
122 | | fzss1 13487 |
. . . . . . . . . . . . . . . . . . 19
β’ (2 β
(β€β₯β1) β (2...π½) β (1...π½)) |
123 | 121, 122 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’
(2...π½) β
(1...π½) |
124 | 123 | sseli 3945 |
. . . . . . . . . . . . . . . . 17
β’ ((π + 1) β (2...π½) β (π + 1) β (1...π½)) |
125 | 120, 124 | syl6bi 253 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π + 1) β ((1 + 1)...((π½ β 1) + 1)) β (π + 1) β (1...π½))) |
126 | 125 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...(π½ β 1))) β ((π + 1) β ((1 + 1)...((π½ β 1) + 1)) β (π + 1) β (1...π½))) |
127 | 116, 126 | mpd 15 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...(π½ β 1))) β (π + 1) β (1...π½)) |
128 | 127 | ex 414 |
. . . . . . . . . . . . 13
β’ (π β (π β (1...(π½ β 1)) β (π + 1) β (1...π½))) |
129 | 107, 128 | syld 47 |
. . . . . . . . . . . 12
β’ (π β ((π β (1...π½) β§ Β¬ π = π½) β (π + 1) β (1...π½))) |
130 | 57, 129 | sylan2d 606 |
. . . . . . . . . . 11
β’ (π β ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β (π + 1) β (1...π½))) |
131 | 130 | imp 408 |
. . . . . . . . . 10
β’ ((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β (π + 1) β (1...π½)) |
132 | 131 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β (π + 1) β (1...π½)) |
133 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β ((πΉβπΆ)βπ) = ((πΉβπΆ)β(π + 1))) |
134 | 133 | breq1d 5120 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β (((πΉβπΆ)βπ) β€ 0 β ((πΉβπΆ)β(π + 1)) β€ 0)) |
135 | 134 | elrab 3650 |
. . . . . . . . . . . 12
β’ ((π + 1) β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β ((π + 1) β (1...π½) β§ ((πΉβπΆ)β(π + 1)) β€ 0)) |
136 | | breq1 5113 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β (π β€ π β (π + 1) β€ π)) |
137 | 136 | rspccva 3583 |
. . . . . . . . . . . 12
β’
((βπ β
{π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π β§ (π + 1) β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}) β (π + 1) β€ π) |
138 | 135, 137 | sylan2br 596 |
. . . . . . . . . . 11
β’
((βπ β
{π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π β§ ((π + 1) β (1...π½) β§ ((πΉβπΆ)β(π + 1)) β€ 0)) β (π + 1) β€ π) |
139 | 138 | expr 458 |
. . . . . . . . . 10
β’
((βπ β
{π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π β§ (π + 1) β (1...π½)) β (((πΉβπΆ)β(π + 1)) β€ 0 β (π + 1) β€ π)) |
140 | 139 | con3d 152 |
. . . . . . . . 9
β’
((βπ β
{π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π β§ (π + 1) β (1...π½)) β (Β¬ (π + 1) β€ π β Β¬ ((πΉβπΆ)β(π + 1)) β€ 0)) |
141 | 20, 132, 140 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β (Β¬ (π + 1) β€ π β Β¬ ((πΉβπΆ)β(π + 1)) β€ 0)) |
142 | 19, 141 | mpd 15 |
. . . . . . 7
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β Β¬ ((πΉβπΆ)β(π + 1)) β€ 0) |
143 | | simplrr 777 |
. . . . . . . . . . 11
β’ (((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β§ Β¬ (π + 1) β πΆ) β βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π) |
144 | 132 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β§ Β¬ (π + 1) β πΆ) β (π + 1) β (1...π½)) |
145 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β π) |
146 | 131 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β (π + 1) β (1...π½)) |
147 | 35 | sseld 3948 |
. . . . . . . . . . . . . . 15
β’ (1 β
(β€β₯β0) β ((π + 1) β (1...π½) β (π + 1) β (0...π½))) |
148 | 34, 146, 147 | mpsyl 68 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β (π + 1) β (0...π½)) |
149 | 44 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π + 1) β (0...π½)) β πΆ β π) |
150 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . 17
β’ ((π + 1) β (0...π½) β (π + 1) β β€) |
151 | 150 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π + 1) β (0...π½)) β (π + 1) β β€) |
152 | 39, 40, 41, 42, 43, 149, 151 | ballotlemfelz 33130 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π + 1) β (0...π½)) β ((πΉβπΆ)β(π + 1)) β β€) |
153 | 152 | zred 12614 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π + 1) β (0...π½)) β ((πΉβπΆ)β(π + 1)) β β) |
154 | 145, 148,
153 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β ((πΉβπΆ)β(π + 1)) β β) |
155 | | 0red 11165 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β 0 β β) |
156 | | simplrr 777 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β ((πΉβπΆ)βπ) β€ 0) |
157 | 6 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β π β (1...π½)) |
158 | 157, 37 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β π β (0...π½)) |
159 | 130 | imdistani 570 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β (π β§ (π + 1) β (1...π½))) |
160 | 44 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π + 1) β (1...π½)) β πΆ β π) |
161 | | elfznn 13477 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π + 1) β (1...π½) β (π + 1) β β) |
162 | 161 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π + 1) β (1...π½)) β (π + 1) β β) |
163 | 39, 40, 41, 42, 43, 160, 162 | ballotlemfp1 33131 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π + 1) β (1...π½)) β ((Β¬ (π + 1) β πΆ β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)β((π + 1) β 1)) β 1)) β§ ((π + 1) β πΆ β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)β((π + 1) β 1)) + 1)))) |
164 | 163 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π + 1) β (1...π½)) β (Β¬ (π + 1) β πΆ β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)β((π + 1) β 1)) β
1))) |
165 | 164 | imp 408 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π + 1) β (1...π½)) β§ Β¬ (π + 1) β πΆ) β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)β((π + 1) β 1)) β
1)) |
166 | 159, 165 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)β((π + 1) β 1)) β
1)) |
167 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1...π½) β π β β€) |
168 | 167 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...π½) β π β β) |
169 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...π½) β 1 β β) |
170 | 168, 169 | pncand 11520 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π½) β ((π + 1) β 1) = π) |
171 | 170 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π½) β ((πΉβπΆ)β((π + 1) β 1)) = ((πΉβπΆ)βπ)) |
172 | 171 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π½) β (((πΉβπΆ)β((π + 1) β 1)) β 1) = (((πΉβπΆ)βπ) β 1)) |
173 | 172 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π½) β (((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)β((π + 1) β 1)) β 1) β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) β 1))) |
174 | 157, 173 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β (((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)β((π + 1) β 1)) β 1) β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) β 1))) |
175 | 166, 174 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) β 1)) |
176 | | 0z 12517 |
. . . . . . . . . . . . . . . . . 18
β’ 0 β
β€ |
177 | | zlem1lt 12562 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπΆ)βπ) β β€ β§ 0 β β€)
β (((πΉβπΆ)βπ) β€ 0 β (((πΉβπΆ)βπ) β 1) < 0)) |
178 | 48, 176, 177 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0...π½)) β (((πΉβπΆ)βπ) β€ 0 β (((πΉβπΆ)βπ) β 1) < 0)) |
179 | 178 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0...π½)) β§ ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) β 1)) β (((πΉβπΆ)βπ) β€ 0 β (((πΉβπΆ)βπ) β 1) < 0)) |
180 | | breq1 5113 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) β 1) β (((πΉβπΆ)β(π + 1)) < 0 β (((πΉβπΆ)βπ) β 1) < 0)) |
181 | 180 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0...π½)) β§ ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) β 1)) β (((πΉβπΆ)β(π + 1)) < 0 β (((πΉβπΆ)βπ) β 1) < 0)) |
182 | 179, 181 | bitr4d 282 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0...π½)) β§ ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) β 1)) β (((πΉβπΆ)βπ) β€ 0 β ((πΉβπΆ)β(π + 1)) < 0)) |
183 | 145, 158,
175, 182 | syl21anc 837 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β (((πΉβπΆ)βπ) β€ 0 β ((πΉβπΆ)β(π + 1)) < 0)) |
184 | 156, 183 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β ((πΉβπΆ)β(π + 1)) < 0) |
185 | 154, 155,
184 | ltled 11310 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ Β¬ (π + 1) β πΆ) β ((πΉβπΆ)β(π + 1)) β€ 0) |
186 | 185 | adantlrr 720 |
. . . . . . . . . . 11
β’ (((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β§ Β¬ (π + 1) β πΆ) β ((πΉβπΆ)β(π + 1)) β€ 0) |
187 | 143, 144,
186, 138 | syl12anc 836 |
. . . . . . . . . 10
β’ (((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β§ Β¬ (π + 1) β πΆ) β (π + 1) β€ π) |
188 | 19 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β§ Β¬ (π + 1) β πΆ) β Β¬ (π + 1) β€ π) |
189 | 187, 188 | condan 817 |
. . . . . . . . 9
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β (π + 1) β πΆ) |
190 | 163 | simprd 497 |
. . . . . . . . . . . . 13
β’ ((π β§ (π + 1) β (1...π½)) β ((π + 1) β πΆ β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)β((π + 1) β 1)) + 1))) |
191 | 190 | imp 408 |
. . . . . . . . . . . 12
β’ (((π β§ (π + 1) β (1...π½)) β§ (π + 1) β πΆ) β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)β((π + 1) β 1)) + 1)) |
192 | 159, 191 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ (π + 1) β πΆ) β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)β((π + 1) β 1)) + 1)) |
193 | 6 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ (π + 1) β πΆ) β π β (1...π½)) |
194 | 171 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (π β (1...π½) β (((πΉβπΆ)β((π + 1) β 1)) + 1) = (((πΉβπΆ)βπ) + 1)) |
195 | 194 | eqeq2d 2748 |
. . . . . . . . . . . 12
β’ (π β (1...π½) β (((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)β((π + 1) β 1)) + 1) β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) + 1))) |
196 | 193, 195 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ (π + 1) β πΆ) β (((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)β((π + 1) β 1)) + 1) β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) + 1))) |
197 | 192, 196 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β§ (π + 1) β πΆ) β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) + 1)) |
198 | 197 | adantlrr 720 |
. . . . . . . . 9
β’ (((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β§ (π + 1) β πΆ) β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) + 1)) |
199 | 189, 198 | mpdan 686 |
. . . . . . . 8
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β ((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) + 1)) |
200 | | breq1 5113 |
. . . . . . . . 9
β’ (((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) + 1) β (((πΉβπΆ)β(π + 1)) β€ 0 β (((πΉβπΆ)βπ) + 1) β€ 0)) |
201 | 200 | notbid 318 |
. . . . . . . 8
β’ (((πΉβπΆ)β(π + 1)) = (((πΉβπΆ)βπ) + 1) β (Β¬ ((πΉβπΆ)β(π + 1)) β€ 0 β Β¬ (((πΉβπΆ)βπ) + 1) β€ 0)) |
202 | 199, 201 | syl 17 |
. . . . . . 7
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β (Β¬ ((πΉβπΆ)β(π + 1)) β€ 0 β Β¬ (((πΉβπΆ)βπ) + 1) β€ 0)) |
203 | 142, 202 | mpbid 231 |
. . . . . 6
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β Β¬ (((πΉβπΆ)βπ) + 1) β€ 0) |
204 | 6, 37 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β π β (0...π½)) |
205 | 204, 48 | syldan 592 |
. . . . . . . 8
β’ ((π β§ (π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0)) β ((πΉβπΆ)βπ) β β€) |
206 | 205 | adantrr 716 |
. . . . . . 7
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β ((πΉβπΆ)βπ) β β€) |
207 | | zleltp1 12561 |
. . . . . . . . 9
β’ ((0
β β€ β§ ((πΉβπΆ)βπ) β β€) β (0 β€ ((πΉβπΆ)βπ) β 0 < (((πΉβπΆ)βπ) + 1))) |
208 | 176, 207 | mpan 689 |
. . . . . . . 8
β’ (((πΉβπΆ)βπ) β β€ β (0 β€ ((πΉβπΆ)βπ) β 0 < (((πΉβπΆ)βπ) + 1))) |
209 | | 0red 11165 |
. . . . . . . . 9
β’ (((πΉβπΆ)βπ) β β€ β 0 β
β) |
210 | | zre 12510 |
. . . . . . . . . 10
β’ (((πΉβπΆ)βπ) β β€ β ((πΉβπΆ)βπ) β β) |
211 | | 1red 11163 |
. . . . . . . . . 10
β’ (((πΉβπΆ)βπ) β β€ β 1 β
β) |
212 | 210, 211 | readdcld 11191 |
. . . . . . . . 9
β’ (((πΉβπΆ)βπ) β β€ β (((πΉβπΆ)βπ) + 1) β β) |
213 | 209, 212 | ltnled 11309 |
. . . . . . . 8
β’ (((πΉβπΆ)βπ) β β€ β (0 < (((πΉβπΆ)βπ) + 1) β Β¬ (((πΉβπΆ)βπ) + 1) β€ 0)) |
214 | 208, 213 | bitrd 279 |
. . . . . . 7
β’ (((πΉβπΆ)βπ) β β€ β (0 β€ ((πΉβπΆ)βπ) β Β¬ (((πΉβπΆ)βπ) + 1) β€ 0)) |
215 | 206, 214 | syl 17 |
. . . . . 6
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β (0 β€ ((πΉβπΆ)βπ) β Β¬ (((πΉβπΆ)βπ) + 1) β€ 0)) |
216 | 203, 215 | mpbird 257 |
. . . . 5
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β 0 β€ ((πΉβπΆ)βπ)) |
217 | 206 | zred 12614 |
. . . . . 6
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β ((πΉβπΆ)βπ) β β) |
218 | | 0red 11165 |
. . . . . 6
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β 0 β β) |
219 | 217, 218 | letri3d 11304 |
. . . . 5
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β (((πΉβπΆ)βπ) = 0 β (((πΉβπΆ)βπ) β€ 0 β§ 0 β€ ((πΉβπΆ)βπ)))) |
220 | 5, 216, 219 | mpbir2and 712 |
. . . 4
β’ ((π β§ ((π β (1...π½) β§ ((πΉβπΆ)βπ) β€ 0) β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β ((πΉβπΆ)βπ) = 0) |
221 | 4, 220 | sylan2b 595 |
. . 3
β’ ((π β§ (π β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β§ βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π)) β ((πΉβπΆ)βπ) = 0) |
222 | | ssrab2 4042 |
. . . . . 6
β’ {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β (1...π½) |
223 | 222, 12 | sstri 3958 |
. . . . 5
β’ {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β β |
224 | 223 | a1i 11 |
. . . 4
β’ (π β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β β) |
225 | | fzfi 13884 |
. . . . . 6
β’
(1...π½) β
Fin |
226 | | ssfi 9124 |
. . . . . 6
β’
(((1...π½) β Fin
β§ {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β (1...π½)) β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β Fin) |
227 | 225, 222,
226 | mp2an 691 |
. . . . 5
β’ {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β Fin |
228 | 227 | a1i 11 |
. . . 4
β’ (π β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β Fin) |
229 | | rabn0 4350 |
. . . . 5
β’ ({π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β β
β βπ β (1...π½)((πΉβπΆ)βπ) β€ 0) |
230 | 60, 229 | sylibr 233 |
. . . 4
β’ (π β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β β
) |
231 | | fimaxre 12106 |
. . . 4
β’ (({π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β β β§ {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β Fin β§ {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β β
) β βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π) |
232 | 224, 228,
230, 231 | syl3anc 1372 |
. . 3
β’ (π β βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0}π β€ π) |
233 | 221, 232 | reximddv 3169 |
. 2
β’ (π β βπ β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} ((πΉβπΆ)βπ) = 0) |
234 | | elrabi 3644 |
. . . 4
β’ (π β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β π β (1...π½)) |
235 | 234 | anim1i 616 |
. . 3
β’ ((π β {π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} β§ ((πΉβπΆ)βπ) = 0) β (π β (1...π½) β§ ((πΉβπΆ)βπ) = 0)) |
236 | 235 | reximi2 3083 |
. 2
β’
(βπ β
{π β (1...π½) β£ ((πΉβπΆ)βπ) β€ 0} ((πΉβπΆ)βπ) = 0 β βπ β (1...π½)((πΉβπΆ)βπ) = 0) |
237 | 233, 236 | syl 17 |
1
β’ (π β βπ β (1...π½)((πΉβπΆ)βπ) = 0) |