Step | Hyp | Ref
| Expression |
1 | | vdwlem1.a |
. . . 4
β’ (π β π΄ β β) |
2 | | vdwlem1.d |
. . . . 5
β’ (π β π·:(1...π)βΆβ) |
3 | | vdwlem1.i |
. . . . 5
β’ (π β πΌ β (1...π)) |
4 | 2, 3 | ffvelcdmd 7088 |
. . . 4
β’ (π β (π·βπΌ) β β) |
5 | | vdwlem1.k |
. . . . . . 7
β’ (π β πΎ β β) |
6 | 5 | nnnn0d 12532 |
. . . . . 6
β’ (π β πΎ β
β0) |
7 | | vdwapun 16907 |
. . . . . 6
β’ ((πΎ β β0
β§ π΄ β β
β§ (π·βπΌ) β β) β (π΄(APβ(πΎ + 1))(π·βπΌ)) = ({π΄} βͺ ((π΄ + (π·βπΌ))(APβπΎ)(π·βπΌ)))) |
8 | 6, 1, 4, 7 | syl3anc 1372 |
. . . . 5
β’ (π β (π΄(APβ(πΎ + 1))(π·βπΌ)) = ({π΄} βͺ ((π΄ + (π·βπΌ))(APβπΎ)(π·βπΌ)))) |
9 | 1 | nnred 12227 |
. . . . . . . . . 10
β’ (π β π΄ β β) |
10 | | vdwlem1.m |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
11 | | nnuz 12865 |
. . . . . . . . . . . . . . 15
β’ β =
(β€β₯β1) |
12 | 10, 11 | eleqtrdi 2844 |
. . . . . . . . . . . . . 14
β’ (π β π β
(β€β₯β1)) |
13 | | eluzfz1 13508 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β1) β 1 β (1...π)) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β 1 β (1...π)) |
15 | 2, 14 | ffvelcdmd 7088 |
. . . . . . . . . . . 12
β’ (π β (π·β1) β β) |
16 | 1, 15 | nnaddcld 12264 |
. . . . . . . . . . 11
β’ (π β (π΄ + (π·β1)) β β) |
17 | 16 | nnred 12227 |
. . . . . . . . . 10
β’ (π β (π΄ + (π·β1)) β β) |
18 | | vdwlem1.w |
. . . . . . . . . . 11
β’ (π β π β β) |
19 | 18 | nnred 12227 |
. . . . . . . . . 10
β’ (π β π β β) |
20 | 15 | nnrpd 13014 |
. . . . . . . . . . . 12
β’ (π β (π·β1) β
β+) |
21 | 9, 20 | ltaddrpd 13049 |
. . . . . . . . . . 11
β’ (π β π΄ < (π΄ + (π·β1))) |
22 | 9, 17, 21 | ltled 11362 |
. . . . . . . . . 10
β’ (π β π΄ β€ (π΄ + (π·β1))) |
23 | | fveq2 6892 |
. . . . . . . . . . . . . 14
β’ (π = 1 β (π·βπ) = (π·β1)) |
24 | 23 | oveq2d 7425 |
. . . . . . . . . . . . 13
β’ (π = 1 β (π΄ + (π·βπ)) = (π΄ + (π·β1))) |
25 | 24 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π = 1 β ((π΄ + (π·βπ)) β (1...π) β (π΄ + (π·β1)) β (1...π))) |
26 | | vdwlem1.s |
. . . . . . . . . . . . . . . 16
β’ (π β βπ β (1...π)((π΄ + (π·βπ))(APβπΎ)(π·βπ)) β (β‘πΉ β {(πΉβ(π΄ + (π·βπ)))})) |
27 | 26 | r19.21bi 3249 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β ((π΄ + (π·βπ))(APβπΎ)(π·βπ)) β (β‘πΉ β {(πΉβ(π΄ + (π·βπ)))})) |
28 | | cnvimass 6081 |
. . . . . . . . . . . . . . . . 17
β’ (β‘πΉ β {(πΉβ(π΄ + (π·βπ)))}) β dom πΉ |
29 | | vdwlem1.f |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ:(1...π)βΆπ
) |
30 | 28, 29 | fssdm 6738 |
. . . . . . . . . . . . . . . 16
β’ (π β (β‘πΉ β {(πΉβ(π΄ + (π·βπ)))}) β (1...π)) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β (β‘πΉ β {(πΉβ(π΄ + (π·βπ)))}) β (1...π)) |
32 | 27, 31 | sstrd 3993 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β ((π΄ + (π·βπ))(APβπΎ)(π·βπ)) β (1...π)) |
33 | | nnm1nn0 12513 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΎ β β β (πΎ β 1) β
β0) |
34 | 5, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΎ β 1) β
β0) |
35 | | nn0uz 12864 |
. . . . . . . . . . . . . . . . . . 19
β’
β0 = (β€β₯β0) |
36 | 34, 35 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΎ β 1) β
(β€β₯β0)) |
37 | | eluzfz1 13508 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β 1) β
(β€β₯β0) β 0 β (0...(πΎ β 1))) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β 0 β (0...(πΎ β 1))) |
39 | 38 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...π)) β 0 β (0...(πΎ β 1))) |
40 | 2 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (1...π)) β (π·βπ) β β) |
41 | 40 | nncnd 12228 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (1...π)) β (π·βπ) β β) |
42 | 41 | mul02d 11412 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β (0 Β· (π·βπ)) = 0) |
43 | 42 | oveq2d 7425 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...π)) β ((π΄ + (π·βπ)) + (0 Β· (π·βπ))) = ((π΄ + (π·βπ)) + 0)) |
44 | 1 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (1...π)) β π΄ β β) |
45 | 44, 40 | nnaddcld 12264 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (1...π)) β (π΄ + (π·βπ)) β β) |
46 | 45 | nncnd 12228 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β (π΄ + (π·βπ)) β β) |
47 | 46 | addridd 11414 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...π)) β ((π΄ + (π·βπ)) + 0) = (π΄ + (π·βπ))) |
48 | 43, 47 | eqtr2d 2774 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...π)) β (π΄ + (π·βπ)) = ((π΄ + (π·βπ)) + (0 Β· (π·βπ)))) |
49 | | oveq1 7416 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β (π Β· (π·βπ)) = (0 Β· (π·βπ))) |
50 | 49 | oveq2d 7425 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β ((π΄ + (π·βπ)) + (π Β· (π·βπ))) = ((π΄ + (π·βπ)) + (0 Β· (π·βπ)))) |
51 | 50 | rspceeqv 3634 |
. . . . . . . . . . . . . . . 16
β’ ((0
β (0...(πΎ β 1))
β§ (π΄ + (π·βπ)) = ((π΄ + (π·βπ)) + (0 Β· (π·βπ)))) β βπ β (0...(πΎ β 1))(π΄ + (π·βπ)) = ((π΄ + (π·βπ)) + (π Β· (π·βπ)))) |
52 | 39, 48, 51 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β βπ β (0...(πΎ β 1))(π΄ + (π·βπ)) = ((π΄ + (π·βπ)) + (π Β· (π·βπ)))) |
53 | 5 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...π)) β πΎ β β) |
54 | 53 | nnnn0d 12532 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...π)) β πΎ β
β0) |
55 | | vdwapval 16906 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β β0
β§ (π΄ + (π·βπ)) β β β§ (π·βπ) β β) β ((π΄ + (π·βπ)) β ((π΄ + (π·βπ))(APβπΎ)(π·βπ)) β βπ β (0...(πΎ β 1))(π΄ + (π·βπ)) = ((π΄ + (π·βπ)) + (π Β· (π·βπ))))) |
56 | 54, 45, 40, 55 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β ((π΄ + (π·βπ)) β ((π΄ + (π·βπ))(APβπΎ)(π·βπ)) β βπ β (0...(πΎ β 1))(π΄ + (π·βπ)) = ((π΄ + (π·βπ)) + (π Β· (π·βπ))))) |
57 | 52, 56 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β (π΄ + (π·βπ)) β ((π΄ + (π·βπ))(APβπΎ)(π·βπ))) |
58 | 32, 57 | sseldd 3984 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (π΄ + (π·βπ)) β (1...π)) |
59 | 58 | ralrimiva 3147 |
. . . . . . . . . . . 12
β’ (π β βπ β (1...π)(π΄ + (π·βπ)) β (1...π)) |
60 | 25, 59, 14 | rspcdva 3614 |
. . . . . . . . . . 11
β’ (π β (π΄ + (π·β1)) β (1...π)) |
61 | | elfzle2 13505 |
. . . . . . . . . . 11
β’ ((π΄ + (π·β1)) β (1...π) β (π΄ + (π·β1)) β€ π) |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
β’ (π β (π΄ + (π·β1)) β€ π) |
63 | 9, 17, 19, 22, 62 | letrd 11371 |
. . . . . . . . 9
β’ (π β π΄ β€ π) |
64 | 1, 11 | eleqtrdi 2844 |
. . . . . . . . . 10
β’ (π β π΄ β
(β€β₯β1)) |
65 | 18 | nnzd 12585 |
. . . . . . . . . 10
β’ (π β π β β€) |
66 | | elfz5 13493 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β1) β§ π β β€) β (π΄ β (1...π) β π΄ β€ π)) |
67 | 64, 65, 66 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π΄ β (1...π) β π΄ β€ π)) |
68 | 63, 67 | mpbird 257 |
. . . . . . . 8
β’ (π β π΄ β (1...π)) |
69 | | eqidd 2734 |
. . . . . . . 8
β’ (π β (πΉβπ΄) = (πΉβπ΄)) |
70 | | ffn 6718 |
. . . . . . . . 9
β’ (πΉ:(1...π)βΆπ
β πΉ Fn (1...π)) |
71 | | fniniseg 7062 |
. . . . . . . . 9
β’ (πΉ Fn (1...π) β (π΄ β (β‘πΉ β {(πΉβπ΄)}) β (π΄ β (1...π) β§ (πΉβπ΄) = (πΉβπ΄)))) |
72 | 29, 70, 71 | 3syl 18 |
. . . . . . . 8
β’ (π β (π΄ β (β‘πΉ β {(πΉβπ΄)}) β (π΄ β (1...π) β§ (πΉβπ΄) = (πΉβπ΄)))) |
73 | 68, 69, 72 | mpbir2and 712 |
. . . . . . 7
β’ (π β π΄ β (β‘πΉ β {(πΉβπ΄)})) |
74 | 73 | snssd 4813 |
. . . . . 6
β’ (π β {π΄} β (β‘πΉ β {(πΉβπ΄)})) |
75 | | fveq2 6892 |
. . . . . . . . . . 11
β’ (π = πΌ β (π·βπ) = (π·βπΌ)) |
76 | 75 | oveq2d 7425 |
. . . . . . . . . 10
β’ (π = πΌ β (π΄ + (π·βπ)) = (π΄ + (π·βπΌ))) |
77 | 76, 75 | oveq12d 7427 |
. . . . . . . . 9
β’ (π = πΌ β ((π΄ + (π·βπ))(APβπΎ)(π·βπ)) = ((π΄ + (π·βπΌ))(APβπΎ)(π·βπΌ))) |
78 | 76 | fveq2d 6896 |
. . . . . . . . . . 11
β’ (π = πΌ β (πΉβ(π΄ + (π·βπ))) = (πΉβ(π΄ + (π·βπΌ)))) |
79 | 78 | sneqd 4641 |
. . . . . . . . . 10
β’ (π = πΌ β {(πΉβ(π΄ + (π·βπ)))} = {(πΉβ(π΄ + (π·βπΌ)))}) |
80 | 79 | imaeq2d 6060 |
. . . . . . . . 9
β’ (π = πΌ β (β‘πΉ β {(πΉβ(π΄ + (π·βπ)))}) = (β‘πΉ β {(πΉβ(π΄ + (π·βπΌ)))})) |
81 | 77, 80 | sseq12d 4016 |
. . . . . . . 8
β’ (π = πΌ β (((π΄ + (π·βπ))(APβπΎ)(π·βπ)) β (β‘πΉ β {(πΉβ(π΄ + (π·βπ)))}) β ((π΄ + (π·βπΌ))(APβπΎ)(π·βπΌ)) β (β‘πΉ β {(πΉβ(π΄ + (π·βπΌ)))}))) |
82 | 81, 26, 3 | rspcdva 3614 |
. . . . . . 7
β’ (π β ((π΄ + (π·βπΌ))(APβπΎ)(π·βπΌ)) β (β‘πΉ β {(πΉβ(π΄ + (π·βπΌ)))})) |
83 | | vdwlem1.e |
. . . . . . . . 9
β’ (π β (πΉβπ΄) = (πΉβ(π΄ + (π·βπΌ)))) |
84 | 83 | sneqd 4641 |
. . . . . . . 8
β’ (π β {(πΉβπ΄)} = {(πΉβ(π΄ + (π·βπΌ)))}) |
85 | 84 | imaeq2d 6060 |
. . . . . . 7
β’ (π β (β‘πΉ β {(πΉβπ΄)}) = (β‘πΉ β {(πΉβ(π΄ + (π·βπΌ)))})) |
86 | 82, 85 | sseqtrrd 4024 |
. . . . . 6
β’ (π β ((π΄ + (π·βπΌ))(APβπΎ)(π·βπΌ)) β (β‘πΉ β {(πΉβπ΄)})) |
87 | 74, 86 | unssd 4187 |
. . . . 5
β’ (π β ({π΄} βͺ ((π΄ + (π·βπΌ))(APβπΎ)(π·βπΌ))) β (β‘πΉ β {(πΉβπ΄)})) |
88 | 8, 87 | eqsstrd 4021 |
. . . 4
β’ (π β (π΄(APβ(πΎ + 1))(π·βπΌ)) β (β‘πΉ β {(πΉβπ΄)})) |
89 | | oveq1 7416 |
. . . . . 6
β’ (π = π΄ β (π(APβ(πΎ + 1))π) = (π΄(APβ(πΎ + 1))π)) |
90 | 89 | sseq1d 4014 |
. . . . 5
β’ (π = π΄ β ((π(APβ(πΎ + 1))π) β (β‘πΉ β {(πΉβπ΄)}) β (π΄(APβ(πΎ + 1))π) β (β‘πΉ β {(πΉβπ΄)}))) |
91 | | oveq2 7417 |
. . . . . 6
β’ (π = (π·βπΌ) β (π΄(APβ(πΎ + 1))π) = (π΄(APβ(πΎ + 1))(π·βπΌ))) |
92 | 91 | sseq1d 4014 |
. . . . 5
β’ (π = (π·βπΌ) β ((π΄(APβ(πΎ + 1))π) β (β‘πΉ β {(πΉβπ΄)}) β (π΄(APβ(πΎ + 1))(π·βπΌ)) β (β‘πΉ β {(πΉβπ΄)}))) |
93 | 90, 92 | rspc2ev 3625 |
. . . 4
β’ ((π΄ β β β§ (π·βπΌ) β β β§ (π΄(APβ(πΎ + 1))(π·βπΌ)) β (β‘πΉ β {(πΉβπ΄)})) β βπ β β βπ β β (π(APβ(πΎ + 1))π) β (β‘πΉ β {(πΉβπ΄)})) |
94 | 1, 4, 88, 93 | syl3anc 1372 |
. . 3
β’ (π β βπ β β βπ β β (π(APβ(πΎ + 1))π) β (β‘πΉ β {(πΉβπ΄)})) |
95 | | fvex 6905 |
. . . 4
β’ (πΉβπ΄) β V |
96 | | sneq 4639 |
. . . . . . 7
β’ (π = (πΉβπ΄) β {π} = {(πΉβπ΄)}) |
97 | 96 | imaeq2d 6060 |
. . . . . 6
β’ (π = (πΉβπ΄) β (β‘πΉ β {π}) = (β‘πΉ β {(πΉβπ΄)})) |
98 | 97 | sseq2d 4015 |
. . . . 5
β’ (π = (πΉβπ΄) β ((π(APβ(πΎ + 1))π) β (β‘πΉ β {π}) β (π(APβ(πΎ + 1))π) β (β‘πΉ β {(πΉβπ΄)}))) |
99 | 98 | 2rexbidv 3220 |
. . . 4
β’ (π = (πΉβπ΄) β (βπ β β βπ β β (π(APβ(πΎ + 1))π) β (β‘πΉ β {π}) β βπ β β βπ β β (π(APβ(πΎ + 1))π) β (β‘πΉ β {(πΉβπ΄)}))) |
100 | 95, 99 | spcev 3597 |
. . 3
β’
(βπ β
β βπ β
β (π(APβ(πΎ + 1))π) β (β‘πΉ β {(πΉβπ΄)}) β βπβπ β β βπ β β (π(APβ(πΎ + 1))π) β (β‘πΉ β {π})) |
101 | 94, 100 | syl 17 |
. 2
β’ (π β βπβπ β β βπ β β (π(APβ(πΎ + 1))π) β (β‘πΉ β {π})) |
102 | | ovex 7442 |
. . 3
β’
(1...π) β
V |
103 | | peano2nn0 12512 |
. . . 4
β’ (πΎ β β0
β (πΎ + 1) β
β0) |
104 | 6, 103 | syl 17 |
. . 3
β’ (π β (πΎ + 1) β
β0) |
105 | 102, 104,
29 | vdwmc 16911 |
. 2
β’ (π β ((πΎ + 1) MonoAP πΉ β βπβπ β β βπ β β (π(APβ(πΎ + 1))π) β (β‘πΉ β {π}))) |
106 | 101, 105 | mpbird 257 |
1
β’ (π β (πΎ + 1) MonoAP πΉ) |