Axiom ax-hgprmladder 41702

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	|- E. d e. ( ZZ>= ` 3 ) E. f e. (RePart ` d ) ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = (; 8 9 x. (; 1 0 ^; 2 9 ) ) ) /\ A. i e. ( 0..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. (; 1 0 ^; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) )

Detailed syntax breakdown of Axiom ax-hgprmladder

Step	Hyp	Ref	Expression
1		cc0 9936	. . . . . . 7 class 0
2		vf	. . . . . . . 8 setvar f
3	2	cv 1482	. . . . . . 7 class f
4	1, 3	cfv 5888	. . . . . 6 class ( f ` 0 )
5		c7 11075	. . . . . 6 class 7
6	4, 5	wceq 1483	. . . . 5 wff ( f ` 0 ) = 7
7		c1 9937	. . . . . . 7 class 1
8	7, 3	cfv 5888	. . . . . 6 class ( f ` 1 )
9		c3 11071	. . . . . . 7 class 3
10	7, 9	cdc 11493	. . . . . 6 class ; 1 3
11	8, 10	wceq 1483	. . . . 5 wff ( f ` 1 ) = ; 1 3
12		vd	. . . . . . . 8 setvar d
13	12	cv 1482	. . . . . . 7 class d
14	13, 3	cfv 5888	. . . . . 6 class ( f ` d )
15		c8 11076	. . . . . . . 8 class 8
16		c9 11077	. . . . . . . 8 class 9
17	15, 16	cdc 11493	. . . . . . 7 class ; 8 9
18	7, 1	cdc 11493	. . . . . . . 8 class ; 1 0
19		c2 11070	. . . . . . . . 9 class 2
20	19, 16	cdc 11493	. . . . . . . 8 class ; 2 9
21		cexp 12860	. . . . . . . 8 class ^
22	18, 20, 21	co 6650	. . . . . . 7 class (; 1 0 ^; 2 9 )
23		cmul 9941	. . . . . . 7 class x.
24	17, 22, 23	co 6650	. . . . . 6 class (; 8 9 x. (; 1 0 ^; 2 9 ) )
25	14, 24	wceq 1483	. . . . 5 wff ( f ` d ) = (; 8 9 x. (; 1 0 ^; 2 9 ) )
26	6, 11, 25	w3a 1037	. . . 4 wff ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = (; 8 9 x. (; 1 0 ^; 2 9 ) ) )
27		vi	. . . . . . . . 9 setvar i
28	27	cv 1482	. . . . . . . 8 class i
29	28, 3	cfv 5888	. . . . . . 7 class ( f ` i )
30		cprime 15385	. . . . . . . 8 class Prime
31	19	csn 4177	. . . . . . . 8 class { 2 }
32	30, 31	cdif 3571	. . . . . . 7 class ( Prime \ { 2 } )
33	29, 32	wcel 1990	. . . . . 6 wff ( f ` i ) e. ( Prime \ { 2 } )
34		caddc 9939	. . . . . . . . . 10 class +
35	28, 7, 34	co 6650	. . . . . . . . 9 class ( i + 1 )
36	35, 3	cfv 5888	. . . . . . . 8 class ( f ` ( i + 1 ) )
37		cmin 10266	. . . . . . . 8 class -
38	36, 29, 37	co 6650	. . . . . . 7 class ( ( f ` ( i + 1 ) ) - ( f ` i ) )
39		c4 11072	. . . . . . . . 9 class 4
40	7, 15	cdc 11493	. . . . . . . . . 10 class ; 1 8
41	18, 40, 21	co 6650	. . . . . . . . 9 class (; 1 0 ^; 1 8 )
42	39, 41, 23	co 6650	. . . . . . . 8 class ( 4 x. (; 1 0 ^; 1 8 ) )
43	42, 39, 37	co 6650	. . . . . . 7 class ( ( 4 x. (; 1 0 ^; 1 8 ) ) - 4 )
44		clt 10074	. . . . . . 7 class <
45	38, 43, 44	wbr 4653	. . . . . 6 wff ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. (; 1 0 ^; 1 8 ) ) - 4 )
46	39, 38, 44	wbr 4653	. . . . . 6 wff 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) )
47	33, 45, 46	w3a 1037	. . . . 5 wff ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. (; 1 0 ^; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) )
48		cfzo 12465	. . . . . 6 class ..^
49	1, 13, 48	co 6650	. . . . 5 class ( 0..^ d )
50	47, 27, 49	wral 2912	. . . 4 wff A. i e. ( 0..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. (; 1 0 ^; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) )
51	26, 50	wa 384	. . 3 wff ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = (; 8 9 x. (; 1 0 ^; 2 9 ) ) ) /\ A. i e. ( 0..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. (; 1 0 ^; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) )
52		ciccp 41349	. . . 4 class RePart
53	13, 52	cfv 5888	. . 3 class (RePart ` d )
54	51, 2, 53	wrex 2913	. 2 wff E. f e. (RePart ` d ) ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = (; 8 9 x. (; 1 0 ^; 2 9 ) ) ) /\ A. i e. ( 0..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. (; 1 0 ^; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) )
55		cuz 11687	. . 3 class ZZ>=
56	9, 55	cfv 5888	. 2 class ( ZZ>= ` 3 )
57	54, 12, 56	wrex 2913	1 wff E. d e. ( ZZ>= ` 3 ) E. f e. (RePart ` d ) ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = (; 8 9 x. (; 1 0 ^; 2 9 ) ) ) /\ A. i e. ( 0..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. (; 1 0 ^; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) )

This axiom is referenced by:  tgblthelfgott  41703