Metamath Proof Explorer

Theorem 2lgsoddprmlem3c

Description: Lemma 3 for 2lgsoddprmlem3 . (Contributed by AV, 20-Jul-2021)

Ref Expression
Assertion 2lgsoddprmlem3c 
|- ( ( ( 5 ^ 2 ) - 1 ) / 8 ) = 3

Proof

Step Hyp Ref Expression
1 df-5 
 |-  5 = ( 4 + 1 )
2 1 oveq1i 
 |-  ( 5 ^ 2 ) = ( ( 4 + 1 ) ^ 2 )
3 4cn 
 |-  4 e. CC
4 binom21 
 |-  ( 4 e. CC -> ( ( 4 + 1 ) ^ 2 ) = ( ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) + 1 ) )
5 3 4 ax-mp 
 |-  ( ( 4 + 1 ) ^ 2 ) = ( ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) + 1 )
6 2 5 eqtri 
 |-  ( 5 ^ 2 ) = ( ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) + 1 )
7 6 oveq1i 
 |-  ( ( 5 ^ 2 ) - 1 ) = ( ( ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) + 1 ) - 1 )
8 3cn 
 |-  3 e. CC
9 8cn 
 |-  8 e. CC
10 8 9 mulcli 
 |-  ( 3 x. 8 ) e. CC
11 ax-1cn 
 |-  1 e. CC
12 sq4e2t8 
 |-  ( 4 ^ 2 ) = ( 2 x. 8 )
13 2cn 
 |-  2 e. CC
14 4t2e8 
 |-  ( 4 x. 2 ) = 8
15 9 mulid2i 
 |-  ( 1 x. 8 ) = 8
16 14 15 eqtr4i 
 |-  ( 4 x. 2 ) = ( 1 x. 8 )
17 3 13 16 mulcomli 
 |-  ( 2 x. 4 ) = ( 1 x. 8 )
18 12 17 oveq12i 
 |-  ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) = ( ( 2 x. 8 ) + ( 1 x. 8 ) )
19 13 11 9 adddiri 
 |-  ( ( 2 + 1 ) x. 8 ) = ( ( 2 x. 8 ) + ( 1 x. 8 ) )
20 2p1e3 
 |-  ( 2 + 1 ) = 3
21 20 oveq1i 
 |-  ( ( 2 + 1 ) x. 8 ) = ( 3 x. 8 )
22 18 19 21 3eqtr2i 
 |-  ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) = ( 3 x. 8 )
23 22 oveq1i 
 |-  ( ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) + 1 ) = ( ( 3 x. 8 ) + 1 )
24 10 11 23 mvrraddi 
 |-  ( ( ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) + 1 ) - 1 ) = ( 3 x. 8 )
25 7 24 eqtri 
 |-  ( ( 5 ^ 2 ) - 1 ) = ( 3 x. 8 )
26 25 oveq1i 
 |-  ( ( ( 5 ^ 2 ) - 1 ) / 8 ) = ( ( 3 x. 8 ) / 8 )
27 0re 
 |-  0 e. RR
28 8pos 
 |-  0 < 8
29 27 28 gtneii 
 |-  8 =/= 0
30 8 9 29 divcan4i 
 |-  ( ( 3 x. 8 ) / 8 ) = 3
31 26 30 eqtri 
 |-  ( ( ( 5 ^ 2 ) - 1 ) / 8 ) = 3