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

Axiom ax-bgbltosilva 46088
Description: The binary Goldbach conjecture is valid for all even numbers less than or equal to 4x10^18, see section 2 in [OeSilva] p. 2042. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.)
Assertion
Ref Expression
ax-bgbltosilva ((๐‘ โˆˆ Even โˆง 4 < ๐‘ โˆง ๐‘ โ‰ค (4 ยท (10โ†‘18))) โ†’ ๐‘ โˆˆ GoldbachEven )

Detailed syntax breakdown of Axiom ax-bgbltosilva
StepHypRef Expression
1 cN . . . 4 class ๐‘
2 ceven 45902 . . . 4 class Even
31, 2wcel 2107 . . 3 wff ๐‘ โˆˆ Even
4 c4 12215 . . . 4 class 4
5 clt 11194 . . . 4 class <
64, 1, 5wbr 5106 . . 3 wff 4 < ๐‘
7 c1 11057 . . . . . . 7 class 1
8 cc0 11056 . . . . . . 7 class 0
97, 8cdc 12623 . . . . . 6 class 10
10 c8 12219 . . . . . . 7 class 8
117, 10cdc 12623 . . . . . 6 class 18
12 cexp 13973 . . . . . 6 class โ†‘
139, 11, 12co 7358 . . . . 5 class (10โ†‘18)
14 cmul 11061 . . . . 5 class ยท
154, 13, 14co 7358 . . . 4 class (4 ยท (10โ†‘18))
16 cle 11195 . . . 4 class โ‰ค
171, 15, 16wbr 5106 . . 3 wff ๐‘ โ‰ค (4 ยท (10โ†‘18))
183, 6, 17w3a 1088 . 2 wff (๐‘ โˆˆ Even โˆง 4 < ๐‘ โˆง ๐‘ โ‰ค (4 ยท (10โ†‘18)))
19 cgbe 46023 . . 3 class GoldbachEven
201, 19wcel 2107 . 2 wff ๐‘ โˆˆ GoldbachEven
2118, 20wi 4 1 wff ((๐‘ โˆˆ Even โˆง 4 < ๐‘ โˆง ๐‘ โ‰ค (4 ยท (10โ†‘18))) โ†’ ๐‘ โˆˆ GoldbachEven )
Colors of variables: wff setvar class
This axiom is referenced by:  bgoldbachlt  46091  tgblthelfgott  46093
  Copyright terms: Public domain W3C validator