Metamath Proof Explorer

Theorem oddge22np1

Description: An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021) (Proof shortened by AV, 9-Jul-2022)

Ref Expression
Assertion oddge22np1 
|- ( N e. ( ZZ>= ` 2 ) -> ( -. 2 || N <-> E. n e. NN ( ( 2 x. n ) + 1 ) = N ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( ( ( 2 x. n ) + 1 ) e. ( ZZ>= ` 2 ) <-> N e. ( ZZ>= ` 2 ) ) )
2 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
3 2 adantl 
 |-  ( ( ( ( 2 x. n ) + 1 ) e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> n e. ZZ )
4 eluz2 
 |-  ( ( ( 2 x. n ) + 1 ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( ( 2 x. n ) + 1 ) e. ZZ /\ 2 <_ ( ( 2 x. n ) + 1 ) ) )
5 2re 
 |-  2 e. RR
6 5 a1i 
 |-  ( n e. NN0 -> 2 e. RR )
7 1red 
 |-  ( n e. NN0 -> 1 e. RR )
8 2nn0 
 |-  2 e. NN0
9 8 a1i 
 |-  ( n e. NN0 -> 2 e. NN0 )
10 id 
 |-  ( n e. NN0 -> n e. NN0 )
11 9 10 nn0mulcld 
 |-  ( n e. NN0 -> ( 2 x. n ) e. NN0 )
12 11 nn0red 
 |-  ( n e. NN0 -> ( 2 x. n ) e. RR )
13 6 7 12 lesubaddd 
 |-  ( n e. NN0 -> ( ( 2 - 1 ) <_ ( 2 x. n ) <-> 2 <_ ( ( 2 x. n ) + 1 ) ) )
14 2m1e1 
 |-  ( 2 - 1 ) = 1
15 14 breq1i 
 |-  ( ( 2 - 1 ) <_ ( 2 x. n ) <-> 1 <_ ( 2 x. n ) )
16 nn0re 
 |-  ( n e. NN0 -> n e. RR )
17 2rp 
 |-  2 e. RR+
18 17 a1i 
 |-  ( n e. NN0 -> 2 e. RR+ )
19 7 16 18 ledivmuld 
 |-  ( n e. NN0 -> ( ( 1 / 2 ) <_ n <-> 1 <_ ( 2 x. n ) ) )
20 halfgt0 
 |-  0 < ( 1 / 2 )
21 0red 
 |-  ( n e. NN0 -> 0 e. RR )
22 halfre 
 |-  ( 1 / 2 ) e. RR
23 22 a1i 
 |-  ( n e. NN0 -> ( 1 / 2 ) e. RR )
24 ltletr 
 |-  ( ( 0 e. RR /\ ( 1 / 2 ) e. RR /\ n e. RR ) -> ( ( 0 < ( 1 / 2 ) /\ ( 1 / 2 ) <_ n ) -> 0 < n ) )
25 21 23 16 24 syl3anc 
 |-  ( n e. NN0 -> ( ( 0 < ( 1 / 2 ) /\ ( 1 / 2 ) <_ n ) -> 0 < n ) )
26 20 25 mpani 
 |-  ( n e. NN0 -> ( ( 1 / 2 ) <_ n -> 0 < n ) )
27 19 26 sylbird 
 |-  ( n e. NN0 -> ( 1 <_ ( 2 x. n ) -> 0 < n ) )
28 15 27 biimtrid 
 |-  ( n e. NN0 -> ( ( 2 - 1 ) <_ ( 2 x. n ) -> 0 < n ) )
29 13 28 sylbird 
 |-  ( n e. NN0 -> ( 2 <_ ( ( 2 x. n ) + 1 ) -> 0 < n ) )
30 29 com12 
 |-  ( 2 <_ ( ( 2 x. n ) + 1 ) -> ( n e. NN0 -> 0 < n ) )
31 30 3ad2ant3 
 |-  ( ( 2 e. ZZ /\ ( ( 2 x. n ) + 1 ) e. ZZ /\ 2 <_ ( ( 2 x. n ) + 1 ) ) -> ( n e. NN0 -> 0 < n ) )
32 4 31 sylbi 
 |-  ( ( ( 2 x. n ) + 1 ) e. ( ZZ>= ` 2 ) -> ( n e. NN0 -> 0 < n ) )
33 32 imp 
 |-  ( ( ( ( 2 x. n ) + 1 ) e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> 0 < n )
34 elnnz 
 |-  ( n e. NN <-> ( n e. ZZ /\ 0 < n ) )
35 3 33 34 sylanbrc 
 |-  ( ( ( ( 2 x. n ) + 1 ) e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> n e. NN )
36 35 ex 
 |-  ( ( ( 2 x. n ) + 1 ) e. ( ZZ>= ` 2 ) -> ( n e. NN0 -> n e. NN ) )
37 1 36 biimtrrdi 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( N e. ( ZZ>= ` 2 ) -> ( n e. NN0 -> n e. NN ) ) )
38 37 com13 
 |-  ( n e. NN0 -> ( N e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. n ) + 1 ) = N -> n e. NN ) ) )
39 38 impcom 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> ( ( ( 2 x. n ) + 1 ) = N -> n e. NN ) )
40 39 pm4.71rd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> ( ( ( 2 x. n ) + 1 ) = N <-> ( n e. NN /\ ( ( 2 x. n ) + 1 ) = N ) ) )
41 40 bicomd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> ( ( n e. NN /\ ( ( 2 x. n ) + 1 ) = N ) <-> ( ( 2 x. n ) + 1 ) = N ) )
42 41 rexbidva 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( E. n e. NN0 ( n e. NN /\ ( ( 2 x. n ) + 1 ) = N ) <-> E. n e. NN0 ( ( 2 x. n ) + 1 ) = N ) )
43 nnssnn0 
 |-  NN C_ NN0
44 rexss 
 |-  ( NN C_ NN0 -> ( E. n e. NN ( ( 2 x. n ) + 1 ) = N <-> E. n e. NN0 ( n e. NN /\ ( ( 2 x. n ) + 1 ) = N ) ) )
45 43 44 mp1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( E. n e. NN ( ( 2 x. n ) + 1 ) = N <-> E. n e. NN0 ( n e. NN /\ ( ( 2 x. n ) + 1 ) = N ) ) )
46 eluzge2nn0 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN0 )
47 oddnn02np1 
 |-  ( N e. NN0 -> ( -. 2 || N <-> E. n e. NN0 ( ( 2 x. n ) + 1 ) = N ) )
48 46 47 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( -. 2 || N <-> E. n e. NN0 ( ( 2 x. n ) + 1 ) = N ) )
49 42 45 48 3bitr4rd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( -. 2 || N <-> E. n e. NN ( ( 2 x. n ) + 1 ) = N ) )