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 ⊢N∈ℕ0→∃n∈ℤ2⁢n+1=N∨∃k∈ℤk⋅2=N

Proof

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