Metamath Proof Explorer

Theorem odd2np1lem

Description: Lemma for odd2np1 . (Contributed by Scott Fenton, 3-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion odd2np1lem ( 𝑁 ∈ ℕ0 → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ ( 𝑗 = 0 → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ↔ ( ( 2 · 𝑛 ) + 1 ) = 0 ) )
2 1 rexbidv ⊢ ( 𝑗 = 0 → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 0 ) )
3 eqeq2 ⊢ ( 𝑗 = 0 → ( ( 𝑘 · 2 ) = 𝑗 ↔ ( 𝑘 · 2 ) = 0 ) )
4 3 rexbidv ⊢ ( 𝑗 = 0 → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑗 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 0 ) )
5 2 4 orbi12d ⊢ ( 𝑗 = 0 → ( ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑗 ) ↔ ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 0 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 0 ) ) )
6 eqeq2 ⊢ ( 𝑗 = 𝑚 → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ↔ ( ( 2 · 𝑛 ) + 1 ) = 𝑚 ) )
7 6 rexbidv ⊢ ( 𝑗 = 𝑚 → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑚 ) )
8 oveq2 ⊢ ( 𝑛 = 𝑥 → ( 2 · 𝑛 ) = ( 2 · 𝑥 ) )
9 8 oveq1d ⊢ ( 𝑛 = 𝑥 → ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑥 ) + 1 ) )
10 9 eqeq1d ⊢ ( 𝑛 = 𝑥 → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑚 ↔ ( ( 2 · 𝑥 ) + 1 ) = 𝑚 ) )
11 10 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑚 ↔ ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = 𝑚 )
12 7 11 bitrdi ⊢ ( 𝑗 = 𝑚 → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ↔ ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = 𝑚 ) )
13 eqeq2 ⊢ ( 𝑗 = 𝑚 → ( ( 𝑘 · 2 ) = 𝑗 ↔ ( 𝑘 · 2 ) = 𝑚 ) )
14 13 rexbidv ⊢ ( 𝑗 = 𝑚 → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑗 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑚 ) )
15 oveq1 ⊢ ( 𝑘 = 𝑦 → ( 𝑘 · 2 ) = ( 𝑦 · 2 ) )
16 15 eqeq1d ⊢ ( 𝑘 = 𝑦 → ( ( 𝑘 · 2 ) = 𝑚 ↔ ( 𝑦 · 2 ) = 𝑚 ) )
17 16 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑚 ↔ ∃ 𝑦 ∈ ℤ ( 𝑦 · 2 ) = 𝑚 )
18 14 17 bitrdi ⊢ ( 𝑗 = 𝑚 → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑗 ↔ ∃ 𝑦 ∈ ℤ ( 𝑦 · 2 ) = 𝑚 ) )
19 12 18 orbi12d ⊢ ( 𝑗 = 𝑚 → ( ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑗 ) ↔ ( ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = 𝑚 ∨ ∃ 𝑦 ∈ ℤ ( 𝑦 · 2 ) = 𝑚 ) ) )
20 eqeq2 ⊢ ( 𝑗 = ( 𝑚 + 1 ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ↔ ( ( 2 · 𝑛 ) + 1 ) = ( 𝑚 + 1 ) ) )
21 20 rexbidv ⊢ ( 𝑗 = ( 𝑚 + 1 ) → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( 𝑚 + 1 ) ) )
22 eqeq2 ⊢ ( 𝑗 = ( 𝑚 + 1 ) → ( ( 𝑘 · 2 ) = 𝑗 ↔ ( 𝑘 · 2 ) = ( 𝑚 + 1 ) ) )
23 22 rexbidv ⊢ ( 𝑗 = ( 𝑚 + 1 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑗 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( 𝑚 + 1 ) ) )
24 21 23 orbi12d ⊢ ( 𝑗 = ( 𝑚 + 1 ) → ( ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑗 ) ↔ ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( 𝑚 + 1 ) ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( 𝑚 + 1 ) ) ) )
25 eqeq2 ⊢ ( 𝑗 = 𝑁 → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ↔ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
26 25 rexbidv ⊢ ( 𝑗 = 𝑁 → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
27 eqeq2 ⊢ ( 𝑗 = 𝑁 → ( ( 𝑘 · 2 ) = 𝑗 ↔ ( 𝑘 · 2 ) = 𝑁 ) )
28 27 rexbidv ⊢ ( 𝑗 = 𝑁 → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑗 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )
29 26 28 orbi12d ⊢ ( 𝑗 = 𝑁 → ( ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑗 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑗 ) ↔ ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) ) )
30 0z ⊢ 0 ∈ ℤ
31 2cn ⊢ 2 ∈ ℂ
32 31 mul02i ⊢ ( 0 · 2 ) = 0
33 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 · 2 ) = ( 0 · 2 ) )
34 33 eqeq1d ⊢ ( 𝑘 = 0 → ( ( 𝑘 · 2 ) = 0 ↔ ( 0 · 2 ) = 0 ) )
35 34 rspcev ⊢ ( ( 0 ∈ ℤ ∧ ( 0 · 2 ) = 0 ) → ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 0 )
36 30 32 35 mp2an ⊢ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 0
37 36 olci ⊢ ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 0 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 0 )
38 orcom ⊢ ( ( ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = 𝑚 ∨ ∃ 𝑦 ∈ ℤ ( 𝑦 · 2 ) = 𝑚 ) ↔ ( ∃ 𝑦 ∈ ℤ ( 𝑦 · 2 ) = 𝑚 ∨ ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = 𝑚 ) )
39 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
40 mulcom ⊢ ( ( 𝑦 ∈ ℂ ∧ 2 ∈ ℂ ) → ( 𝑦 · 2 ) = ( 2 · 𝑦 ) )
41 39 31 40 sylancl ⊢ ( 𝑦 ∈ ℤ → ( 𝑦 · 2 ) = ( 2 · 𝑦 ) )
42 41 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) → ( 𝑦 · 2 ) = ( 2 · 𝑦 ) )
43 42 eqeq1d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) → ( ( 𝑦 · 2 ) = 𝑚 ↔ ( 2 · 𝑦 ) = 𝑚 ) )
44 eqid ⊢ ( ( 2 · 𝑦 ) + 1 ) = ( ( 2 · 𝑦 ) + 1 )
45 oveq2 ⊢ ( 𝑛 = 𝑦 → ( 2 · 𝑛 ) = ( 2 · 𝑦 ) )
46 45 oveq1d ⊢ ( 𝑛 = 𝑦 → ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑦 ) + 1 ) )
47 46 eqeq1d ⊢ ( 𝑛 = 𝑦 → ( ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑦 ) + 1 ) ↔ ( ( 2 · 𝑦 ) + 1 ) = ( ( 2 · 𝑦 ) + 1 ) ) )
48 47 rspcev ⊢ ( ( 𝑦 ∈ ℤ ∧ ( ( 2 · 𝑦 ) + 1 ) = ( ( 2 · 𝑦 ) + 1 ) ) → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑦 ) + 1 ) )
49 44 48 mpan2 ⊢ ( 𝑦 ∈ ℤ → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑦 ) + 1 ) )
50 oveq1 ⊢ ( ( 2 · 𝑦 ) = 𝑚 → ( ( 2 · 𝑦 ) + 1 ) = ( 𝑚 + 1 ) )
51 50 eqeq2d ⊢ ( ( 2 · 𝑦 ) = 𝑚 → ( ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑦 ) + 1 ) ↔ ( ( 2 · 𝑛 ) + 1 ) = ( 𝑚 + 1 ) ) )
52 51 rexbidv ⊢ ( ( 2 · 𝑦 ) = 𝑚 → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑦 ) + 1 ) ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( 𝑚 + 1 ) ) )
53 49 52 syl5ibcom ⊢ ( 𝑦 ∈ ℤ → ( ( 2 · 𝑦 ) = 𝑚 → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( 𝑚 + 1 ) ) )
54 53 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) → ( ( 2 · 𝑦 ) = 𝑚 → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( 𝑚 + 1 ) ) )
55 43 54 sylbid ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) → ( ( 𝑦 · 2 ) = 𝑚 → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( 𝑚 + 1 ) ) )
56 55 rexlimdva ⊢ ( 𝑚 ∈ ℕ0 → ( ∃ 𝑦 ∈ ℤ ( 𝑦 · 2 ) = 𝑚 → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( 𝑚 + 1 ) ) )
57 peano2z ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 + 1 ) ∈ ℤ )
58 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
59 mulcom ⊢ ( ( 𝑥 ∈ ℂ ∧ 2 ∈ ℂ ) → ( 𝑥 · 2 ) = ( 2 · 𝑥 ) )
60 31 59 mpan2 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 2 ) = ( 2 · 𝑥 ) )
61 31 mulid2i ⊢ ( 1 · 2 ) = 2
62 61 a1i ⊢ ( 𝑥 ∈ ℂ → ( 1 · 2 ) = 2 )
63 60 62 oveq12d ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 · 2 ) + ( 1 · 2 ) ) = ( ( 2 · 𝑥 ) + 2 ) )
64 df-2 ⊢ 2 = ( 1 + 1 )
65 64 oveq2i ⊢ ( ( 2 · 𝑥 ) + 2 ) = ( ( 2 · 𝑥 ) + ( 1 + 1 ) )
66 63 65 eqtrdi ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 · 2 ) + ( 1 · 2 ) ) = ( ( 2 · 𝑥 ) + ( 1 + 1 ) ) )
67 ax-1cn ⊢ 1 ∈ ℂ
68 adddir ⊢ ( ( 𝑥 ∈ ℂ ∧ 1 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 𝑥 + 1 ) · 2 ) = ( ( 𝑥 · 2 ) + ( 1 · 2 ) ) )
69 67 31 68 mp3an23 ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 + 1 ) · 2 ) = ( ( 𝑥 · 2 ) + ( 1 · 2 ) ) )
70 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 2 · 𝑥 ) ∈ ℂ )
71 31 70 mpan ⊢ ( 𝑥 ∈ ℂ → ( 2 · 𝑥 ) ∈ ℂ )
72 addass ⊢ ( ( ( 2 · 𝑥 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) = ( ( 2 · 𝑥 ) + ( 1 + 1 ) ) )
73 67 67 72 mp3an23 ⊢ ( ( 2 · 𝑥 ) ∈ ℂ → ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) = ( ( 2 · 𝑥 ) + ( 1 + 1 ) ) )
74 71 73 syl ⊢ ( 𝑥 ∈ ℂ → ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) = ( ( 2 · 𝑥 ) + ( 1 + 1 ) ) )
75 66 69 74 3eqtr4d ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 + 1 ) · 2 ) = ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) )
76 58 75 syl ⊢ ( 𝑥 ∈ ℤ → ( ( 𝑥 + 1 ) · 2 ) = ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) )
77 76 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 + 1 ) · 2 ) = ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) )
78 oveq1 ⊢ ( 𝑘 = ( 𝑥 + 1 ) → ( 𝑘 · 2 ) = ( ( 𝑥 + 1 ) · 2 ) )
79 78 eqeq1d ⊢ ( 𝑘 = ( 𝑥 + 1 ) → ( ( 𝑘 · 2 ) = ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) ↔ ( ( 𝑥 + 1 ) · 2 ) = ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) ) )
80 79 rspcev ⊢ ( ( ( 𝑥 + 1 ) ∈ ℤ ∧ ( ( 𝑥 + 1 ) · 2 ) = ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) ) → ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) )
81 57 77 80 syl2an2 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) )
82 oveq1 ⊢ ( ( ( 2 · 𝑥 ) + 1 ) = 𝑚 → ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) = ( 𝑚 + 1 ) )
83 82 eqeq2d ⊢ ( ( ( 2 · 𝑥 ) + 1 ) = 𝑚 → ( ( 𝑘 · 2 ) = ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) ↔ ( 𝑘 · 2 ) = ( 𝑚 + 1 ) ) )
84 83 rexbidv ⊢ ( ( ( 2 · 𝑥 ) + 1 ) = 𝑚 → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( ( ( 2 · 𝑥 ) + 1 ) + 1 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( 𝑚 + 1 ) ) )
85 81 84 syl5ibcom ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ( ( ( 2 · 𝑥 ) + 1 ) = 𝑚 → ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( 𝑚 + 1 ) ) )
86 85 rexlimdva ⊢ ( 𝑚 ∈ ℕ0 → ( ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = 𝑚 → ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( 𝑚 + 1 ) ) )
87 56 86 orim12d ⊢ ( 𝑚 ∈ ℕ0 → ( ( ∃ 𝑦 ∈ ℤ ( 𝑦 · 2 ) = 𝑚 ∨ ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = 𝑚 ) → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( 𝑚 + 1 ) ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( 𝑚 + 1 ) ) ) )
88 38 87 syl5bi ⊢ ( 𝑚 ∈ ℕ0 → ( ( ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = 𝑚 ∨ ∃ 𝑦 ∈ ℤ ( 𝑦 · 2 ) = 𝑚 ) → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( 𝑚 + 1 ) ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = ( 𝑚 + 1 ) ) ) )
89 5 19 24 29 37 88 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )