This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∃ 𝑑 ∈ ( ℤ≥ ‘ 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 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) )