Metamath Proof Explorer

Axiom ax-hgprmladder

Description: There is a partition ("ladder") of primes from 7 to 8.8 x 10^30 with parts ("rungs") having lengths of at least 4 and at most N - 4, see section 1.2.2 in Helfgott p. 4. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020) (Revised by AV, 9-Sep-2021)

Ref Expression
Assertion ax-hgprmladder ⊢∃d∈ℤ≥3∃f∈RePart⁡df⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i

Detailed syntax breakdown

Step Hyp Ref Expression
0 vd setvard
1 cuz classℤ≥
2 c3 class3
3 2 1 cfv classℤ≥3
4 vf setvarf
5 ciccp classRePart
6 0 cv setvard
7 6 5 cfv classRePart⁡d
8 4 cv setvarf
9 cc0 class0
10 9 8 cfv classf⁡0
11 c7 class7
12 10 11 wceq wfff⁡0=7
13 c1 class1
14 13 8 cfv classf⁡1
15 13 2 cdc class13
16 14 15 wceq wfff⁡1=13
17 6 8 cfv classf⁡d
18 c8 class8
19 c9 class9
20 18 19 cdc class89
21 cmul class×
22 13 9 cdc class10
23 cexp class^
24 c2 class2
25 24 19 cdc class29
26 22 25 23 co class1029
27 20 26 21 co class89⁢1029
28 17 27 wceq wfff⁡d=89⁢1029
29 12 16 28 w3a wfff⁡0=7∧f⁡1=13∧f⁡d=89⁢1029
30 vi setvari
31 cfzo class..^
32 9 6 31 co class0..^d
33 30 cv setvari
34 33 8 cfv classf⁡i
35 cprime classℙ
36 24 csn class2
37 35 36 cdif classℙ∖2
38 34 37 wcel wfff⁡i∈ℙ∖2
39 caddc class+
40 33 13 39 co classi+1
41 40 8 cfv classf⁡i+1
42 cmin class−
43 41 34 42 co classf⁡i+1−f⁡i
44 clt class<
45 c4 class4
46 13 18 cdc class18
47 22 46 23 co class1018
48 45 47 21 co class4⁢1018
49 48 45 42 co class4⁢1018−4
50 43 49 44 wbr wfff⁡i+1−f⁡i<4⁢1018−4
51 45 43 44 wbr wff4<f⁡i+1−f⁡i
52 38 50 51 w3a wfff⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i
53 52 30 32 wral wff∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i
54 29 53 wa wfff⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i
55 54 4 7 wrex wff∃f∈RePart⁡df⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i
56 55 0 3 wrex wff∃d∈ℤ≥3∃f∈RePart⁡df⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i