Axiom ax-hgprmladder 45154

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.)

Assertion

Ref	Expression
ax-hgprmladder	⊢ ∃𝑑 ∈ (ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))

Detailed syntax breakdown of Axiom ax-hgprmladder

Step	Hyp	Ref	Expression
1		cc0 10802	. . . . . . 7 class 0
2		vf	. . . . . . . 8 setvar 𝑓
3	2	cv 1538	. . . . . . 7 class 𝑓
4	1, 3	cfv 6418	. . . . . 6 class (𝑓‘0)
5		c7 11963	. . . . . 6 class 7
6	4, 5	wceq 1539	. . . . 5 wff (𝑓‘0) = 7
7		c1 10803	. . . . . . 7 class 1
8	7, 3	cfv 6418	. . . . . 6 class (𝑓‘1)
9		c3 11959	. . . . . . 7 class 3
10	7, 9	cdc 12366	. . . . . 6 class ;13
11	8, 10	wceq 1539	. . . . 5 wff (𝑓‘1) = ;13
12		vd	. . . . . . . 8 setvar 𝑑
13	12	cv 1538	. . . . . . 7 class 𝑑
14	13, 3	cfv 6418	. . . . . 6 class (𝑓‘𝑑)
15		c8 11964	. . . . . . . 8 class 8
16		c9 11965	. . . . . . . 8 class 9
17	15, 16	cdc 12366	. . . . . . 7 class ;89
18	7, 1	cdc 12366	. . . . . . . 8 class ;10
19		c2 11958	. . . . . . . . 9 class 2
20	19, 16	cdc 12366	. . . . . . . 8 class ;29
21		cexp 13710	. . . . . . . 8 class ↑
22	18, 20, 21	co 7255	. . . . . . 7 class (;10↑;29)
23		cmul 10807	. . . . . . 7 class ·
24	17, 22, 23	co 7255	. . . . . 6 class (;89 · (;10↑;29))
25	14, 24	wceq 1539	. . . . 5 wff (𝑓‘𝑑) = (;89 · (;10↑;29))
26	6, 11, 25	w3a 1085	. . . 4 wff ((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29)))
27		vi	. . . . . . . . 9 setvar 𝑖
28	27	cv 1538	. . . . . . . 8 class 𝑖
29	28, 3	cfv 6418	. . . . . . 7 class (𝑓‘𝑖)
30		cprime 16304	. . . . . . . 8 class ℙ
31	19	csn 4558	. . . . . . . 8 class {2}
32	30, 31	cdif 3880	. . . . . . 7 class (ℙ ∖ {2})
33	29, 32	wcel 2108	. . . . . 6 wff (𝑓‘𝑖) ∈ (ℙ ∖ {2})
34		caddc 10805	. . . . . . . . . 10 class +
35	28, 7, 34	co 7255	. . . . . . . . 9 class (𝑖 + 1)
36	35, 3	cfv 6418	. . . . . . . 8 class (𝑓‘(𝑖 + 1))
37		cmin 11135	. . . . . . . 8 class −
38	36, 29, 37	co 7255	. . . . . . 7 class ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))
39		c4 11960	. . . . . . . . 9 class 4
40	7, 15	cdc 12366	. . . . . . . . . 10 class ;18
41	18, 40, 21	co 7255	. . . . . . . . 9 class (;10↑;18)
42	39, 41, 23	co 7255	. . . . . . . 8 class (4 · (;10↑;18))
43	42, 39, 37	co 7255	. . . . . . 7 class ((4 · (;10↑;18)) − 4)
44		clt 10940	. . . . . . 7 class <
45	38, 43, 44	wbr 5070	. . . . . 6 wff ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4)
46	39, 38, 44	wbr 5070	. . . . . 6 wff 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))
47	33, 45, 46	w3a 1085	. . . . 5 wff ((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))
48		cfzo 13311	. . . . . 6 class ..^
49	1, 13, 48	co 7255	. . . . 5 class (0..^𝑑)
50	47, 27, 49	wral 3063	. . . 4 wff ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))
51	26, 50	wa 395	. . 3 wff (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))
52		ciccp 44753	. . . 4 class RePart
53	13, 52	cfv 6418	. . 3 class (RePart‘𝑑)
54	51, 2, 53	wrex 3064	. 2 wff ∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))
55		cuz 12511	. . 3 class ℤ≥
56	9, 55	cfv 6418	. 2 class (ℤ≥‘3)
57	54, 12, 56	wrex 3064	1 wff ∃𝑑 ∈ (ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))

This axiom is referenced by:  tgblthelfgott  45155