Step | Hyp | Ref
| Expression |
1 | | vdwlem8.a |
. . . . . . . . . 10
β’ (π β π΄ β β) |
2 | 1 | nncnd 12232 |
. . . . . . . . 9
β’ (π β π΄ β β) |
3 | | vdwlem8.d |
. . . . . . . . . 10
β’ (π β π· β β) |
4 | 3 | nncnd 12232 |
. . . . . . . . 9
β’ (π β π· β β) |
5 | 2, 4 | addcomd 11420 |
. . . . . . . 8
β’ (π β (π΄ + π·) = (π· + π΄)) |
6 | 5 | oveq2d 7427 |
. . . . . . 7
β’ (π β (π β (π΄ + π·)) = (π β (π· + π΄))) |
7 | | vdwlem8.w |
. . . . . . . . 9
β’ (π β π β β) |
8 | 7 | nncnd 12232 |
. . . . . . . 8
β’ (π β π β β) |
9 | 8, 4, 2 | subsub4d 11606 |
. . . . . . 7
β’ (π β ((π β π·) β π΄) = (π β (π· + π΄))) |
10 | 6, 9 | eqtr4d 2773 |
. . . . . 6
β’ (π β (π β (π΄ + π·)) = ((π β π·) β π΄)) |
11 | 10 | oveq2d 7427 |
. . . . 5
β’ (π β ((π΄ + π΄) + (π β (π΄ + π·))) = ((π΄ + π΄) + ((π β π·) β π΄))) |
12 | 8, 4 | subcld 11575 |
. . . . . 6
β’ (π β (π β π·) β β) |
13 | 2, 2, 12 | ppncand 11615 |
. . . . 5
β’ (π β ((π΄ + π΄) + ((π β π·) β π΄)) = (π΄ + (π β π·))) |
14 | 11, 13 | eqtrd 2770 |
. . . 4
β’ (π β ((π΄ + π΄) + (π β (π΄ + π·))) = (π΄ + (π β π·))) |
15 | 1, 1 | nnaddcld 12268 |
. . . . 5
β’ (π β (π΄ + π΄) β β) |
16 | | vdwlem8.s |
. . . . . . . 8
β’ (π β (π΄(APβπΎ)π·) β (β‘πΊ β {πΆ})) |
17 | | cnvimass 6079 |
. . . . . . . . 9
β’ (β‘πΊ β {πΆ}) β dom πΊ |
18 | | fvex 6903 |
. . . . . . . . . 10
β’ (πΉβ(π₯ + π)) β V |
19 | | vdwlem8.g |
. . . . . . . . . 10
β’ πΊ = (π₯ β (1...π) β¦ (πΉβ(π₯ + π))) |
20 | 18, 19 | dmmpti 6693 |
. . . . . . . . 9
β’ dom πΊ = (1...π) |
21 | 17, 20 | sseqtri 4017 |
. . . . . . . 8
β’ (β‘πΊ β {πΆ}) β (1...π) |
22 | 16, 21 | sstrdi 3993 |
. . . . . . 7
β’ (π β (π΄(APβπΎ)π·) β (1...π)) |
23 | | ssun2 4172 |
. . . . . . . . 9
β’ ((π΄ + π·)(APβ(πΎ β 1))π·) β ({π΄} βͺ ((π΄ + π·)(APβ(πΎ β 1))π·)) |
24 | | vdwlem8.k |
. . . . . . . . . . 11
β’ (π β πΎ β
(β€β₯β2)) |
25 | | uz2m1nn 12911 |
. . . . . . . . . . 11
β’ (πΎ β
(β€β₯β2) β (πΎ β 1) β β) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΎ β 1) β β) |
27 | 1, 3 | nnaddcld 12268 |
. . . . . . . . . 10
β’ (π β (π΄ + π·) β β) |
28 | | vdwapid1 16912 |
. . . . . . . . . 10
β’ (((πΎ β 1) β β β§
(π΄ + π·) β β β§ π· β β) β (π΄ + π·) β ((π΄ + π·)(APβ(πΎ β 1))π·)) |
29 | 26, 27, 3, 28 | syl3anc 1369 |
. . . . . . . . 9
β’ (π β (π΄ + π·) β ((π΄ + π·)(APβ(πΎ β 1))π·)) |
30 | 23, 29 | sselid 3979 |
. . . . . . . 8
β’ (π β (π΄ + π·) β ({π΄} βͺ ((π΄ + π·)(APβ(πΎ β 1))π·))) |
31 | | eluz2nn 12872 |
. . . . . . . . . . . . . 14
β’ (πΎ β
(β€β₯β2) β πΎ β β) |
32 | 24, 31 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β πΎ β β) |
33 | 32 | nncnd 12232 |
. . . . . . . . . . . 12
β’ (π β πΎ β β) |
34 | | ax-1cn 11170 |
. . . . . . . . . . . 12
β’ 1 β
β |
35 | | npcan 11473 |
. . . . . . . . . . . 12
β’ ((πΎ β β β§ 1 β
β) β ((πΎ β
1) + 1) = πΎ) |
36 | 33, 34, 35 | sylancl 584 |
. . . . . . . . . . 11
β’ (π β ((πΎ β 1) + 1) = πΎ) |
37 | 36 | fveq2d 6894 |
. . . . . . . . . 10
β’ (π β (APβ((πΎ β 1) + 1)) =
(APβπΎ)) |
38 | 37 | oveqd 7428 |
. . . . . . . . 9
β’ (π β (π΄(APβ((πΎ β 1) + 1))π·) = (π΄(APβπΎ)π·)) |
39 | 26 | nnnn0d 12536 |
. . . . . . . . . 10
β’ (π β (πΎ β 1) β
β0) |
40 | | vdwapun 16911 |
. . . . . . . . . 10
β’ (((πΎ β 1) β
β0 β§ π΄
β β β§ π·
β β) β (π΄(APβ((πΎ β 1) + 1))π·) = ({π΄} βͺ ((π΄ + π·)(APβ(πΎ β 1))π·))) |
41 | 39, 1, 3, 40 | syl3anc 1369 |
. . . . . . . . 9
β’ (π β (π΄(APβ((πΎ β 1) + 1))π·) = ({π΄} βͺ ((π΄ + π·)(APβ(πΎ β 1))π·))) |
42 | 38, 41 | eqtr3d 2772 |
. . . . . . . 8
β’ (π β (π΄(APβπΎ)π·) = ({π΄} βͺ ((π΄ + π·)(APβ(πΎ β 1))π·))) |
43 | 30, 42 | eleqtrrd 2834 |
. . . . . . 7
β’ (π β (π΄ + π·) β (π΄(APβπΎ)π·)) |
44 | 22, 43 | sseldd 3982 |
. . . . . 6
β’ (π β (π΄ + π·) β (1...π)) |
45 | | elfzuz3 13502 |
. . . . . 6
β’ ((π΄ + π·) β (1...π) β π β (β€β₯β(π΄ + π·))) |
46 | | uznn0sub 12865 |
. . . . . 6
β’ (π β
(β€β₯β(π΄ + π·)) β (π β (π΄ + π·)) β
β0) |
47 | 44, 45, 46 | 3syl 18 |
. . . . 5
β’ (π β (π β (π΄ + π·)) β
β0) |
48 | | nnnn0addcl 12506 |
. . . . 5
β’ (((π΄ + π΄) β β β§ (π β (π΄ + π·)) β β0) β
((π΄ + π΄) + (π β (π΄ + π·))) β β) |
49 | 15, 47, 48 | syl2anc 582 |
. . . 4
β’ (π β ((π΄ + π΄) + (π β (π΄ + π·))) β β) |
50 | 14, 49 | eqeltrrd 2832 |
. . 3
β’ (π β (π΄ + (π β π·)) β β) |
51 | | 1nn 12227 |
. . . . . . . 8
β’ 1 β
β |
52 | | f1osng 6873 |
. . . . . . . 8
β’ ((1
β β β§ π·
β β) β {β¨1, π·β©}:{1}β1-1-ontoβ{π·}) |
53 | 51, 3, 52 | sylancr 585 |
. . . . . . 7
β’ (π β {β¨1, π·β©}:{1}β1-1-ontoβ{π·}) |
54 | | f1of 6832 |
. . . . . . 7
β’
({β¨1, π·β©}:{1}β1-1-ontoβ{π·} β {β¨1, π·β©}:{1}βΆ{π·}) |
55 | 53, 54 | syl 17 |
. . . . . 6
β’ (π β {β¨1, π·β©}:{1}βΆ{π·}) |
56 | 3 | snssd 4811 |
. . . . . 6
β’ (π β {π·} β β) |
57 | 55, 56 | fssd 6734 |
. . . . 5
β’ (π β {β¨1, π·β©}:{1}βΆβ) |
58 | | 1z 12596 |
. . . . . . 7
β’ 1 β
β€ |
59 | | fzsn 13547 |
. . . . . . 7
β’ (1 β
β€ β (1...1) = {1}) |
60 | 58, 59 | ax-mp 5 |
. . . . . 6
β’ (1...1) =
{1} |
61 | 60 | feq2i 6708 |
. . . . 5
β’
({β¨1, π·β©}:(1...1)βΆβ β
{β¨1, π·β©}:{1}βΆβ) |
62 | 57, 61 | sylibr 233 |
. . . 4
β’ (π β {β¨1, π·β©}:(1...1)βΆβ) |
63 | | nnex 12222 |
. . . . 5
β’ β
β V |
64 | | ovex 7444 |
. . . . 5
β’ (1...1)
β V |
65 | 63, 64 | elmap 8867 |
. . . 4
β’
({β¨1, π·β©}
β (β βm (1...1)) β {β¨1, π·β©}:(1...1)βΆβ) |
66 | 62, 65 | sylibr 233 |
. . 3
β’ (π β {β¨1, π·β©} β (β
βm (1...1))) |
67 | 1, 7 | nnaddcld 12268 |
. . . . . . . . . . . . . 14
β’ (π β (π΄ + π) β β) |
68 | 67 | adantr 479 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΎ β 1))) β (π΄ + π) β β) |
69 | | elfznn0 13598 |
. . . . . . . . . . . . . 14
β’ (π β (0...(πΎ β 1)) β π β β0) |
70 | 3 | nnnn0d 12536 |
. . . . . . . . . . . . . 14
β’ (π β π· β
β0) |
71 | | nn0mulcl 12512 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π· β
β0) β (π Β· π·) β
β0) |
72 | 69, 70, 71 | syl2anr 595 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΎ β 1))) β (π Β· π·) β
β0) |
73 | | nnnn0addcl 12506 |
. . . . . . . . . . . . 13
β’ (((π΄ + π) β β β§ (π Β· π·) β β0) β ((π΄ + π) + (π Β· π·)) β β) |
74 | 68, 72, 73 | syl2anc 582 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΎ β 1))) β ((π΄ + π) + (π Β· π·)) β β) |
75 | | nnuz 12869 |
. . . . . . . . . . . 12
β’ β =
(β€β₯β1) |
76 | 74, 75 | eleqtrdi 2841 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΎ β 1))) β ((π΄ + π) + (π Β· π·)) β
(β€β₯β1)) |
77 | 16 | adantr 479 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...(πΎ β 1))) β (π΄(APβπΎ)π·) β (β‘πΊ β {πΆ})) |
78 | | eqid 2730 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ + (π Β· π·)) = (π΄ + (π Β· π·)) |
79 | | oveq1 7418 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π Β· π·) = (π Β· π·)) |
80 | 79 | oveq2d 7427 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π΄ + (π Β· π·)) = (π΄ + (π Β· π·))) |
81 | 80 | rspceeqv 3632 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0...(πΎ β 1)) β§ (π΄ + (π Β· π·)) = (π΄ + (π Β· π·))) β βπ β (0...(πΎ β 1))(π΄ + (π Β· π·)) = (π΄ + (π Β· π·))) |
82 | 78, 81 | mpan2 687 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...(πΎ β 1)) β βπ β (0...(πΎ β 1))(π΄ + (π Β· π·)) = (π΄ + (π Β· π·))) |
83 | 32 | nnnn0d 12536 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΎ β
β0) |
84 | | vdwapval 16910 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΎ β β0
β§ π΄ β β
β§ π· β β)
β ((π΄ + (π Β· π·)) β (π΄(APβπΎ)π·) β βπ β (0...(πΎ β 1))(π΄ + (π Β· π·)) = (π΄ + (π Β· π·)))) |
85 | 83, 1, 3, 84 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π΄ + (π Β· π·)) β (π΄(APβπΎ)π·) β βπ β (0...(πΎ β 1))(π΄ + (π Β· π·)) = (π΄ + (π Β· π·)))) |
86 | 85 | biimpar 476 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ βπ β (0...(πΎ β 1))(π΄ + (π Β· π·)) = (π΄ + (π Β· π·))) β (π΄ + (π Β· π·)) β (π΄(APβπΎ)π·)) |
87 | 82, 86 | sylan2 591 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...(πΎ β 1))) β (π΄ + (π Β· π·)) β (π΄(APβπΎ)π·)) |
88 | 77, 87 | sseldd 3982 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...(πΎ β 1))) β (π΄ + (π Β· π·)) β (β‘πΊ β {πΆ})) |
89 | 18, 19 | fnmpti 6692 |
. . . . . . . . . . . . . . . 16
β’ πΊ Fn (1...π) |
90 | | fniniseg 7060 |
. . . . . . . . . . . . . . . 16
β’ (πΊ Fn (1...π) β ((π΄ + (π Β· π·)) β (β‘πΊ β {πΆ}) β ((π΄ + (π Β· π·)) β (1...π) β§ (πΊβ(π΄ + (π Β· π·))) = πΆ))) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ ((π΄ + (π Β· π·)) β (β‘πΊ β {πΆ}) β ((π΄ + (π Β· π·)) β (1...π) β§ (πΊβ(π΄ + (π Β· π·))) = πΆ)) |
92 | 88, 91 | sylib 217 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΎ β 1))) β ((π΄ + (π Β· π·)) β (1...π) β§ (πΊβ(π΄ + (π Β· π·))) = πΆ)) |
93 | 92 | simpld 493 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΎ β 1))) β (π΄ + (π Β· π·)) β (1...π)) |
94 | | elfzuz3 13502 |
. . . . . . . . . . . . 13
β’ ((π΄ + (π Β· π·)) β (1...π) β π β (β€β₯β(π΄ + (π Β· π·)))) |
95 | | eluzelz 12836 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β(π΄ + (π Β· π·))) β π β β€) |
96 | | eluzadd 12855 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β(π΄ + (π Β· π·))) β§ π β β€) β (π + π) β
(β€β₯β((π΄ + (π Β· π·)) + π))) |
97 | 95, 96 | mpdan 683 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β(π΄ + (π Β· π·))) β (π + π) β
(β€β₯β((π΄ + (π Β· π·)) + π))) |
98 | 93, 94, 97 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΎ β 1))) β (π + π) β
(β€β₯β((π΄ + (π Β· π·)) + π))) |
99 | 8 | 2timesd 12459 |
. . . . . . . . . . . . 13
β’ (π β (2 Β· π) = (π + π)) |
100 | 99 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΎ β 1))) β (2 Β· π) = (π + π)) |
101 | 2 | adantr 479 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΎ β 1))) β π΄ β β) |
102 | 8 | adantr 479 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΎ β 1))) β π β β) |
103 | 72 | nn0cnd 12538 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΎ β 1))) β (π Β· π·) β β) |
104 | 101, 102,
103 | add32d 11445 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΎ β 1))) β ((π΄ + π) + (π Β· π·)) = ((π΄ + (π Β· π·)) + π)) |
105 | 104 | fveq2d 6894 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΎ β 1))) β
(β€β₯β((π΄ + π) + (π Β· π·))) = (β€β₯β((π΄ + (π Β· π·)) + π))) |
106 | 98, 100, 105 | 3eltr4d 2846 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΎ β 1))) β (2 Β· π) β
(β€β₯β((π΄ + π) + (π Β· π·)))) |
107 | | elfzuzb 13499 |
. . . . . . . . . . 11
β’ (((π΄ + π) + (π Β· π·)) β (1...(2 Β· π)) β (((π΄ + π) + (π Β· π·)) β (β€β₯β1)
β§ (2 Β· π) β
(β€β₯β((π΄ + π) + (π Β· π·))))) |
108 | 76, 106, 107 | sylanbrc 581 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(πΎ β 1))) β ((π΄ + π) + (π Β· π·)) β (1...(2 Β· π))) |
109 | 104 | fveq2d 6894 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΎ β 1))) β (πΉβ((π΄ + π) + (π Β· π·))) = (πΉβ((π΄ + (π Β· π·)) + π))) |
110 | | fvoveq1 7434 |
. . . . . . . . . . . . 13
β’ (π₯ = (π΄ + (π Β· π·)) β (πΉβ(π₯ + π)) = (πΉβ((π΄ + (π Β· π·)) + π))) |
111 | | fvex 6903 |
. . . . . . . . . . . . 13
β’ (πΉβ((π΄ + (π Β· π·)) + π)) β V |
112 | 110, 19, 111 | fvmpt 6997 |
. . . . . . . . . . . 12
β’ ((π΄ + (π Β· π·)) β (1...π) β (πΊβ(π΄ + (π Β· π·))) = (πΉβ((π΄ + (π Β· π·)) + π))) |
113 | 93, 112 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΎ β 1))) β (πΊβ(π΄ + (π Β· π·))) = (πΉβ((π΄ + (π Β· π·)) + π))) |
114 | 92 | simprd 494 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΎ β 1))) β (πΊβ(π΄ + (π Β· π·))) = πΆ) |
115 | 109, 113,
114 | 3eqtr2d 2776 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(πΎ β 1))) β (πΉβ((π΄ + π) + (π Β· π·))) = πΆ) |
116 | 108, 115 | jca 510 |
. . . . . . . . 9
β’ ((π β§ π β (0...(πΎ β 1))) β (((π΄ + π) + (π Β· π·)) β (1...(2 Β· π)) β§ (πΉβ((π΄ + π) + (π Β· π·))) = πΆ)) |
117 | | eleq1 2819 |
. . . . . . . . . 10
β’ (π₯ = ((π΄ + π) + (π Β· π·)) β (π₯ β (1...(2 Β· π)) β ((π΄ + π) + (π Β· π·)) β (1...(2 Β· π)))) |
118 | | fveqeq2 6899 |
. . . . . . . . . 10
β’ (π₯ = ((π΄ + π) + (π Β· π·)) β ((πΉβπ₯) = πΆ β (πΉβ((π΄ + π) + (π Β· π·))) = πΆ)) |
119 | 117, 118 | anbi12d 629 |
. . . . . . . . 9
β’ (π₯ = ((π΄ + π) + (π Β· π·)) β ((π₯ β (1...(2 Β· π)) β§ (πΉβπ₯) = πΆ) β (((π΄ + π) + (π Β· π·)) β (1...(2 Β· π)) β§ (πΉβ((π΄ + π) + (π Β· π·))) = πΆ))) |
120 | 116, 119 | syl5ibrcom 246 |
. . . . . . . 8
β’ ((π β§ π β (0...(πΎ β 1))) β (π₯ = ((π΄ + π) + (π Β· π·)) β (π₯ β (1...(2 Β· π)) β§ (πΉβπ₯) = πΆ))) |
121 | 120 | rexlimdva 3153 |
. . . . . . 7
β’ (π β (βπ β (0...(πΎ β 1))π₯ = ((π΄ + π) + (π Β· π·)) β (π₯ β (1...(2 Β· π)) β§ (πΉβπ₯) = πΆ))) |
122 | | vdwapval 16910 |
. . . . . . . 8
β’ ((πΎ β β0
β§ (π΄ + π) β β β§ π· β β) β (π₯ β ((π΄ + π)(APβπΎ)π·) β βπ β (0...(πΎ β 1))π₯ = ((π΄ + π) + (π Β· π·)))) |
123 | 83, 67, 3, 122 | syl3anc 1369 |
. . . . . . 7
β’ (π β (π₯ β ((π΄ + π)(APβπΎ)π·) β βπ β (0...(πΎ β 1))π₯ = ((π΄ + π) + (π Β· π·)))) |
124 | | vdwlem8.f |
. . . . . . . 8
β’ (π β πΉ:(1...(2 Β· π))βΆπ
) |
125 | | ffn 6716 |
. . . . . . . 8
β’ (πΉ:(1...(2 Β· π))βΆπ
β πΉ Fn (1...(2 Β· π))) |
126 | | fniniseg 7060 |
. . . . . . . 8
β’ (πΉ Fn (1...(2 Β· π)) β (π₯ β (β‘πΉ β {πΆ}) β (π₯ β (1...(2 Β· π)) β§ (πΉβπ₯) = πΆ))) |
127 | 124, 125,
126 | 3syl 18 |
. . . . . . 7
β’ (π β (π₯ β (β‘πΉ β {πΆ}) β (π₯ β (1...(2 Β· π)) β§ (πΉβπ₯) = πΆ))) |
128 | 121, 123,
127 | 3imtr4d 293 |
. . . . . 6
β’ (π β (π₯ β ((π΄ + π)(APβπΎ)π·) β π₯ β (β‘πΉ β {πΆ}))) |
129 | 128 | ssrdv 3987 |
. . . . 5
β’ (π β ((π΄ + π)(APβπΎ)π·) β (β‘πΉ β {πΆ})) |
130 | | fvsng 7179 |
. . . . . . . . 9
β’ ((1
β β β§ π·
β β) β ({β¨1, π·β©}β1) = π·) |
131 | 51, 3, 130 | sylancr 585 |
. . . . . . . 8
β’ (π β ({β¨1, π·β©}β1) = π·) |
132 | 131 | oveq2d 7427 |
. . . . . . 7
β’ (π β ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)) = ((π΄ + (π β π·)) + π·)) |
133 | 2, 12, 4 | addassd 11240 |
. . . . . . 7
β’ (π β ((π΄ + (π β π·)) + π·) = (π΄ + ((π β π·) + π·))) |
134 | 8, 4 | npcand 11579 |
. . . . . . . 8
β’ (π β ((π β π·) + π·) = π) |
135 | 134 | oveq2d 7427 |
. . . . . . 7
β’ (π β (π΄ + ((π β π·) + π·)) = (π΄ + π)) |
136 | 132, 133,
135 | 3eqtrd 2774 |
. . . . . 6
β’ (π β ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)) = (π΄ + π)) |
137 | 136, 131 | oveq12d 7429 |
. . . . 5
β’ (π β (((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) = ((π΄ + π)(APβπΎ)π·)) |
138 | 136 | fveq2d 6894 |
. . . . . . . 8
β’ (π β (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))) = (πΉβ(π΄ + π))) |
139 | | vdwapid1 16912 |
. . . . . . . . . . . . 13
β’ ((πΎ β β β§ π΄ β β β§ π· β β) β π΄ β (π΄(APβπΎ)π·)) |
140 | 32, 1, 3, 139 | syl3anc 1369 |
. . . . . . . . . . . 12
β’ (π β π΄ β (π΄(APβπΎ)π·)) |
141 | 16, 140 | sseldd 3982 |
. . . . . . . . . . 11
β’ (π β π΄ β (β‘πΊ β {πΆ})) |
142 | | fniniseg 7060 |
. . . . . . . . . . . 12
β’ (πΊ Fn (1...π) β (π΄ β (β‘πΊ β {πΆ}) β (π΄ β (1...π) β§ (πΊβπ΄) = πΆ))) |
143 | 89, 142 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π΄ β (β‘πΊ β {πΆ}) β (π΄ β (1...π) β§ (πΊβπ΄) = πΆ)) |
144 | 141, 143 | sylib 217 |
. . . . . . . . . 10
β’ (π β (π΄ β (1...π) β§ (πΊβπ΄) = πΆ)) |
145 | 144 | simpld 493 |
. . . . . . . . 9
β’ (π β π΄ β (1...π)) |
146 | | fvoveq1 7434 |
. . . . . . . . . 10
β’ (π₯ = π΄ β (πΉβ(π₯ + π)) = (πΉβ(π΄ + π))) |
147 | | fvex 6903 |
. . . . . . . . . 10
β’ (πΉβ(π΄ + π)) β V |
148 | 146, 19, 147 | fvmpt 6997 |
. . . . . . . . 9
β’ (π΄ β (1...π) β (πΊβπ΄) = (πΉβ(π΄ + π))) |
149 | 145, 148 | syl 17 |
. . . . . . . 8
β’ (π β (πΊβπ΄) = (πΉβ(π΄ + π))) |
150 | 144 | simprd 494 |
. . . . . . . 8
β’ (π β (πΊβπ΄) = πΆ) |
151 | 138, 149,
150 | 3eqtr2d 2776 |
. . . . . . 7
β’ (π β (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))) = πΆ) |
152 | 151 | sneqd 4639 |
. . . . . 6
β’ (π β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))} = {πΆ}) |
153 | 152 | imaeq2d 6058 |
. . . . 5
β’ (π β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))}) = (β‘πΉ β {πΆ})) |
154 | 129, 137,
153 | 3sstr4d 4028 |
. . . 4
β’ (π β (((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))})) |
155 | 154 | ralrimivw 3148 |
. . 3
β’ (π β βπ β (1...1)(((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))})) |
156 | 151 | mpteq2dv 5249 |
. . . . . . . 8
β’ (π β (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))) = (π β (1...1) β¦ πΆ)) |
157 | | fconstmpt 5737 |
. . . . . . . 8
β’ ((1...1)
Γ {πΆ}) = (π β (1...1) β¦ πΆ) |
158 | 156, 157 | eqtr4di 2788 |
. . . . . . 7
β’ (π β (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))) = ((1...1) Γ
{πΆ})) |
159 | 158 | rneqd 5936 |
. . . . . 6
β’ (π β ran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))) = ran ((1...1) Γ
{πΆ})) |
160 | | elfz3 13515 |
. . . . . . . 8
β’ (1 β
β€ β 1 β (1...1)) |
161 | | ne0i 4333 |
. . . . . . . 8
β’ (1 β
(1...1) β (1...1) β β
) |
162 | 58, 160, 161 | mp2b 10 |
. . . . . . 7
β’ (1...1)
β β
|
163 | | rnxp 6168 |
. . . . . . 7
β’ ((1...1)
β β
β ran ((1...1) Γ {πΆ}) = {πΆ}) |
164 | 162, 163 | ax-mp 5 |
. . . . . 6
β’ ran
((1...1) Γ {πΆ}) =
{πΆ} |
165 | 159, 164 | eqtrdi 2786 |
. . . . 5
β’ (π β ran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))) = {πΆ}) |
166 | 165 | fveq2d 6894 |
. . . 4
β’ (π β (β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) = (β―β{πΆ})) |
167 | | vdwlem8.c |
. . . . 5
β’ πΆ β V |
168 | | hashsng 14333 |
. . . . 5
β’ (πΆ β V β
(β―β{πΆ}) =
1) |
169 | 167, 168 | ax-mp 5 |
. . . 4
β’
(β―β{πΆ})
= 1 |
170 | 166, 169 | eqtrdi 2786 |
. . 3
β’ (π β (β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) = 1) |
171 | | oveq1 7418 |
. . . . . . . 8
β’ (π = (π΄ + (π β π·)) β (π + (πβπ)) = ((π΄ + (π β π·)) + (πβπ))) |
172 | 171 | oveq1d 7426 |
. . . . . . 7
β’ (π = (π΄ + (π β π·)) β ((π + (πβπ))(APβπΎ)(πβπ)) = (((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ))) |
173 | | fvoveq1 7434 |
. . . . . . . . 9
β’ (π = (π΄ + (π β π·)) β (πΉβ(π + (πβπ))) = (πΉβ((π΄ + (π β π·)) + (πβπ)))) |
174 | 173 | sneqd 4639 |
. . . . . . . 8
β’ (π = (π΄ + (π β π·)) β {(πΉβ(π + (πβπ)))} = {(πΉβ((π΄ + (π β π·)) + (πβπ)))}) |
175 | 174 | imaeq2d 6058 |
. . . . . . 7
β’ (π = (π΄ + (π β π·)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) = (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))})) |
176 | 172, 175 | sseq12d 4014 |
. . . . . 6
β’ (π = (π΄ + (π β π·)) β (((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) β (((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}))) |
177 | 176 | ralbidv 3175 |
. . . . 5
β’ (π = (π΄ + (π β π·)) β (βπ β (1...1)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) β βπ β (1...1)(((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}))) |
178 | 173 | mpteq2dv 5249 |
. . . . . . 7
β’ (π = (π΄ + (π β π·)) β (π β (1...1) β¦ (πΉβ(π + (πβπ)))) = (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ))))) |
179 | 178 | rneqd 5936 |
. . . . . 6
β’ (π = (π΄ + (π β π·)) β ran (π β (1...1) β¦ (πΉβ(π + (πβπ)))) = ran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ))))) |
180 | 179 | fveqeq2d 6898 |
. . . . 5
β’ (π = (π΄ + (π β π·)) β ((β―βran (π β (1...1) β¦ (πΉβ(π + (πβπ))))) = 1 β (β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ))))) = 1)) |
181 | 177, 180 | anbi12d 629 |
. . . 4
β’ (π = (π΄ + (π β π·)) β ((βπ β (1...1)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) β§ (β―βran (π β (1...1) β¦ (πΉβ(π + (πβπ))))) = 1) β (βπ β (1...1)(((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}) β§ (β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ))))) = 1))) |
182 | | fveq1 6889 |
. . . . . . . . . 10
β’ (π = {β¨1, π·β©} β (πβπ) = ({β¨1, π·β©}βπ)) |
183 | | elfz1eq 13516 |
. . . . . . . . . . 11
β’ (π β (1...1) β π = 1) |
184 | 183 | fveq2d 6894 |
. . . . . . . . . 10
β’ (π β (1...1) β
({β¨1, π·β©}βπ) = ({β¨1, π·β©}β1)) |
185 | 182, 184 | sylan9eq 2790 |
. . . . . . . . 9
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β (πβπ) = ({β¨1, π·β©}β1)) |
186 | 185 | oveq2d 7427 |
. . . . . . . 8
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β ((π΄ + (π β π·)) + (πβπ)) = ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))) |
187 | 186, 185 | oveq12d 7429 |
. . . . . . 7
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β (((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) = (((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1))) |
188 | 186 | fveq2d 6894 |
. . . . . . . . 9
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β (πΉβ((π΄ + (π β π·)) + (πβπ))) = (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))) |
189 | 188 | sneqd 4639 |
. . . . . . . 8
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β {(πΉβ((π΄ + (π β π·)) + (πβπ)))} = {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))}) |
190 | 189 | imaeq2d 6058 |
. . . . . . 7
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}) = (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))})) |
191 | 187, 190 | sseq12d 4014 |
. . . . . 6
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β ((((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}) β (((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))}))) |
192 | 191 | ralbidva 3173 |
. . . . 5
β’ (π = {β¨1, π·β©} β (βπ β (1...1)(((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}) β βπ β (1...1)(((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))}))) |
193 | 188 | mpteq2dva 5247 |
. . . . . . 7
β’ (π = {β¨1, π·β©} β (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ)))) = (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) |
194 | 193 | rneqd 5936 |
. . . . . 6
β’ (π = {β¨1, π·β©} β ran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ)))) = ran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) |
195 | 194 | fveqeq2d 6898 |
. . . . 5
β’ (π = {β¨1, π·β©} β ((β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ))))) = 1 β (β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) = 1)) |
196 | 192, 195 | anbi12d 629 |
. . . 4
β’ (π = {β¨1, π·β©} β ((βπ β (1...1)(((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}) β§ (β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ))))) = 1) β (βπ β (1...1)(((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))}) β§
(β―βran (π
β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) = 1))) |
197 | 181, 196 | rspc2ev 3623 |
. . 3
β’ (((π΄ + (π β π·)) β β β§ {β¨1, π·β©} β (β
βm (1...1)) β§ (βπ β (1...1)(((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))}) β§
(β―βran (π
β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) = 1)) β
βπ β β
βπ β (β
βm (1...1))(βπ β (1...1)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) β§ (β―βran (π β (1...1) β¦ (πΉβ(π + (πβπ))))) = 1)) |
198 | 50, 66, 155, 170, 197 | syl112anc 1372 |
. 2
β’ (π β βπ β β βπ β (β βm
(1...1))(βπ β
(1...1)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) β§ (β―βran (π β (1...1) β¦ (πΉβ(π + (πβπ))))) = 1)) |
199 | | ovex 7444 |
. . 3
β’ (1...(2
Β· π)) β
V |
200 | 51 | a1i 11 |
. . 3
β’ (π β 1 β
β) |
201 | | eqid 2730 |
. . 3
β’ (1...1) =
(1...1) |
202 | 199, 83, 124, 200, 201 | vdwpc 16917 |
. 2
β’ (π β (β¨1, πΎβ© PolyAP πΉ β βπ β β βπ β (β βm
(1...1))(βπ β
(1...1)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) β§ (β―βran (π β (1...1) β¦ (πΉβ(π + (πβπ))))) = 1))) |
203 | 198, 202 | mpbird 256 |
1
β’ (π β β¨1, πΎβ© PolyAP πΉ) |