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 ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ )

Proof

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