nno - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > nno		GIF version

Theorem nno 12332

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

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

**Proof of Theorem nno**
Step	Hyp	Ref	Expression
1		eluz2b3 9760	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1))
2		nnnn0 9337	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
3		nn0o1gt2 12331	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → (𝑁 = 1 ∨ 2 < 𝑁))
4	2, 3	sylan 283	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → (𝑁 = 1 ∨ 2 < 𝑁))
5		eqneqall 2388	. . . . . . 7 ⊢ (𝑁 = 1 → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈ ℕ))
6	5	a1d 22	. . . . . 6 ⊢ (𝑁 = 1 → ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈ ℕ)))
7		nn0z 9427	. . . . . . . . . . . 12 ⊢ (((𝑁 + 1) / 2) ∈ ℕ₀ → ((𝑁 + 1) / 2) ∈ ℤ)
8		peano2zm 9445	. . . . . . . . . . . 12 ⊢ (((𝑁 + 1) / 2) ∈ ℤ → (((𝑁 + 1) / 2) − 1) ∈ ℤ)
9	7, 8	syl 14	. . . . . . . . . . 11 ⊢ (((𝑁 + 1) / 2) ∈ ℕ₀ → (((𝑁 + 1) / 2) − 1) ∈ ℤ)
10	9	ad2antlr 489	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) ∧ 2 < 𝑁) → (((𝑁 + 1) / 2) − 1) ∈ ℤ)
11		2cn 9142	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
12	11	mullidi 8110	. . . . . . . . . . . . . 14 ⊢ (1 · 2) = 2
13		nnre 9078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
14	13	ltp1d 9038	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1))
15	14	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → 𝑁 < (𝑁 + 1))
16		2re 9141	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
17	16	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℝ)
18		peano2nn 9083	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
19	18	nnred 9084	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
20		lttr 8181	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ) → ((2 < 𝑁 ∧ 𝑁 < (𝑁 + 1)) → 2 < (𝑁 + 1)))
21	17, 13, 19, 20	syl3anc 1250	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((2 < 𝑁 ∧ 𝑁 < (𝑁 + 1)) → 2 < (𝑁 + 1)))
22	21	expdimp 259	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → (𝑁 < (𝑁 + 1) → 2 < (𝑁 + 1)))
23	15, 22	mpd 13	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → 2 < (𝑁 + 1))
24	12, 23	eqbrtrid 4094	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → (1 · 2) < (𝑁 + 1))
25		1red 8122	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → 1 ∈ ℝ)
26	19	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → (𝑁 + 1) ∈ ℝ)
27		2pos 9162	. . . . . . . . . . . . . . . 16 ⊢ 0 < 2
28	16, 27	pm3.2i 272	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℝ ∧ 0 < 2)
29	28	a1i 9	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → (2 ∈ ℝ ∧ 0 < 2))
30		ltmuldiv 8982	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((1 · 2) < (𝑁 + 1) ↔ 1 < ((𝑁 + 1) / 2)))
31	25, 26, 29, 30	syl3anc 1250	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → ((1 · 2) < (𝑁 + 1) ↔ 1 < ((𝑁 + 1) / 2)))
32	24, 31	mpbid 147	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → 1 < ((𝑁 + 1) / 2))
33	19	rehalfcld 9319	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 2) ∈ ℝ)
34	33	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → ((𝑁 + 1) / 2) ∈ ℝ)
35	25, 34	posdifd 8640	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → (1 < ((𝑁 + 1) / 2) ↔ 0 < (((𝑁 + 1) / 2) − 1)))
36	32, 35	mpbid 147	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 2 < 𝑁) → 0 < (((𝑁 + 1) / 2) − 1))
37	36	adantlr 477	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) ∧ 2 < 𝑁) → 0 < (((𝑁 + 1) / 2) − 1))
38		elnnz 9417	. . . . . . . . . 10 ⊢ ((((𝑁 + 1) / 2) − 1) ∈ ℕ ↔ ((((𝑁 + 1) / 2) − 1) ∈ ℤ ∧ 0 < (((𝑁 + 1) / 2) − 1)))
39	10, 37, 38	sylanbrc 417	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) ∧ 2 < 𝑁) → (((𝑁 + 1) / 2) − 1) ∈ ℕ)
40		nncn 9079	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
41		xp1d2m1eqxm1d2 9325	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → (((𝑁 + 1) / 2) − 1) = ((𝑁 − 1) / 2))
42	40, 41	syl 14	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 2) − 1) = ((𝑁 − 1) / 2))
43	42	eleq1d 2276	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1) / 2) − 1) ∈ ℕ ↔ ((𝑁 − 1) / 2) ∈ ℕ))
44	43	adantr 276	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → ((((𝑁 + 1) / 2) − 1) ∈ ℕ ↔ ((𝑁 − 1) / 2) ∈ ℕ))
45	44	adantr 276	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) ∧ 2 < 𝑁) → ((((𝑁 + 1) / 2) − 1) ∈ ℕ ↔ ((𝑁 − 1) / 2) ∈ ℕ))
46	39, 45	mpbid 147	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) ∧ 2 < 𝑁) → ((𝑁 − 1) / 2) ∈ ℕ)
47	46	a1d 22	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) ∧ 2 < 𝑁) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈ ℕ))
48	47	expcom 116	. . . . . 6 ⊢ (2 < 𝑁 → ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈ ℕ)))
49	6, 48	jaoi 718	. . . . 5 ⊢ ((𝑁 = 1 ∨ 2 < 𝑁) → ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈ ℕ)))
50	4, 49	mpcom 36	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → (𝑁 ≠ 1 → ((𝑁 − 1) / 2) ∈ ℕ))
51	50	impancom 260	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → (((𝑁 + 1) / 2) ∈ ℕ₀ → ((𝑁 − 1) / 2) ∈ ℕ))
52	1, 51	sylbi 121	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (((𝑁 + 1) / 2) ∈ ℕ₀ → ((𝑁 − 1) / 2) ∈ ℕ))
53	52	imp 124	1 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ₀) → ((𝑁 − 1) / 2) ∈ ℕ)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 710 = wceq 1373 ∈ wcel 2178 ≠ wne 2378 class class class wbr 4059 ‘cfv 5290 (class class class)co 5967 ℂcc 7958 ℝcr 7959 0cc0 7960 1c1 7961 + caddc 7963 · cmul 7965 < clt 8142 − cmin 8278 / cdiv 8780 ℕcn 9071 2c2 9122 ℕ₀cn0 9330 ℤcz 9407 ℤ_≥cuz 9683

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2180 ax-14 2181 ax-ext 2189 ax-sep 4178 ax-pow 4234 ax-pr 4269 ax-un 4498 ax-setind 4603 ax-cnex 8051 ax-resscn 8052 ax-1cn 8053 ax-1re 8054 ax-icn 8055 ax-addcl 8056 ax-addrcl 8057 ax-mulcl 8058 ax-mulrcl 8059 ax-addcom 8060 ax-mulcom 8061 ax-addass 8062 ax-mulass 8063 ax-distr 8064 ax-i2m1 8065 ax-0lt1 8066 ax-1rid 8067 ax-0id 8068 ax-rnegex 8069 ax-precex 8070 ax-cnre 8071 ax-pre-ltirr 8072 ax-pre-ltwlin 8073 ax-pre-lttrn 8074 ax-pre-apti 8075 ax-pre-ltadd 8076 ax-pre-mulgt0 8077 ax-pre-mulext 8078

This theorem depends on definitions: df-bi 117 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ne 2379 df-nel 2474 df-ral 2491 df-rex 2492 df-reu 2493 df-rmo 2494 df-rab 2495 df-v 2778 df-sbc 3006 df-dif 3176 df-un 3178 df-in 3180 df-ss 3187 df-pw 3628 df-sn 3649 df-pr 3650 df-op 3652 df-uni 3865 df-int 3900 df-br 4060 df-opab 4122 df-mpt 4123 df-id 4358 df-po 4361 df-iso 4362 df-xp 4699 df-rel 4700 df-cnv 4701 df-co 4702 df-dm 4703 df-iota 5251 df-fun 5292 df-fv 5298 df-riota 5922 df-ov 5970 df-oprab 5971 df-mpo 5972 df-pnf 8144 df-mnf 8145 df-xr 8146 df-ltxr 8147 df-le 8148 df-sub 8280 df-neg 8281 df-reap 8683 df-ap 8690 df-div 8781 df-inn 9072 df-2 9130 df-3 9131 df-4 9132 df-n0 9331 df-z 9408 df-uz 9684

This theorem is referenced by: nn0o 12333 gausslemma2dlem0b 15642

W3C validator