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 mullidi ⊢ ( 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 ) ∈ ℕ )