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	|- E. m e. NN ( m <_ ( 10 ^; 2 7 ) /\ A. n e. Odd ( m < n -> n e. GoldbachOdd ) )

Distinct variable group:   m, n

Detailed syntax breakdown of Axiom ax-tgoldbachgtOLD

Step	Hyp	Ref	Expression
1		vm	. . . . 5 setvar m
2	1	cv 1482	. . . 4 class m
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 ; 2 7
7		cexp 12860	. . . . 5 class ^
8	3, 6, 7	co 6650	. . . 4 class ( 10 ^; 2 7 )
9		cle 10075	. . . 4 class <_
10	2, 8, 9	wbr 4653	. . 3 wff m <_ ( 10 ^; 2 7 )
11		vn	. . . . . . 7 setvar n
12	11	cv 1482	. . . . . 6 class n
13		clt 10074	. . . . . 6 class <
14	2, 12, 13	wbr 4653	. . . . 5 wff m < n
15		cgbo 41635	. . . . . 6 class GoldbachOdd
16	12, 15	wcel 1990	. . . . 5 wff n e. GoldbachOdd
17	14, 16	wi 4	. . . 4 wff ( m < n -> n e. GoldbachOdd )
18		codd 41538	. . . 4 class Odd
19	17, 11, 18	wral 2912	. . 3 wff A. n e. Odd ( m < n -> n e. GoldbachOdd )
20	10, 19	wa 384	. 2 wff ( m <_ ( 10 ^; 2 7 ) /\ A. n e. Odd ( m < n -> n e. GoldbachOdd ) )
21		cn 11020	. 2 class NN
22	20, 1, 21	wrex 2913	1 wff E. m e. NN ( m <_ ( 10 ^; 2 7 ) /\ A. n e. Odd ( m < n -> n e. GoldbachOdd ) )

This axiom is referenced by:  tgoldbachOLD  41712