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

Metamath Proof Explorer

Theorem dfodd6

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

Ref Expression
Assertion dfodd6 Odd = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) }

Proof

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