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 e. NN0 -> ( E. n e. ZZ ( ( 2 x. n ) + 1 ) = N \/ E. k e. ZZ ( k x. 2 ) = N ) )

Proof

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