Detailed syntax breakdown of Axiom ax-hgprmladderOLD
Step | Hyp | Ref
| Expression |
1 | | cc0 9815 |
. . . . . . 7
class
0 |
2 | | vf |
. . . . . . . 8
setvar 𝑓 |
3 | 2 | cv 1474 |
. . . . . . 7
class 𝑓 |
4 | 1, 3 | cfv 5804 |
. . . . . 6
class (𝑓‘0) |
5 | | c7 10952 |
. . . . . 6
class
7 |
6 | 4, 5 | wceq 1475 |
. . . . 5
wff (𝑓‘0) = 7 |
7 | | c1 9816 |
. . . . . . 7
class
1 |
8 | 7, 3 | cfv 5804 |
. . . . . 6
class (𝑓‘1) |
9 | | c3 10948 |
. . . . . . 7
class
3 |
10 | 7, 9 | cdc 11369 |
. . . . . 6
class ;13 |
11 | 8, 10 | wceq 1475 |
. . . . 5
wff (𝑓‘1) = ;13 |
12 | | vd |
. . . . . . . 8
setvar 𝑑 |
13 | 12 | cv 1474 |
. . . . . . 7
class 𝑑 |
14 | 13, 3 | cfv 5804 |
. . . . . 6
class (𝑓‘𝑑) |
15 | | c8 10953 |
. . . . . . . 8
class
8 |
16 | | c9 10954 |
. . . . . . . 8
class
9 |
17 | 15, 16 | cdc 11369 |
. . . . . . 7
class ;89 |
18 | | c10 10955 |
. . . . . . . 8
class
10 |
19 | | c2 10947 |
. . . . . . . . 9
class
2 |
20 | 19, 16 | cdc 11369 |
. . . . . . . 8
class ;29 |
21 | | cexp 12722 |
. . . . . . . 8
class
↑ |
22 | 18, 20, 21 | co 6549 |
. . . . . . 7
class
(10↑;29) |
23 | | cmul 9820 |
. . . . . . 7
class
· |
24 | 17, 22, 23 | co 6549 |
. . . . . 6
class (;89 · (10↑;29)) |
25 | 14, 24 | wceq 1475 |
. . . . 5
wff (𝑓‘𝑑) = (;89 · (10↑;29)) |
26 | 6, 11, 25 | w3a 1031 |
. . . 4
wff ((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) |
27 | | vi |
. . . . . . . . 9
setvar 𝑖 |
28 | 27 | cv 1474 |
. . . . . . . 8
class 𝑖 |
29 | 28, 3 | cfv 5804 |
. . . . . . 7
class (𝑓‘𝑖) |
30 | | cprime 15223 |
. . . . . . . 8
class
ℙ |
31 | 19 | csn 4125 |
. . . . . . . 8
class
{2} |
32 | 30, 31 | cdif 3537 |
. . . . . . 7
class (ℙ
∖ {2}) |
33 | 29, 32 | wcel 1977 |
. . . . . 6
wff (𝑓‘𝑖) ∈ (ℙ ∖
{2}) |
34 | | caddc 9818 |
. . . . . . . . . 10
class
+ |
35 | 28, 7, 34 | co 6549 |
. . . . . . . . 9
class (𝑖 + 1) |
36 | 35, 3 | cfv 5804 |
. . . . . . . 8
class (𝑓‘(𝑖 + 1)) |
37 | | cmin 10145 |
. . . . . . . 8
class
− |
38 | 36, 29, 37 | co 6549 |
. . . . . . 7
class ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) |
39 | | c4 10949 |
. . . . . . . . 9
class
4 |
40 | 7, 15 | cdc 11369 |
. . . . . . . . . 10
class ;18 |
41 | 18, 40, 21 | co 6549 |
. . . . . . . . 9
class
(10↑;18) |
42 | 39, 41, 23 | co 6549 |
. . . . . . . 8
class (4
· (10↑;18)) |
43 | 42, 39, 37 | co 6549 |
. . . . . . 7
class ((4
· (10↑;18)) −
4) |
44 | | clt 9953 |
. . . . . . 7
class
< |
45 | 38, 43, 44 | wbr 4583 |
. . . . . 6
wff ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) |
46 | 39, 38, 44 | wbr 4583 |
. . . . . 6
wff 4 <
((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) |
47 | 33, 45, 46 | w3a 1031 |
. . . . 5
wff ((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))) |
48 | | cfzo 12334 |
. . . . . 6
class
..^ |
49 | 1, 13, 48 | co 6549 |
. . . . 5
class
(0..^𝑑) |
50 | 47, 27, 49 | wral 2896 |
. . . 4
wff
∀𝑖 ∈
(0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))) |
51 | 26, 50 | wa 383 |
. . 3
wff (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) |
52 | | ciccp 39951 |
. . . 4
class
RePart |
53 | 13, 52 | cfv 5804 |
. . 3
class
(RePart‘𝑑) |
54 | 51, 2, 53 | wrex 2897 |
. 2
wff
∃𝑓 ∈
(RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) |
55 | | cuz 11563 |
. . 3
class
ℤ≥ |
56 | 9, 55 | cfv 5804 |
. 2
class
(ℤ≥‘3) |
57 | 54, 12, 56 | wrex 2897 |
1
wff
∃𝑑 ∈
(ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) |