Axiom ax-tgoldbachgtOLD 40238

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

Assertion

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

Distinct variable group:   𝑚,𝑛

Detailed syntax breakdown of Axiom ax-tgoldbachgtOLD

Step	Hyp	Ref	Expression
1		vm	. . . . 5 setvar 𝑚
2	1	cv 1474	. . . 4 class 𝑚
3		c10 10955	. . . . 5 class 10
4		c2 10947	. . . . . 6 class 2
5		c7 10952	. . . . . 6 class 7
6	4, 5	cdc 11369	. . . . 5 class ;27
7		cexp 12722	. . . . 5 class ↑
8	3, 6, 7	co 6549	. . . 4 class (10↑;27)
9		cle 9954	. . . 4 class ≤
10	2, 8, 9	wbr 4583	. . 3 wff 𝑚 ≤ (10↑;27)
11		vn	. . . . . . 7 setvar 𝑛
12	11	cv 1474	. . . . . 6 class 𝑛
13		clt 9953	. . . . . 6 class <
14	2, 12, 13	wbr 4583	. . . . 5 wff 𝑚 < 𝑛
15		cgboa 40169	. . . . . 6 class GoldbachOddALTV
16	12, 15	wcel 1977	. . . . 5 wff 𝑛 ∈ GoldbachOddALTV
17	14, 16	wi 4	. . . 4 wff (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOddALTV )
18		codd 40076	. . . 4 class Odd
19	17, 11, 18	wral 2896	. . 3 wff ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOddALTV )
20	10, 19	wa 383	. 2 wff (𝑚 ≤ (10↑;27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOddALTV ))
21		cn 10897	. 2 class ℕ
22	20, 1, 21	wrex 2897	1 wff ∃𝑚 ∈ ℕ (𝑚 ≤ (10↑;27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOddALTV ))

This axiom is referenced by:  tgoldbachOLD  40239