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

Axiom ax-bgbltosilvaOLD 41024
Description: Obsolete version of ax-bgbltosilva 41017 as of 9-Sep-2021. (Contributed by AV, 3-Aug-2020.) (New usage is discouraged.)
Assertion
Ref Expression
ax-bgbltosilvaOLD ((𝑁 ∈ Even ∧ 4 < 𝑁𝑁 ≤ (4 · (10↑18))) → 𝑁 ∈ GoldbachEven )

Detailed syntax breakdown of Axiom ax-bgbltosilvaOLD
StepHypRef Expression
1 cN . . . 4 class 𝑁
2 ceven 40866 . . . 4 class Even
31, 2wcel 1987 . . 3 wff 𝑁 ∈ Even
4 c4 11032 . . . 4 class 4
5 clt 10034 . . . 4 class <
64, 1, 5wbr 4623 . . 3 wff 4 < 𝑁
7 c10 11038 . . . . . 6 class 10
8 c1 9897 . . . . . . 7 class 1
9 c8 11036 . . . . . . 7 class 8
108, 9cdc 11453 . . . . . 6 class 18
11 cexp 12816 . . . . . 6 class
127, 10, 11co 6615 . . . . 5 class (10↑18)
13 cmul 9901 . . . . 5 class ·
144, 12, 13co 6615 . . . 4 class (4 · (10↑18))
15 cle 10035 . . . 4 class
161, 14, 15wbr 4623 . . 3 wff 𝑁 ≤ (4 · (10↑18))
173, 6, 16w3a 1036 . 2 wff (𝑁 ∈ Even ∧ 4 < 𝑁𝑁 ≤ (4 · (10↑18)))
18 cgbe 40958 . . 3 class GoldbachEven
191, 18wcel 1987 . 2 wff 𝑁 ∈ GoldbachEven
2017, 19wi 4 1 wff ((𝑁 ∈ Even ∧ 4 < 𝑁𝑁 ≤ (4 · (10↑18))) → 𝑁 ∈ GoldbachEven )
Colors of variables: wff setvar class
This axiom is referenced by:  bgoldbachltOLD  41025  tgblthelfgottOLD  41027
  Copyright terms: Public domain W3C validator