nno - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nno		Structured version Visualization version GIF version

Theorem nno 16311

Description: An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020.) (Proof shortened by AV, 10-Jul-2022.)

**Assertion**
Ref	Expression
nno	⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → ((𝑁 − 1) / 2) ∈ ℕ)

**Proof of Theorem nno**
Step	Hyp	Ref	Expression
1		eluz2b3 12837	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1))
2		nnnn0 12410	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
3		nn0o1gt2 16310	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → (𝑁 = 1 ∨ 2 < 𝑁))
4	2, 3	sylan 581	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → (𝑁 = 1 ∨ 2 < 𝑁))
5		eqneqall 2942	. . . . . . 7 ⊢ (𝑁 = 1 → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈ ℕ))
6	5	a1d 25	. . . . . 6 ⊢ (𝑁 = 1 → ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈ ℕ)))
7		nn0z 12514	. . . . . . . . . . . 12 ⊢ (((𝑁 + 1) / 2) ∈ ℕ₀ → ((𝑁 + 1) / 2) ∈ ℤ)
8		peano2zm 12536	. . . . . . . . . . . 12 ⊢ (((𝑁 + 1) / 2) ∈ ℤ → (((𝑁 + 1) / 2) − 1) ∈ ℤ)
9	7, 8	syl 17	. . . . . . . . . . 11 ⊢ (((𝑁 + 1) / 2) ∈ ℕ₀ → (((𝑁 + 1) / 2) − 1) ∈ ℤ)
10	9	ad2antlr 728	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) ∧ 2 < 𝑁) → (((𝑁 + 1) / 2) − 1) ∈ ℤ)
11		2cn 12222	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
12	11	mullidi 11139	. . . . . . . . . . . . . 14 ⊢ (1 · 2) = 2
13		nnre 12154	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
14	13	ltp1d 12074	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1))
15	14	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → 𝑁 < (𝑁 + 1))
16		2re 12221	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
17		peano2nn 12159	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
18	17	nnred 12162	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
19		lttr 11211	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ) → ((2 < 𝑁 ∧ 𝑁 < (𝑁 + 1)) → 2 < (𝑁 + 1)))
20	16, 13, 18, 19	mp3an2i 1469	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((2 < 𝑁 ∧ 𝑁 < (𝑁 + 1)) → 2 < (𝑁 + 1)))
21	20	expdimp 452	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → (𝑁 < (𝑁 + 1) → 2 < (𝑁 + 1)))
22	15, 21	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → 2 < (𝑁 + 1))
23	12, 22	eqbrtrid 5132	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → (1 · 2) < (𝑁 + 1))
24		1red 11135	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → 1 ∈ ℝ)
25	18	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → (𝑁 + 1) ∈ ℝ)
26		2rp 12912	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ⁺
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → 2 ∈ ℝ⁺)
28	24, 25, 27	ltmuldivd 12998	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → ((1 · 2) < (𝑁 + 1) ↔ 1 < ((𝑁 + 1) / 2)))
29	23, 28	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → 1 < ((𝑁 + 1) / 2))
30	18	rehalfcld 12390	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 2) ∈ ℝ)
31	30	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → ((𝑁 + 1) / 2) ∈ ℝ)
32	24, 31	posdifd 11726	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → (1 < ((𝑁 + 1) / 2) ↔ 0 < (((𝑁 + 1) / 2) − 1)))
33	29, 32	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → 0 < (((𝑁 + 1) / 2) − 1))
34	33	adantlr 716	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) ∧ 2 < 𝑁) → 0 < (((𝑁 + 1) / 2) − 1))
35		elnnz 12500	. . . . . . . . . 10 ⊢ ((((𝑁 + 1) / 2) − 1) ∈ ℕ ↔ ((((𝑁 + 1) / 2) − 1) ∈ ℤ ∧ 0 < (((𝑁 + 1) / 2) − 1)))
36	10, 34, 35	sylanbrc 584	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) ∧ 2 < 𝑁) → (((𝑁 + 1) / 2) − 1) ∈ ℕ)
37		nncn 12155	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
38		xp1d2m1eqxm1d2 12397	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → (((𝑁 + 1) / 2) − 1) = ((𝑁 − 1) / 2))
39	37, 38	syl 17	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 2) − 1) = ((𝑁 − 1) / 2))
40	39	eleq1d 2820	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1) / 2) − 1) ∈ ℕ ↔ ((𝑁 − 1) / 2) ∈ ℕ))
41	40	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → ((((𝑁 + 1) / 2) − 1) ∈ ℕ ↔ ((𝑁 − 1) / 2) ∈ ℕ))
42	41	adantr 480	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) ∧ 2 < 𝑁) → ((((𝑁 + 1) / 2) − 1) ∈ ℕ ↔ ((𝑁 − 1) / 2) ∈ ℕ))
43	36, 42	mpbid 232	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) ∧ 2 < 𝑁) → ((𝑁 − 1) / 2) ∈ ℕ)
44	43	a1d 25	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) ∧ 2 < 𝑁) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈ ℕ))
45	44	expcom 413	. . . . . 6 ⊢ (2 < 𝑁 → ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈ ℕ)))
46	6, 45	jaoi 858	. . . . 5 ⊢ ((𝑁 = 1 ∨ 2 < 𝑁) → ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈ ℕ)))
47	4, 46	mpcom 38	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈ ℕ))
48	47	impancom 451	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → (((𝑁 + 1) / 2) ∈ ℕ₀ → ((𝑁 − 1) / 2) ∈ ℕ))
49	1, 48	sylbi 217	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (((𝑁 + 1) / 2) ∈ ℕ₀ → ((𝑁 − 1) / 2) ∈ ℕ))
50	49	imp 406	1 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → ((𝑁 − 1) / 2) ∈ ℕ)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2931 class class class wbr 5097 ‘cfv 6491 (class class class)co 7358 ℂcc 11026 ℝcr 11027 0cc0 11028 1c1 11029 + caddc 11031 · cmul 11033 < clt 11168 − cmin 11366 / cdiv 11796 ℕcn 12147 2c2 12202 ℕ₀cn0 12403 ℤcz 12490 ℤ_≥cuz 12753 ℝ⁺crp 12907

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2183 ax-ext 2707 ax-sep 5240 ax-nul 5250 ax-pow 5309 ax-pr 5376 ax-un 7680 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3349 df-reu 3350 df-rab 3399 df-v 3441 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4285 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-iun 4947 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6258 df-ord 6319 df-on 6320 df-lim 6321 df-suc 6322 df-iota 6447 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-er 8635 df-en 8886 df-dom 8887 df-sdom 8888 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12148 df-2 12210 df-3 12211 df-4 12212 df-n0 12404 df-z 12491 df-uz 12754 df-rp 12908

This theorem is referenced by: nn0o 16312 gausslemma2dlem0b 27326 blennngt2o2 48875 dignn0flhalf 48901

W3C validator