Theorem zeot 6201

Description: An integer is even or odd.

Assertion

Ref	Expression
zeot	⊢ (N ∈ ℤ → ((N / 2) ∈ ℤ ⋁ ((N + 1) / 2) ∈ ℤ))

Proof of Theorem zeot

Step	Hyp	Ref	Expression
1		elz 6139	. . 3 ⊢ (N ∈ ℤ ↔ (N ∈ ℝ ⋀ (N = 0 ⋁ N ∈ ℕ ⋁ -N ∈ ℕ)))
2		opreq1 3974	. . . . . . 7 ⊢ (N = 0 → (N / 2) = (0 / 2))
3		2cn 5982	. . . . . . . . 9 ⊢ 2 ∈ ℂ
4		2ne0 5992	. . . . . . . . 9 ⊢ 2 ≠ 0
5	3, 4	div0 5772	. . . . . . . 8 ⊢ (0 / 2) = 0
6		0z 6148	. . . . . . . 8 ⊢ 0 ∈ ℤ
7	5, 6	eqeltr 1547	. . . . . . 7 ⊢ (0 / 2) ∈ ℤ
8	2, 7	syl6eqel 1559	. . . . . 6 ⊢ (N = 0 → (N / 2) ∈ ℤ)
9	8	pm2.24d 105	. . . . 5 ⊢ (N = 0 → (¬ (N / 2) ∈ ℤ → ((N + 1) / 2) ∈ ℤ))
10	9	adantl 390	. . . 4 ⊢ ((N ∈ ℝ ⋀ N = 0) → (¬ (N / 2) ∈ ℤ → ((N + 1) / 2) ∈ ℤ))
11		nneot 6200	. . . . . . . . 9 ⊢ (N ∈ ℕ → ((N / 2) ∈ ℕ ↔ ¬ ((N + 1) / 2) ∈ ℕ))
12	11	biimprd 154	. . . . . . . 8 ⊢ (N ∈ ℕ → (¬ ((N + 1) / 2) ∈ ℕ → (N / 2) ∈ ℕ))
13	12	con1d 93	. . . . . . 7 ⊢ (N ∈ ℕ → (¬ (N / 2) ∈ ℕ → ((N + 1) / 2) ∈ ℕ))
14		nnzt 6155	. . . . . . . 8 ⊢ ((N / 2) ∈ ℕ → (N / 2) ∈ ℤ)
15	14	con3i 98	. . . . . . 7 ⊢ (¬ (N / 2) ∈ ℤ → ¬ (N / 2) ∈ ℕ)
16	13, 15	syl5 21	. . . . . 6 ⊢ (N ∈ ℕ → (¬ (N / 2) ∈ ℤ → ((N + 1) / 2) ∈ ℕ))
17		nnzt 6155	. . . . . 6 ⊢ (((N + 1) / 2) ∈ ℕ → ((N + 1) / 2) ∈ ℤ)
18	16, 17	syl6 22	. . . . 5 ⊢ (N ∈ ℕ → (¬ (N / 2) ∈ ℤ → ((N + 1) / 2) ∈ ℤ))
19	18	adantl 390	. . . 4 ⊢ ((N ∈ ℝ ⋀ N ∈ ℕ) → (¬ (N / 2) ∈ ℤ → ((N + 1) / 2) ∈ ℤ))
20		recnt 5325	. . . . . . . . . . 11 ⊢ (N ∈ ℝ → N ∈ ℂ)
21		divnegt 5775	. . . . . . . . . . . 12 ⊢ ((N ∈ ℂ ⋀ 2 ∈ ℂ ⋀ 2 ≠ 0) → -(N / 2) = (-N / 2))
22	3, 4, 21	mp3an23 910	. . . . . . . . . . 11 ⊢ (N ∈ ℂ → -(N / 2) = (-N / 2))
23	20, 22	syl 10	. . . . . . . . . 10 ⊢ (N ∈ ℝ → -(N / 2) = (-N / 2))
24	23	eleq1d 1543	. . . . . . . . 9 ⊢ (N ∈ ℝ → (-(N / 2) ∈ ℕ ↔ (-N / 2) ∈ ℕ))
25		nnnegz 6140	. . . . . . . . 9 ⊢ (-(N / 2) ∈ ℕ → --(N / 2) ∈ ℤ)
26	24, 25	syl6bir 215	. . . . . . . 8 ⊢ (N ∈ ℝ → ((-N / 2) ∈ ℕ → --(N / 2) ∈ ℤ))
27		halfclt 6035	. . . . . . . . . 10 ⊢ (N ∈ ℂ → (N / 2) ∈ ℂ)
28		negnegt 5405	. . . . . . . . . 10 ⊢ ((N / 2) ∈ ℂ → --(N / 2) = (N / 2))
29	20, 27, 28	3syl 20	. . . . . . . . 9 ⊢ (N ∈ ℝ → --(N / 2) = (N / 2))
30	29	eleq1d 1543	. . . . . . . 8 ⊢ (N ∈ ℝ → (--(N / 2) ∈ ℤ ↔ (N / 2) ∈ ℤ))
31	26, 30	sylibd 202	. . . . . . 7 ⊢ (N ∈ ℝ → ((-N / 2) ∈ ℕ → (N / 2) ∈ ℤ))
32	31	adantr 391	. . . . . 6 ⊢ ((N ∈ ℝ ⋀ -N ∈ ℕ) → ((-N / 2) ∈ ℕ → (N / 2) ∈ ℤ))
33	32	con3d 95	. . . . 5 ⊢ ((N ∈ ℝ ⋀ -N ∈ ℕ) → (¬ (N / 2) ∈ ℤ → ¬ (-N / 2) ∈ ℕ))
34		nneot 6200	. . . . . . . 8 ⊢ (-N ∈ ℕ → ((-N / 2) ∈ ℕ ↔ ¬ ((-N + 1) / 2) ∈ ℕ))
35	34	biimprd 154	. . . . . . 7 ⊢ (-N ∈ ℕ → (¬ ((-N + 1) / 2) ∈ ℕ → (-N / 2) ∈ ℕ))
36	35	con1d 93	. . . . . 6 ⊢ (-N ∈ ℕ → (¬ (-N / 2) ∈ ℕ → ((-N + 1) / 2) ∈ ℕ))
37		ax1cn 5281	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℂ
38	37, 3	negsubdi2 5462	. . . . . . . . . . . . . . . . . 18 ⊢ -(1 − 2) = (2 − 1)
39		df-2 5972	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 = (1 + 1)
40	39	eqcomi 1482	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 + 1) = 2
41	3, 37, 37, 40	subaddri 5384	. . . . . . . . . . . . . . . . . 18 ⊢ (2 − 1) = 1
42	38, 41	eqtr2 1499	. . . . . . . . . . . . . . . . 17 ⊢ 1 = -(1 − 2)
43	37, 3	subcl 5378	. . . . . . . . . . . . . . . . . 18 ⊢ (1 − 2) ∈ ℂ
44	37, 43	negcon2 5420	. . . . . . . . . . . . . . . . 17 ⊢ (1 = -(1 − 2) ↔ (1 − 2) = -1)
45	42, 44	mpbi 189	. . . . . . . . . . . . . . . 16 ⊢ (1 − 2) = -1
46	45	opreq2i 3978	. . . . . . . . . . . . . . 15 ⊢ (-N + (1 − 2)) = (-N + -1)
47		negclt 5380	. . . . . . . . . . . . . . . 16 ⊢ (N ∈ ℂ → -N ∈ ℂ)
48		addsubasst 5395	. . . . . . . . . . . . . . . . 17 ⊢ ((-N ∈ ℂ ⋀ 1 ∈ ℂ ⋀ 2 ∈ ℂ) → ((-N + 1) − 2) = (-N + (1 − 2)))
49	37, 3, 48	mp3an23 910	. . . . . . . . . . . . . . . 16 ⊢ (-N ∈ ℂ → ((-N + 1) − 2) = (-N + (1 − 2)))
50	47, 49	syl 10	. . . . . . . . . . . . . . 15 ⊢ (N ∈ ℂ → ((-N + 1) − 2) = (-N + (1 − 2)))
51		negdit 5467	. . . . . . . . . . . . . . . 16 ⊢ ((N ∈ ℂ ⋀ 1 ∈ ℂ) → -(N + 1) = (-N + -1))
52	37, 51	mpan2 698	. . . . . . . . . . . . . . 15 ⊢ (N ∈ ℂ → -(N + 1) = (-N + -1))
53	46, 50, 52	3eqtr4a 1535	. . . . . . . . . . . . . 14 ⊢ (N ∈ ℂ → ((-N + 1) − 2) = -(N + 1))
54	53	opreq1d 3981	. . . . . . . . . . . . 13 ⊢ (N ∈ ℂ → (((-N + 1) − 2) / 2) = (-(N + 1) / 2))
55		peano2cn 5356	. . . . . . . . . . . . . . 15 ⊢ (-N ∈ ℂ → (-N + 1) ∈ ℂ)
56		divsubdirtOLD 5777	. . . . . . . . . . . . . . . . 17 ⊢ ((((-N + 1) ∈ ℂ ⋀ 2 ∈ ℂ ⋀ 2 ∈ ℂ) ⋀ 2 ≠ 0) → (((-N + 1) − 2) / 2) = (((-N + 1) / 2) − (2 / 2)))
57	4, 56	mpan2 698	. . . . . . . . . . . . . . . 16 ⊢ (((-N + 1) ∈ ℂ ⋀ 2 ∈ ℂ ⋀ 2 ∈ ℂ) → (((-N + 1) − 2) / 2) = (((-N + 1) / 2) − (2 / 2)))
58	3, 3, 57	mp3an23 910	. . . . . . . . . . . . . . 15 ⊢ ((-N + 1) ∈ ℂ → (((-N + 1) − 2) / 2) = (((-N + 1) / 2) − (2 / 2)))
59	47, 55, 58	3syl 20	. . . . . . . . . . . . . 14 ⊢ (N ∈ ℂ → (((-N + 1) − 2) / 2) = (((-N + 1) / 2) − (2 / 2)))
60	3, 4	divid 5771	. . . . . . . . . . . . . . . 16 ⊢ (2 / 2) = 1
61	60	eqcomi 1482	. . . . . . . . . . . . . . 15 ⊢ 1 = (2 / 2)
62	61	opreq2i 3978	. . . . . . . . . . . . . 14 ⊢ (((-N + 1) / 2) − 1) = (((-N + 1) / 2) − (2 / 2))
63	59, 62	syl6reqr 1529	. . . . . . . . . . . . 13 ⊢ (N ∈ ℂ → (((-N + 1) / 2) − 1) = (((-N + 1) − 2) / 2))
64		peano2cn 5356	. . . . . . . . . . . . . 14 ⊢ (N ∈ ℂ → (N + 1) ∈ ℂ)
65		divnegt 5775	. . . . . . . . . . . . . . 15 ⊢ (((N + 1) ∈ ℂ ⋀ 2 ∈ ℂ ⋀ 2 ≠ 0) → -((N + 1) / 2) = (-(N + 1) / 2))
66	3, 4, 65	mp3an23 910	. . . . . . . . . . . . . 14 ⊢ ((N + 1) ∈ ℂ → -((N + 1) / 2) = (-(N + 1) / 2))
67	64, 66	syl 10	. . . . . . . . . . . . 13 ⊢ (N ∈ ℂ → -((N + 1) / 2) = (-(N + 1) / 2))
68	54, 63, 67	3eqtr4d 1520	. . . . . . . . . . . 12 ⊢ (N ∈ ℂ → (((-N + 1) / 2) − 1) = -((N + 1) / 2))
69	20, 68	syl 10	. . . . . . . . . . 11 ⊢ (N ∈ ℝ → (((-N + 1) / 2) − 1) = -((N + 1) / 2))
70	69	eleq1d 1543	. . . . . . . . . 10 ⊢ (N ∈ ℝ → ((((-N + 1) / 2) − 1) ∈ ℤ ↔ -((N + 1) / 2) ∈ ℤ))
71		peano2zm 6171	. . . . . . . . . 10 ⊢ (((-N + 1) / 2) ∈ ℤ → (((-N + 1) / 2) − 1) ∈ ℤ)
72	70, 71	syl5bi 208	. . . . . . . . 9 ⊢ (N ∈ ℝ → (((-N + 1) / 2) ∈ ℤ → -((N + 1) / 2) ∈ ℤ))
73		znegclt 6165	. . . . . . . . 9 ⊢ (-((N + 1) / 2) ∈ ℤ → --((N + 1) / 2) ∈ ℤ)
74	72, 73	syl6 22	. . . . . . . 8 ⊢ (N ∈ ℝ → (((-N + 1) / 2) ∈ ℤ → --((N + 1) / 2) ∈ ℤ))
75		peano2re 5448	. . . . . . . . . . 11 ⊢ (N ∈ ℝ → (N + 1) ∈ ℝ)
76	75	recnd 5327	. . . . . . . . . 10 ⊢ (N ∈ ℝ → (N + 1) ∈ ℂ)
77		halfclt 6035	. . . . . . . . . 10 ⊢ ((N + 1) ∈ ℂ → ((N + 1) / 2) ∈ ℂ)
78		negnegt 5405	. . . . . . . . . 10 ⊢ (((N + 1) / 2) ∈ ℂ → --((N + 1) / 2) = ((N + 1) / 2))
79	76, 77, 78	3syl 20	. . . . . . . . 9 ⊢ (N ∈ ℝ → --((N + 1) / 2) = ((N + 1) / 2))
80	79	eleq1d 1543	. . . . . . . 8 ⊢ (N ∈ ℝ → (--((N + 1) / 2) ∈ ℤ ↔ ((N + 1) / 2) ∈ ℤ))
81	74, 80	sylibd 202	. . . . . . 7 ⊢ (N ∈ ℝ → (((-N + 1) / 2) ∈ ℤ → ((N + 1) / 2) ∈ ℤ))
82		nnzt 6155	. . . . . . 7 ⊢ (((-N + 1) / 2) ∈ ℕ → ((-N + 1) / 2) ∈ ℤ)
83	81, 82	syl5 21	. . . . . 6 ⊢ (N ∈ ℝ → (((-N + 1) / 2) ∈ ℕ → ((N + 1) / 2) ∈ ℤ))
84	36, 83	sylan9r 471	. . . . 5 ⊢ ((N ∈ ℝ ⋀ -N ∈ ℕ) → (¬ (-N / 2) ∈ ℕ → ((N + 1) / 2) ∈ ℤ))
85	33, 84	syld 27	. . . 4 ⊢ ((N ∈ ℝ ⋀ -N ∈ ℕ) → (¬ (N / 2) ∈ ℤ → ((N + 1) / 2) ∈ ℤ))
86	10, 19, 85	3jaodan 892	. . 3 ⊢ ((N ∈ ℝ ⋀ (N = 0 ⋁ N ∈ ℕ ⋁ -N ∈ ℕ)) → (¬ (N / 2) ∈ ℤ → ((N + 1) / 2) ∈ ℤ))
87	1, 86	sylbi 199	. 2 ⊢ (N ∈ ℤ → (¬ (N / 2) ∈ ℤ → ((N + 1) / 2) ∈ ℤ))
88	87	orrd 233	1 ⊢ (N ∈ ℤ → ((N / 2) ∈ ℤ ⋁ ((N + 1) / 2) ∈ ℤ))

Syntax hints:  ¬ wn 2   → wi 3   ⋁ wo 222   ⋀ wa 223   ⋁ w3o 776   ⋀ w3a 777   = wceq 958   ∈ wcel 960   ≠ wne 1588  (class class class)co 3969  ℂcc 5244  ℝcr 5245  0cc0 5246  1c1 5247   + caddc 5249   − cmin 5304  -cneg 5305   / cdiv 5306  ℕcn 5308  ℤcz 5310  2c2 5963

This theorem is referenced by:  flhalft 6248  sinkpi 8692  abssinper 8707

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-nel 1591  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-csb 2005  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-pss 2058  df-nul 2284  df-if 2366  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419  df-op 2420  df-uni 2508  df-int 2538  df-iun 2572  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-id 2841  df-po 2846  df-so 2856  df-fr 2923  df-we 2940  df-ord 2957  df-on 2958  df-lim 2959  df-suc 2960  df-om 3138  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-f1 3201  df-fo 3202  df-f1o 3203  df-fv 3204  df-rdg 3938  df-opr 3971  df-oprab 3972  df-1st 4085  df-2nd 4086  df-1o 4139  df-oadd 4141  df-omul 4142  df-er 4267  df-ec 4269  df-qs 4272  df-en 4374  df-dom 4375  df-sdom 4376  df-ni 5012  df-pli 5013  df-mi 5014  df-lti 5015  df-plpq 5047  df-mpq 5048  df-enq 5049  df-nq 5050  df-plq 5051  df-mq 5052  df-rq 5053  df-ltq 5054  df-1q 5055  df-np 5098  df-1p 5099  df-plp 5100  df-mp 5101  df-ltp 5102  df-plpr 5176  df-mpr 5177  df-enr 5178  df-nr 5179  df-plr 5180  df-mr 5181  df-ltr 5182  df-0r 5183  df-1r 5184  df-m1r 5185  df-c 5252  df-0 5253  df-1 5254  df-i 5255  df-r 5256  df-plus 5257  df-mul 5258  df-lt 5259  df-sub 5368  df-neg 5370  df-pnf 5499  df-mnf 5500  df-xr 5501  df-ltxr 5502  df-le 5503  df-div 5715  df-n 5927  df-2 5972  df-n0 6102  df-z 6138

Copyright terms: Public domain