Theorem 2nodd

Description: 2 is not 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	2nodd	|- 2 e/ O

Proof

Step	Hyp	Ref	Expression
1		oddinmgm.e	|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }
2		halfnz	|- -. ( 1 / 2 ) e. ZZ
3		eleq1	|- ( ( 1 / 2 ) = x -> ( ( 1 / 2 ) e. ZZ <-> x e. ZZ ) )
4	2 3	mtbii	|- ( ( 1 / 2 ) = x -> -. x e. ZZ )
5	4	con2i	|- ( x e. ZZ -> -. ( 1 / 2 ) = x )
6		1cnd	|- ( x e. ZZ -> 1 e. CC )
7		zcn	|- ( x e. ZZ -> x e. CC )
8		2cnd	|- ( x e. ZZ -> 2 e. CC )
9		2ne0	|- 2 =/= 0
10	9	a1i	|- ( x e. ZZ -> 2 =/= 0 )
11	6 7 8 10	divmul2d	|- ( x e. ZZ -> ( ( 1 / 2 ) = x <-> 1 = ( 2 x. x ) ) )
12	5 11	mtbid	|- ( x e. ZZ -> -. 1 = ( 2 x. x ) )
13		eqcom	|- ( 2 = ( ( 2 x. x ) + 1 ) <-> ( ( 2 x. x ) + 1 ) = 2 )
14	13	a1i	|- ( x e. ZZ -> ( 2 = ( ( 2 x. x ) + 1 ) <-> ( ( 2 x. x ) + 1 ) = 2 ) )
15	8 7	mulcld	|- ( x e. ZZ -> ( 2 x. x ) e. CC )
16		subadd2	|- ( ( 2 e. CC /\ 1 e. CC /\ ( 2 x. x ) e. CC ) -> ( ( 2 - 1 ) = ( 2 x. x ) <-> ( ( 2 x. x ) + 1 ) = 2 ) )
17	16	bicomd	|- ( ( 2 e. CC /\ 1 e. CC /\ ( 2 x. x ) e. CC ) -> ( ( ( 2 x. x ) + 1 ) = 2 <-> ( 2 - 1 ) = ( 2 x. x ) ) )
18	8 6 15 17	syl3anc	|- ( x e. ZZ -> ( ( ( 2 x. x ) + 1 ) = 2 <-> ( 2 - 1 ) = ( 2 x. x ) ) )
19		2m1e1	|- ( 2 - 1 ) = 1
20	19	a1i	|- ( x e. ZZ -> ( 2 - 1 ) = 1 )
21	20	eqeq1d	|- ( x e. ZZ -> ( ( 2 - 1 ) = ( 2 x. x ) <-> 1 = ( 2 x. x ) ) )
22	14 18 21	3bitrd	|- ( x e. ZZ -> ( 2 = ( ( 2 x. x ) + 1 ) <-> 1 = ( 2 x. x ) ) )
23	12 22	mtbird	|- ( x e. ZZ -> -. 2 = ( ( 2 x. x ) + 1 ) )
24	23	nrex	|- -. E. x e. ZZ 2 = ( ( 2 x. x ) + 1 )
25	24	intnan	|- -. ( 2 e. ZZ /\ E. x e. ZZ 2 = ( ( 2 x. x ) + 1 ) )
26		eqeq1	|- ( z = 2 -> ( z = ( ( 2 x. x ) + 1 ) <-> 2 = ( ( 2 x. x ) + 1 ) ) )
27	26	rexbidv	|- ( z = 2 -> ( E. x e. ZZ z = ( ( 2 x. x ) + 1 ) <-> E. x e. ZZ 2 = ( ( 2 x. x ) + 1 ) ) )
28	27 1	elrab2	|- ( 2 e. O <-> ( 2 e. ZZ /\ E. x e. ZZ 2 = ( ( 2 x. x ) + 1 ) ) )
29	25 28	mtbir	|- -. 2 e. O
30	29	nelir	|- 2 e/ O