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	$$⊢\exists d\in {\mathbb{Z}}_{\ge 3}\exists f\in \mathrm{RePart}\left(d\right)\left(\left(f\left(0\right)=7\wedge f\left(1\right)=13\wedge f\left(d\right)=89{10}^{29}\right)\wedge \forall i\in \left(0..^d\right)\left(f\left(i\right)\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\wedge f\left(i+1\right)-f\left(i\right)<4{10}^{18}-4\wedge 4<f\left(i+1\right)-f\left(i\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vd	$$setvard$$
1		cuz	$$class{\mathbb{Z}}_{\ge }$$
2		c3	$$class3$$
3	2 1	cfv	$$class{\mathbb{Z}}_{\ge 3}$$
4		vf	$$setvarf$$
5		ciccp	$$class\mathrm{RePart}$$
6	0	cv	$$setvard$$
7	6 5	cfv	$$class\mathrm{RePart}\left(d\right)$$
8	4	cv	$$setvarf$$
9		cc0	$$class0$$
10	9 8	cfv	$$classf\left(0\right)$$
11		c7	$$class7$$
12	10 11	wceq	$$wfff\left(0\right)=7$$
13		c1	$$class1$$
14	13 8	cfv	$$classf\left(1\right)$$
15	13 2	cdc	$$class13$$
16	14 15	wceq	$$wfff\left(1\right)=13$$
17	6 8	cfv	$$classf\left(d\right)$$
18		c8	$$class8$$
19		c9	$$class9$$
20	18 19	cdc	$$class89$$
21		cmul	$$class\times$$
22	13 9	cdc	$$class10$$
23		cexp	$$class^$$
24		c2	$$class2$$
25	24 19	cdc	$$class29$$
26	22 25 23	co	$$class{10}^{29}$$
27	20 26 21	co	$$class89{10}^{29}$$
28	17 27	wceq	$$wfff\left(d\right)=89{10}^{29}$$
29	12 16 28	w3a	$$wff\left(f\left(0\right)=7\wedge f\left(1\right)=13\wedge f\left(d\right)=89{10}^{29}\right)$$
30		vi	$$setvari$$
31		cfzo	$$class..^$$
32	9 6 31	co	$$class\left(0..^d\right)$$
33	30	cv	$$setvari$$
34	33 8	cfv	$$classf\left(i\right)$$
35		cprime	$$class\mathbb{P}$$
36	24	csn	$$class\left\{2\right\}$$
37	35 36	cdif	$$class\left(\mathbb{P}\setminus \left\{2\right\}\right)$$
38	34 37	wcel	$$wfff\left(i\right)\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
39		caddc	$$class+$$
40	33 13 39	co	$$class\left(i+1\right)$$
41	40 8	cfv	$$classf\left(i+1\right)$$
42		cmin	$$class-$$
43	41 34 42	co	$$class\left(f\left(i+1\right)-f\left(i\right)\right)$$
44		clt	$$class<$$
45		c4	$$class4$$
46	13 18	cdc	$$class18$$
47	22 46 23	co	$$class{10}^{18}$$
48	45 47 21	co	$$class4{10}^{18}$$
49	48 45 42	co	$$class\left(4{10}^{18}-4\right)$$
50	43 49 44	wbr	$$wfff\left(i+1\right)-f\left(i\right)<4{10}^{18}-4$$
51	45 43 44	wbr	$$wff4<f\left(i+1\right)-f\left(i\right)$$
52	38 50 51	w3a	$$wff\left(f\left(i\right)\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\wedge f\left(i+1\right)-f\left(i\right)<4{10}^{18}-4\wedge 4<f\left(i+1\right)-f\left(i\right)\right)$$
53	52 30 32	wral	$$wff\forall i\in \left(0..^d\right)\left(f\left(i\right)\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\wedge f\left(i+1\right)-f\left(i\right)<4{10}^{18}-4\wedge 4<f\left(i+1\right)-f\left(i\right)\right)$$
54	29 53	wa	$$wff\left(\left(f\left(0\right)=7\wedge f\left(1\right)=13\wedge f\left(d\right)=89{10}^{29}\right)\wedge \forall i\in \left(0..^d\right)\left(f\left(i\right)\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\wedge f\left(i+1\right)-f\left(i\right)<4{10}^{18}-4\wedge 4<f\left(i+1\right)-f\left(i\right)\right)\right)$$
55	54 4 7	wrex	$$wff\exists f\in \mathrm{RePart}\left(d\right)\left(\left(f\left(0\right)=7\wedge f\left(1\right)=13\wedge f\left(d\right)=89{10}^{29}\right)\wedge \forall i\in \left(0..^d\right)\left(f\left(i\right)\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\wedge f\left(i+1\right)-f\left(i\right)<4{10}^{18}-4\wedge 4<f\left(i+1\right)-f\left(i\right)\right)\right)$$
56	55 0 3	wrex	$$wff\exists d\in {\mathbb{Z}}_{\ge 3}\exists f\in \mathrm{RePart}\left(d\right)\left(\left(f\left(0\right)=7\wedge f\left(1\right)=13\wedge f\left(d\right)=89{10}^{29}\right)\wedge \forall i\in \left(0..^d\right)\left(f\left(i\right)\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\wedge f\left(i+1\right)-f\left(i\right)<4{10}^{18}-4\wedge 4<f\left(i+1\right)-f\left(i\right)\right)\right)$$