Axiom ax-tgoldbachgtOLD 41711

Description: Obsolete version of ax-tgoldbachgt 41699 as of 9-Sep-2021. (Contributed by AV, 2-Aug-2020.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-tgoldbachgtOLD	⊢ ∃𝑚 ∈ ℕ (𝑚 ≤ (10↑;27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ))

Distinct variable group:   𝑚,𝑛

Detailed syntax breakdown of Axiom ax-tgoldbachgtOLD

Step	Hyp	Ref	Expression
1		vm	. . . . 5 setvar 𝑚
2	1	cv 1482	. . . 4 class 𝑚
3		c10 11078	. . . . 5 class 10
4		c2 11070	. . . . . 6 class 2
5		c7 11075	. . . . . 6 class 7
6	4, 5	cdc 11493	. . . . 5 class ;27
7		cexp 12860	. . . . 5 class ↑
8	3, 6, 7	co 6650	. . . 4 class (10↑;27)
9		cle 10075	. . . 4 class ≤
10	2, 8, 9	wbr 4653	. . 3 wff 𝑚 ≤ (10↑;27)
11		vn	. . . . . . 7 setvar 𝑛
12	11	cv 1482	. . . . . 6 class 𝑛
13		clt 10074	. . . . . 6 class <
14	2, 12, 13	wbr 4653	. . . . 5 wff 𝑚 < 𝑛
15		cgbo 41635	. . . . . 6 class GoldbachOdd
16	12, 15	wcel 1990	. . . . 5 wff 𝑛 ∈ GoldbachOdd
17	14, 16	wi 4	. . . 4 wff (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd )
18		codd 41538	. . . 4 class Odd
19	17, 11, 18	wral 2912	. . 3 wff ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd )
20	10, 19	wa 384	. 2 wff (𝑚 ≤ (10↑;27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ))
21		cn 11020	. 2 class ℕ
22	20, 1, 21	wrex 2913	1 wff ∃𝑚 ∈ ℕ (𝑚 ≤ (10↑;27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ))

This axiom is referenced by:  tgoldbachOLD  41712