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 · 3 )

Proof

Step Hyp Ref Expression
1 6cn ⊢ 6 ∈ ℂ
2 8cn ⊢ 8 ∈ ℂ
3 0re ⊢ 0 ∈ ℝ
4 8pos ⊢ 0 < 8
5 3 4 gtneii ⊢ 8 ≠ 0
6 1 2 5 divcan4i ⊢ ( ( 6 · 8 ) / 8 ) = 6
7 1 2 mulcli ⊢ ( 6 · 8 ) ∈ ℂ
8 ax-1cn ⊢ 1 ∈ ℂ
9 4p3e7 ⊢ ( 4 + 3 ) = 7
10 9 eqcomi ⊢ 7 = ( 4 + 3 )
11 10 oveq1i ⊢ ( 7 ↑ 2 ) = ( ( 4 + 3 ) ↑ 2 )
12 4cn ⊢ 4 ∈ ℂ
13 3cn ⊢ 3 ∈ ℂ
14 12 13 binom2i ⊢ ( ( 4 + 3 ) ↑ 2 ) = ( ( ( 4 ↑ 2 ) + ( 2 · ( 4 · 3 ) ) ) + ( 3 ↑ 2 ) )
15 sq4e2t8 ⊢ ( 4 ↑ 2 ) = ( 2 · 8 )
16 2t4e8 ⊢ ( 2 · 4 ) = 8
17 16 oveq1i ⊢ ( ( 2 · 4 ) · 3 ) = ( 8 · 3 )
18 2cn ⊢ 2 ∈ ℂ
19 18 12 13 mulassi ⊢ ( ( 2 · 4 ) · 3 ) = ( 2 · ( 4 · 3 ) )
20 2 13 mulcomi ⊢ ( 8 · 3 ) = ( 3 · 8 )
21 17 19 20 3eqtr3i ⊢ ( 2 · ( 4 · 3 ) ) = ( 3 · 8 )
22 15 21 oveq12i ⊢ ( ( 4 ↑ 2 ) + ( 2 · ( 4 · 3 ) ) ) = ( ( 2 · 8 ) + ( 3 · 8 ) )
23 18 13 2 adddiri ⊢ ( ( 2 + 3 ) · 8 ) = ( ( 2 · 8 ) + ( 3 · 8 ) )
24 3p2e5 ⊢ ( 3 + 2 ) = 5
25 13 18 24 addcomli ⊢ ( 2 + 3 ) = 5
26 25 oveq1i ⊢ ( ( 2 + 3 ) · 8 ) = ( 5 · 8 )
27 22 23 26 3eqtr2i ⊢ ( ( 4 ↑ 2 ) + ( 2 · ( 4 · 3 ) ) ) = ( 5 · 8 )
28 sq3 ⊢ ( 3 ↑ 2 ) = 9
29 df-9 ⊢ 9 = ( 8 + 1 )
30 28 29 eqtri ⊢ ( 3 ↑ 2 ) = ( 8 + 1 )
31 27 30 oveq12i ⊢ ( ( ( 4 ↑ 2 ) + ( 2 · ( 4 · 3 ) ) ) + ( 3 ↑ 2 ) ) = ( ( 5 · 8 ) + ( 8 + 1 ) )
32 5cn ⊢ 5 ∈ ℂ
33 32 2 mulcli ⊢ ( 5 · 8 ) ∈ ℂ
34 33 2 8 addassi ⊢ ( ( ( 5 · 8 ) + 8 ) + 1 ) = ( ( 5 · 8 ) + ( 8 + 1 ) )
35 df-6 ⊢ 6 = ( 5 + 1 )
36 35 oveq1i ⊢ ( 6 · 8 ) = ( ( 5 + 1 ) · 8 )
37 32 a1i ⊢ ( 8 ∈ ℂ → 5 ∈ ℂ )
38 id ⊢ ( 8 ∈ ℂ → 8 ∈ ℂ )
39 37 38 adddirp1d ⊢ ( 8 ∈ ℂ → ( ( 5 + 1 ) · 8 ) = ( ( 5 · 8 ) + 8 ) )
40 2 39 ax-mp ⊢ ( ( 5 + 1 ) · 8 ) = ( ( 5 · 8 ) + 8 )
41 36 40 eqtri ⊢ ( 6 · 8 ) = ( ( 5 · 8 ) + 8 )
42 41 eqcomi ⊢ ( ( 5 · 8 ) + 8 ) = ( 6 · 8 )
43 42 oveq1i ⊢ ( ( ( 5 · 8 ) + 8 ) + 1 ) = ( ( 6 · 8 ) + 1 )
44 31 34 43 3eqtr2i ⊢ ( ( ( 4 ↑ 2 ) + ( 2 · ( 4 · 3 ) ) ) + ( 3 ↑ 2 ) ) = ( ( 6 · 8 ) + 1 )
45 14 44 eqtri ⊢ ( ( 4 + 3 ) ↑ 2 ) = ( ( 6 · 8 ) + 1 )
46 11 45 eqtri ⊢ ( 7 ↑ 2 ) = ( ( 6 · 8 ) + 1 )
47 7 8 46 mvrraddi ⊢ ( ( 7 ↑ 2 ) − 1 ) = ( 6 · 8 )
48 47 oveq1i ⊢ ( ( ( 7 ↑ 2 ) − 1 ) / 8 ) = ( ( 6 · 8 ) / 8 )
49 2t3e6 ⊢ ( 2 · 3 ) = 6
50 6 48 49 3eqtr4i ⊢ ( ( ( 7 ↑ 2 ) − 1 ) / 8 ) = ( 2 · 3 )