Step |
Hyp |
Ref |
Expression |
1 |
|
zcn |
|- ( N e. ZZ -> N e. CC ) |
2 |
|
sqval |
|- ( N e. CC -> ( N ^ 2 ) = ( N x. N ) ) |
3 |
1 2
|
syl |
|- ( N e. ZZ -> ( N ^ 2 ) = ( N x. N ) ) |
4 |
3
|
oveq1d |
|- ( N e. ZZ -> ( ( N ^ 2 ) / 2 ) = ( ( N x. N ) / 2 ) ) |
5 |
|
2cnd |
|- ( N e. ZZ -> 2 e. CC ) |
6 |
|
2ne0 |
|- 2 =/= 0 |
7 |
6
|
a1i |
|- ( N e. ZZ -> 2 =/= 0 ) |
8 |
1 1 5 7
|
divassd |
|- ( N e. ZZ -> ( ( N x. N ) / 2 ) = ( N x. ( N / 2 ) ) ) |
9 |
4 8
|
eqtrd |
|- ( N e. ZZ -> ( ( N ^ 2 ) / 2 ) = ( N x. ( N / 2 ) ) ) |
10 |
9
|
adantr |
|- ( ( N e. ZZ /\ ( N / 2 ) e. ZZ ) -> ( ( N ^ 2 ) / 2 ) = ( N x. ( N / 2 ) ) ) |
11 |
|
zmulcl |
|- ( ( N e. ZZ /\ ( N / 2 ) e. ZZ ) -> ( N x. ( N / 2 ) ) e. ZZ ) |
12 |
10 11
|
eqeltrd |
|- ( ( N e. ZZ /\ ( N / 2 ) e. ZZ ) -> ( ( N ^ 2 ) / 2 ) e. ZZ ) |
13 |
1
|
adantr |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> N e. CC ) |
14 |
|
sqcl |
|- ( N e. CC -> ( N ^ 2 ) e. CC ) |
15 |
13 14
|
syl |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( N ^ 2 ) e. CC ) |
16 |
|
peano2cn |
|- ( ( N ^ 2 ) e. CC -> ( ( N ^ 2 ) + 1 ) e. CC ) |
17 |
15 16
|
syl |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N ^ 2 ) + 1 ) e. CC ) |
18 |
17
|
halfcld |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( N ^ 2 ) + 1 ) / 2 ) e. CC ) |
19 |
18 13
|
pncand |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + N ) - N ) = ( ( ( N ^ 2 ) + 1 ) / 2 ) ) |
20 |
|
binom21 |
|- ( N e. CC -> ( ( N + 1 ) ^ 2 ) = ( ( ( N ^ 2 ) + ( 2 x. N ) ) + 1 ) ) |
21 |
13 20
|
syl |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) ^ 2 ) = ( ( ( N ^ 2 ) + ( 2 x. N ) ) + 1 ) ) |
22 |
|
peano2cn |
|- ( N e. CC -> ( N + 1 ) e. CC ) |
23 |
13 22
|
syl |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( N + 1 ) e. CC ) |
24 |
|
sqval |
|- ( ( N + 1 ) e. CC -> ( ( N + 1 ) ^ 2 ) = ( ( N + 1 ) x. ( N + 1 ) ) ) |
25 |
23 24
|
syl |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) ^ 2 ) = ( ( N + 1 ) x. ( N + 1 ) ) ) |
26 |
|
2cn |
|- 2 e. CC |
27 |
|
mulcl |
|- ( ( 2 e. CC /\ N e. CC ) -> ( 2 x. N ) e. CC ) |
28 |
26 13 27
|
sylancr |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( 2 x. N ) e. CC ) |
29 |
|
1cnd |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> 1 e. CC ) |
30 |
15 28 29
|
add32d |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( N ^ 2 ) + ( 2 x. N ) ) + 1 ) = ( ( ( N ^ 2 ) + 1 ) + ( 2 x. N ) ) ) |
31 |
21 25 30
|
3eqtr3d |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) x. ( N + 1 ) ) = ( ( ( N ^ 2 ) + 1 ) + ( 2 x. N ) ) ) |
32 |
31
|
oveq1d |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( N + 1 ) x. ( N + 1 ) ) / 2 ) = ( ( ( ( N ^ 2 ) + 1 ) + ( 2 x. N ) ) / 2 ) ) |
33 |
|
2cnd |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> 2 e. CC ) |
34 |
6
|
a1i |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> 2 =/= 0 ) |
35 |
23 23 33 34
|
divassd |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( N + 1 ) x. ( N + 1 ) ) / 2 ) = ( ( N + 1 ) x. ( ( N + 1 ) / 2 ) ) ) |
36 |
17 28 33 34
|
divdird |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( N ^ 2 ) + 1 ) + ( 2 x. N ) ) / 2 ) = ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + ( ( 2 x. N ) / 2 ) ) ) |
37 |
13 33 34
|
divcan3d |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( 2 x. N ) / 2 ) = N ) |
38 |
37
|
oveq2d |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + ( ( 2 x. N ) / 2 ) ) = ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + N ) ) |
39 |
36 38
|
eqtrd |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( N ^ 2 ) + 1 ) + ( 2 x. N ) ) / 2 ) = ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + N ) ) |
40 |
32 35 39
|
3eqtr3d |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) x. ( ( N + 1 ) / 2 ) ) = ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + N ) ) |
41 |
|
peano2z |
|- ( N e. ZZ -> ( N + 1 ) e. ZZ ) |
42 |
|
zmulcl |
|- ( ( ( N + 1 ) e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) x. ( ( N + 1 ) / 2 ) ) e. ZZ ) |
43 |
41 42
|
sylan |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) x. ( ( N + 1 ) / 2 ) ) e. ZZ ) |
44 |
40 43
|
eqeltrrd |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + N ) e. ZZ ) |
45 |
|
simpl |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> N e. ZZ ) |
46 |
44 45
|
zsubcld |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( ( N ^ 2 ) + 1 ) / 2 ) + N ) - N ) e. ZZ ) |
47 |
19 46
|
eqeltrrd |
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( N ^ 2 ) + 1 ) / 2 ) e. ZZ ) |
48 |
47
|
ex |
|- ( N e. ZZ -> ( ( ( N + 1 ) / 2 ) e. ZZ -> ( ( ( N ^ 2 ) + 1 ) / 2 ) e. ZZ ) ) |
49 |
48
|
con3d |
|- ( N e. ZZ -> ( -. ( ( ( N ^ 2 ) + 1 ) / 2 ) e. ZZ -> -. ( ( N + 1 ) / 2 ) e. ZZ ) ) |
50 |
|
zsqcl |
|- ( N e. ZZ -> ( N ^ 2 ) e. ZZ ) |
51 |
|
zeo2 |
|- ( ( N ^ 2 ) e. ZZ -> ( ( ( N ^ 2 ) / 2 ) e. ZZ <-> -. ( ( ( N ^ 2 ) + 1 ) / 2 ) e. ZZ ) ) |
52 |
50 51
|
syl |
|- ( N e. ZZ -> ( ( ( N ^ 2 ) / 2 ) e. ZZ <-> -. ( ( ( N ^ 2 ) + 1 ) / 2 ) e. ZZ ) ) |
53 |
|
zeo2 |
|- ( N e. ZZ -> ( ( N / 2 ) e. ZZ <-> -. ( ( N + 1 ) / 2 ) e. ZZ ) ) |
54 |
49 52 53
|
3imtr4d |
|- ( N e. ZZ -> ( ( ( N ^ 2 ) / 2 ) e. ZZ -> ( N / 2 ) e. ZZ ) ) |
55 |
54
|
imp |
|- ( ( N e. ZZ /\ ( ( N ^ 2 ) / 2 ) e. ZZ ) -> ( N / 2 ) e. ZZ ) |
56 |
12 55
|
impbida |
|- ( N e. ZZ -> ( ( N / 2 ) e. ZZ <-> ( ( N ^ 2 ) / 2 ) e. ZZ ) ) |