Theorem 0nodd 39914

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

Hypothesis

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

Assertion

Ref	Expression
0nodd	|- 0 e/ O

Distinct variable group:   x, z

Allowed substitution hints:   O( x, z)

Proof of Theorem 0nodd

Step	Hyp	Ref	Expression
1		halfnz 11021	. . . . . . . . . . 11 |- -. ( 1 / 2 ) e. ZZ
2		eleq1 2519	. . . . . . . . . . 11 |- ( ( 1 / 2 ) = -u x -> ( ( 1 / 2 ) e. ZZ <-> -u x e. ZZ ) )
3	1, 2	mtbii 304	. . . . . . . . . 10 |- ( ( 1 / 2 ) = -u x -> -. -u x e. ZZ )
4		znegcl 10979	. . . . . . . . . 10 |- ( x e. ZZ -> -u x e. ZZ )
5	3, 4	nsyl3 123	. . . . . . . . 9 |- ( x e. ZZ -> -. ( 1 / 2 ) = -u x )
6		eqcom 2460	. . . . . . . . 9 |- ( -u x = ( 1 / 2 ) <-> ( 1 / 2 ) = -u x )
7	5, 6	sylnibr 307	. . . . . . . 8 |- ( x e. ZZ -> -. -u x = ( 1 / 2 ) )
8		ax-1cn 9602	. . . . . . . . . . . 12 |- 1 e. CC
9		2cn 10687	. . . . . . . . . . . 12 |- 2 e. CC
10		2ne0 10709	. . . . . . . . . . . 12 |- 2 =/= 0
11		divneg 10309	. . . . . . . . . . . . 13 |- ( ( 1 e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( 1 / 2 ) = ( -u 1 / 2 ) )
12	11	eqcomd 2459	. . . . . . . . . . . 12 |- ( ( 1 e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( -u 1 / 2 ) = -u ( 1 / 2 ) )
13	8, 9, 10, 12	mp3an 1366	. . . . . . . . . . 11 |- ( -u 1 / 2 ) = -u ( 1 / 2 )
14	13	a1i 11	. . . . . . . . . 10 |- ( x e. ZZ -> ( -u 1 / 2 ) = -u ( 1 / 2 ) )
15	14	eqeq1d 2455	. . . . . . . . 9 |- ( x e. ZZ -> ( ( -u 1 / 2 ) = x <-> -u ( 1 / 2 ) = x ) )
16		halfcn 10836	. . . . . . . . . . 11 |- ( 1 / 2 ) e. CC
17	16	a1i 11	. . . . . . . . . 10 |- ( x e. ZZ -> ( 1 / 2 ) e. CC )
18		zcn 10949	. . . . . . . . . 10 |- ( x e. ZZ -> x e. CC )
19	17, 18	negcon1d 9985	. . . . . . . . 9 |- ( x e. ZZ -> ( -u ( 1 / 2 ) = x <-> -u x = ( 1 / 2 ) ) )
20	15, 19	bitrd 257	. . . . . . . 8 |- ( x e. ZZ -> ( ( -u 1 / 2 ) = x <-> -u x = ( 1 / 2 ) ) )
21	7, 20	mtbird 303	. . . . . . 7 |- ( x e. ZZ -> -. ( -u 1 / 2 ) = x )
22		neg1cn 10720	. . . . . . . . 9 |- -u 1 e. CC
23	22	a1i 11	. . . . . . . 8 |- ( x e. ZZ -> -u 1 e. CC )
24		2cnd 10689	. . . . . . . 8 |- ( x e. ZZ -> 2 e. CC )
25	10	a1i 11	. . . . . . . 8 |- ( x e. ZZ -> 2 =/= 0 )
26	23, 18, 24, 25	divmul2d 10423	. . . . . . 7 |- ( x e. ZZ -> ( ( -u 1 / 2 ) = x <-> -u 1 = ( 2 x. x ) ) )
27	21, 26	mtbid 302	. . . . . 6 |- ( x e. ZZ -> -. -u 1 = ( 2 x. x ) )
28		eqcom 2460	. . . . . . . 8 |- ( 0 = ( ( 2 x. x ) + 1 ) <-> ( ( 2 x. x ) + 1 ) = 0 )
29	28	a1i 11	. . . . . . 7 |- ( x e. ZZ -> ( 0 = ( ( 2 x. x ) + 1 ) <-> ( ( 2 x. x ) + 1 ) = 0 ) )
30		0cnd 9641	. . . . . . . 8 |- ( x e. ZZ -> 0 e. CC )
31		1cnd 9664	. . . . . . . 8 |- ( x e. ZZ -> 1 e. CC )
32	24, 18	mulcld 9668	. . . . . . . 8 |- ( x e. ZZ -> ( 2 x. x ) e. CC )
33		subadd2 9884	. . . . . . . . 9 |- ( ( 0 e. CC /\ 1 e. CC /\ ( 2 x. x ) e. CC ) -> ( ( 0 - 1 ) = ( 2 x. x ) <-> ( ( 2 x. x ) + 1 ) = 0 ) )
34	33	bicomd 205	. . . . . . . 8 |- ( ( 0 e. CC /\ 1 e. CC /\ ( 2 x. x ) e. CC ) -> ( ( ( 2 x. x ) + 1 ) = 0 <-> ( 0 - 1 ) = ( 2 x. x ) ) )
35	30, 31, 32, 34	syl3anc 1269	. . . . . . 7 |- ( x e. ZZ -> ( ( ( 2 x. x ) + 1 ) = 0 <-> ( 0 - 1 ) = ( 2 x. x ) ) )
36		df-neg 9868	. . . . . . . . . 10 |- -u 1 = ( 0 - 1 )
37	36	eqcomi 2462	. . . . . . . . 9 |- ( 0 - 1 ) = -u 1
38	37	a1i 11	. . . . . . . 8 |- ( x e. ZZ -> ( 0 - 1 ) = -u 1 )
39	38	eqeq1d 2455	. . . . . . 7 |- ( x e. ZZ -> ( ( 0 - 1 ) = ( 2 x. x ) <-> -u 1 = ( 2 x. x ) ) )
40	29, 35, 39	3bitrd 283	. . . . . 6 |- ( x e. ZZ -> ( 0 = ( ( 2 x. x ) + 1 ) <-> -u 1 = ( 2 x. x ) ) )
41	27, 40	mtbird 303	. . . . 5 |- ( x e. ZZ -> -. 0 = ( ( 2 x. x ) + 1 ) )
42	41	nrex 2844	. . . 4 |- -. E. x e. ZZ 0 = ( ( 2 x. x ) + 1 )
43	42	intnan 926	. . 3 |- -. ( 0 e. ZZ /\ E. x e. ZZ 0 = ( ( 2 x. x ) + 1 ) )
44		eqeq1 2457	. . . . 5 |- ( z = 0 -> ( z = ( ( 2 x. x ) + 1 ) <-> 0 = ( ( 2 x. x ) + 1 ) ) )
45	44	rexbidv 2903	. . . 4 |- ( z = 0 -> ( E. x e. ZZ z = ( ( 2 x. x ) + 1 ) <-> E. x e. ZZ 0 = ( ( 2 x. x ) + 1 ) ) )
46		oddinmgm.e	. . . 4 |- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }
47	45, 46	elrab2 3200	. . 3 |- ( 0 e. O <-> ( 0 e. ZZ /\ E. x e. ZZ 0 = ( ( 2 x. x ) + 1 ) ) )
48	43, 47	mtbir 301	. 2 |- -. 0 e. O
49	48	nelir 2729	1 |- 0 e/ O

Syntax hints:   <-> wb 188   /\ wa 371   /\ w3a 986   = wceq 1446   e. wcel 1889   =/= wne 2624   e/ wnel 2625   E.wrex 2740   {crab 2743  (class class class)co 6295   CCcc 9542   0cc0 9544   1c1 9545   + caddc 9547   x. cmul 9549   - cmin 9865   -ucneg 9866   / cdiv 10276   2c2 10666   ZZcz 10944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-resscn 9601  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-mulcom 9608  ax-addass 9609  ax-mulass 9610  ax-distr 9611  ax-i2m1 9612  ax-1ne0 9613  ax-1rid 9614  ax-rnegex 9615  ax-rrecex 9616  ax-cnre 9617  ax-pre-lttri 9618  ax-pre-lttrn 9619  ax-pre-ltadd 9620  ax-pre-mulgt0 9621

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-pnf 9682  df-mnf 9683  df-xr 9684  df-ltxr 9685  df-le 9686  df-sub 9867  df-neg 9868  df-div 10277  df-nn 10617  df-2 10675  df-n0 10877  df-z 10945

This theorem is referenced by: (None)