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	⊢ ∃ 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∃ 𝑓 ∈ ( RePart ‘ 𝑑 ) ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = ; 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( ; 8 9 · ( ; 1 0 ↑ ; 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( ; 1 0 ↑ ; 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vd	⊢ 𝑑
1		cuz	⊢ ℤ≥
2		c3	⊢ 3
3	2 1	cfv	⊢ ( ℤ≥ ‘ 3 )
4		vf	⊢ 𝑓
5		ciccp	⊢ RePart
6	0	cv	⊢ 𝑑
7	6 5	cfv	⊢ ( RePart ‘ 𝑑 )
8	4	cv	⊢ 𝑓
9		cc0	⊢ 0
10	9 8	cfv	⊢ ( 𝑓 ‘ 0 )
11		c7	⊢ 7
12	10 11	wceq	⊢ ( 𝑓 ‘ 0 ) = 7
13		c1	⊢ 1
14	13 8	cfv	⊢ ( 𝑓 ‘ 1 )
15	13 2	cdc	⊢ ; 1 3
16	14 15	wceq	⊢ ( 𝑓 ‘ 1 ) = ; 1 3
17	6 8	cfv	⊢ ( 𝑓 ‘ 𝑑 )
18		c8	⊢ 8
19		c9	⊢ 9
20	18 19	cdc	⊢ ; 8 9
21		cmul	⊢ ·
22	13 9	cdc	⊢ ; 1 0
23		cexp	⊢ ↑
24		c2	⊢ 2
25	24 19	cdc	⊢ ; 2 9
26	22 25 23	co	⊢ ( ; 1 0 ↑ ; 2 9 )
27	20 26 21	co	⊢ ( ; 8 9 · ( ; 1 0 ↑ ; 2 9 ) )
28	17 27	wceq	⊢ ( 𝑓 ‘ 𝑑 ) = ( ; 8 9 · ( ; 1 0 ↑ ; 2 9 ) )
29	12 16 28	w3a	⊢ ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = ; 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( ; 8 9 · ( ; 1 0 ↑ ; 2 9 ) ) )
30		vi	⊢ 𝑖
31		cfzo	⊢ ..^
32	9 6 31	co	⊢ ( 0 ..^ 𝑑 )
33	30	cv	⊢ 𝑖
34	33 8	cfv	⊢ ( 𝑓 ‘ 𝑖 )
35		cprime	⊢ ℙ
36	24	csn	⊢ { 2 }
37	35 36	cdif	⊢ ( ℙ ∖ { 2 } )
38	34 37	wcel	⊢ ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } )
39		caddc	⊢ +
40	33 13 39	co	⊢ ( 𝑖 + 1 )
41	40 8	cfv	⊢ ( 𝑓 ‘ ( 𝑖 + 1 ) )
42		cmin	⊢ −
43	41 34 42	co	⊢ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) )
44		clt	⊢ <
45		c4	⊢ 4
46	13 18	cdc	⊢ ; 1 8
47	22 46 23	co	⊢ ( ; 1 0 ↑ ; 1 8 )
48	45 47 21	co	⊢ ( 4 · ( ; 1 0 ↑ ; 1 8 ) )
49	48 45 42	co	⊢ ( ( 4 · ( ; 1 0 ↑ ; 1 8 ) ) − 4 )
50	43 49 44	wbr	⊢ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( ; 1 0 ↑ ; 1 8 ) ) − 4 )
51	45 43 44	wbr	⊢ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) )
52	38 50 51	w3a	⊢ ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( ; 1 0 ↑ ; 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) )
53	52 30 32	wral	⊢ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( ; 1 0 ↑ ; 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) )
54	29 53	wa	⊢ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = ; 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( ; 8 9 · ( ; 1 0 ↑ ; 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( ; 1 0 ↑ ; 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) )
55	54 4 7	wrex	⊢ ∃ 𝑓 ∈ ( RePart ‘ 𝑑 ) ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = ; 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( ; 8 9 · ( ; 1 0 ↑ ; 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( ; 1 0 ↑ ; 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) )
56	55 0 3	wrex	⊢ ∃ 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∃ 𝑓 ∈ ( RePart ‘ 𝑑 ) ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = ; 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( ; 8 9 · ( ; 1 0 ↑ ; 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( ; 1 0 ↑ ; 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) )