Metamath Proof Explorer

Theorem dfodd6

Description: Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020)

Ref Expression
Assertion dfodd6 
|- Odd = { z e. ZZ | E. i e. ZZ z = ( ( 2 x. i ) + 1 ) }

Proof

Step Hyp Ref Expression
1 dfodd2 
 |-  Odd = { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ }
2 simpr 
 |-  ( ( z e. ZZ /\ ( ( z - 1 ) / 2 ) e. ZZ ) -> ( ( z - 1 ) / 2 ) e. ZZ )
3 oveq2 
 |-  ( i = ( ( z - 1 ) / 2 ) -> ( 2 x. i ) = ( 2 x. ( ( z - 1 ) / 2 ) ) )
4 peano2zm 
 |-  ( z e. ZZ -> ( z - 1 ) e. ZZ )
5 4 zcnd 
 |-  ( z e. ZZ -> ( z - 1 ) e. CC )
6 2cnd 
 |-  ( z e. ZZ -> 2 e. CC )
7 2ne0 
 |-  2 =/= 0
8 7 a1i 
 |-  ( z e. ZZ -> 2 =/= 0 )
9 5 6 8 3jca 
 |-  ( z e. ZZ -> ( ( z - 1 ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) )
10 9 adantr 
 |-  ( ( z e. ZZ /\ ( ( z - 1 ) / 2 ) e. ZZ ) -> ( ( z - 1 ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) )
11 divcan2 
 |-  ( ( ( z - 1 ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( ( z - 1 ) / 2 ) ) = ( z - 1 ) )
12 10 11 syl 
 |-  ( ( z e. ZZ /\ ( ( z - 1 ) / 2 ) e. ZZ ) -> ( 2 x. ( ( z - 1 ) / 2 ) ) = ( z - 1 ) )
13 3 12 sylan9eqr 
 |-  ( ( ( z e. ZZ /\ ( ( z - 1 ) / 2 ) e. ZZ ) /\ i = ( ( z - 1 ) / 2 ) ) -> ( 2 x. i ) = ( z - 1 ) )
14 13 oveq1d 
 |-  ( ( ( z e. ZZ /\ ( ( z - 1 ) / 2 ) e. ZZ ) /\ i = ( ( z - 1 ) / 2 ) ) -> ( ( 2 x. i ) + 1 ) = ( ( z - 1 ) + 1 ) )
15 zcn 
 |-  ( z e. ZZ -> z e. CC )
16 npcan1 
 |-  ( z e. CC -> ( ( z - 1 ) + 1 ) = z )
17 15 16 syl 
 |-  ( z e. ZZ -> ( ( z - 1 ) + 1 ) = z )
18 17 adantr 
 |-  ( ( z e. ZZ /\ ( ( z - 1 ) / 2 ) e. ZZ ) -> ( ( z - 1 ) + 1 ) = z )
19 18 adantr 
 |-  ( ( ( z e. ZZ /\ ( ( z - 1 ) / 2 ) e. ZZ ) /\ i = ( ( z - 1 ) / 2 ) ) -> ( ( z - 1 ) + 1 ) = z )
20 14 19 eqtrd 
 |-  ( ( ( z e. ZZ /\ ( ( z - 1 ) / 2 ) e. ZZ ) /\ i = ( ( z - 1 ) / 2 ) ) -> ( ( 2 x. i ) + 1 ) = z )
21 20 eqeq2d 
 |-  ( ( ( z e. ZZ /\ ( ( z - 1 ) / 2 ) e. ZZ ) /\ i = ( ( z - 1 ) / 2 ) ) -> ( z = ( ( 2 x. i ) + 1 ) <-> z = z ) )
22 eqidd 
 |-  ( ( z e. ZZ /\ ( ( z - 1 ) / 2 ) e. ZZ ) -> z = z )
23 2 21 22 rspcedvd 
 |-  ( ( z e. ZZ /\ ( ( z - 1 ) / 2 ) e. ZZ ) -> E. i e. ZZ z = ( ( 2 x. i ) + 1 ) )
24 23 ex 
 |-  ( z e. ZZ -> ( ( ( z - 1 ) / 2 ) e. ZZ -> E. i e. ZZ z = ( ( 2 x. i ) + 1 ) ) )
25 oveq1 
 |-  ( z = ( ( 2 x. i ) + 1 ) -> ( z - 1 ) = ( ( ( 2 x. i ) + 1 ) - 1 ) )
26 zcn 
 |-  ( i e. ZZ -> i e. CC )
27 mulcl 
 |-  ( ( 2 e. CC /\ i e. CC ) -> ( 2 x. i ) e. CC )
28 6 26 27 syl2an 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> ( 2 x. i ) e. CC )
29 pncan1 
 |-  ( ( 2 x. i ) e. CC -> ( ( ( 2 x. i ) + 1 ) - 1 ) = ( 2 x. i ) )
30 28 29 syl 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> ( ( ( 2 x. i ) + 1 ) - 1 ) = ( 2 x. i ) )
31 25 30 sylan9eqr 
 |-  ( ( ( z e. ZZ /\ i e. ZZ ) /\ z = ( ( 2 x. i ) + 1 ) ) -> ( z - 1 ) = ( 2 x. i ) )
32 31 oveq1d 
 |-  ( ( ( z e. ZZ /\ i e. ZZ ) /\ z = ( ( 2 x. i ) + 1 ) ) -> ( ( z - 1 ) / 2 ) = ( ( 2 x. i ) / 2 ) )
33 26 adantl 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> i e. CC )
34 2cnd 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> 2 e. CC )
35 7 a1i 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> 2 =/= 0 )
36 33 34 35 divcan3d 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> ( ( 2 x. i ) / 2 ) = i )
37 36 adantr 
 |-  ( ( ( z e. ZZ /\ i e. ZZ ) /\ z = ( ( 2 x. i ) + 1 ) ) -> ( ( 2 x. i ) / 2 ) = i )
38 32 37 eqtrd 
 |-  ( ( ( z e. ZZ /\ i e. ZZ ) /\ z = ( ( 2 x. i ) + 1 ) ) -> ( ( z - 1 ) / 2 ) = i )
39 simpr 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> i e. ZZ )
40 39 adantr 
 |-  ( ( ( z e. ZZ /\ i e. ZZ ) /\ z = ( ( 2 x. i ) + 1 ) ) -> i e. ZZ )
41 38 40 eqeltrd 
 |-  ( ( ( z e. ZZ /\ i e. ZZ ) /\ z = ( ( 2 x. i ) + 1 ) ) -> ( ( z - 1 ) / 2 ) e. ZZ )
42 41 rexlimdva2 
 |-  ( z e. ZZ -> ( E. i e. ZZ z = ( ( 2 x. i ) + 1 ) -> ( ( z - 1 ) / 2 ) e. ZZ ) )
43 24 42 impbid 
 |-  ( z e. ZZ -> ( ( ( z - 1 ) / 2 ) e. ZZ <-> E. i e. ZZ z = ( ( 2 x. i ) + 1 ) ) )
44 43 rabbiia 
 |-  { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ } = { z e. ZZ | E. i e. ZZ z = ( ( 2 x. i ) + 1 ) }
45 1 44 eqtri 
 |-  Odd = { z e. ZZ | E. i e. ZZ z = ( ( 2 x. i ) + 1 ) }