Step | Hyp | Ref
| Expression |
1 | | simprr 771 |
. . . . . . 7
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π΄βπ) β 0) |
2 | | ffun 6717 |
. . . . . . . . . . . 12
β’ (π΄:β0βΆβ β
Fun π΄) |
3 | 2 | adantl 482 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄:β0βΆβ) β
Fun π΄) |
4 | | peano2nn0 12508 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (π + 1) β
β0) |
5 | 4 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π + 1) β
β0) |
6 | | eluznn0 12897 |
. . . . . . . . . . . . . . 15
β’ (((π + 1) β β0
β§ π β
(β€β₯β(π + 1))) β π β β0) |
7 | 6 | ex 413 |
. . . . . . . . . . . . . 14
β’ ((π + 1) β β0
β (π β
(β€β₯β(π + 1)) β π β
β0)) |
8 | 5, 7 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π β
(β€β₯β(π + 1)) β π β
β0)) |
9 | 8 | ssrdv 3987 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄:β0βΆβ) β
(β€β₯β(π + 1)) β
β0) |
10 | | fdm 6723 |
. . . . . . . . . . . . 13
β’ (π΄:β0βΆβ β
dom π΄ =
β0) |
11 | 10 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄:β0βΆβ) β
dom π΄ =
β0) |
12 | 9, 11 | sseqtrrd 4022 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄:β0βΆβ) β
(β€β₯β(π + 1)) β dom π΄) |
13 | | funfvima2 7229 |
. . . . . . . . . . 11
β’ ((Fun
π΄ β§
(β€β₯β(π + 1)) β dom π΄) β (π β (β€β₯β(π + 1)) β (π΄βπ) β (π΄ β
(β€β₯β(π + 1))))) |
14 | 3, 12, 13 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π β
(β€β₯β(π + 1)) β (π΄βπ) β (π΄ β
(β€β₯β(π + 1))))) |
15 | 14 | ad2antrr 724 |
. . . . . . . . 9
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π β (β€β₯β(π + 1)) β (π΄βπ) β (π΄ β
(β€β₯β(π + 1))))) |
16 | | nn0z 12579 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β€) |
17 | 16 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄:β0βΆβ) β
π β
β€) |
18 | 17 | peano2zd 12665 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π + 1) β
β€) |
19 | 18 | ad2antrr 724 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π + 1) β β€) |
20 | | nn0z 12579 |
. . . . . . . . . . 11
β’ (π β β0
β π β
β€) |
21 | 20 | ad2antrl 726 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β π β β€) |
22 | | eluz 12832 |
. . . . . . . . . 10
β’ (((π + 1) β β€ β§ π β β€) β (π β
(β€β₯β(π + 1)) β (π + 1) β€ π)) |
23 | 19, 21, 22 | syl2anc 584 |
. . . . . . . . 9
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π β (β€β₯β(π + 1)) β (π + 1) β€ π)) |
24 | | simplr 767 |
. . . . . . . . . . 11
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π΄ β
(β€β₯β(π + 1))) = {0}) |
25 | 24 | eleq2d 2819 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β ((π΄βπ) β (π΄ β
(β€β₯β(π + 1))) β (π΄βπ) β {0})) |
26 | | fvex 6901 |
. . . . . . . . . . 11
β’ (π΄βπ) β V |
27 | 26 | elsn 4642 |
. . . . . . . . . 10
β’ ((π΄βπ) β {0} β (π΄βπ) = 0) |
28 | 25, 27 | bitrdi 286 |
. . . . . . . . 9
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β ((π΄βπ) β (π΄ β
(β€β₯β(π + 1))) β (π΄βπ) = 0)) |
29 | 15, 23, 28 | 3imtr3d 292 |
. . . . . . . 8
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β ((π + 1) β€ π β (π΄βπ) = 0)) |
30 | 29 | necon3ad 2953 |
. . . . . . 7
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β ((π΄βπ) β 0 β Β¬ (π + 1) β€ π)) |
31 | 1, 30 | mpd 15 |
. . . . . 6
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β Β¬ (π + 1) β€ π) |
32 | | nn0re 12477 |
. . . . . . . 8
β’ (π β β0
β π β
β) |
33 | 32 | ad2antrl 726 |
. . . . . . 7
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β π β β) |
34 | 18 | zred 12662 |
. . . . . . . 8
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π + 1) β
β) |
35 | 34 | ad2antrr 724 |
. . . . . . 7
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π + 1) β β) |
36 | 33, 35 | ltnled 11357 |
. . . . . 6
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π < (π + 1) β Β¬ (π + 1) β€ π)) |
37 | 31, 36 | mpbird 256 |
. . . . 5
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β π < (π + 1)) |
38 | 17 | ad2antrr 724 |
. . . . . 6
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β π β β€) |
39 | | zleltp1 12609 |
. . . . . 6
β’ ((π β β€ β§ π β β€) β (π β€ π β π < (π + 1))) |
40 | 21, 38, 39 | syl2anc 584 |
. . . . 5
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π β€ π β π < (π + 1))) |
41 | 37, 40 | mpbird 256 |
. . . 4
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β π β€ π) |
42 | 41 | expr 457 |
. . 3
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ π β β0) β ((π΄βπ) β 0 β π β€ π)) |
43 | 42 | ralrimiva 3146 |
. 2
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β βπ β β0
((π΄βπ) β 0 β π β€ π)) |
44 | | simpr 485 |
. . . . . . . 8
β’
((βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1))) β π β
(β€β₯β(π + 1))) |
45 | | eluznn0 12897 |
. . . . . . . 8
β’ (((π + 1) β β0
β§ π β
(β€β₯β(π + 1))) β π β β0) |
46 | 5, 44, 45 | syl2an 596 |
. . . . . . 7
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π β
β0) |
47 | | nn0re 12477 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
β) |
48 | 47 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄:β0βΆβ) β
π β
β) |
49 | 48 | adantr 481 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π β
β) |
50 | 34 | adantr 481 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β (π + 1) β
β) |
51 | 46 | nn0red 12529 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π β
β) |
52 | 49 | ltp1d 12140 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π < (π + 1)) |
53 | | eluzle 12831 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β(π + 1)) β (π + 1) β€ π) |
54 | 53 | ad2antll 727 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β (π + 1) β€ π) |
55 | 49, 50, 51, 52, 54 | ltletrd 11370 |
. . . . . . . . 9
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π < π) |
56 | 49, 51 | ltnled 11357 |
. . . . . . . . 9
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β (π < π β Β¬ π β€ π)) |
57 | 55, 56 | mpbid 231 |
. . . . . . . 8
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β Β¬ π β€ π) |
58 | | fveq2 6888 |
. . . . . . . . . . . 12
β’ (π = π β (π΄βπ) = (π΄βπ)) |
59 | 58 | neeq1d 3000 |
. . . . . . . . . . 11
β’ (π = π β ((π΄βπ) β 0 β (π΄βπ) β 0)) |
60 | | breq1 5150 |
. . . . . . . . . . 11
β’ (π = π β (π β€ π β π β€ π)) |
61 | 59, 60 | imbi12d 344 |
. . . . . . . . . 10
β’ (π = π β (((π΄βπ) β 0 β π β€ π) β ((π΄βπ) β 0 β π β€ π))) |
62 | | simprl 769 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β βπ β β0
((π΄βπ) β 0 β π β€ π)) |
63 | 61, 62, 46 | rspcdva 3613 |
. . . . . . . . 9
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β ((π΄βπ) β 0 β π β€ π)) |
64 | 63 | necon1bd 2958 |
. . . . . . . 8
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β (Β¬ π β€ π β (π΄βπ) = 0)) |
65 | 57, 64 | mpd 15 |
. . . . . . 7
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β (π΄βπ) = 0) |
66 | | ffn 6714 |
. . . . . . . . 9
β’ (π΄:β0βΆβ β
π΄ Fn
β0) |
67 | 66 | ad2antlr 725 |
. . . . . . . 8
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π΄ Fn
β0) |
68 | | fniniseg 7058 |
. . . . . . . 8
β’ (π΄ Fn β0 β
(π β (β‘π΄ β {0}) β (π β β0 β§ (π΄βπ) = 0))) |
69 | 67, 68 | syl 17 |
. . . . . . 7
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β (π β (β‘π΄ β {0}) β (π β β0 β§ (π΄βπ) = 0))) |
70 | 46, 65, 69 | mpbir2and 711 |
. . . . . 6
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π β (β‘π΄ β {0})) |
71 | 70 | expr 457 |
. . . . 5
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β (π β (β€β₯β(π + 1)) β π β (β‘π΄ β {0}))) |
72 | 71 | ssrdv 3987 |
. . . 4
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β
(β€β₯β(π + 1)) β (β‘π΄ β {0})) |
73 | | funimass3 7052 |
. . . . . 6
β’ ((Fun
π΄ β§
(β€β₯β(π + 1)) β dom π΄) β ((π΄ β
(β€β₯β(π + 1))) β {0} β
(β€β₯β(π + 1)) β (β‘π΄ β {0}))) |
74 | 3, 12, 73 | syl2anc 584 |
. . . . 5
β’ ((π β β0
β§ π΄:β0βΆβ) β
((π΄ β
(β€β₯β(π + 1))) β {0} β
(β€β₯β(π + 1)) β (β‘π΄ β {0}))) |
75 | 74 | adantr 481 |
. . . 4
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β ((π΄ β
(β€β₯β(π + 1))) β {0} β
(β€β₯β(π + 1)) β (β‘π΄ β {0}))) |
76 | 72, 75 | mpbird 256 |
. . 3
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β (π΄ β
(β€β₯β(π + 1))) β {0}) |
77 | 48 | ltp1d 12140 |
. . . . . . . 8
β’ ((π β β0
β§ π΄:β0βΆβ) β
π < (π + 1)) |
78 | 48, 34 | ltnled 11357 |
. . . . . . . 8
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π < (π + 1) β Β¬ (π + 1) β€ π)) |
79 | 77, 78 | mpbid 231 |
. . . . . . 7
β’ ((π β β0
β§ π΄:β0βΆβ) β
Β¬ (π + 1) β€ π) |
80 | 79 | adantr 481 |
. . . . . 6
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β Β¬ (π + 1) β€ π) |
81 | | fveq2 6888 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (π΄βπ) = (π΄β(π + 1))) |
82 | 81 | neeq1d 3000 |
. . . . . . . . . 10
β’ (π = (π + 1) β ((π΄βπ) β 0 β (π΄β(π + 1)) β 0)) |
83 | | breq1 5150 |
. . . . . . . . . 10
β’ (π = (π + 1) β (π β€ π β (π + 1) β€ π)) |
84 | 82, 83 | imbi12d 344 |
. . . . . . . . 9
β’ (π = (π + 1) β (((π΄βπ) β 0 β π β€ π) β ((π΄β(π + 1)) β 0 β (π + 1) β€ π))) |
85 | 84 | rspcva 3610 |
. . . . . . . 8
β’ (((π + 1) β β0
β§ βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β ((π΄β(π + 1)) β 0 β (π + 1) β€ π)) |
86 | 5, 85 | sylan 580 |
. . . . . . 7
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β ((π΄β(π + 1)) β 0 β (π + 1) β€ π)) |
87 | 86 | necon1bd 2958 |
. . . . . 6
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β (Β¬ (π + 1) β€ π β (π΄β(π + 1)) = 0)) |
88 | 80, 87 | mpd 15 |
. . . . 5
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β (π΄β(π + 1)) = 0) |
89 | | uzid 12833 |
. . . . . . . 8
β’ ((π + 1) β β€ β
(π + 1) β
(β€β₯β(π + 1))) |
90 | 18, 89 | syl 17 |
. . . . . . 7
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π + 1) β
(β€β₯β(π + 1))) |
91 | | funfvima2 7229 |
. . . . . . . 8
β’ ((Fun
π΄ β§
(β€β₯β(π + 1)) β dom π΄) β ((π + 1) β
(β€β₯β(π + 1)) β (π΄β(π + 1)) β (π΄ β
(β€β₯β(π + 1))))) |
92 | 3, 12, 91 | syl2anc 584 |
. . . . . . 7
β’ ((π β β0
β§ π΄:β0βΆβ) β
((π + 1) β
(β€β₯β(π + 1)) β (π΄β(π + 1)) β (π΄ β
(β€β₯β(π + 1))))) |
93 | 90, 92 | mpd 15 |
. . . . . 6
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π΄β(π + 1)) β (π΄ β
(β€β₯β(π + 1)))) |
94 | 93 | adantr 481 |
. . . . 5
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β (π΄β(π + 1)) β (π΄ β
(β€β₯β(π + 1)))) |
95 | 88, 94 | eqeltrrd 2834 |
. . . 4
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β 0 β (π΄ β
(β€β₯β(π + 1)))) |
96 | 95 | snssd 4811 |
. . 3
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β {0} β (π΄ β
(β€β₯β(π + 1)))) |
97 | 76, 96 | eqssd 3998 |
. 2
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β (π΄ β
(β€β₯β(π + 1))) = {0}) |
98 | 43, 97 | impbida 799 |
1
β’ ((π β β0
β§ π΄:β0βΆβ) β
((π΄ β
(β€β₯β(π + 1))) = {0} β βπ β β0
((π΄βπ) β 0 β π β€ π))) |