Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . . 6
β’ (π = 0 β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ ((π Dπ πΉ)βπ))β0)) |
2 | | oveq2 7370 |
. . . . . . 7
β’ (π = 0 β (π + π) = (π + 0)) |
3 | 2 | fveq2d 6851 |
. . . . . 6
β’ (π = 0 β ((π Dπ πΉ)β(π + π)) = ((π Dπ πΉ)β(π + 0))) |
4 | 1, 3 | eqeq12d 2753 |
. . . . 5
β’ (π = 0 β (((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π)) β ((π Dπ ((π Dπ πΉ)βπ))β0) = ((π Dπ πΉ)β(π + 0)))) |
5 | 4 | imbi2d 341 |
. . . 4
β’ (π = 0 β ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π))) β (((π β {β, β} β§ πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ ((π Dπ πΉ)βπ))β0) = ((π Dπ πΉ)β(π + 0))))) |
6 | | fveq2 6847 |
. . . . . 6
β’ (π = π β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ ((π Dπ πΉ)βπ))βπ)) |
7 | | oveq2 7370 |
. . . . . . 7
β’ (π = π β (π + π) = (π + π)) |
8 | 7 | fveq2d 6851 |
. . . . . 6
β’ (π = π β ((π Dπ πΉ)β(π + π)) = ((π Dπ πΉ)β(π + π))) |
9 | 6, 8 | eqeq12d 2753 |
. . . . 5
β’ (π = π β (((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π)) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π)))) |
10 | 9 | imbi2d 341 |
. . . 4
β’ (π = π β ((((π β {β, β} β§ πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π))) β (((π β {β, β} β§ πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π))))) |
11 | | fveq2 6847 |
. . . . . 6
β’ (π = (π + 1) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ ((π Dπ πΉ)βπ))β(π + 1))) |
12 | | oveq2 7370 |
. . . . . . 7
β’ (π = (π + 1) β (π + π) = (π + (π + 1))) |
13 | 12 | fveq2d 6851 |
. . . . . 6
β’ (π = (π + 1) β ((π Dπ πΉ)β(π + π)) = ((π Dπ πΉ)β(π + (π + 1)))) |
14 | 11, 13 | eqeq12d 2753 |
. . . . 5
β’ (π = (π + 1) β (((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π)) β ((π Dπ ((π Dπ πΉ)βπ))β(π + 1)) = ((π Dπ πΉ)β(π + (π + 1))))) |
15 | 14 | imbi2d 341 |
. . . 4
β’ (π = (π + 1) β ((((π β {β, β} β§ πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π))) β (((π β {β, β} β§ πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ ((π Dπ πΉ)βπ))β(π + 1)) = ((π Dπ πΉ)β(π + (π + 1)))))) |
16 | | fveq2 6847 |
. . . . . 6
β’ (π = π β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ ((π Dπ πΉ)βπ))βπ)) |
17 | | oveq2 7370 |
. . . . . . 7
β’ (π = π β (π + π) = (π + π)) |
18 | 17 | fveq2d 6851 |
. . . . . 6
β’ (π = π β ((π Dπ πΉ)β(π + π)) = ((π Dπ πΉ)β(π + π))) |
19 | 16, 18 | eqeq12d 2753 |
. . . . 5
β’ (π = π β (((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π)) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π)))) |
20 | 19 | imbi2d 341 |
. . . 4
β’ (π = π β ((((π β {β, β} β§ πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π))) β (((π β {β, β} β§ πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π))))) |
21 | | recnprss 25284 |
. . . . . . 7
β’ (π β {β, β}
β π β
β) |
22 | 21 | ad2antrr 725 |
. . . . . 6
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β π β β) |
23 | | ssidd 3972 |
. . . . . . . . 9
β’ ((π β {β, β} β§
πΉ β (β
βpm π))
β β β β) |
24 | | cnex 11139 |
. . . . . . . . . . 11
β’ β
β V |
25 | | elpm2g 8789 |
. . . . . . . . . . 11
β’ ((β
β V β§ π β
{β, β}) β (πΉ β (β βpm π) β (πΉ:dom πΉβΆβ β§ dom πΉ β π))) |
26 | 24, 25 | mpan 689 |
. . . . . . . . . 10
β’ (π β {β, β}
β (πΉ β (β
βpm π)
β (πΉ:dom πΉβΆβ β§ dom πΉ β π))) |
27 | 26 | simplbda 501 |
. . . . . . . . 9
β’ ((π β {β, β} β§
πΉ β (β
βpm π))
β dom πΉ β π) |
28 | 24 | a1i 11 |
. . . . . . . . 9
β’ ((π β {β, β} β§
πΉ β (β
βpm π))
β β β V) |
29 | | simpl 484 |
. . . . . . . . 9
β’ ((π β {β, β} β§
πΉ β (β
βpm π))
β π β {β,
β}) |
30 | | pmss12g 8814 |
. . . . . . . . 9
β’
(((β β β β§ dom πΉ β π) β§ (β β V β§ π β {β, β}))
β (β βpm dom πΉ) β (β βpm π)) |
31 | 23, 27, 28, 29, 30 | syl22anc 838 |
. . . . . . . 8
β’ ((π β {β, β} β§
πΉ β (β
βpm π))
β (β βpm dom πΉ) β (β βpm π)) |
32 | 31 | adantr 482 |
. . . . . . 7
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β (β βpm dom πΉ) β (β βpm π)) |
33 | | dvnff 25303 |
. . . . . . . 8
β’ ((π β {β, β} β§
πΉ β (β
βpm π))
β (π
Dπ πΉ):β0βΆ(β
βpm dom πΉ)) |
34 | 33 | ffvelcdmda 7040 |
. . . . . . 7
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ πΉ)βπ) β (β βpm dom
πΉ)) |
35 | 32, 34 | sseldd 3950 |
. . . . . 6
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ πΉ)βπ) β (β βpm π)) |
36 | | dvn0 25304 |
. . . . . 6
β’ ((π β β β§ ((π Dπ πΉ)βπ) β (β βpm π)) β ((π Dπ ((π Dπ πΉ)βπ))β0) = ((π Dπ πΉ)βπ)) |
37 | 22, 35, 36 | syl2anc 585 |
. . . . 5
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ ((π Dπ πΉ)βπ))β0) = ((π Dπ πΉ)βπ)) |
38 | | nn0cn 12430 |
. . . . . . . 8
β’ (π β β0
β π β
β) |
39 | 38 | adantl 483 |
. . . . . . 7
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β π β β) |
40 | 39 | addid1d 11362 |
. . . . . 6
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β (π + 0) = π) |
41 | 40 | fveq2d 6851 |
. . . . 5
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ πΉ)β(π + 0)) = ((π Dπ πΉ)βπ)) |
42 | 37, 41 | eqtr4d 2780 |
. . . 4
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ ((π Dπ πΉ)βπ))β0) = ((π Dπ πΉ)β(π + 0))) |
43 | | oveq2 7370 |
. . . . . . 7
β’ (((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π)) β (π D ((π Dπ ((π Dπ πΉ)βπ))βπ)) = (π D ((π Dπ πΉ)β(π + π)))) |
44 | 22 | adantr 482 |
. . . . . . . . 9
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β π β
β) |
45 | 35 | adantr 482 |
. . . . . . . . 9
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β ((π Dπ πΉ)βπ) β (β βpm π)) |
46 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β π β
β0) |
47 | | dvnp1 25305 |
. . . . . . . . 9
β’ ((π β β β§ ((π Dπ πΉ)βπ) β (β βpm π) β§ π β β0) β ((π Dπ ((π Dπ πΉ)βπ))β(π + 1)) = (π D ((π Dπ ((π Dπ πΉ)βπ))βπ))) |
48 | 44, 45, 46, 47 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β ((π Dπ ((π Dπ πΉ)βπ))β(π + 1)) = (π D ((π Dπ ((π Dπ πΉ)βπ))βπ))) |
49 | 39 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β π β
β) |
50 | | nn0cn 12430 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
β) |
51 | 50 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β π β
β) |
52 | | 1cnd 11157 |
. . . . . . . . . . 11
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β 1 β
β) |
53 | 49, 51, 52 | addassd 11184 |
. . . . . . . . . 10
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β ((π + π) + 1) = (π + (π + 1))) |
54 | 53 | fveq2d 6851 |
. . . . . . . . 9
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β ((π Dπ πΉ)β((π + π) + 1)) = ((π Dπ πΉ)β(π + (π + 1)))) |
55 | | simpllr 775 |
. . . . . . . . . 10
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β πΉ β (β
βpm π)) |
56 | | nn0addcl 12455 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π β
β0) β (π + π) β
β0) |
57 | 56 | adantll 713 |
. . . . . . . . . 10
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β (π + π) β
β0) |
58 | | dvnp1 25305 |
. . . . . . . . . 10
β’ ((π β β β§ πΉ β (β
βpm π)
β§ (π + π) β β0)
β ((π
Dπ πΉ)β((π + π) + 1)) = (π D ((π Dπ πΉ)β(π + π)))) |
59 | 44, 55, 57, 58 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β ((π Dπ πΉ)β((π + π) + 1)) = (π D ((π Dπ πΉ)β(π + π)))) |
60 | 54, 59 | eqtr3d 2779 |
. . . . . . . 8
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β ((π Dπ πΉ)β(π + (π + 1))) = (π D ((π Dπ πΉ)β(π + π)))) |
61 | 48, 60 | eqeq12d 2753 |
. . . . . . 7
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β (((π Dπ ((π Dπ πΉ)βπ))β(π + 1)) = ((π Dπ πΉ)β(π + (π + 1))) β (π D ((π Dπ ((π Dπ πΉ)βπ))βπ)) = (π D ((π Dπ πΉ)β(π + π))))) |
62 | 43, 61 | syl5ibr 246 |
. . . . . 6
β’ ((((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β§ π β β0) β (((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π)) β ((π Dπ ((π Dπ πΉ)βπ))β(π + 1)) = ((π Dπ πΉ)β(π + (π + 1))))) |
63 | 62 | expcom 415 |
. . . . 5
β’ (π β β0
β (((π β
{β, β} β§ πΉ
β (β βpm π)) β§ π β β0) β (((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π)) β ((π Dπ ((π Dπ πΉ)βπ))β(π + 1)) = ((π Dπ πΉ)β(π + (π + 1)))))) |
64 | 63 | a2d 29 |
. . . 4
β’ (π β β0
β ((((π β
{β, β} β§ πΉ
β (β βpm π)) β§ π β β0) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π))) β (((π β {β, β} β§ πΉ β (β
βpm π))
β§ π β
β0) β ((π Dπ ((π Dπ πΉ)βπ))β(π + 1)) = ((π Dπ πΉ)β(π + (π + 1)))))) |
65 | 5, 10, 15, 20, 42, 64 | nn0ind 12605 |
. . 3
β’ (π β β0
β (((π β
{β, β} β§ πΉ
β (β βpm π)) β§ π β β0) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π)))) |
66 | 65 | com12 32 |
. 2
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ π β
β0) β (π β β0 β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π)))) |
67 | 66 | impr 456 |
1
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ (π β
β0 β§ π
β β0)) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π))) |