Metamath Proof Explorer

Theorem nno

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

Ref Expression
Assertion nno ⊢N∈ℤ≥2∧N+12∈ℕ0→N−12∈ℕ

Proof

Step Hyp Ref Expression
1 eluz2b3 ⊢N∈ℤ≥2↔N∈ℕ∧N≠1
2 nnnn0 ⊢N∈ℕ→N∈ℕ0
3 nn0o1gt2 ⊢N∈ℕ0∧N+12∈ℕ0→N=1∨2<N
4 2 3 sylan ⊢N∈ℕ∧N+12∈ℕ0→N=1∨2<N
5 eqneqall ⊢N=1→N≠1→N−12∈ℕ
6 5 a1d ⊢N=1→N∈ℕ∧N+12∈ℕ0→N≠1→N−12∈ℕ
7 nn0z ⊢N+12∈ℕ0→N+12∈ℤ
8 peano2zm ⊢N+12∈ℤ→N+12−1∈ℤ
9 7 8 syl ⊢N+12∈ℕ0→N+12−1∈ℤ
10 9 ad2antlr ⊢N∈ℕ∧N+12∈ℕ0∧2<N→N+12−1∈ℤ
11 2cn ⊢2∈ℂ
12 11 mullidi ⊢1⋅2=2
13 nnre ⊢N∈ℕ→N∈ℝ
14 13 ltp1d ⊢N∈ℕ→N<N+1
15 14 adantr ⊢N∈ℕ∧2<N→N<N+1
16 2re ⊢2∈ℝ
17 peano2nn ⊢N∈ℕ→N+1∈ℕ
18 17 nnred ⊢N∈ℕ→N+1∈ℝ
19 lttr ⊢2∈ℝ∧N∈ℝ∧N+1∈ℝ→2<N∧N<N+1→2<N+1
20 16 13 18 19 mp3an2i ⊢N∈ℕ→2<N∧N<N+1→2<N+1
21 20 expdimp ⊢N∈ℕ∧2<N→N<N+1→2<N+1
22 15 21 mpd ⊢N∈ℕ∧2<N→2<N+1
23 12 22 eqbrtrid ⊢N∈ℕ∧2<N→1⋅2<N+1
24 1red ⊢N∈ℕ∧2<N→1∈ℝ
25 18 adantr ⊢N∈ℕ∧2<N→N+1∈ℝ
26 2rp ⊢2∈ℝ+
27 26 a1i ⊢N∈ℕ∧2<N→2∈ℝ+
28 24 25 27 ltmuldivd ⊢N∈ℕ∧2<N→1⋅2<N+1↔1<N+12
29 23 28 mpbid ⊢N∈ℕ∧2<N→1<N+12
30 18 rehalfcld ⊢N∈ℕ→N+12∈ℝ
31 30 adantr ⊢N∈ℕ∧2<N→N+12∈ℝ
32 24 31 posdifd ⊢N∈ℕ∧2<N→1<N+12↔0<N+12−1
33 29 32 mpbid ⊢N∈ℕ∧2<N→0<N+12−1
34 33 adantlr ⊢N∈ℕ∧N+12∈ℕ0∧2<N→0<N+12−1
35 elnnz ⊢N+12−1∈ℕ↔N+12−1∈ℤ∧0<N+12−1
36 10 34 35 sylanbrc ⊢N∈ℕ∧N+12∈ℕ0∧2<N→N+12−1∈ℕ
37 nncn ⊢N∈ℕ→N∈ℂ
38 xp1d2m1eqxm1d2 ⊢N∈ℂ→N+12−1=N−12
39 37 38 syl ⊢N∈ℕ→N+12−1=N−12
40 39 eleq1d ⊢N∈ℕ→N+12−1∈ℕ↔N−12∈ℕ
41 40 adantr ⊢N∈ℕ∧N+12∈ℕ0→N+12−1∈ℕ↔N−12∈ℕ
42 41 adantr ⊢N∈ℕ∧N+12∈ℕ0∧2<N→N+12−1∈ℕ↔N−12∈ℕ
43 36 42 mpbid ⊢N∈ℕ∧N+12∈ℕ0∧2<N→N−12∈ℕ
44 43 a1d ⊢N∈ℕ∧N+12∈ℕ0∧2<N→N≠1→N−12∈ℕ
45 44 expcom ⊢2<N→N∈ℕ∧N+12∈ℕ0→N≠1→N−12∈ℕ
46 6 45 jaoi ⊢N=1∨2<N→N∈ℕ∧N+12∈ℕ0→N≠1→N−12∈ℕ
47 4 46 mpcom ⊢N∈ℕ∧N+12∈ℕ0→N≠1→N−12∈ℕ
48 47 impancom ⊢N∈ℕ∧N≠1→N+12∈ℕ0→N−12∈ℕ
49 1 48 sylbi ⊢N∈ℤ≥2→N+12∈ℕ0→N−12∈ℕ
50 49 imp ⊢N∈ℤ≥2∧N+12∈ℕ0→N−12∈ℕ