Axiom ax-bgbltosilvaOLD 40233

Description: Obsolete version of ax-bgbltosilva 40226 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

Step	Hyp	Ref	Expression
1		cN	. . . 4 class 𝑁
2		ceven 40075	. . . 4 class Even
3	1, 2	wcel 1977	. . 3 wff 𝑁 ∈ Even
4		c4 10949	. . . 4 class 4
5		clt 9953	. . . 4 class <
6	4, 1, 5	wbr 4583	. . 3 wff 4 < 𝑁
7		c10 10955	. . . . . 6 class 10
8		c1 9816	. . . . . . 7 class 1
9		c8 10953	. . . . . . 7 class 8
10	8, 9	cdc 11369	. . . . . 6 class ;18
11		cexp 12722	. . . . . 6 class ↑
12	7, 10, 11	co 6549	. . . . 5 class (10↑;18)
13		cmul 9820	. . . . 5 class ·
14	4, 12, 13	co 6549	. . . 4 class (4 · (10↑;18))
15		cle 9954	. . . 4 class ≤
16	1, 14, 15	wbr 4583	. . 3 wff 𝑁 ≤ (4 · (10↑;18))
17	3, 6, 16	w3a 1031	. 2 wff (𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (10↑;18)))
18		cgbe 40167	. . 3 class GoldbachEven
19	1, 18	wcel 1977	. 2 wff 𝑁 ∈ GoldbachEven
20	17, 19	wi 4	1 wff ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (10↑;18))) → 𝑁 ∈ GoldbachEven )

This axiom is referenced by:  bgoldbachltOLD  40234  tgblthelfgottOLD  40236