Step | Hyp | Ref
| Expression |
1 | | smuval.n |
. . . . 5
β’ (π β π β
β0) |
2 | | nn0uz 12812 |
. . . . 5
β’
β0 = (β€β₯β0) |
3 | 1, 2 | eleqtrdi 2848 |
. . . 4
β’ (π β π β
(β€β₯β0)) |
4 | | seqp1 13928 |
. . . 4
β’ (π β
(β€β₯β0) β (seq0((π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β
, (π β 1))))β(π + 1)) = ((seq0((π β π«
β0, π
β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β
, (π β 1))))βπ)(π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))((π β β0 β¦ if(π = 0, β
, (π β 1)))β(π + 1)))) |
5 | 3, 4 | syl 17 |
. . 3
β’ (π β (seq0((π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β
, (π β 1))))β(π + 1)) = ((seq0((π β π«
β0, π
β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β
, (π β 1))))βπ)(π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))((π β β0 β¦ if(π = 0, β
, (π β 1)))β(π + 1)))) |
6 | | smuval.p |
. . . 4
β’ π = seq0((π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β
, (π β 1)))) |
7 | 6 | fveq1i 6848 |
. . 3
β’ (πβ(π + 1)) = (seq0((π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β
, (π β 1))))β(π + 1)) |
8 | 6 | fveq1i 6848 |
. . . 4
β’ (πβπ) = (seq0((π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β
, (π β 1))))βπ) |
9 | 8 | oveq1i 7372 |
. . 3
β’ ((πβπ)(π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))((π β β0 β¦ if(π = 0, β
, (π β 1)))β(π + 1))) = ((seq0((π β π«
β0, π
β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β
, (π β 1))))βπ)(π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))((π β β0 β¦ if(π = 0, β
, (π β 1)))β(π + 1))) |
10 | 5, 7, 9 | 3eqtr4g 2802 |
. 2
β’ (π β (πβ(π + 1)) = ((πβπ)(π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))((π β β0 β¦ if(π = 0, β
, (π β 1)))β(π + 1)))) |
11 | | 1nn0 12436 |
. . . . . . 7
β’ 1 β
β0 |
12 | 11 | a1i 11 |
. . . . . 6
β’ (π β 1 β
β0) |
13 | 1, 12 | nn0addcld 12484 |
. . . . 5
β’ (π β (π + 1) β
β0) |
14 | | eqeq1 2741 |
. . . . . . 7
β’ (π = (π + 1) β (π = 0 β (π + 1) = 0)) |
15 | | oveq1 7369 |
. . . . . . 7
β’ (π = (π + 1) β (π β 1) = ((π + 1) β 1)) |
16 | 14, 15 | ifbieq2d 4517 |
. . . . . 6
β’ (π = (π + 1) β if(π = 0, β
, (π β 1)) = if((π + 1) = 0, β
, ((π + 1) β 1))) |
17 | | eqid 2737 |
. . . . . 6
β’ (π β β0
β¦ if(π = 0, β
,
(π β 1))) = (π β β0
β¦ if(π = 0, β
,
(π β
1))) |
18 | | 0ex 5269 |
. . . . . . 7
β’ β
β V |
19 | | ovex 7395 |
. . . . . . 7
β’ ((π + 1) β 1) β
V |
20 | 18, 19 | ifex 4541 |
. . . . . 6
β’ if((π + 1) = 0, β
, ((π + 1) β 1)) β
V |
21 | 16, 17, 20 | fvmpt 6953 |
. . . . 5
β’ ((π + 1) β β0
β ((π β
β0 β¦ if(π = 0, β
, (π β 1)))β(π + 1)) = if((π + 1) = 0, β
, ((π + 1) β 1))) |
22 | 13, 21 | syl 17 |
. . . 4
β’ (π β ((π β β0 β¦ if(π = 0, β
, (π β 1)))β(π + 1)) = if((π + 1) = 0, β
, ((π + 1) β 1))) |
23 | | nn0p1nn 12459 |
. . . . . . 7
β’ (π β β0
β (π + 1) β
β) |
24 | 1, 23 | syl 17 |
. . . . . 6
β’ (π β (π + 1) β β) |
25 | 24 | nnne0d 12210 |
. . . . 5
β’ (π β (π + 1) β 0) |
26 | | ifnefalse 4503 |
. . . . 5
β’ ((π + 1) β 0 β if((π + 1) = 0, β
, ((π + 1) β 1)) = ((π + 1) β
1)) |
27 | 25, 26 | syl 17 |
. . . 4
β’ (π β if((π + 1) = 0, β
, ((π + 1) β 1)) = ((π + 1) β 1)) |
28 | 1 | nn0cnd 12482 |
. . . . 5
β’ (π β π β β) |
29 | 12 | nn0cnd 12482 |
. . . . 5
β’ (π β 1 β
β) |
30 | 28, 29 | pncand 11520 |
. . . 4
β’ (π β ((π + 1) β 1) = π) |
31 | 22, 27, 30 | 3eqtrd 2781 |
. . 3
β’ (π β ((π β β0 β¦ if(π = 0, β
, (π β 1)))β(π + 1)) = π) |
32 | 31 | oveq2d 7378 |
. 2
β’ (π β ((πβπ)(π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))((π β β0 β¦ if(π = 0, β
, (π β 1)))β(π + 1))) = ((πβπ)(π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))π)) |
33 | | smuval.a |
. . . . 5
β’ (π β π΄ β
β0) |
34 | | smuval.b |
. . . . 5
β’ (π β π΅ β
β0) |
35 | 33, 34, 6 | smupf 16365 |
. . . 4
β’ (π β π:β0βΆπ«
β0) |
36 | 35, 1 | ffvelcdmd 7041 |
. . 3
β’ (π β (πβπ) β π«
β0) |
37 | | simpl 484 |
. . . . 5
β’ ((π₯ = (πβπ) β§ π¦ = π) β π₯ = (πβπ)) |
38 | | simpr 486 |
. . . . . . . . 9
β’ ((π₯ = (πβπ) β§ π¦ = π) β π¦ = π) |
39 | 38 | eleq1d 2823 |
. . . . . . . 8
β’ ((π₯ = (πβπ) β§ π¦ = π) β (π¦ β π΄ β π β π΄)) |
40 | 38 | oveq2d 7378 |
. . . . . . . . 9
β’ ((π₯ = (πβπ) β§ π¦ = π) β (π β π¦) = (π β π)) |
41 | 40 | eleq1d 2823 |
. . . . . . . 8
β’ ((π₯ = (πβπ) β§ π¦ = π) β ((π β π¦) β π΅ β (π β π) β π΅)) |
42 | 39, 41 | anbi12d 632 |
. . . . . . 7
β’ ((π₯ = (πβπ) β§ π¦ = π) β ((π¦ β π΄ β§ (π β π¦) β π΅) β (π β π΄ β§ (π β π) β π΅))) |
43 | 42 | rabbidv 3418 |
. . . . . 6
β’ ((π₯ = (πβπ) β§ π¦ = π) β {π β β0 β£ (π¦ β π΄ β§ (π β π¦) β π΅)} = {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) |
44 | | oveq1 7369 |
. . . . . . . . 9
β’ (π = π β (π β π) = (π β π)) |
45 | 44 | eleq1d 2823 |
. . . . . . . 8
β’ (π = π β ((π β π) β π΅ β (π β π) β π΅)) |
46 | 45 | anbi2d 630 |
. . . . . . 7
β’ (π = π β ((π β π΄ β§ (π β π) β π΅) β (π β π΄ β§ (π β π) β π΅))) |
47 | 46 | cbvrabv 3420 |
. . . . . 6
β’ {π β β0
β£ (π β π΄ β§ (π β π) β π΅)} = {π β β0 β£ (π β π΄ β§ (π β π) β π΅)} |
48 | 43, 47 | eqtrdi 2793 |
. . . . 5
β’ ((π₯ = (πβπ) β§ π¦ = π) β {π β β0 β£ (π¦ β π΄ β§ (π β π¦) β π΅)} = {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) |
49 | 37, 48 | oveq12d 7380 |
. . . 4
β’ ((π₯ = (πβπ) β§ π¦ = π) β (π₯ sadd {π β β0 β£ (π¦ β π΄ β§ (π β π¦) β π΅)}) = ((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})) |
50 | | oveq1 7369 |
. . . . 5
β’ (π = π₯ β (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) = (π₯ sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})) |
51 | | eleq1w 2821 |
. . . . . . . . 9
β’ (π = π¦ β (π β π΄ β π¦ β π΄)) |
52 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π¦ β (π β π) = (π β π¦)) |
53 | 52 | eleq1d 2823 |
. . . . . . . . 9
β’ (π = π¦ β ((π β π) β π΅ β (π β π¦) β π΅)) |
54 | 51, 53 | anbi12d 632 |
. . . . . . . 8
β’ (π = π¦ β ((π β π΄ β§ (π β π) β π΅) β (π¦ β π΄ β§ (π β π¦) β π΅))) |
55 | 54 | rabbidv 3418 |
. . . . . . 7
β’ (π = π¦ β {π β β0 β£ (π β π΄ β§ (π β π) β π΅)} = {π β β0 β£ (π¦ β π΄ β§ (π β π¦) β π΅)}) |
56 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π = π β (π β π¦) = (π β π¦)) |
57 | 56 | eleq1d 2823 |
. . . . . . . . 9
β’ (π = π β ((π β π¦) β π΅ β (π β π¦) β π΅)) |
58 | 57 | anbi2d 630 |
. . . . . . . 8
β’ (π = π β ((π¦ β π΄ β§ (π β π¦) β π΅) β (π¦ β π΄ β§ (π β π¦) β π΅))) |
59 | 58 | cbvrabv 3420 |
. . . . . . 7
β’ {π β β0
β£ (π¦ β π΄ β§ (π β π¦) β π΅)} = {π β β0 β£ (π¦ β π΄ β§ (π β π¦) β π΅)} |
60 | 55, 59 | eqtr4di 2795 |
. . . . . 6
β’ (π = π¦ β {π β β0 β£ (π β π΄ β§ (π β π) β π΅)} = {π β β0 β£ (π¦ β π΄ β§ (π β π¦) β π΅)}) |
61 | 60 | oveq2d 7378 |
. . . . 5
β’ (π = π¦ β (π₯ sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) = (π₯ sadd {π β β0 β£ (π¦ β π΄ β§ (π β π¦) β π΅)})) |
62 | 50, 61 | cbvmpov 7457 |
. . . 4
β’ (π β π«
β0, π
β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})) = (π₯ β π« β0, π¦ β β0
β¦ (π₯ sadd {π β β0
β£ (π¦ β π΄ β§ (π β π¦) β π΅)})) |
63 | | ovex 7395 |
. . . 4
β’ ((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) β V |
64 | 49, 62, 63 | ovmpoa 7515 |
. . 3
β’ (((πβπ) β π« β0 β§
π β
β0) β ((πβπ)(π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))π) = ((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})) |
65 | 36, 1, 64 | syl2anc 585 |
. 2
β’ (π β ((πβπ)(π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)}))π) = ((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})) |
66 | 10, 32, 65 | 3eqtrd 2781 |
1
β’ (π β (πβ(π + 1)) = ((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})) |