Step | Hyp | Ref
| Expression |
1 | | ovex 7442 |
. . 3
β’
(1...π) β
V |
2 | | 2nn0 12489 |
. . . 4
β’ 2 β
β0 |
3 | | vdwlem7.k |
. . . 4
β’ (π β πΎ β
(β€β₯β2)) |
4 | | eluznn0 12901 |
. . . 4
β’ ((2
β β0 β§ πΎ β (β€β₯β2))
β πΎ β
β0) |
5 | 2, 3, 4 | sylancr 588 |
. . 3
β’ (π β πΎ β
β0) |
6 | | vdwlem7.g |
. . 3
β’ (π β πΊ:(1...π)βΆπ
) |
7 | | vdwlem7.m |
. . 3
β’ (π β π β β) |
8 | | eqid 2733 |
. . 3
β’
(1...π) = (1...π) |
9 | 1, 5, 6, 7, 8 | vdwpc 16913 |
. 2
β’ (π β (β¨π, πΎβ© PolyAP πΊ β βπ β β βπ β (β βm
(1...π))(βπ β (1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π))) |
10 | | vdwlem3.v |
. . . . . 6
β’ (π β π β β) |
11 | 10 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β π β β) |
12 | | vdwlem3.w |
. . . . . 6
β’ (π β π β β) |
13 | 12 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β π β β) |
14 | | vdwlem4.r |
. . . . . 6
β’ (π β π
β Fin) |
15 | 14 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β π
β Fin) |
16 | | vdwlem4.h |
. . . . . 6
β’ (π β π»:(1...(π Β· (2 Β· π)))βΆπ
) |
17 | 16 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β π»:(1...(π Β· (2 Β· π)))βΆπ
) |
18 | | vdwlem4.f |
. . . . 5
β’ πΉ = (π₯ β (1...π) β¦ (π¦ β (1...π) β¦ (π»β(π¦ + (π Β· ((π₯ β 1) + π)))))) |
19 | 7 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β π β β) |
20 | 6 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β πΊ:(1...π)βΆπ
) |
21 | 3 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β πΎ β
(β€β₯β2)) |
22 | | vdwlem7.a |
. . . . . 6
β’ (π β π΄ β β) |
23 | 22 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β π΄ β β) |
24 | | vdwlem7.d |
. . . . . 6
β’ (π β π· β β) |
25 | 24 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β π· β β) |
26 | | vdwlem7.s |
. . . . . 6
β’ (π β (π΄(APβπΎ)π·) β (β‘πΉ β {πΊ})) |
27 | 26 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β (π΄(APβπΎ)π·) β (β‘πΉ β {πΊ})) |
28 | | simplrl 776 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β π β β) |
29 | | simplrr 777 |
. . . . . 6
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β π β (β βm
(1...π))) |
30 | | nnex 12218 |
. . . . . . 7
β’ β
β V |
31 | | ovex 7442 |
. . . . . . 7
β’
(1...π) β
V |
32 | 30, 31 | elmap 8865 |
. . . . . 6
β’ (π β (β
βm (1...π))
β π:(1...π)βΆβ) |
33 | 29, 32 | sylib 217 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β π:(1...π)βΆβ) |
34 | | simprl 770 |
. . . . . 6
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β βπ β (1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))})) |
35 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π = π β (πβπ) = (πβπ)) |
36 | 35 | oveq2d 7425 |
. . . . . . . . 9
β’ (π = π β (π + (πβπ)) = (π + (πβπ))) |
37 | 36, 35 | oveq12d 7427 |
. . . . . . . 8
β’ (π = π β ((π + (πβπ))(APβπΎ)(πβπ)) = ((π + (πβπ))(APβπΎ)(πβπ))) |
38 | 36 | fveq2d 6896 |
. . . . . . . . . 10
β’ (π = π β (πΊβ(π + (πβπ))) = (πΊβ(π + (πβπ)))) |
39 | 38 | sneqd 4641 |
. . . . . . . . 9
β’ (π = π β {(πΊβ(π + (πβπ)))} = {(πΊβ(π + (πβπ)))}) |
40 | 39 | imaeq2d 6060 |
. . . . . . . 8
β’ (π = π β (β‘πΊ β {(πΊβ(π + (πβπ)))}) = (β‘πΊ β {(πΊβ(π + (πβπ)))})) |
41 | 37, 40 | sseq12d 4016 |
. . . . . . 7
β’ (π = π β (((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β ((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}))) |
42 | 41 | cbvralvw 3235 |
. . . . . 6
β’
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β βπ β (1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))})) |
43 | 34, 42 | sylib 217 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β βπ β (1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))})) |
44 | 38 | cbvmptv 5262 |
. . . . 5
β’ (π β (1...π) β¦ (πΊβ(π + (πβπ)))) = (π β (1...π) β¦ (πΊβ(π + (πβπ)))) |
45 | | simprr 772 |
. . . . 5
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π) |
46 | | eqid 2733 |
. . . . 5
β’ (π + (π Β· ((π΄ + (π β π·)) β 1))) = (π + (π Β· ((π΄ + (π β π·)) β 1))) |
47 | | eqid 2733 |
. . . . 5
β’ (π β (1...(π + 1)) β¦ (if(π = (π + 1), 0, (πβπ)) + (π Β· π·))) = (π β (1...(π + 1)) β¦ (if(π = (π + 1), 0, (πβπ)) + (π Β· π·))) |
48 | 11, 13, 15, 17, 18, 19, 20, 21, 23, 25, 27, 28, 33, 43, 44, 45, 46, 47 | vdwlem6 16919 |
. . . 4
β’ (((π β§ (π β β β§ π β (β βm
(1...π)))) β§
(βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π)) β (β¨(π + 1), πΎβ© PolyAP π» β¨ (πΎ + 1) MonoAP πΊ)) |
49 | 48 | ex 414 |
. . 3
β’ ((π β§ (π β β β§ π β (β βm
(1...π)))) β
((βπ β
(1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π) β (β¨(π + 1), πΎβ© PolyAP π» β¨ (πΎ + 1) MonoAP πΊ))) |
50 | 49 | rexlimdvva 3212 |
. 2
β’ (π β (βπ β β βπ β (β βm
(1...π))(βπ β (1...π)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΊ β {(πΊβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πΊβ(π + (πβπ))))) = π) β (β¨(π + 1), πΎβ© PolyAP π» β¨ (πΎ + 1) MonoAP πΊ))) |
51 | 9, 50 | sylbid 239 |
1
β’ (π β (β¨π, πΎβ© PolyAP πΊ β (β¨(π + 1), πΎβ© PolyAP π» β¨ (πΎ + 1) MonoAP πΊ))) |