This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0o

Description: An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020) (Proof shortened by AV, 2-Jun-2020)

Ref Expression
Assertion nn0o 
|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 )

Proof

Step Hyp Ref Expression
1 nn0o1gt2 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N = 1 \/ 2 < N ) )
2 1m1e0 
 |-  ( 1 - 1 ) = 0
3 2 oveq1i 
 |-  ( ( 1 - 1 ) / 2 ) = ( 0 / 2 )
4 2cn 
 |-  2 e. CC
5 2ne0 
 |-  2 =/= 0
6 4 5 div0i 
 |-  ( 0 / 2 ) = 0
7 3 6 eqtri 
 |-  ( ( 1 - 1 ) / 2 ) = 0
8 0nn0 
 |-  0 e. NN0
9 7 8 eqeltri 
 |-  ( ( 1 - 1 ) / 2 ) e. NN0
10 oveq1 
 |-  ( N = 1 -> ( N - 1 ) = ( 1 - 1 ) )
11 10 oveq1d 
 |-  ( N = 1 -> ( ( N - 1 ) / 2 ) = ( ( 1 - 1 ) / 2 ) )
12 11 eleq1d 
 |-  ( N = 1 -> ( ( ( N - 1 ) / 2 ) e. NN0 <-> ( ( 1 - 1 ) / 2 ) e. NN0 ) )
13 12 adantr 
 |-  ( ( N = 1 /\ ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) ) -> ( ( ( N - 1 ) / 2 ) e. NN0 <-> ( ( 1 - 1 ) / 2 ) e. NN0 ) )
14 9 13 mpbiri 
 |-  ( ( N = 1 /\ ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) ) -> ( ( N - 1 ) / 2 ) e. NN0 )
15 14 ex 
 |-  ( N = 1 -> ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 ) )
16 2z 
 |-  2 e. ZZ
17 16 a1i 
 |-  ( ( 2 < N /\ ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) ) -> 2 e. ZZ )
18 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
19 18 ad2antrl 
 |-  ( ( 2 < N /\ ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) ) -> N e. ZZ )
20 2re 
 |-  2 e. RR
21 nn0re 
 |-  ( N e. NN0 -> N e. RR )
22 ltle 
 |-  ( ( 2 e. RR /\ N e. RR ) -> ( 2 < N -> 2 <_ N ) )
23 20 21 22 sylancr 
 |-  ( N e. NN0 -> ( 2 < N -> 2 <_ N ) )
24 23 adantr 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( 2 < N -> 2 <_ N ) )
25 24 impcom 
 |-  ( ( 2 < N /\ ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) ) -> 2 <_ N )
26 eluz2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) )
27 17 19 25 26 syl3anbrc 
 |-  ( ( 2 < N /\ ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) ) -> N e. ( ZZ>= ` 2 ) )
28 simprr 
 |-  ( ( 2 < N /\ ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) ) -> ( ( N + 1 ) / 2 ) e. NN0 )
29 27 28 jca 
 |-  ( ( 2 < N /\ ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) ) -> ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) )
30 nno 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN )
31 nnnn0 
 |-  ( ( ( N - 1 ) / 2 ) e. NN -> ( ( N - 1 ) / 2 ) e. NN0 )
32 29 30 31 3syl 
 |-  ( ( 2 < N /\ ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) ) -> ( ( N - 1 ) / 2 ) e. NN0 )
33 32 ex 
 |-  ( 2 < N -> ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 ) )
34 15 33 jaoi 
 |-  ( ( N = 1 \/ 2 < N ) -> ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 ) )
35 1 34 mpcom 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 )