Step |
Hyp |
Ref |
Expression |
1 |
|
halfnz |
|- -. ( 1 / 2 ) e. ZZ |
2 |
|
2cn |
|- 2 e. CC |
3 |
|
zcn |
|- ( A e. ZZ -> A e. CC ) |
4 |
3
|
adantr |
|- ( ( A e. ZZ /\ B e. ZZ ) -> A e. CC ) |
5 |
|
mulcl |
|- ( ( 2 e. CC /\ A e. CC ) -> ( 2 x. A ) e. CC ) |
6 |
2 4 5
|
sylancr |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( 2 x. A ) e. CC ) |
7 |
|
zcn |
|- ( B e. ZZ -> B e. CC ) |
8 |
7
|
adantl |
|- ( ( A e. ZZ /\ B e. ZZ ) -> B e. CC ) |
9 |
|
mulcl |
|- ( ( 2 e. CC /\ B e. CC ) -> ( 2 x. B ) e. CC ) |
10 |
2 8 9
|
sylancr |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( 2 x. B ) e. CC ) |
11 |
|
1cnd |
|- ( ( A e. ZZ /\ B e. ZZ ) -> 1 e. CC ) |
12 |
6 10 11
|
subaddd |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( 2 x. A ) - ( 2 x. B ) ) = 1 <-> ( ( 2 x. B ) + 1 ) = ( 2 x. A ) ) ) |
13 |
2
|
a1i |
|- ( ( A e. ZZ /\ B e. ZZ ) -> 2 e. CC ) |
14 |
13 4 8
|
subdid |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( 2 x. ( A - B ) ) = ( ( 2 x. A ) - ( 2 x. B ) ) ) |
15 |
14
|
oveq1d |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 2 x. ( A - B ) ) / 2 ) = ( ( ( 2 x. A ) - ( 2 x. B ) ) / 2 ) ) |
16 |
|
zsubcl |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A - B ) e. ZZ ) |
17 |
|
zcn |
|- ( ( A - B ) e. ZZ -> ( A - B ) e. CC ) |
18 |
16 17
|
syl |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A - B ) e. CC ) |
19 |
|
2ne0 |
|- 2 =/= 0 |
20 |
19
|
a1i |
|- ( ( A e. ZZ /\ B e. ZZ ) -> 2 =/= 0 ) |
21 |
18 13 20
|
divcan3d |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 2 x. ( A - B ) ) / 2 ) = ( A - B ) ) |
22 |
15 21
|
eqtr3d |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( 2 x. A ) - ( 2 x. B ) ) / 2 ) = ( A - B ) ) |
23 |
22 16
|
eqeltrd |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( 2 x. A ) - ( 2 x. B ) ) / 2 ) e. ZZ ) |
24 |
|
oveq1 |
|- ( ( ( 2 x. A ) - ( 2 x. B ) ) = 1 -> ( ( ( 2 x. A ) - ( 2 x. B ) ) / 2 ) = ( 1 / 2 ) ) |
25 |
24
|
eleq1d |
|- ( ( ( 2 x. A ) - ( 2 x. B ) ) = 1 -> ( ( ( ( 2 x. A ) - ( 2 x. B ) ) / 2 ) e. ZZ <-> ( 1 / 2 ) e. ZZ ) ) |
26 |
23 25
|
syl5ibcom |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( 2 x. A ) - ( 2 x. B ) ) = 1 -> ( 1 / 2 ) e. ZZ ) ) |
27 |
12 26
|
sylbird |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( 2 x. B ) + 1 ) = ( 2 x. A ) -> ( 1 / 2 ) e. ZZ ) ) |
28 |
27
|
necon3bd |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( -. ( 1 / 2 ) e. ZZ -> ( ( 2 x. B ) + 1 ) =/= ( 2 x. A ) ) ) |
29 |
1 28
|
mpi |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 2 x. B ) + 1 ) =/= ( 2 x. A ) ) |
30 |
29
|
necomd |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( 2 x. A ) =/= ( ( 2 x. B ) + 1 ) ) |