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 ) = 𝑁 ) )