Step | Hyp | Ref
| Expression |
1 | | axcaucvg.g |
. . . . 5
β’ πΊ = (π β N β¦
(β©π§ β
R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©]
~Q }, {π’ β£ [β¨π, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©)) |
2 | 1 | a1i 9 |
. . . 4
β’ ((π β§ π½ β N) β πΊ = (π β N β¦
(β©π§ β
R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©]
~Q }, {π’ β£ [β¨π, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©))) |
3 | | opeq1 3779 |
. . . . . . . . . . . . . . . 16
β’ (π = π½ β β¨π, 1oβ© = β¨π½,
1oβ©) |
4 | 3 | eceq1d 6571 |
. . . . . . . . . . . . . . 15
β’ (π = π½ β [β¨π, 1oβ©]
~Q = [β¨π½, 1oβ©]
~Q ) |
5 | 4 | breq2d 4016 |
. . . . . . . . . . . . . 14
β’ (π = π½ β (π <Q [β¨π, 1oβ©]
~Q β π <Q [β¨π½, 1oβ©]
~Q )) |
6 | 5 | abbidv 2295 |
. . . . . . . . . . . . 13
β’ (π = π½ β {π β£ π <Q [β¨π, 1oβ©]
~Q } = {π β£ π <Q [β¨π½, 1oβ©]
~Q }) |
7 | 4 | breq1d 4014 |
. . . . . . . . . . . . . 14
β’ (π = π½ β ([β¨π, 1oβ©]
~Q <Q π’ β [β¨π½, 1oβ©]
~Q <Q π’)) |
8 | 7 | abbidv 2295 |
. . . . . . . . . . . . 13
β’ (π = π½ β {π’ β£ [β¨π, 1oβ©]
~Q <Q π’} = {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}) |
9 | 6, 8 | opeq12d 3787 |
. . . . . . . . . . . 12
β’ (π = π½ β β¨{π β£ π <Q [β¨π, 1oβ©]
~Q }, {π’ β£ [β¨π, 1oβ©]
~Q <Q π’}β© = β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β©) |
10 | 9 | oveq1d 5890 |
. . . . . . . . . . 11
β’ (π = π½ β (β¨{π β£ π <Q [β¨π, 1oβ©]
~Q }, {π’ β£ [β¨π, 1oβ©]
~Q <Q π’}β© +P
1P) = (β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P)) |
11 | 10 | opeq1d 3785 |
. . . . . . . . . 10
β’ (π = π½ β β¨(β¨{π β£ π <Q [β¨π, 1oβ©]
~Q }, {π’ β£ [β¨π, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ© =
β¨(β¨{π β£
π
<Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P),
1Pβ©) |
12 | 11 | eceq1d 6571 |
. . . . . . . . 9
β’ (π = π½ β [β¨(β¨{π β£ π <Q [β¨π, 1oβ©]
~Q }, {π’ β£ [β¨π, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R = [β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R ) |
13 | 12 | opeq1d 3785 |
. . . . . . . 8
β’ (π = π½ β β¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©]
~Q }, {π’ β£ [β¨π, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ© =
β¨[β¨(β¨{π
β£ π
<Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R ,
0Rβ©) |
14 | 13 | fveq2d 5520 |
. . . . . . 7
β’ (π = π½ β (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©]
~Q }, {π’ β£ [β¨π, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R ,
0Rβ©)) |
15 | 14 | eqeq1d 2186 |
. . . . . 6
β’ (π = π½ β ((πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©]
~Q }, {π’ β£ [β¨π, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ© β (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©)) |
16 | 15 | riotabidv 5833 |
. . . . 5
β’ (π = π½ β (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©]
~Q }, {π’ β£ [β¨π, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©) = (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©)) |
17 | 16 | adantl 277 |
. . . 4
β’ (((π β§ π½ β N) β§ π = π½) β (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π, 1oβ©]
~Q }, {π’ β£ [β¨π, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©) = (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©)) |
18 | | simpr 110 |
. . . 4
β’ ((π β§ π½ β N) β π½ β
N) |
19 | | axcaucvg.n |
. . . . 5
β’ π = β©
{π₯ β£ (1 β π₯ β§ βπ¦ β π₯ (π¦ + 1) β π₯)} |
20 | | axcaucvg.f |
. . . . 5
β’ (π β πΉ:πβΆβ) |
21 | 19, 20 | axcaucvglemcl 7894 |
. . . 4
β’ ((π β§ π½ β N) β
(β©π§ β
R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©) β R) |
22 | 2, 17, 18, 21 | fvmptd 5598 |
. . 3
β’ ((π β§ π½ β N) β (πΊβπ½) = (β©π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©)) |
23 | 22 | eqcomd 2183 |
. 2
β’ ((π β§ π½ β N) β
(β©π§ β
R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©) = (πΊβπ½)) |
24 | 22, 21 | eqeltrd 2254 |
. . 3
β’ ((π β§ π½ β N) β (πΊβπ½) β R) |
25 | 20 | adantr 276 |
. . . . . 6
β’ ((π β§ π½ β N) β πΉ:πβΆβ) |
26 | | pitonn 7847 |
. . . . . . . 8
β’ (π½ β N β
β¨[β¨(β¨{π
β£ π
<Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ© β β© {π₯
β£ (1 β π₯ β§
βπ¦ β π₯ (π¦ + 1) β π₯)}) |
27 | 26, 19 | eleqtrrdi 2271 |
. . . . . . 7
β’ (π½ β N β
β¨[β¨(β¨{π
β£ π
<Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ© β π) |
28 | 27 | adantl 277 |
. . . . . 6
β’ ((π β§ π½ β N) β
β¨[β¨(β¨{π
β£ π
<Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ© β π) |
29 | 25, 28 | ffvelcdmd 5653 |
. . . . 5
β’ ((π β§ π½ β N) β (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) β
β) |
30 | | elrealeu 7828 |
. . . . 5
β’ ((πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) β β
β β!π§ β
R β¨π§,
0Rβ© = (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R ,
0Rβ©)) |
31 | 29, 30 | sylib 122 |
. . . 4
β’ ((π β§ π½ β N) β
β!π§ β
R β¨π§,
0Rβ© = (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R ,
0Rβ©)) |
32 | | eqcom 2179 |
. . . . 5
β’
(β¨π§,
0Rβ© = (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) β (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©) |
33 | 32 | reubii 2663 |
. . . 4
β’
(β!π§ β
R β¨π§,
0Rβ© = (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) β
β!π§ β
R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©) |
34 | 31, 33 | sylib 122 |
. . 3
β’ ((π β§ π½ β N) β
β!π§ β
R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©) |
35 | | opeq1 3779 |
. . . . 5
β’ (π§ = (πΊβπ½) β β¨π§, 0Rβ© =
β¨(πΊβπ½),
0Rβ©) |
36 | 35 | eqeq2d 2189 |
. . . 4
β’ (π§ = (πΊβπ½) β ((πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ© β (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨(πΊβπ½),
0Rβ©)) |
37 | 36 | riota2 5853 |
. . 3
β’ (((πΊβπ½) β R β§ β!π§ β R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©) β ((πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨(πΊβπ½), 0Rβ© β
(β©π§ β
R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©) = (πΊβπ½))) |
38 | 24, 34, 37 | syl2anc 411 |
. 2
β’ ((π β§ π½ β N) β ((πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨(πΊβπ½), 0Rβ© β
(β©π§ β
R (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨π§,
0Rβ©) = (πΊβπ½))) |
39 | 23, 38 | mpbird 167 |
1
β’ ((π β§ π½ β N) β (πΉββ¨[β¨(β¨{π β£ π <Q [β¨π½, 1oβ©]
~Q }, {π’ β£ [β¨π½, 1oβ©]
~Q <Q π’}β© +P
1P), 1Pβ©]
~R , 0Rβ©) = β¨(πΊβπ½),
0Rβ©) |