Step | Hyp | Ref
| Expression |
1 | | fveq2 6800 |
. . . . 5
β’ (π₯ = 0 β (πβπ₯) = (πβ0)) |
2 | | id 22 |
. . . . 5
β’ (π₯ = 0 β π₯ = 0) |
3 | 1, 2 | breq12d 5094 |
. . . 4
β’ (π₯ = 0 β ((πβπ₯)πΊπ₯ β (πβ0)πΊ0)) |
4 | 3 | imbi2d 342 |
. . 3
β’ (π₯ = 0 β ((π β (πβπ₯)πΊπ₯) β (π β (πβ0)πΊ0))) |
5 | | fveq2 6800 |
. . . . 5
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
6 | | id 22 |
. . . . 5
β’ (π₯ = π β π₯ = π) |
7 | 5, 6 | breq12d 5094 |
. . . 4
β’ (π₯ = π β ((πβπ₯)πΊπ₯ β (πβπ)πΊπ)) |
8 | 7 | imbi2d 342 |
. . 3
β’ (π₯ = π β ((π β (πβπ₯)πΊπ₯) β (π β (πβπ)πΊπ))) |
9 | | fveq2 6800 |
. . . . 5
β’ (π₯ = (π + 1) β (πβπ₯) = (πβ(π + 1))) |
10 | | id 22 |
. . . . 5
β’ (π₯ = (π + 1) β π₯ = (π + 1)) |
11 | 9, 10 | breq12d 5094 |
. . . 4
β’ (π₯ = (π + 1) β ((πβπ₯)πΊπ₯ β (πβ(π + 1))πΊ(π + 1))) |
12 | 11 | imbi2d 342 |
. . 3
β’ (π₯ = (π + 1) β ((π β (πβπ₯)πΊπ₯) β (π β (πβ(π + 1))πΊ(π + 1)))) |
13 | | fveq2 6800 |
. . . . 5
β’ (π₯ = π΄ β (πβπ₯) = (πβπ΄)) |
14 | | id 22 |
. . . . 5
β’ (π₯ = π΄ β π₯ = π΄) |
15 | 13, 14 | breq12d 5094 |
. . . 4
β’ (π₯ = π΄ β ((πβπ₯)πΊπ₯ β (πβπ΄)πΊπ΄)) |
16 | 15 | imbi2d 342 |
. . 3
β’ (π₯ = π΄ β ((π β (πβπ₯)πΊπ₯) β (π β (πβπ΄)πΊπ΄))) |
17 | | heibor.11 |
. . . . . . 7
β’ π = seq0(π, (π β β0 β¦ if(π = 0, πΆ, (π β 1)))) |
18 | 17 | fveq1i 6801 |
. . . . . 6
β’ (πβ0) = (seq0(π, (π β β0 β¦ if(π = 0, πΆ, (π β 1))))β0) |
19 | | 0z 12372 |
. . . . . . 7
β’ 0 β
β€ |
20 | | seq1 13776 |
. . . . . . 7
β’ (0 β
β€ β (seq0(π,
(π β
β0 β¦ if(π = 0, πΆ, (π β 1))))β0) = ((π β β0
β¦ if(π = 0, πΆ, (π β 1)))β0)) |
21 | 19, 20 | ax-mp 5 |
. . . . . 6
β’
(seq0(π, (π β β0
β¦ if(π = 0, πΆ, (π β 1))))β0) = ((π β β0
β¦ if(π = 0, πΆ, (π β 1)))β0) |
22 | 18, 21 | eqtri 2764 |
. . . . 5
β’ (πβ0) = ((π β β0 β¦ if(π = 0, πΆ, (π β 1)))β0) |
23 | | 0nn0 12290 |
. . . . . 6
β’ 0 β
β0 |
24 | | heibor.10 |
. . . . . . 7
β’ (π β πΆπΊ0) |
25 | | heibor.4 |
. . . . . . . . 9
β’ πΊ = {β¨π¦, πβ© β£ (π β β0 β§ π¦ β (πΉβπ) β§ (π¦π΅π) β πΎ)} |
26 | 25 | relopabiv 5738 |
. . . . . . . 8
β’ Rel πΊ |
27 | 26 | brrelex1i 5650 |
. . . . . . 7
β’ (πΆπΊ0 β πΆ β V) |
28 | 24, 27 | syl 17 |
. . . . . 6
β’ (π β πΆ β V) |
29 | | iftrue 4471 |
. . . . . . 7
β’ (π = 0 β if(π = 0, πΆ, (π β 1)) = πΆ) |
30 | | eqid 2736 |
. . . . . . 7
β’ (π β β0
β¦ if(π = 0, πΆ, (π β 1))) = (π β β0 β¦ if(π = 0, πΆ, (π β 1))) |
31 | 29, 30 | fvmptg 6901 |
. . . . . 6
β’ ((0
β β0 β§ πΆ β V) β ((π β β0 β¦ if(π = 0, πΆ, (π β 1)))β0) = πΆ) |
32 | 23, 28, 31 | sylancr 588 |
. . . . 5
β’ (π β ((π β β0 β¦ if(π = 0, πΆ, (π β 1)))β0) = πΆ) |
33 | 22, 32 | eqtrid 2788 |
. . . 4
β’ (π β (πβ0) = πΆ) |
34 | 33, 24 | eqbrtrd 5103 |
. . 3
β’ (π β (πβ0)πΊ0) |
35 | | df-br 5082 |
. . . . . 6
β’ ((πβπ)πΊπ β β¨(πβπ), πβ© β πΊ) |
36 | | heibor.9 |
. . . . . . 7
β’ (π β βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ)) |
37 | | fveq2 6800 |
. . . . . . . . . . 11
β’ (π₯ = β¨(πβπ), πβ© β (πβπ₯) = (πββ¨(πβπ), πβ©)) |
38 | | df-ov 7306 |
. . . . . . . . . . 11
β’ ((πβπ)ππ) = (πββ¨(πβπ), πβ©) |
39 | 37, 38 | eqtr4di 2794 |
. . . . . . . . . 10
β’ (π₯ = β¨(πβπ), πβ© β (πβπ₯) = ((πβπ)ππ)) |
40 | | fvex 6813 |
. . . . . . . . . . . 12
β’ (πβπ) β V |
41 | | vex 3441 |
. . . . . . . . . . . 12
β’ π β V |
42 | 40, 41 | op2ndd 7870 |
. . . . . . . . . . 11
β’ (π₯ = β¨(πβπ), πβ© β (2nd βπ₯) = π) |
43 | 42 | oveq1d 7318 |
. . . . . . . . . 10
β’ (π₯ = β¨(πβπ), πβ© β ((2nd βπ₯) + 1) = (π + 1)) |
44 | 39, 43 | breq12d 5094 |
. . . . . . . . 9
β’ (π₯ = β¨(πβπ), πβ© β ((πβπ₯)πΊ((2nd βπ₯) + 1) β ((πβπ)ππ)πΊ(π + 1))) |
45 | | fveq2 6800 |
. . . . . . . . . . . 12
β’ (π₯ = β¨(πβπ), πβ© β (π΅βπ₯) = (π΅ββ¨(πβπ), πβ©)) |
46 | | df-ov 7306 |
. . . . . . . . . . . 12
β’ ((πβπ)π΅π) = (π΅ββ¨(πβπ), πβ©) |
47 | 45, 46 | eqtr4di 2794 |
. . . . . . . . . . 11
β’ (π₯ = β¨(πβπ), πβ© β (π΅βπ₯) = ((πβπ)π΅π)) |
48 | 39, 43 | oveq12d 7321 |
. . . . . . . . . . 11
β’ (π₯ = β¨(πβπ), πβ© β ((πβπ₯)π΅((2nd βπ₯) + 1)) = (((πβπ)ππ)π΅(π + 1))) |
49 | 47, 48 | ineq12d 4153 |
. . . . . . . . . 10
β’ (π₯ = β¨(πβπ), πβ© β ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) = (((πβπ)π΅π) β© (((πβπ)ππ)π΅(π + 1)))) |
50 | 49 | eleq1d 2821 |
. . . . . . . . 9
β’ (π₯ = β¨(πβπ), πβ© β (((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ β (((πβπ)π΅π) β© (((πβπ)ππ)π΅(π + 1))) β πΎ)) |
51 | 44, 50 | anbi12d 632 |
. . . . . . . 8
β’ (π₯ = β¨(πβπ), πβ© β (((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ) β (((πβπ)ππ)πΊ(π + 1) β§ (((πβπ)π΅π) β© (((πβπ)ππ)π΅(π + 1))) β πΎ))) |
52 | 51 | rspccv 3563 |
. . . . . . 7
β’
(βπ₯ β
πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ) β (β¨(πβπ), πβ© β πΊ β (((πβπ)ππ)πΊ(π + 1) β§ (((πβπ)π΅π) β© (((πβπ)ππ)π΅(π + 1))) β πΎ))) |
53 | 36, 52 | syl 17 |
. . . . . 6
β’ (π β (β¨(πβπ), πβ© β πΊ β (((πβπ)ππ)πΊ(π + 1) β§ (((πβπ)π΅π) β© (((πβπ)ππ)π΅(π + 1))) β πΎ))) |
54 | 35, 53 | syl5bi 243 |
. . . . 5
β’ (π β ((πβπ)πΊπ β (((πβπ)ππ)πΊ(π + 1) β§ (((πβπ)π΅π) β© (((πβπ)ππ)π΅(π + 1))) β πΎ))) |
55 | | seqp1 13778 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β0) β (seq0(π, (π β β0 β¦ if(π = 0, πΆ, (π β 1))))β(π + 1)) = ((seq0(π, (π β β0 β¦ if(π = 0, πΆ, (π β 1))))βπ)π((π β β0 β¦ if(π = 0, πΆ, (π β 1)))β(π + 1)))) |
56 | | nn0uz 12662 |
. . . . . . . . . . 11
β’
β0 = (β€β₯β0) |
57 | 55, 56 | eleq2s 2855 |
. . . . . . . . . 10
β’ (π β β0
β (seq0(π, (π β β0
β¦ if(π = 0, πΆ, (π β 1))))β(π + 1)) = ((seq0(π, (π β β0 β¦ if(π = 0, πΆ, (π β 1))))βπ)π((π β β0 β¦ if(π = 0, πΆ, (π β 1)))β(π + 1)))) |
58 | 17 | fveq1i 6801 |
. . . . . . . . . 10
β’ (πβ(π + 1)) = (seq0(π, (π β β0 β¦ if(π = 0, πΆ, (π β 1))))β(π + 1)) |
59 | 17 | fveq1i 6801 |
. . . . . . . . . . 11
β’ (πβπ) = (seq0(π, (π β β0 β¦ if(π = 0, πΆ, (π β 1))))βπ) |
60 | 59 | oveq1i 7313 |
. . . . . . . . . 10
β’ ((πβπ)π((π β β0 β¦ if(π = 0, πΆ, (π β 1)))β(π + 1))) = ((seq0(π, (π β β0 β¦ if(π = 0, πΆ, (π β 1))))βπ)π((π β β0 β¦ if(π = 0, πΆ, (π β 1)))β(π + 1))) |
61 | 57, 58, 60 | 3eqtr4g 2801 |
. . . . . . . . 9
β’ (π β β0
β (πβ(π + 1)) = ((πβπ)π((π β β0 β¦ if(π = 0, πΆ, (π β 1)))β(π + 1)))) |
62 | | eqeq1 2740 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β (π = 0 β (π + 1) = 0)) |
63 | | oveq1 7310 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β (π β 1) = ((π + 1) β 1)) |
64 | 62, 63 | ifbieq2d 4491 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β if(π = 0, πΆ, (π β 1)) = if((π + 1) = 0, πΆ, ((π + 1) β 1))) |
65 | | peano2nn0 12315 |
. . . . . . . . . . . 12
β’ (π β β0
β (π + 1) β
β0) |
66 | | nn0p1nn 12314 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (π + 1) β
β) |
67 | | nnne0 12049 |
. . . . . . . . . . . . . . 15
β’ ((π + 1) β β β
(π + 1) β
0) |
68 | 67 | neneqd 2946 |
. . . . . . . . . . . . . 14
β’ ((π + 1) β β β
Β¬ (π + 1) =
0) |
69 | | iffalse 4474 |
. . . . . . . . . . . . . 14
β’ (Β¬
(π + 1) = 0 β
if((π + 1) = 0, πΆ, ((π + 1) β 1)) = ((π + 1) β 1)) |
70 | 66, 68, 69 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β β0
β if((π + 1) = 0,
πΆ, ((π + 1) β 1)) = ((π + 1) β 1)) |
71 | | ovex 7336 |
. . . . . . . . . . . . 13
β’ ((π + 1) β 1) β
V |
72 | 70, 71 | eqeltrdi 2845 |
. . . . . . . . . . . 12
β’ (π β β0
β if((π + 1) = 0,
πΆ, ((π + 1) β 1)) β V) |
73 | 30, 64, 65, 72 | fvmptd3 6926 |
. . . . . . . . . . 11
β’ (π β β0
β ((π β
β0 β¦ if(π = 0, πΆ, (π β 1)))β(π + 1)) = if((π + 1) = 0, πΆ, ((π + 1) β 1))) |
74 | | nn0cn 12285 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
β) |
75 | | ax-1cn 10971 |
. . . . . . . . . . . 12
β’ 1 β
β |
76 | | pncan 11269 |
. . . . . . . . . . . 12
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
77 | 74, 75, 76 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β β0
β ((π + 1) β 1)
= π) |
78 | 73, 70, 77 | 3eqtrd 2780 |
. . . . . . . . . 10
β’ (π β β0
β ((π β
β0 β¦ if(π = 0, πΆ, (π β 1)))β(π + 1)) = π) |
79 | 78 | oveq2d 7319 |
. . . . . . . . 9
β’ (π β β0
β ((πβπ)π((π β β0 β¦ if(π = 0, πΆ, (π β 1)))β(π + 1))) = ((πβπ)ππ)) |
80 | 61, 79 | eqtrd 2776 |
. . . . . . . 8
β’ (π β β0
β (πβ(π + 1)) = ((πβπ)ππ)) |
81 | 80 | breq1d 5091 |
. . . . . . 7
β’ (π β β0
β ((πβ(π + 1))πΊ(π + 1) β ((πβπ)ππ)πΊ(π + 1))) |
82 | 81 | biimprd 249 |
. . . . . 6
β’ (π β β0
β (((πβπ)ππ)πΊ(π + 1) β (πβ(π + 1))πΊ(π + 1))) |
83 | 82 | adantrd 493 |
. . . . 5
β’ (π β β0
β ((((πβπ)ππ)πΊ(π + 1) β§ (((πβπ)π΅π) β© (((πβπ)ππ)π΅(π + 1))) β πΎ) β (πβ(π + 1))πΊ(π + 1))) |
84 | 54, 83 | syl9r 78 |
. . . 4
β’ (π β β0
β (π β ((πβπ)πΊπ β (πβ(π + 1))πΊ(π + 1)))) |
85 | 84 | a2d 29 |
. . 3
β’ (π β β0
β ((π β (πβπ)πΊπ) β (π β (πβ(π + 1))πΊ(π + 1)))) |
86 | 4, 8, 12, 16, 34, 85 | nn0ind 12457 |
. 2
β’ (π΄ β β0
β (π β (πβπ΄)πΊπ΄)) |
87 | 86 | impcom 409 |
1
β’ ((π β§ π΄ β β0) β (πβπ΄)πΊπ΄) |