Step | Hyp | Ref
| Expression |
1 | | cc0 11056 |
. . . . . . 7
class
0 |
2 | | vf |
. . . . . . . 8
setvar π |
3 | 2 | cv 1541 |
. . . . . . 7
class π |
4 | 1, 3 | cfv 6497 |
. . . . . 6
class (πβ0) |
5 | | c7 12218 |
. . . . . 6
class
7 |
6 | 4, 5 | wceq 1542 |
. . . . 5
wff (πβ0) = 7 |
7 | | c1 11057 |
. . . . . . 7
class
1 |
8 | 7, 3 | cfv 6497 |
. . . . . 6
class (πβ1) |
9 | | c3 12214 |
. . . . . . 7
class
3 |
10 | 7, 9 | cdc 12623 |
. . . . . 6
class ;13 |
11 | 8, 10 | wceq 1542 |
. . . . 5
wff (πβ1) = ;13 |
12 | | vd |
. . . . . . . 8
setvar π |
13 | 12 | cv 1541 |
. . . . . . 7
class π |
14 | 13, 3 | cfv 6497 |
. . . . . 6
class (πβπ) |
15 | | c8 12219 |
. . . . . . . 8
class
8 |
16 | | c9 12220 |
. . . . . . . 8
class
9 |
17 | 15, 16 | cdc 12623 |
. . . . . . 7
class ;89 |
18 | 7, 1 | cdc 12623 |
. . . . . . . 8
class ;10 |
19 | | c2 12213 |
. . . . . . . . 9
class
2 |
20 | 19, 16 | cdc 12623 |
. . . . . . . 8
class ;29 |
21 | | cexp 13973 |
. . . . . . . 8
class
β |
22 | 18, 20, 21 | co 7358 |
. . . . . . 7
class (;10β;29) |
23 | | cmul 11061 |
. . . . . . 7
class
Β· |
24 | 17, 22, 23 | co 7358 |
. . . . . 6
class (;89 Β· (;10β;29)) |
25 | 14, 24 | wceq 1542 |
. . . . 5
wff (πβπ) = (;89 Β· (;10β;29)) |
26 | 6, 11, 25 | w3a 1088 |
. . . 4
wff ((πβ0) = 7 β§ (πβ1) = ;13 β§ (πβπ) = (;89 Β· (;10β;29))) |
27 | | vi |
. . . . . . . . 9
setvar π |
28 | 27 | cv 1541 |
. . . . . . . 8
class π |
29 | 28, 3 | cfv 6497 |
. . . . . . 7
class (πβπ) |
30 | | cprime 16552 |
. . . . . . . 8
class
β |
31 | 19 | csn 4587 |
. . . . . . . 8
class
{2} |
32 | 30, 31 | cdif 3908 |
. . . . . . 7
class (β
β {2}) |
33 | 29, 32 | wcel 2107 |
. . . . . 6
wff (πβπ) β (β β
{2}) |
34 | | caddc 11059 |
. . . . . . . . . 10
class
+ |
35 | 28, 7, 34 | co 7358 |
. . . . . . . . 9
class (π + 1) |
36 | 35, 3 | cfv 6497 |
. . . . . . . 8
class (πβ(π + 1)) |
37 | | cmin 11390 |
. . . . . . . 8
class
β |
38 | 36, 29, 37 | co 7358 |
. . . . . . 7
class ((πβ(π + 1)) β (πβπ)) |
39 | | c4 12215 |
. . . . . . . . 9
class
4 |
40 | 7, 15 | cdc 12623 |
. . . . . . . . . 10
class ;18 |
41 | 18, 40, 21 | co 7358 |
. . . . . . . . 9
class (;10β;18) |
42 | 39, 41, 23 | co 7358 |
. . . . . . . 8
class (4
Β· (;10β;18)) |
43 | 42, 39, 37 | co 7358 |
. . . . . . 7
class ((4
Β· (;10β;18)) β 4) |
44 | | clt 11194 |
. . . . . . 7
class
< |
45 | 38, 43, 44 | wbr 5106 |
. . . . . 6
wff ((πβ(π + 1)) β (πβπ)) < ((4 Β· (;10β;18)) β 4) |
46 | 39, 38, 44 | wbr 5106 |
. . . . . 6
wff 4 <
((πβ(π + 1)) β (πβπ)) |
47 | 33, 45, 46 | w3a 1088 |
. . . . 5
wff ((πβπ) β (β β {2}) β§ ((πβ(π + 1)) β (πβπ)) < ((4 Β· (;10β;18)) β 4) β§ 4 < ((πβ(π + 1)) β (πβπ))) |
48 | | cfzo 13573 |
. . . . . 6
class
..^ |
49 | 1, 13, 48 | co 7358 |
. . . . 5
class
(0..^π) |
50 | 47, 27, 49 | wral 3061 |
. . . 4
wff
βπ β
(0..^π)((πβπ) β (β β {2}) β§ ((πβ(π + 1)) β (πβπ)) < ((4 Β· (;10β;18)) β 4) β§ 4 < ((πβ(π + 1)) β (πβπ))) |
51 | 26, 50 | wa 397 |
. . 3
wff (((πβ0) = 7 β§ (πβ1) = ;13 β§ (πβπ) = (;89 Β· (;10β;29))) β§ βπ β (0..^π)((πβπ) β (β β {2}) β§ ((πβ(π + 1)) β (πβπ)) < ((4 Β· (;10β;18)) β 4) β§ 4 < ((πβ(π + 1)) β (πβπ)))) |
52 | | ciccp 45691 |
. . . 4
class
RePart |
53 | 13, 52 | cfv 6497 |
. . 3
class
(RePartβπ) |
54 | 51, 2, 53 | wrex 3070 |
. 2
wff
βπ β
(RePartβπ)(((πβ0) = 7 β§ (πβ1) = ;13 β§ (πβπ) = (;89 Β· (;10β;29))) β§ βπ β (0..^π)((πβπ) β (β β {2}) β§ ((πβ(π + 1)) β (πβπ)) < ((4 Β· (;10β;18)) β 4) β§ 4 < ((πβ(π + 1)) β (πβπ)))) |
55 | | cuz 12768 |
. . 3
class
β€β₯ |
56 | 9, 55 | cfv 6497 |
. 2
class
(β€β₯β3) |
57 | 54, 12, 56 | wrex 3070 |
1
wff
βπ β
(β€β₯β3)βπ β (RePartβπ)(((πβ0) = 7 β§ (πβ1) = ;13 β§ (πβπ) = (;89 Β· (;10β;29))) β§ βπ β (0..^π)((πβπ) β (β β {2}) β§ ((πβ(π + 1)) β (πβπ)) < ((4 Β· (;10β;18)) β 4) β§ 4 < ((πβ(π + 1)) β (πβπ)))) |