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

Step Hyp Ref Expression
0 vd 
 |-  d
1 cuz 
 |-  ZZ>=
2 c3 
 |-  3
3 2 1 cfv 
 |-  ( ZZ>= ` 3 )
4 vf 
 |-  f
5 ciccp 
 |-  RePart
6 0 cv 
 |-  d
7 6 5 cfv 
 |-  ( RePart ` d )
8 4 cv 
 |-  f
9 cc0 
 |-  0
10 9 8 cfv 
 |-  ( f ` 0 )
11 c7 
 |-  7
12 10 11 wceq 
 |-  ( f ` 0 ) = 7
13 c1 
 |-  1
14 13 8 cfv 
 |-  ( f ` 1 )
15 13 2 cdc 
 |-  ; 1 3
16 14 15 wceq 
 |-  ( f ` 1 ) = ; 1 3
17 6 8 cfv 
 |-  ( f ` d )
18 c8 
 |-  8
19 c9 
 |-  9
20 18 19 cdc 
 |-  ; 8 9
21 cmul 
 |-  x.
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 x. ( ; 1 0 ^ ; 2 9 ) )
28 17 27 wceq 
 |-  ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) )
29 12 16 28 w3a 
 |-  ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = ( ; 8 9 x. ( ; 1 0 ^ ; 2 9 ) ) )
30 vi 
 |-  i
31 cfzo 
 |-  ..^
32 9 6 31 co 
 |-  ( 0 ..^ d )
33 30 cv 
 |-  i
34 33 8 cfv 
 |-  ( f ` i )
35 cprime 
 |-  Prime
36 24 csn 
 |-  { 2 }
37 35 36 cdif 
 |-  ( Prime \ { 2 } )
38 34 37 wcel 
 |-  ( f ` i ) e. ( Prime \ { 2 } )
39 caddc 
 |-  +
40 33 13 39 co 
 |-  ( i + 1 )
41 40 8 cfv 
 |-  ( f ` ( i + 1 ) )
42 cmin 
 |-  -
43 41 34 42 co 
 |-  ( ( f ` ( i + 1 ) ) - ( f ` i ) )
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 x. ( ; 1 0 ^ ; 1 8 ) )
49 48 45 42 co 
 |-  ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 )
50 43 49 44 wbr 
 |-  ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 )
51 45 43 44 wbr 
 |-  4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) )
52 38 50 51 w3a 
 |-  ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) )
53 52 30 32 wral 
 |-  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 ) ) )
54 29 53 wa 
 |-  ( ( ( 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 54 4 7 wrex 
 |-  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 ) ) ) )
56 55 0 3 wrex 
 |-  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 ) ) ) )