Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem nneo 4719

Description: A natural number is even or odd but not both.

**Hypothesis**
Ref	Expression
nnsqcl.1	⊢ A ∈ ℕ

**Assertion**
Ref	Expression
nneo	⊢ ((A / 2) ∈ ℕ ↔ ¬ ((A + 1) / 2) ∈ ℕ)

**Proof of Theorem nneo**
Step	Hyp	Ref	Expression
1		ax1re 4064	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
2	1	ltplus1 4384	. . . . . . . . 9 ⊢ 1 < (1 + 1)
3		df-2 4462	. . . . . . . . 9 ⊢ 2 = (1 + 1)
4	2, 3	breqtrr 2082	. . . . . . . 8 ⊢ 1 < 2
5		2re 4470	. . . . . . . . 9 ⊢ 2 ∈ ℝ
6		nnsqcl.1	. . . . . . . . . 10 ⊢ A ∈ ℕ
7	6	nnre 4429	. . . . . . . . 9 ⊢ A ∈ ℝ
8	1, 5, 7	ltadd2 4312	. . . . . . . 8 ⊢ (1 < 2 ↔ (A + 1) < (A + 2))
9	4, 8	mpbi 164	. . . . . . 7 ⊢ (A + 1) < (A + 2)
10		2cn 4471	. . . . . . . 8 ⊢ 2 ∈ ℂ
11	7, 1	readdcl 4118	. . . . . . . . 9 ⊢ (A + 1) ∈ ℝ
12	11	recn 4098	. . . . . . . 8 ⊢ (A + 1) ∈ ℂ
13		2pos 4479	. . . . . . . . 9 ⊢ 0 < 2
14	5, 13	gt0ne0i 4345	. . . . . . . 8 ⊢ 2 ≠ 0
15	10, 12, 14	divcan2 4224	. . . . . . 7 ⊢ (2 · ((A + 1) / 2)) = (A + 1)
16	6	nncn 4430	. . . . . . . . . 10 ⊢ A ∈ ℂ
17	16, 10, 14	divcl 4221	. . . . . . . . 9 ⊢ (A / 2) ∈ ℂ
18		1cn 4101	. . . . . . . . 9 ⊢ 1 ∈ ℂ
19	10, 17, 18	adddi 4110	. . . . . . . 8 ⊢ (2 · ((A / 2) + 1)) = ((2 · (A / 2)) + (2 · 1))
20	10, 16, 14	divcan2 4224	. . . . . . . . 9 ⊢ (2 · (A / 2)) = A
21	10	mulid1 4114	. . . . . . . . 9 ⊢ (2 · 1) = 2
22	20, 21	opreq12i 3011	. . . . . . . 8 ⊢ ((2 · (A / 2)) + (2 · 1)) = (A + 2)
23	19, 22	eqtr 1119	. . . . . . 7 ⊢ (2 · ((A / 2) + 1)) = (A + 2)
24	9, 15, 23	3brtr4 2085	. . . . . 6 ⊢ (2 · ((A + 1) / 2)) < (2 · ((A / 2) + 1))
25	11, 5, 14	redivcl 4274	. . . . . . . 8 ⊢ ((A + 1) / 2) ∈ ℝ
26	7, 5, 14	redivcl 4274	. . . . . . . . 9 ⊢ (A / 2) ∈ ℝ
27	26, 1	readdcl 4118	. . . . . . . 8 ⊢ ((A / 2) + 1) ∈ ℝ
28	25, 27, 5	ltmul2 4395	. . . . . . 7 ⊢ (0 < 2 → (((A + 1) / 2) < ((A / 2) + 1) ↔ (2 · ((A + 1) / 2)) < (2 · ((A / 2) + 1))))
29	13, 28	ax-mp 6	. . . . . 6 ⊢ (((A + 1) / 2) < ((A / 2) + 1) ↔ (2 · ((A + 1) / 2)) < (2 · ((A / 2) + 1)))
30	24, 29	mpbir 165	. . . . 5 ⊢ ((A + 1) / 2) < ((A / 2) + 1)
31	27, 25	lelt 4301	. . . . . 6 ⊢ (((A / 2) + 1) ≤ ((A + 1) / 2) ↔ ¬ ((A + 1) / 2) < ((A / 2) + 1))
32	31	bicon2i 194	. . . . 5 ⊢ (((A + 1) / 2) < ((A / 2) + 1) ↔ ¬ ((A / 2) + 1) ≤ ((A + 1) / 2))
33	30, 32	mpbi 164	. . . 4 ⊢ ¬ ((A / 2) + 1) ≤ ((A + 1) / 2)
34	7	ltplus1 4384	. . . . . 6 ⊢ A < (A + 1)
35	7, 11, 5, 13	ltdivi 4398	. . . . . 6 ⊢ (A < (A + 1) ↔ (A / 2) < ((A + 1) / 2))
36	34, 35	mpbi 164	. . . . 5 ⊢ (A / 2) < ((A + 1) / 2)
37		nnltp1let 4449	. . . . 5 ⊢ (((A / 2) ∈ ℕ ∧ ((A + 1) / 2) ∈ ℕ) → ((A / 2) < ((A + 1) / 2) ↔ ((A / 2) + 1) ≤ ((A + 1) / 2)))
38	36, 37	mpbii 168	. . . 4 ⊢ (((A / 2) ∈ ℕ ∧ ((A + 1) / 2) ∈ ℕ) → ((A / 2) + 1) ≤ ((A + 1) / 2))
39	33, 38	mto 93	. . 3 ⊢ ¬ ((A / 2) ∈ ℕ ∧ ((A + 1) / 2) ∈ ℕ)
40		imnan 207	. . 3 ⊢ (((A / 2) ∈ ℕ → ¬ ((A + 1) / 2) ∈ ℕ) ↔ ¬ ((A / 2) ∈ ℕ ∧ ((A + 1) / 2) ∈ ℕ))
41	39, 40	mpbir 165	. 2 ⊢ ((A / 2) ∈ ℕ → ¬ ((A + 1) / 2) ∈ ℕ)
42		opreq1 3006	. . . . . . . 8 ⊢ (x = 1 → (x + 1) = (1 + 1))
43	42	opreq1d 3012	. . . . . . 7 ⊢ (x = 1 → ((x + 1) / 2) = ((1 + 1) / 2))
44	43	eleq1d 1155	. . . . . 6 ⊢ (x = 1 → (((x + 1) / 2) ∈ ℕ ↔ ((1 + 1) / 2) ∈ ℕ))
45		opreq1 3006	. . . . . . 7 ⊢ (x = 1 → (x / 2) = (1 / 2))
46	45	eleq1d 1155	. . . . . 6 ⊢ (x = 1 → ((x / 2) ∈ ℕ ↔ (1 / 2) ∈ ℕ))
47	44, 46	orbi12d 475	. . . . 5 ⊢ (x = 1 → ((((x + 1) / 2) ∈ ℕ ∨ (x / 2) ∈ ℕ) ↔ (((1 + 1) / 2) ∈ ℕ ∨ (1 / 2) ∈ ℕ)))
48		opreq1 3006	. . . . . . . 8 ⊢ (x = y → (x + 1) = (y + 1))
49	48	opreq1d 3012	. . . . . . 7 ⊢ (x = y → ((x + 1) / 2) = ((y + 1) / 2))
50	49	eleq1d 1155	. . . . . 6 ⊢ (x = y → (((x + 1) / 2) ∈ ℕ ↔ ((y + 1) / 2) ∈ ℕ))
51		opreq1 3006	. . . . . . 7 ⊢ (x = y → (x / 2) = (y / 2))
52	51	eleq1d 1155	. . . . . 6 ⊢ (x = y → ((x / 2) ∈ ℕ ↔ (y / 2) ∈ ℕ))
53	50, 52	orbi12d 475	. . . . 5 ⊢ (x = y → ((((x + 1) / 2) ∈ ℕ ∨ (x / 2) ∈ ℕ) ↔ (((y + 1) / 2) ∈ ℕ ∨ (y / 2) ∈ ℕ)))
54		opreq1 3006	. . . . . . . 8 ⊢ (x = (y + 1) → (x + 1) = ((y + 1) + 1))
55	54	opreq1d 3012	. . . . . . 7 ⊢ (x = (y + 1) → ((x + 1) / 2) = (((y + 1) + 1) / 2))
56	55	eleq1d 1155	. . . . . 6 ⊢ (x = (y + 1) → (((x + 1) / 2) ∈ ℕ ↔ (((y + 1) + 1) / 2) ∈ ℕ))
57		opreq1 3006	. . . . . . 7 ⊢ (x = (y + 1) → (x / 2) = ((y + 1) / 2))
58	57	eleq1d 1155	. . . . . 6 ⊢ (x = (y + 1) → ((x / 2) ∈ ℕ ↔ ((y + 1) / 2) ∈ ℕ))
59	56, 58	orbi12d 475	. . . . 5 ⊢ (x = (y + 1) → ((((x + 1) / 2) ∈ ℕ ∨ (x / 2) ∈ ℕ) ↔ ((((y + 1) + 1) / 2) ∈ ℕ ∨ ((y + 1) / 2) ∈ ℕ)))
60		opreq1 3006	. . . . . . . 8 ⊢ (x = A → (x + 1) = (A + 1))
61	60	opreq1d 3012	. . . . . . 7 ⊢ (x = A → ((x + 1) / 2) = ((A + 1) / 2))
62	61	eleq1d 1155	. . . . . 6 ⊢ (x = A → (((x + 1) / 2) ∈ ℕ ↔ ((A + 1) / 2) ∈ ℕ))
63		opreq1 3006	. . . . . . 7 ⊢ (x = A → (x / 2) = (A / 2))
64	63	eleq1d 1155	. . . . . 6 ⊢ (x = A → ((x / 2) ∈ ℕ ↔ (A / 2) ∈ ℕ))
65	62, 64	orbi12d 475	. . . . 5 ⊢ (x = A → ((((x + 1) / 2) ∈ ℕ ∨ (x / 2) ∈ ℕ) ↔ (((A + 1) / 2) ∈ ℕ ∨ (A / 2) ∈ ℕ)))
66	3	opreq1i 3009	. . . . . . . . 9 ⊢ (2 / 2) = ((1 + 1) / 2)
67	10, 14	divid 4254	. . . . . . . . 9 ⊢ (2 / 2) = 1
68	66, 67	eqtr3 1121	. . . . . . . 8 ⊢ ((1 + 1) / 2) = 1
69		1nn 4432	. . . . . . . 8 ⊢ 1 ∈ ℕ
70	68, 69	eqeltr 1159	. . . . . . 7 ⊢ ((1 + 1) / 2) ∈ ℕ
71	70	pm2.21ni 92	. . . . . 6 ⊢ (¬ ((1 + 1) / 2) ∈ ℕ → (1 / 2) ∈ ℕ)
72	71	orri 201	. . . . 5 ⊢ (((1 + 1) / 2) ∈ ℕ ∨ (1 / 2) ∈ ℕ)
73		nncnt 4428	. . . . . . . . . 10 ⊢ (y ∈ ℕ → y ∈ ℂ)
74		axaddass 4072	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((y + 1) + 1) = (y + (1 + 1)))
75	18, 74	mp3an3 641	. . . . . . . . . . . . . 14 ⊢ ((y ∈ ℂ ∧ 1 ∈ ℂ) → ((y + 1) + 1) = (y + (1 + 1)))
76	18, 75	mpan2 519	. . . . . . . . . . . . 13 ⊢ (y ∈ ℂ → ((y + 1) + 1) = (y + (1 + 1)))
77	3	opreq2i 3010	. . . . . . . . . . . . 13 ⊢ (y + 2) = (y + (1 + 1))
78	76, 77	syl6eqr 1142	. . . . . . . . . . . 12 ⊢ (y ∈ ℂ → ((y + 1) + 1) = (y + 2))
79	78	opreq1d 3012	. . . . . . . . . . 11 ⊢ (y ∈ ℂ → (((y + 1) + 1) / 2) = ((y + 2) / 2))
80		opreq1 3006	. . . . . . . . . . . . . . 15 ⊢ (y = if(y ∈ ℂ, y, 2) → (y + 2) = (if(y ∈ ℂ, y, 2) + 2))
81	80	opreq1d 3012	. . . . . . . . . . . . . 14 ⊢ (y = if(y ∈ ℂ, y, 2) → ((y + 2) / 2) = ((if(y ∈ ℂ, y, 2) + 2) / 2))
82		opreq1 3006	. . . . . . . . . . . . . . 15 ⊢ (y = if(y ∈ ℂ, y, 2) → (y / 2) = (if(y ∈ ℂ, y, 2) / 2))
83	82	opreq1d 3012	. . . . . . . . . . . . . 14 ⊢ (y = if(y ∈ ℂ, y, 2) → ((y / 2) + (2 / 2)) = ((if(y ∈ ℂ, y, 2) / 2) + (2 / 2)))
84	81, 83	cleq12d 1115	. . . . . . . . . . . . 13 ⊢ (y = if(y ∈ ℂ, y, 2) → (((y + 2) / 2) = ((y / 2) + (2 / 2)) ↔ ((if(y ∈ ℂ, y, 2) + 2) / 2) = ((if(y ∈ ℂ, y, 2) / 2) + (2 / 2))))
85	10	elimel 1793	. . . . . . . . . . . . . 14 ⊢ if(y ∈ ℂ, y, 2) ∈ ℂ
86	85, 10, 10, 14	divdistr 4243	. . . . . . . . . . . . 13 ⊢ ((if(y ∈ ℂ, y, 2) + 2) / 2) = ((if(y ∈ ℂ, y, 2) / 2) + (2 / 2))
87	84, 86	dedth 1784	. . . . . . . . . . . 12 ⊢ (y ∈ ℂ → ((y + 2) / 2) = ((y / 2) + (2 / 2)))
88	67	opreq2i 3010	. . . . . . . . . . . 12 ⊢ ((y / 2) + (2 / 2)) = ((y / 2) + 1)
89	87, 88	syl6eq 1140	. . . . . . . . . . 11 ⊢ (y ∈ ℂ → ((y + 2) / 2) = ((y / 2) + 1))
90	79, 89	eqtrd 1128	. . . . . . . . . 10 ⊢ (y ∈ ℂ → (((y + 1) + 1) / 2) = ((y / 2) + 1))
91	73, 90	syl 12	. . . . . . . . 9 ⊢ (y ∈ ℕ → (((y + 1) + 1) / 2) = ((y / 2) + 1))
92	91	eleq1d 1155	. . . . . . . 8 ⊢ (y ∈ ℕ → ((((y + 1) + 1) / 2) ∈ ℕ ↔ ((y / 2) + 1) ∈ ℕ))
93		peano2nn 4433	. . . . . . . 8 ⊢ ((y / 2) ∈ ℕ → ((y / 2) + 1) ∈ ℕ)
94	92, 93	syl5bir 184	. . . . . . 7 ⊢ (y ∈ ℕ → ((y / 2) ∈ ℕ → (((y + 1) + 1) / 2) ∈ ℕ))
95	94	orim2d 438	. . . . . 6 ⊢ (y ∈ ℕ → ((((y + 1) / 2) ∈ ℕ ∨ (y / 2) ∈ ℕ) → (((y + 1) / 2) ∈ ℕ ∨ (((y + 1) + 1) / 2) ∈ ℕ)))
96		orcom 209	. . . . . 6 ⊢ ((((y + 1) / 2) ∈ ℕ ∨ (((y + 1) + 1) / 2) ∈ ℕ) ↔ ((((y + 1) + 1) / 2) ∈ ℕ ∨ ((y + 1) / 2) ∈ ℕ))
97	95, 96	syl6ib 185	. . . . 5 ⊢ (y ∈ ℕ → ((((y + 1) / 2) ∈ ℕ ∨ (y / 2) ∈ ℕ) → ((((y + 1) + 1) / 2) ∈ ℕ ∨ ((y + 1) / 2) ∈ ℕ)))
98	47, 53, 59, 65, 72, 97	nnind 4434	. . . 4 ⊢ (A ∈ ℕ → (((A + 1) / 2) ∈ ℕ ∨ (A / 2) ∈ ℕ))
99	6, 98	ax-mp 6	. . 3 ⊢ (((A + 1) / 2) ∈ ℕ ∨ (A / 2) ∈ ℕ)
100	99	ori 200	. 2 ⊢ (¬ ((A + 1) / 2) ∈ ℕ → (A / 2) ∈ ℕ)
101	41, 100	impbi 139	1 ⊢ ((A / 2) ∈ ℕ ↔ ¬ ((A + 1) / 2) ∈ ℕ)

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∨ wo 195 ∧ wa 196 = weq 797 = wceq 1091 ∈ wcel 1092 ifcif 1776 class class class wbr 2054 (class class class)co 3001 ℂcc 4026 0cc0 4028 1c1 4029 + caddc 4031 · cmulc 4032 < clt 4033 / cdiv 4091 ≤ cle 4092 ℕcn 4093 2c2 4454

This theorem is referenced by: nnesq 4720

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-div 4216 df-le 4277 df-n 4423 df-2 4462

metamath.org