Step | Hyp | Ref
| Expression |
1 | | vdwnn.1 |
. . 3
β’ (π β π
β Fin) |
2 | | vdwnn.3 |
. . . . . . 7
β’ π = {π β β β£ Β¬ βπ β β βπ β β βπ β (0...(π β 1))(π + (π Β· π)) β (β‘πΉ β {π})} |
3 | 2 | ssrab3 4075 |
. . . . . 6
β’ π β
β |
4 | | nnuz 12869 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
5 | 3, 4 | sseqtri 4013 |
. . . . . . 7
β’ π β
(β€β₯β1) |
6 | | vdwnn.4 |
. . . . . . . 8
β’ (π β βπ β π
π β β
) |
7 | 6 | r19.21bi 3242 |
. . . . . . 7
β’ ((π β§ π β π
) β π β β
) |
8 | | infssuzcl 12920 |
. . . . . . 7
β’ ((π β
(β€β₯β1) β§ π β β
) β inf(π, β, < ) β π) |
9 | 5, 7, 8 | sylancr 586 |
. . . . . 6
β’ ((π β§ π β π
) β inf(π, β, < ) β π) |
10 | 3, 9 | sselid 3975 |
. . . . 5
β’ ((π β§ π β π
) β inf(π, β, < ) β
β) |
11 | 10 | nnred 12231 |
. . . 4
β’ ((π β§ π β π
) β inf(π, β, < ) β
β) |
12 | 11 | ralrimiva 3140 |
. . 3
β’ (π β βπ β π
inf(π, β, < ) β
β) |
13 | | fimaxre3 12164 |
. . 3
β’ ((π
β Fin β§ βπ β π
inf(π, β, < ) β β) β
βπ₯ β β
βπ β π
inf(π, β, < ) β€ π₯) |
14 | 1, 12, 13 | syl2anc 583 |
. 2
β’ (π β βπ₯ β β βπ β π
inf(π, β, < ) β€ π₯) |
15 | | vdwnn.2 |
. . . . . . . . 9
β’ (π β πΉ:ββΆπ
) |
16 | | 1nn 12227 |
. . . . . . . . 9
β’ 1 β
β |
17 | | ffvelcdm 7077 |
. . . . . . . . 9
β’ ((πΉ:ββΆπ
β§ 1 β β) β
(πΉβ1) β π
) |
18 | 15, 16, 17 | sylancl 585 |
. . . . . . . 8
β’ (π β (πΉβ1) β π
) |
19 | 18 | ne0d 4330 |
. . . . . . 7
β’ (π β π
β β
) |
20 | 19 | adantr 480 |
. . . . . 6
β’ ((π β§ π₯ β β) β π
β β
) |
21 | | r19.2z 4489 |
. . . . . . 7
β’ ((π
β β
β§
βπ β π
inf(π, β, < ) β€ π₯) β βπ β π
inf(π, β, < ) β€ π₯) |
22 | 21 | ex 412 |
. . . . . 6
β’ (π
β β
β
(βπ β π
inf(π, β, < ) β€ π₯ β βπ β π
inf(π, β, < ) β€ π₯)) |
23 | 20, 22 | syl 17 |
. . . . 5
β’ ((π β§ π₯ β β) β (βπ β π
inf(π, β, < ) β€ π₯ β βπ β π
inf(π, β, < ) β€ π₯)) |
24 | | simplr 766 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β π
) β π₯ β β) |
25 | | fllep1 13772 |
. . . . . . . . . 10
β’ (π₯ β β β π₯ β€ ((ββπ₯) + 1)) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π β π
) β π₯ β€ ((ββπ₯) + 1)) |
27 | 11 | adantlr 712 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β π
) β inf(π, β, < ) β
β) |
28 | 24 | flcld 13769 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π β π
) β (ββπ₯) β β€) |
29 | 28 | peano2zd 12673 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π β π
) β ((ββπ₯) + 1) β β€) |
30 | 29 | zred 12670 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β π
) β ((ββπ₯) + 1) β β) |
31 | | letr 11312 |
. . . . . . . . . 10
β’
((inf(π, β,
< ) β β β§ π₯ β β β§ ((ββπ₯) + 1) β β) β
((inf(π, β, < )
β€ π₯ β§ π₯ β€ ((ββπ₯) + 1)) β inf(π, β, < ) β€
((ββπ₯) +
1))) |
32 | 27, 24, 30, 31 | syl3anc 1368 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π β π
) β ((inf(π, β, < ) β€ π₯ β§ π₯ β€ ((ββπ₯) + 1)) β inf(π, β, < ) β€ ((ββπ₯) + 1))) |
33 | 26, 32 | mpan2d 691 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π β π
) β (inf(π, β, < ) β€ π₯ β inf(π, β, < ) β€ ((ββπ₯) + 1))) |
34 | 10 | adantlr 712 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π β π
) β inf(π, β, < ) β
β) |
35 | 34 | nnzd 12589 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β π
) β inf(π, β, < ) β
β€) |
36 | | eluz 12840 |
. . . . . . . . . 10
β’
((inf(π, β,
< ) β β€ β§ ((ββπ₯) + 1) β β€) β
(((ββπ₯) + 1)
β (β€β₯βinf(π, β, < )) β inf(π, β, < ) β€
((ββπ₯) +
1))) |
37 | 35, 29, 36 | syl2anc 583 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π β π
) β (((ββπ₯) + 1) β
(β€β₯βinf(π, β, < )) β inf(π, β, < ) β€
((ββπ₯) +
1))) |
38 | | simpll 764 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β π
) β π) |
39 | 9 | adantlr 712 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β π
) β inf(π, β, < ) β π) |
40 | 1, 15, 2 | vdwnnlem2 16938 |
. . . . . . . . . . 11
β’ ((π β§ ((ββπ₯) + 1) β
(β€β₯βinf(π, β, < ))) β (inf(π, β, < ) β π β ((ββπ₯) + 1) β π)) |
41 | 40 | impancom 451 |
. . . . . . . . . 10
β’ ((π β§ inf(π, β, < ) β π) β (((ββπ₯) + 1) β
(β€β₯βinf(π, β, < )) β
((ββπ₯) + 1)
β π)) |
42 | 38, 39, 41 | syl2anc 583 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π β π
) β (((ββπ₯) + 1) β
(β€β₯βinf(π, β, < )) β
((ββπ₯) + 1)
β π)) |
43 | 37, 42 | sylbird 260 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π β π
) β (inf(π, β, < ) β€ ((ββπ₯) + 1) β
((ββπ₯) + 1)
β π)) |
44 | 33, 43 | syld 47 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ π β π
) β (inf(π, β, < ) β€ π₯ β ((ββπ₯) + 1) β π)) |
45 | 3 | sseli 3973 |
. . . . . . . 8
β’
(((ββπ₯)
+ 1) β π β
((ββπ₯) + 1)
β β) |
46 | 45 | nnnn0d 12536 |
. . . . . . 7
β’
(((ββπ₯)
+ 1) β π β
((ββπ₯) + 1)
β β0) |
47 | 44, 46 | syl6 35 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ π β π
) β (inf(π, β, < ) β€ π₯ β ((ββπ₯) + 1) β
β0)) |
48 | 47 | rexlimdva 3149 |
. . . . 5
β’ ((π β§ π₯ β β) β (βπ β π
inf(π, β, < ) β€ π₯ β ((ββπ₯) + 1) β
β0)) |
49 | 1 | adantr 480 |
. . . . . . . 8
β’ ((π β§ ((ββπ₯) + 1) β
β0) β π
β Fin) |
50 | 15 | adantr 480 |
. . . . . . . 8
β’ ((π β§ ((ββπ₯) + 1) β
β0) β πΉ:ββΆπ
) |
51 | | simpr 484 |
. . . . . . . 8
β’ ((π β§ ((ββπ₯) + 1) β
β0) β ((ββπ₯) + 1) β
β0) |
52 | | vdwnnlem1 16937 |
. . . . . . . 8
β’ ((π
β Fin β§ πΉ:ββΆπ
β§ ((ββπ₯) + 1) β
β0) β βπ β π
βπ β β βπ β β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π})) |
53 | 49, 50, 51, 52 | syl3anc 1368 |
. . . . . . 7
β’ ((π β§ ((ββπ₯) + 1) β
β0) β βπ β π
βπ β β βπ β β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π})) |
54 | 53 | ex 412 |
. . . . . 6
β’ (π β (((ββπ₯) + 1) β
β0 β βπ β π
βπ β β βπ β β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π}))) |
55 | 54 | adantr 480 |
. . . . 5
β’ ((π β§ π₯ β β) β
(((ββπ₯) + 1)
β β0 β βπ β π
βπ β β βπ β β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π}))) |
56 | 23, 48, 55 | 3syld 60 |
. . . 4
β’ ((π β§ π₯ β β) β (βπ β π
inf(π, β, < ) β€ π₯ β βπ β π
βπ β β βπ β β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π}))) |
57 | | oveq1 7412 |
. . . . . . . . . . . . 13
β’ (π = ((ββπ₯) + 1) β (π β 1) =
(((ββπ₯) + 1)
β 1)) |
58 | 57 | oveq2d 7421 |
. . . . . . . . . . . 12
β’ (π = ((ββπ₯) + 1) β (0...(π β 1)) =
(0...(((ββπ₯) +
1) β 1))) |
59 | 58 | raleqdv 3319 |
. . . . . . . . . . 11
β’ (π = ((ββπ₯) + 1) β (βπ β (0...(π β 1))(π + (π Β· π)) β (β‘πΉ β {π}) β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π}))) |
60 | 59 | 2rexbidv 3213 |
. . . . . . . . . 10
β’ (π = ((ββπ₯) + 1) β (βπ β β βπ β β βπ β (0...(π β 1))(π + (π Β· π)) β (β‘πΉ β {π}) β βπ β β βπ β β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π}))) |
61 | 60 | notbid 318 |
. . . . . . . . 9
β’ (π = ((ββπ₯) + 1) β (Β¬
βπ β β
βπ β β
βπ β
(0...(π β 1))(π + (π Β· π)) β (β‘πΉ β {π}) β Β¬ βπ β β βπ β β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π}))) |
62 | 61, 2 | elrab2 3681 |
. . . . . . . 8
β’
(((ββπ₯)
+ 1) β π β
(((ββπ₯) + 1)
β β β§ Β¬ βπ β β βπ β β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π}))) |
63 | 62 | simprbi 496 |
. . . . . . 7
β’
(((ββπ₯)
+ 1) β π β Β¬
βπ β β
βπ β β
βπ β
(0...(((ββπ₯) +
1) β 1))(π + (π Β· π)) β (β‘πΉ β {π})) |
64 | 44, 63 | syl6 35 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ π β π
) β (inf(π, β, < ) β€ π₯ β Β¬ βπ β β βπ β β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π}))) |
65 | 64 | ralimdva 3161 |
. . . . 5
β’ ((π β§ π₯ β β) β (βπ β π
inf(π, β, < ) β€ π₯ β βπ β π
Β¬ βπ β β βπ β β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π}))) |
66 | | ralnex 3066 |
. . . . 5
β’
(βπ β
π
Β¬ βπ β β βπ β β βπ β
(0...(((ββπ₯) +
1) β 1))(π + (π Β· π)) β (β‘πΉ β {π}) β Β¬ βπ β π
βπ β β βπ β β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π})) |
67 | 65, 66 | imbitrdi 250 |
. . . 4
β’ ((π β§ π₯ β β) β (βπ β π
inf(π, β, < ) β€ π₯ β Β¬ βπ β π
βπ β β βπ β β βπ β (0...(((ββπ₯) + 1) β 1))(π + (π Β· π)) β (β‘πΉ β {π}))) |
68 | 56, 67 | pm2.65d 195 |
. . 3
β’ ((π β§ π₯ β β) β Β¬ βπ β π
inf(π, β, < ) β€ π₯) |
69 | 68 | nrexdv 3143 |
. 2
β’ (π β Β¬ βπ₯ β β βπ β π
inf(π, β, < ) β€ π₯) |
70 | 14, 69 | pm2.65i 193 |
1
β’ Β¬
π |