Metamath Proof Explorer

Theorem sqoddm1div8

Description: A squared odd number minus 1 divided by 8 is the odd number multiplied with its successor divided by 2. (Contributed by AV, 19-Jul-2021)

Ref Expression
Assertion sqoddm1div8 
|- ( ( N e. ZZ /\ M = ( ( 2 x. N ) + 1 ) ) -> ( ( ( M ^ 2 ) - 1 ) / 8 ) = ( ( N x. ( N + 1 ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( M = ( ( 2 x. N ) + 1 ) -> ( M ^ 2 ) = ( ( ( 2 x. N ) + 1 ) ^ 2 ) )
2 2z 
 |-  2 e. ZZ
3 2 a1i 
 |-  ( N e. ZZ -> 2 e. ZZ )
4 id 
 |-  ( N e. ZZ -> N e. ZZ )
5 3 4 zmulcld 
 |-  ( N e. ZZ -> ( 2 x. N ) e. ZZ )
6 5 zcnd 
 |-  ( N e. ZZ -> ( 2 x. N ) e. CC )
7 binom21 
 |-  ( ( 2 x. N ) e. CC -> ( ( ( 2 x. N ) + 1 ) ^ 2 ) = ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( 2 x. N ) ) ) + 1 ) )
8 6 7 syl 
 |-  ( N e. ZZ -> ( ( ( 2 x. N ) + 1 ) ^ 2 ) = ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( 2 x. N ) ) ) + 1 ) )
9 1 8 sylan9eqr 
 |-  ( ( N e. ZZ /\ M = ( ( 2 x. N ) + 1 ) ) -> ( M ^ 2 ) = ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( 2 x. N ) ) ) + 1 ) )
10 9 oveq1d 
 |-  ( ( N e. ZZ /\ M = ( ( 2 x. N ) + 1 ) ) -> ( ( M ^ 2 ) - 1 ) = ( ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( 2 x. N ) ) ) + 1 ) - 1 ) )
11 2cnd 
 |-  ( N e. ZZ -> 2 e. CC )
12 zcn 
 |-  ( N e. ZZ -> N e. CC )
13 11 12 sqmuld 
 |-  ( N e. ZZ -> ( ( 2 x. N ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) )
14 sq2 
 |-  ( 2 ^ 2 ) = 4
15 14 a1i 
 |-  ( N e. ZZ -> ( 2 ^ 2 ) = 4 )
16 15 oveq1d 
 |-  ( N e. ZZ -> ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) = ( 4 x. ( N ^ 2 ) ) )
17 13 16 eqtrd 
 |-  ( N e. ZZ -> ( ( 2 x. N ) ^ 2 ) = ( 4 x. ( N ^ 2 ) ) )
18 mulass 
 |-  ( ( 2 e. CC /\ 2 e. CC /\ N e. CC ) -> ( ( 2 x. 2 ) x. N ) = ( 2 x. ( 2 x. N ) ) )
19 18 eqcomd 
 |-  ( ( 2 e. CC /\ 2 e. CC /\ N e. CC ) -> ( 2 x. ( 2 x. N ) ) = ( ( 2 x. 2 ) x. N ) )
20 11 11 12 19 syl3anc 
 |-  ( N e. ZZ -> ( 2 x. ( 2 x. N ) ) = ( ( 2 x. 2 ) x. N ) )
21 2t2e4 
 |-  ( 2 x. 2 ) = 4
22 21 a1i 
 |-  ( N e. ZZ -> ( 2 x. 2 ) = 4 )
23 22 oveq1d 
 |-  ( N e. ZZ -> ( ( 2 x. 2 ) x. N ) = ( 4 x. N ) )
24 20 23 eqtrd 
 |-  ( N e. ZZ -> ( 2 x. ( 2 x. N ) ) = ( 4 x. N ) )
25 17 24 oveq12d 
 |-  ( N e. ZZ -> ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( 2 x. N ) ) ) = ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) )
26 25 oveq1d 
 |-  ( N e. ZZ -> ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( 2 x. N ) ) ) + 1 ) = ( ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) + 1 ) )
27 26 oveq1d 
 |-  ( N e. ZZ -> ( ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( 2 x. N ) ) ) + 1 ) - 1 ) = ( ( ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) + 1 ) - 1 ) )
28 4z 
 |-  4 e. ZZ
29 28 a1i 
 |-  ( N e. ZZ -> 4 e. ZZ )
30 zsqcl 
 |-  ( N e. ZZ -> ( N ^ 2 ) e. ZZ )
31 29 30 zmulcld 
 |-  ( N e. ZZ -> ( 4 x. ( N ^ 2 ) ) e. ZZ )
32 31 zcnd 
 |-  ( N e. ZZ -> ( 4 x. ( N ^ 2 ) ) e. CC )
33 29 4 zmulcld 
 |-  ( N e. ZZ -> ( 4 x. N ) e. ZZ )
34 33 zcnd 
 |-  ( N e. ZZ -> ( 4 x. N ) e. CC )
35 32 34 addcld 
 |-  ( N e. ZZ -> ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) e. CC )
36 pncan1 
 |-  ( ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) e. CC -> ( ( ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) + 1 ) - 1 ) = ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) )
37 35 36 syl 
 |-  ( N e. ZZ -> ( ( ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) + 1 ) - 1 ) = ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) )
38 27 37 eqtrd 
 |-  ( N e. ZZ -> ( ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( 2 x. N ) ) ) + 1 ) - 1 ) = ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) )
39 38 adantr 
 |-  ( ( N e. ZZ /\ M = ( ( 2 x. N ) + 1 ) ) -> ( ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( 2 x. N ) ) ) + 1 ) - 1 ) = ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) )
40 10 39 eqtrd 
 |-  ( ( N e. ZZ /\ M = ( ( 2 x. N ) + 1 ) ) -> ( ( M ^ 2 ) - 1 ) = ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) )
41 40 oveq1d 
 |-  ( ( N e. ZZ /\ M = ( ( 2 x. N ) + 1 ) ) -> ( ( ( M ^ 2 ) - 1 ) / 8 ) = ( ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) / 8 ) )
42 4cn 
 |-  4 e. CC
43 42 a1i 
 |-  ( N e. ZZ -> 4 e. CC )
44 30 zcnd 
 |-  ( N e. ZZ -> ( N ^ 2 ) e. CC )
45 43 44 12 adddid 
 |-  ( N e. ZZ -> ( 4 x. ( ( N ^ 2 ) + N ) ) = ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) )
46 45 eqcomd 
 |-  ( N e. ZZ -> ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) = ( 4 x. ( ( N ^ 2 ) + N ) ) )
47 46 oveq1d 
 |-  ( N e. ZZ -> ( ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) / 8 ) = ( ( 4 x. ( ( N ^ 2 ) + N ) ) / 8 ) )
48 47 adantr 
 |-  ( ( N e. ZZ /\ M = ( ( 2 x. N ) + 1 ) ) -> ( ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) / 8 ) = ( ( 4 x. ( ( N ^ 2 ) + N ) ) / 8 ) )
49 4t2e8 
 |-  ( 4 x. 2 ) = 8
50 49 a1i 
 |-  ( N e. ZZ -> ( 4 x. 2 ) = 8 )
51 50 eqcomd 
 |-  ( N e. ZZ -> 8 = ( 4 x. 2 ) )
52 51 oveq2d 
 |-  ( N e. ZZ -> ( ( 4 x. ( ( N ^ 2 ) + N ) ) / 8 ) = ( ( 4 x. ( ( N ^ 2 ) + N ) ) / ( 4 x. 2 ) ) )
53 30 4 zaddcld 
 |-  ( N e. ZZ -> ( ( N ^ 2 ) + N ) e. ZZ )
54 53 zcnd 
 |-  ( N e. ZZ -> ( ( N ^ 2 ) + N ) e. CC )
55 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
56 55 a1i 
 |-  ( N e. ZZ -> ( 2 e. CC /\ 2 =/= 0 ) )
57 4ne0 
 |-  4 =/= 0
58 42 57 pm3.2i 
 |-  ( 4 e. CC /\ 4 =/= 0 )
59 58 a1i 
 |-  ( N e. ZZ -> ( 4 e. CC /\ 4 =/= 0 ) )
60 divcan5 
 |-  ( ( ( ( N ^ 2 ) + N ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( ( 4 x. ( ( N ^ 2 ) + N ) ) / ( 4 x. 2 ) ) = ( ( ( N ^ 2 ) + N ) / 2 ) )
61 54 56 59 60 syl3anc 
 |-  ( N e. ZZ -> ( ( 4 x. ( ( N ^ 2 ) + N ) ) / ( 4 x. 2 ) ) = ( ( ( N ^ 2 ) + N ) / 2 ) )
62 12 sqvald 
 |-  ( N e. ZZ -> ( N ^ 2 ) = ( N x. N ) )
63 62 oveq1d 
 |-  ( N e. ZZ -> ( ( N ^ 2 ) + N ) = ( ( N x. N ) + N ) )
64 12 mulid1d 
 |-  ( N e. ZZ -> ( N x. 1 ) = N )
65 64 eqcomd 
 |-  ( N e. ZZ -> N = ( N x. 1 ) )
66 65 oveq2d 
 |-  ( N e. ZZ -> ( ( N x. N ) + N ) = ( ( N x. N ) + ( N x. 1 ) ) )
67 1cnd 
 |-  ( N e. ZZ -> 1 e. CC )
68 adddi 
 |-  ( ( N e. CC /\ N e. CC /\ 1 e. CC ) -> ( N x. ( N + 1 ) ) = ( ( N x. N ) + ( N x. 1 ) ) )
69 68 eqcomd 
 |-  ( ( N e. CC /\ N e. CC /\ 1 e. CC ) -> ( ( N x. N ) + ( N x. 1 ) ) = ( N x. ( N + 1 ) ) )
70 12 12 67 69 syl3anc 
 |-  ( N e. ZZ -> ( ( N x. N ) + ( N x. 1 ) ) = ( N x. ( N + 1 ) ) )
71 63 66 70 3eqtrd 
 |-  ( N e. ZZ -> ( ( N ^ 2 ) + N ) = ( N x. ( N + 1 ) ) )
72 71 oveq1d 
 |-  ( N e. ZZ -> ( ( ( N ^ 2 ) + N ) / 2 ) = ( ( N x. ( N + 1 ) ) / 2 ) )
73 52 61 72 3eqtrd 
 |-  ( N e. ZZ -> ( ( 4 x. ( ( N ^ 2 ) + N ) ) / 8 ) = ( ( N x. ( N + 1 ) ) / 2 ) )
74 73 adantr 
 |-  ( ( N e. ZZ /\ M = ( ( 2 x. N ) + 1 ) ) -> ( ( 4 x. ( ( N ^ 2 ) + N ) ) / 8 ) = ( ( N x. ( N + 1 ) ) / 2 ) )
75 41 48 74 3eqtrd 
 |-  ( ( N e. ZZ /\ M = ( ( 2 x. N ) + 1 ) ) -> ( ( ( M ^ 2 ) - 1 ) / 8 ) = ( ( N x. ( N + 1 ) ) / 2 ) )