Metamath Proof Explorer

Theorem dfodd6

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

Ref Expression
Assertion dfodd6 ⊢Odd=z∈ℤ|∃i∈ℤz=2⁢i+1

Proof

Step Hyp Ref Expression
1 dfodd2 ⊢Odd=z∈ℤ|z−12∈ℤ
2 simpr ⊢z∈ℤ∧z−12∈ℤ→z−12∈ℤ
3 oveq2 ⊢i=z−12→2⁢i=2⁢z−12
4 peano2zm ⊢z∈ℤ→z−1∈ℤ
5 4 zcnd ⊢z∈ℤ→z−1∈ℂ
6 2cnd ⊢z∈ℤ→2∈ℂ
7 2ne0 ⊢2≠0
8 7 a1i ⊢z∈ℤ→2≠0
9 5 6 8 3jca ⊢z∈ℤ→z−1∈ℂ∧2∈ℂ∧2≠0
10 9 adantr ⊢z∈ℤ∧z−12∈ℤ→z−1∈ℂ∧2∈ℂ∧2≠0
11 divcan2 ⊢z−1∈ℂ∧2∈ℂ∧2≠0→2⁢z−12=z−1
12 10 11 syl ⊢z∈ℤ∧z−12∈ℤ→2⁢z−12=z−1
13 3 12 sylan9eqr ⊢z∈ℤ∧z−12∈ℤ∧i=z−12→2⁢i=z−1
14 13 oveq1d ⊢z∈ℤ∧z−12∈ℤ∧i=z−12→2⁢i+1=z-1+1
15 zcn ⊢z∈ℤ→z∈ℂ
16 npcan1 ⊢z∈ℂ→z-1+1=z
17 15 16 syl ⊢z∈ℤ→z-1+1=z
18 17 adantr ⊢z∈ℤ∧z−12∈ℤ→z-1+1=z
19 18 adantr ⊢z∈ℤ∧z−12∈ℤ∧i=z−12→z-1+1=z
20 14 19 eqtrd ⊢z∈ℤ∧z−12∈ℤ∧i=z−12→2⁢i+1=z
21 20 eqeq2d ⊢z∈ℤ∧z−12∈ℤ∧i=z−12→z=2⁢i+1↔z=z
22 eqidd ⊢z∈ℤ∧z−12∈ℤ→z=z
23 2 21 22 rspcedvd ⊢z∈ℤ∧z−12∈ℤ→∃i∈ℤz=2⁢i+1
24 23 ex ⊢z∈ℤ→z−12∈ℤ→∃i∈ℤz=2⁢i+1
25 oveq1 ⊢z=2⁢i+1→z−1=2⁢i+1-1
26 zcn ⊢i∈ℤ→i∈ℂ
27 mulcl ⊢2∈ℂ∧i∈ℂ→2⁢i∈ℂ
28 6 26 27 syl2an ⊢z∈ℤ∧i∈ℤ→2⁢i∈ℂ
29 pncan1 ⊢2⁢i∈ℂ→2⁢i+1-1=2⁢i
30 28 29 syl ⊢z∈ℤ∧i∈ℤ→2⁢i+1-1=2⁢i
31 25 30 sylan9eqr ⊢z∈ℤ∧i∈ℤ∧z=2⁢i+1→z−1=2⁢i
32 31 oveq1d ⊢z∈ℤ∧i∈ℤ∧z=2⁢i+1→z−12=2⁢i2
33 26 adantl ⊢z∈ℤ∧i∈ℤ→i∈ℂ
34 2cnd ⊢z∈ℤ∧i∈ℤ→2∈ℂ
35 7 a1i ⊢z∈ℤ∧i∈ℤ→2≠0
36 33 34 35 divcan3d ⊢z∈ℤ∧i∈ℤ→2⁢i2=i
37 36 adantr ⊢z∈ℤ∧i∈ℤ∧z=2⁢i+1→2⁢i2=i
38 32 37 eqtrd ⊢z∈ℤ∧i∈ℤ∧z=2⁢i+1→z−12=i
39 simpr ⊢z∈ℤ∧i∈ℤ→i∈ℤ
40 39 adantr ⊢z∈ℤ∧i∈ℤ∧z=2⁢i+1→i∈ℤ
41 38 40 eqeltrd ⊢z∈ℤ∧i∈ℤ∧z=2⁢i+1→z−12∈ℤ
42 41 rexlimdva2 ⊢z∈ℤ→∃i∈ℤz=2⁢i+1→z−12∈ℤ
43 24 42 impbid ⊢z∈ℤ→z−12∈ℤ↔∃i∈ℤz=2⁢i+1
44 43 rabbiia ⊢z∈ℤ|z−12∈ℤ=z∈ℤ|∃i∈ℤz=2⁢i+1
45 1 44 eqtri ⊢Odd=z∈ℤ|∃i∈ℤz=2⁢i+1