Theorem 1odd

Description: 1 is an odd integer. (Contributed by AV, 3-Feb-2020)

	Ref	Expression
Hypothesis	oddinmgm.e	|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }
Assertion	1odd	|- 1 e. O

Proof

Step	Hyp	Ref	Expression
1		oddinmgm.e	|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }
2		1z	|- 1 e. ZZ
3		0z	|- 0 e. ZZ
4		id	|- ( 0 e. ZZ -> 0 e. ZZ )
5		oveq2	|- ( x = 0 -> ( 2 x. x ) = ( 2 x. 0 ) )
6		2t0e0	|- ( 2 x. 0 ) = 0
7	5 6	eqtrdi	|- ( x = 0 -> ( 2 x. x ) = 0 )
8	7	oveq1d	|- ( x = 0 -> ( ( 2 x. x ) + 1 ) = ( 0 + 1 ) )
9	8	eqeq2d	|- ( x = 0 -> ( 1 = ( ( 2 x. x ) + 1 ) <-> 1 = ( 0 + 1 ) ) )
10	9	adantl	|- ( ( 0 e. ZZ /\ x = 0 ) -> ( 1 = ( ( 2 x. x ) + 1 ) <-> 1 = ( 0 + 1 ) ) )
11		1e0p1	|- 1 = ( 0 + 1 )
12	11	a1i	|- ( 0 e. ZZ -> 1 = ( 0 + 1 ) )
13	4 10 12	rspcedvd	|- ( 0 e. ZZ -> E. x e. ZZ 1 = ( ( 2 x. x ) + 1 ) )
14	3 13	ax-mp	|- E. x e. ZZ 1 = ( ( 2 x. x ) + 1 )
15		eqeq1	|- ( z = 1 -> ( z = ( ( 2 x. x ) + 1 ) <-> 1 = ( ( 2 x. x ) + 1 ) ) )
16	15	rexbidv	|- ( z = 1 -> ( E. x e. ZZ z = ( ( 2 x. x ) + 1 ) <-> E. x e. ZZ 1 = ( ( 2 x. x ) + 1 ) ) )
17	16 1	elrab2	|- ( 1 e. O <-> ( 1 e. ZZ /\ E. x e. ZZ 1 = ( ( 2 x. x ) + 1 ) ) )
18	2 14 17	mpbir2an	|- 1 e. O