Metamath Proof Explorer

Theorem 2lgsoddprmlem1

Description: Lemma 1 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( N = ( ( 8 x. A ) + B ) -> ( N ^ 2 ) = ( ( ( 8 x. A ) + B ) ^ 2 ) )
2 1 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N = ( ( 8 x. A ) + B ) ) -> ( N ^ 2 ) = ( ( ( 8 x. A ) + B ) ^ 2 ) )
3 2 oveq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N = ( ( 8 x. A ) + B ) ) -> ( ( N ^ 2 ) - 1 ) = ( ( ( ( 8 x. A ) + B ) ^ 2 ) - 1 ) )
4 3 oveq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N = ( ( 8 x. A ) + B ) ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) = ( ( ( ( ( 8 x. A ) + B ) ^ 2 ) - 1 ) / 8 ) )
5 zcn 
 |-  ( A e. ZZ -> A e. CC )
6 5 adantr 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> A e. CC )
7 zcn 
 |-  ( B e. ZZ -> B e. CC )
8 7 adantl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> B e. CC )
9 1cnd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> 1 e. CC )
10 8cn 
 |-  8 e. CC
11 8re 
 |-  8 e. RR
12 8pos 
 |-  0 < 8
13 11 12 gt0ne0ii 
 |-  8 =/= 0
14 10 13 pm3.2i 
 |-  ( 8 e. CC /\ 8 =/= 0 )
15 14 a1i 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( 8 e. CC /\ 8 =/= 0 ) )
16 mulsubdivbinom2 
 |-  ( ( ( A e. CC /\ B e. CC /\ 1 e. CC ) /\ ( 8 e. CC /\ 8 =/= 0 ) ) -> ( ( ( ( ( 8 x. A ) + B ) ^ 2 ) - 1 ) / 8 ) = ( ( ( 8 x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - 1 ) / 8 ) ) )
17 6 8 9 15 16 syl31anc 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( ( ( 8 x. A ) + B ) ^ 2 ) - 1 ) / 8 ) = ( ( ( 8 x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - 1 ) / 8 ) ) )
18 17 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N = ( ( 8 x. A ) + B ) ) -> ( ( ( ( ( 8 x. A ) + B ) ^ 2 ) - 1 ) / 8 ) = ( ( ( 8 x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - 1 ) / 8 ) ) )
19 4 18 eqtrd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N = ( ( 8 x. A ) + B ) ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) = ( ( ( 8 x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - 1 ) / 8 ) ) )