Metamath Proof Explorer


Theorem 2lgsoddprmlem3d

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

Ref Expression
Assertion 2lgsoddprmlem3d
|- ( ( ( 7 ^ 2 ) - 1 ) / 8 ) = ( 2 x. 3 )

Proof

Step Hyp Ref Expression
1 6cn
 |-  6 e. CC
2 8cn
 |-  8 e. CC
3 0re
 |-  0 e. RR
4 8pos
 |-  0 < 8
5 3 4 gtneii
 |-  8 =/= 0
6 1 2 5 divcan4i
 |-  ( ( 6 x. 8 ) / 8 ) = 6
7 1 2 mulcli
 |-  ( 6 x. 8 ) e. CC
8 ax-1cn
 |-  1 e. CC
9 4p3e7
 |-  ( 4 + 3 ) = 7
10 9 eqcomi
 |-  7 = ( 4 + 3 )
11 10 oveq1i
 |-  ( 7 ^ 2 ) = ( ( 4 + 3 ) ^ 2 )
12 4cn
 |-  4 e. CC
13 3cn
 |-  3 e. CC
14 12 13 binom2i
 |-  ( ( 4 + 3 ) ^ 2 ) = ( ( ( 4 ^ 2 ) + ( 2 x. ( 4 x. 3 ) ) ) + ( 3 ^ 2 ) )
15 sq4e2t8
 |-  ( 4 ^ 2 ) = ( 2 x. 8 )
16 2cn
 |-  2 e. CC
17 4t2e8
 |-  ( 4 x. 2 ) = 8
18 12 16 17 mulcomli
 |-  ( 2 x. 4 ) = 8
19 18 oveq1i
 |-  ( ( 2 x. 4 ) x. 3 ) = ( 8 x. 3 )
20 16 12 13 mulassi
 |-  ( ( 2 x. 4 ) x. 3 ) = ( 2 x. ( 4 x. 3 ) )
21 2 13 mulcomi
 |-  ( 8 x. 3 ) = ( 3 x. 8 )
22 19 20 21 3eqtr3i
 |-  ( 2 x. ( 4 x. 3 ) ) = ( 3 x. 8 )
23 15 22 oveq12i
 |-  ( ( 4 ^ 2 ) + ( 2 x. ( 4 x. 3 ) ) ) = ( ( 2 x. 8 ) + ( 3 x. 8 ) )
24 16 13 2 adddiri
 |-  ( ( 2 + 3 ) x. 8 ) = ( ( 2 x. 8 ) + ( 3 x. 8 ) )
25 3p2e5
 |-  ( 3 + 2 ) = 5
26 13 16 25 addcomli
 |-  ( 2 + 3 ) = 5
27 26 oveq1i
 |-  ( ( 2 + 3 ) x. 8 ) = ( 5 x. 8 )
28 23 24 27 3eqtr2i
 |-  ( ( 4 ^ 2 ) + ( 2 x. ( 4 x. 3 ) ) ) = ( 5 x. 8 )
29 sq3
 |-  ( 3 ^ 2 ) = 9
30 df-9
 |-  9 = ( 8 + 1 )
31 29 30 eqtri
 |-  ( 3 ^ 2 ) = ( 8 + 1 )
32 28 31 oveq12i
 |-  ( ( ( 4 ^ 2 ) + ( 2 x. ( 4 x. 3 ) ) ) + ( 3 ^ 2 ) ) = ( ( 5 x. 8 ) + ( 8 + 1 ) )
33 5cn
 |-  5 e. CC
34 33 2 mulcli
 |-  ( 5 x. 8 ) e. CC
35 34 2 8 addassi
 |-  ( ( ( 5 x. 8 ) + 8 ) + 1 ) = ( ( 5 x. 8 ) + ( 8 + 1 ) )
36 df-6
 |-  6 = ( 5 + 1 )
37 36 oveq1i
 |-  ( 6 x. 8 ) = ( ( 5 + 1 ) x. 8 )
38 33 a1i
 |-  ( 8 e. CC -> 5 e. CC )
39 id
 |-  ( 8 e. CC -> 8 e. CC )
40 38 39 adddirp1d
 |-  ( 8 e. CC -> ( ( 5 + 1 ) x. 8 ) = ( ( 5 x. 8 ) + 8 ) )
41 2 40 ax-mp
 |-  ( ( 5 + 1 ) x. 8 ) = ( ( 5 x. 8 ) + 8 )
42 37 41 eqtri
 |-  ( 6 x. 8 ) = ( ( 5 x. 8 ) + 8 )
43 42 eqcomi
 |-  ( ( 5 x. 8 ) + 8 ) = ( 6 x. 8 )
44 43 oveq1i
 |-  ( ( ( 5 x. 8 ) + 8 ) + 1 ) = ( ( 6 x. 8 ) + 1 )
45 32 35 44 3eqtr2i
 |-  ( ( ( 4 ^ 2 ) + ( 2 x. ( 4 x. 3 ) ) ) + ( 3 ^ 2 ) ) = ( ( 6 x. 8 ) + 1 )
46 14 45 eqtri
 |-  ( ( 4 + 3 ) ^ 2 ) = ( ( 6 x. 8 ) + 1 )
47 11 46 eqtri
 |-  ( 7 ^ 2 ) = ( ( 6 x. 8 ) + 1 )
48 7 8 47 mvrraddi
 |-  ( ( 7 ^ 2 ) - 1 ) = ( 6 x. 8 )
49 48 oveq1i
 |-  ( ( ( 7 ^ 2 ) - 1 ) / 8 ) = ( ( 6 x. 8 ) / 8 )
50 3t2e6
 |-  ( 3 x. 2 ) = 6
51 13 16 50 mulcomli
 |-  ( 2 x. 3 ) = 6
52 6 49 51 3eqtr4i
 |-  ( ( ( 7 ^ 2 ) - 1 ) / 8 ) = ( 2 x. 3 )