Step | Hyp | Ref
| Expression |
1 | | simprr 772 |
. . . . . . 7
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π΄βπ) β 0) |
2 | | ffun 6676 |
. . . . . . . . . . . 12
β’ (π΄:β0βΆβ β
Fun π΄) |
3 | 2 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄:β0βΆβ) β
Fun π΄) |
4 | | peano2nn0 12460 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (π + 1) β
β0) |
5 | 4 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π + 1) β
β0) |
6 | | eluznn0 12849 |
. . . . . . . . . . . . . . 15
β’ (((π + 1) β β0
β§ π β
(β€β₯β(π + 1))) β π β β0) |
7 | 6 | ex 414 |
. . . . . . . . . . . . . 14
β’ ((π + 1) β β0
β (π β
(β€β₯β(π + 1)) β π β
β0)) |
8 | 5, 7 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π β
(β€β₯β(π + 1)) β π β
β0)) |
9 | 8 | ssrdv 3955 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄:β0βΆβ) β
(β€β₯β(π + 1)) β
β0) |
10 | | fdm 6682 |
. . . . . . . . . . . . 13
β’ (π΄:β0βΆβ β
dom π΄ =
β0) |
11 | 10 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄:β0βΆβ) β
dom π΄ =
β0) |
12 | 9, 11 | sseqtrrd 3990 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄:β0βΆβ) β
(β€β₯β(π + 1)) β dom π΄) |
13 | | funfvima2 7186 |
. . . . . . . . . . 11
β’ ((Fun
π΄ β§
(β€β₯β(π + 1)) β dom π΄) β (π β (β€β₯β(π + 1)) β (π΄βπ) β (π΄ β
(β€β₯β(π + 1))))) |
14 | 3, 12, 13 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π β
(β€β₯β(π + 1)) β (π΄βπ) β (π΄ β
(β€β₯β(π + 1))))) |
15 | 14 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π β (β€β₯β(π + 1)) β (π΄βπ) β (π΄ β
(β€β₯β(π + 1))))) |
16 | | nn0z 12531 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β€) |
17 | 16 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄:β0βΆβ) β
π β
β€) |
18 | 17 | peano2zd 12617 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π + 1) β
β€) |
19 | 18 | ad2antrr 725 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π + 1) β β€) |
20 | | nn0z 12531 |
. . . . . . . . . . 11
β’ (π β β0
β π β
β€) |
21 | 20 | ad2antrl 727 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β π β β€) |
22 | | eluz 12784 |
. . . . . . . . . 10
β’ (((π + 1) β β€ β§ π β β€) β (π β
(β€β₯β(π + 1)) β (π + 1) β€ π)) |
23 | 19, 21, 22 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π β (β€β₯β(π + 1)) β (π + 1) β€ π)) |
24 | | simplr 768 |
. . . . . . . . . . 11
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π΄ β
(β€β₯β(π + 1))) = {0}) |
25 | 24 | eleq2d 2824 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β ((π΄βπ) β (π΄ β
(β€β₯β(π + 1))) β (π΄βπ) β {0})) |
26 | | fvex 6860 |
. . . . . . . . . . 11
β’ (π΄βπ) β V |
27 | 26 | elsn 4606 |
. . . . . . . . . 10
β’ ((π΄βπ) β {0} β (π΄βπ) = 0) |
28 | 25, 27 | bitrdi 287 |
. . . . . . . . 9
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β ((π΄βπ) β (π΄ β
(β€β₯β(π + 1))) β (π΄βπ) = 0)) |
29 | 15, 23, 28 | 3imtr3d 293 |
. . . . . . . 8
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β ((π + 1) β€ π β (π΄βπ) = 0)) |
30 | 29 | necon3ad 2957 |
. . . . . . 7
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β ((π΄βπ) β 0 β Β¬ (π + 1) β€ π)) |
31 | 1, 30 | mpd 15 |
. . . . . 6
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β Β¬ (π + 1) β€ π) |
32 | | nn0re 12429 |
. . . . . . . 8
β’ (π β β0
β π β
β) |
33 | 32 | ad2antrl 727 |
. . . . . . 7
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β π β β) |
34 | 18 | zred 12614 |
. . . . . . . 8
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π + 1) β
β) |
35 | 34 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π + 1) β β) |
36 | 33, 35 | ltnled 11309 |
. . . . . 6
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π < (π + 1) β Β¬ (π + 1) β€ π)) |
37 | 31, 36 | mpbird 257 |
. . . . 5
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β π < (π + 1)) |
38 | 17 | ad2antrr 725 |
. . . . . 6
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β π β β€) |
39 | | zleltp1 12561 |
. . . . . 6
β’ ((π β β€ β§ π β β€) β (π β€ π β π < (π + 1))) |
40 | 21, 38, 39 | syl2anc 585 |
. . . . 5
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β (π β€ π β π < (π + 1))) |
41 | 37, 40 | mpbird 257 |
. . . 4
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ (π β β0 β§ (π΄βπ) β 0)) β π β€ π) |
42 | 41 | expr 458 |
. . 3
β’ ((((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β§ π β β0) β ((π΄βπ) β 0 β π β€ π)) |
43 | 42 | ralrimiva 3144 |
. 2
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(π΄ β
(β€β₯β(π + 1))) = {0}) β βπ β β0
((π΄βπ) β 0 β π β€ π)) |
44 | | simpr 486 |
. . . . . . . 8
β’
((βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1))) β π β
(β€β₯β(π + 1))) |
45 | | eluznn0 12849 |
. . . . . . . 8
β’ (((π + 1) β β0
β§ π β
(β€β₯β(π + 1))) β π β β0) |
46 | 5, 44, 45 | syl2an 597 |
. . . . . . 7
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π β
β0) |
47 | | nn0re 12429 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
β) |
48 | 47 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄:β0βΆβ) β
π β
β) |
49 | 48 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π β
β) |
50 | 34 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β (π + 1) β
β) |
51 | 46 | nn0red 12481 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π β
β) |
52 | 49 | ltp1d 12092 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π < (π + 1)) |
53 | | eluzle 12783 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β(π + 1)) β (π + 1) β€ π) |
54 | 53 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β (π + 1) β€ π) |
55 | 49, 50, 51, 52, 54 | ltletrd 11322 |
. . . . . . . . 9
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π < π) |
56 | 49, 51 | ltnled 11309 |
. . . . . . . . 9
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β (π < π β Β¬ π β€ π)) |
57 | 55, 56 | mpbid 231 |
. . . . . . . 8
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β Β¬ π β€ π) |
58 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (π΄βπ) = (π΄βπ)) |
59 | 58 | neeq1d 3004 |
. . . . . . . . . . 11
β’ (π = π β ((π΄βπ) β 0 β (π΄βπ) β 0)) |
60 | | breq1 5113 |
. . . . . . . . . . 11
β’ (π = π β (π β€ π β π β€ π)) |
61 | 59, 60 | imbi12d 345 |
. . . . . . . . . 10
β’ (π = π β (((π΄βπ) β 0 β π β€ π) β ((π΄βπ) β 0 β π β€ π))) |
62 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β βπ β β0
((π΄βπ) β 0 β π β€ π)) |
63 | 61, 62, 46 | rspcdva 3585 |
. . . . . . . . 9
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β ((π΄βπ) β 0 β π β€ π)) |
64 | 63 | necon1bd 2962 |
. . . . . . . 8
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β (Β¬ π β€ π β (π΄βπ) = 0)) |
65 | 57, 64 | mpd 15 |
. . . . . . 7
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β (π΄βπ) = 0) |
66 | | ffn 6673 |
. . . . . . . . 9
β’ (π΄:β0βΆβ β
π΄ Fn
β0) |
67 | 66 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π΄ Fn
β0) |
68 | | fniniseg 7015 |
. . . . . . . 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 712 |
. . . . . 6
β’ (((π β β0
β§ π΄:β0βΆβ) β§
(βπ β
β0 ((π΄βπ) β 0 β π β€ π) β§ π β (β€β₯β(π + 1)))) β π β (β‘π΄ β {0})) |
71 | 70 | expr 458 |
. . . . 5
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β (π β (β€β₯β(π + 1)) β π β (β‘π΄ β {0}))) |
72 | 71 | ssrdv 3955 |
. . . 4
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β
(β€β₯β(π + 1)) β (β‘π΄ β {0})) |
73 | | funimass3 7009 |
. . . . . 6
β’ ((Fun
π΄ β§
(β€β₯β(π + 1)) β dom π΄) β ((π΄ β
(β€β₯β(π + 1))) β {0} β
(β€β₯β(π + 1)) β (β‘π΄ β {0}))) |
74 | 3, 12, 73 | syl2anc 585 |
. . . . 5
β’ ((π β β0
β§ π΄:β0βΆβ) β
((π΄ β
(β€β₯β(π + 1))) β {0} β
(β€β₯β(π + 1)) β (β‘π΄ β {0}))) |
75 | 74 | adantr 482 |
. . . 4
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β ((π΄ β
(β€β₯β(π + 1))) β {0} β
(β€β₯β(π + 1)) β (β‘π΄ β {0}))) |
76 | 72, 75 | mpbird 257 |
. . 3
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β (π΄ β
(β€β₯β(π + 1))) β {0}) |
77 | 48 | ltp1d 12092 |
. . . . . . . 8
β’ ((π β β0
β§ π΄:β0βΆβ) β
π < (π + 1)) |
78 | 48, 34 | ltnled 11309 |
. . . . . . . 8
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π < (π + 1) β Β¬ (π + 1) β€ π)) |
79 | 77, 78 | mpbid 231 |
. . . . . . 7
β’ ((π β β0
β§ π΄:β0βΆβ) β
Β¬ (π + 1) β€ π) |
80 | 79 | adantr 482 |
. . . . . 6
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β Β¬ (π + 1) β€ π) |
81 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (π΄βπ) = (π΄β(π + 1))) |
82 | 81 | neeq1d 3004 |
. . . . . . . . . 10
β’ (π = (π + 1) β ((π΄βπ) β 0 β (π΄β(π + 1)) β 0)) |
83 | | breq1 5113 |
. . . . . . . . . 10
β’ (π = (π + 1) β (π β€ π β (π + 1) β€ π)) |
84 | 82, 83 | imbi12d 345 |
. . . . . . . . 9
β’ (π = (π + 1) β (((π΄βπ) β 0 β π β€ π) β ((π΄β(π + 1)) β 0 β (π + 1) β€ π))) |
85 | 84 | rspcva 3582 |
. . . . . . . 8
β’ (((π + 1) β β0
β§ βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β ((π΄β(π + 1)) β 0 β (π + 1) β€ π)) |
86 | 5, 85 | sylan 581 |
. . . . . . 7
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β ((π΄β(π + 1)) β 0 β (π + 1) β€ π)) |
87 | 86 | necon1bd 2962 |
. . . . . 6
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β (Β¬ (π + 1) β€ π β (π΄β(π + 1)) = 0)) |
88 | 80, 87 | mpd 15 |
. . . . 5
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β (π΄β(π + 1)) = 0) |
89 | | uzid 12785 |
. . . . . . . 8
β’ ((π + 1) β β€ β
(π + 1) β
(β€β₯β(π + 1))) |
90 | 18, 89 | syl 17 |
. . . . . . 7
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π + 1) β
(β€β₯β(π + 1))) |
91 | | funfvima2 7186 |
. . . . . . . 8
β’ ((Fun
π΄ β§
(β€β₯β(π + 1)) β dom π΄) β ((π + 1) β
(β€β₯β(π + 1)) β (π΄β(π + 1)) β (π΄ β
(β€β₯β(π + 1))))) |
92 | 3, 12, 91 | syl2anc 585 |
. . . . . . 7
β’ ((π β β0
β§ π΄:β0βΆβ) β
((π + 1) β
(β€β₯β(π + 1)) β (π΄β(π + 1)) β (π΄ β
(β€β₯β(π + 1))))) |
93 | 90, 92 | mpd 15 |
. . . . . 6
β’ ((π β β0
β§ π΄:β0βΆβ) β
(π΄β(π + 1)) β (π΄ β
(β€β₯β(π + 1)))) |
94 | 93 | adantr 482 |
. . . . 5
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β (π΄β(π + 1)) β (π΄ β
(β€β₯β(π + 1)))) |
95 | 88, 94 | eqeltrrd 2839 |
. . . 4
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β 0 β (π΄ β
(β€β₯β(π + 1)))) |
96 | 95 | snssd 4774 |
. . 3
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β {0} β (π΄ β
(β€β₯β(π + 1)))) |
97 | 76, 96 | eqssd 3966 |
. 2
β’ (((π β β0
β§ π΄:β0βΆβ) β§
βπ β
β0 ((π΄βπ) β 0 β π β€ π)) β (π΄ β
(β€β₯β(π + 1))) = {0}) |
98 | 43, 97 | impbida 800 |
1
β’ ((π β β0
β§ π΄:β0βΆβ) β
((π΄ β
(β€β₯β(π + 1))) = {0} β βπ β β0
((π΄βπ) β 0 β π β€ π))) |