Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-hgprmladder Structured version   Visualization version   GIF version

Axiom ax-hgprmladder 46092
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 βˆƒπ‘‘ ∈ (β„€β‰₯β€˜3)βˆƒπ‘“ ∈ (RePartβ€˜π‘‘)(((π‘“β€˜0) = 7 ∧ (π‘“β€˜1) = 13 ∧ (π‘“β€˜π‘‘) = (89 Β· (10↑29))) ∧ βˆ€π‘– ∈ (0..^𝑑)((π‘“β€˜π‘–) ∈ (β„™ βˆ– {2}) ∧ ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–)) < ((4 Β· (10↑18)) βˆ’ 4) ∧ 4 < ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–))))

Detailed syntax breakdown of Axiom ax-hgprmladder
StepHypRef Expression
1 cc0 11056 . . . . . . 7 class 0
2 vf . . . . . . . 8 setvar 𝑓
32cv 1541 . . . . . . 7 class 𝑓
41, 3cfv 6497 . . . . . 6 class (π‘“β€˜0)
5 c7 12218 . . . . . 6 class 7
64, 5wceq 1542 . . . . 5 wff (π‘“β€˜0) = 7
7 c1 11057 . . . . . . 7 class 1
87, 3cfv 6497 . . . . . 6 class (π‘“β€˜1)
9 c3 12214 . . . . . . 7 class 3
107, 9cdc 12623 . . . . . 6 class 13
118, 10wceq 1542 . . . . 5 wff (π‘“β€˜1) = 13
12 vd . . . . . . . 8 setvar 𝑑
1312cv 1541 . . . . . . 7 class 𝑑
1413, 3cfv 6497 . . . . . 6 class (π‘“β€˜π‘‘)
15 c8 12219 . . . . . . . 8 class 8
16 c9 12220 . . . . . . . 8 class 9
1715, 16cdc 12623 . . . . . . 7 class 89
187, 1cdc 12623 . . . . . . . 8 class 10
19 c2 12213 . . . . . . . . 9 class 2
2019, 16cdc 12623 . . . . . . . 8 class 29
21 cexp 13973 . . . . . . . 8 class ↑
2218, 20, 21co 7358 . . . . . . 7 class (10↑29)
23 cmul 11061 . . . . . . 7 class Β·
2417, 22, 23co 7358 . . . . . 6 class (89 Β· (10↑29))
2514, 24wceq 1542 . . . . 5 wff (π‘“β€˜π‘‘) = (89 Β· (10↑29))
266, 11, 25w3a 1088 . . . 4 wff ((π‘“β€˜0) = 7 ∧ (π‘“β€˜1) = 13 ∧ (π‘“β€˜π‘‘) = (89 Β· (10↑29)))
27 vi . . . . . . . . 9 setvar 𝑖
2827cv 1541 . . . . . . . 8 class 𝑖
2928, 3cfv 6497 . . . . . . 7 class (π‘“β€˜π‘–)
30 cprime 16552 . . . . . . . 8 class β„™
3119csn 4587 . . . . . . . 8 class {2}
3230, 31cdif 3908 . . . . . . 7 class (β„™ βˆ– {2})
3329, 32wcel 2107 . . . . . 6 wff (π‘“β€˜π‘–) ∈ (β„™ βˆ– {2})
34 caddc 11059 . . . . . . . . . 10 class +
3528, 7, 34co 7358 . . . . . . . . 9 class (𝑖 + 1)
3635, 3cfv 6497 . . . . . . . 8 class (π‘“β€˜(𝑖 + 1))
37 cmin 11390 . . . . . . . 8 class βˆ’
3836, 29, 37co 7358 . . . . . . 7 class ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–))
39 c4 12215 . . . . . . . . 9 class 4
407, 15cdc 12623 . . . . . . . . . 10 class 18
4118, 40, 21co 7358 . . . . . . . . 9 class (10↑18)
4239, 41, 23co 7358 . . . . . . . 8 class (4 Β· (10↑18))
4342, 39, 37co 7358 . . . . . . 7 class ((4 Β· (10↑18)) βˆ’ 4)
44 clt 11194 . . . . . . 7 class <
4538, 43, 44wbr 5106 . . . . . 6 wff ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–)) < ((4 Β· (10↑18)) βˆ’ 4)
4639, 38, 44wbr 5106 . . . . . 6 wff 4 < ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–))
4733, 45, 46w3a 1088 . . . . 5 wff ((π‘“β€˜π‘–) ∈ (β„™ βˆ– {2}) ∧ ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–)) < ((4 Β· (10↑18)) βˆ’ 4) ∧ 4 < ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–)))
48 cfzo 13573 . . . . . 6 class ..^
491, 13, 48co 7358 . . . . 5 class (0..^𝑑)
5047, 27, 49wral 3061 . . . 4 wff βˆ€π‘– ∈ (0..^𝑑)((π‘“β€˜π‘–) ∈ (β„™ βˆ– {2}) ∧ ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–)) < ((4 Β· (10↑18)) βˆ’ 4) ∧ 4 < ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–)))
5126, 50wa 397 . . 3 wff (((π‘“β€˜0) = 7 ∧ (π‘“β€˜1) = 13 ∧ (π‘“β€˜π‘‘) = (89 Β· (10↑29))) ∧ βˆ€π‘– ∈ (0..^𝑑)((π‘“β€˜π‘–) ∈ (β„™ βˆ– {2}) ∧ ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–)) < ((4 Β· (10↑18)) βˆ’ 4) ∧ 4 < ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–))))
52 ciccp 45691 . . . 4 class RePart
5313, 52cfv 6497 . . 3 class (RePartβ€˜π‘‘)
5451, 2, 53wrex 3070 . 2 wff βˆƒπ‘“ ∈ (RePartβ€˜π‘‘)(((π‘“β€˜0) = 7 ∧ (π‘“β€˜1) = 13 ∧ (π‘“β€˜π‘‘) = (89 Β· (10↑29))) ∧ βˆ€π‘– ∈ (0..^𝑑)((π‘“β€˜π‘–) ∈ (β„™ βˆ– {2}) ∧ ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–)) < ((4 Β· (10↑18)) βˆ’ 4) ∧ 4 < ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–))))
55 cuz 12768 . . 3 class β„€β‰₯
569, 55cfv 6497 . 2 class (β„€β‰₯β€˜3)
5754, 12, 56wrex 3070 1 wff βˆƒπ‘‘ ∈ (β„€β‰₯β€˜3)βˆƒπ‘“ ∈ (RePartβ€˜π‘‘)(((π‘“β€˜0) = 7 ∧ (π‘“β€˜1) = 13 ∧ (π‘“β€˜π‘‘) = (89 Β· (10↑29))) ∧ βˆ€π‘– ∈ (0..^𝑑)((π‘“β€˜π‘–) ∈ (β„™ βˆ– {2}) ∧ ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–)) < ((4 Β· (10↑18)) βˆ’ 4) ∧ 4 < ((π‘“β€˜(𝑖 + 1)) βˆ’ (π‘“β€˜π‘–))))
Colors of variables: wff setvar class
This axiom is referenced by:  tgblthelfgott  46093
  Copyright terms: Public domain W3C validator