Metamath Proof Explorer

Theorem 2lgsoddprmlem3c

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

Ref Expression
Assertion 2lgsoddprmlem3c ${⊢}\frac{{5}^{2}-1}{8}=3$

Proof

Step Hyp Ref Expression
1 df-5 ${⊢}5=4+1$
2 1 oveq1i ${⊢}{5}^{2}={\left(4+1\right)}^{2}$
3 4cn ${⊢}4\in ℂ$
4 binom21 ${⊢}4\in ℂ\to {\left(4+1\right)}^{2}={4}^{2}+2\cdot 4+1$
5 3 4 ax-mp ${⊢}{\left(4+1\right)}^{2}={4}^{2}+2\cdot 4+1$
6 2 5 eqtri ${⊢}{5}^{2}={4}^{2}+2\cdot 4+1$
7 6 oveq1i ${⊢}{5}^{2}-1=\left({4}^{2}+2\cdot 4\right)+1-1$
8 3cn ${⊢}3\in ℂ$
9 8cn ${⊢}8\in ℂ$
10 8 9 mulcli ${⊢}3\cdot 8\in ℂ$
11 ax-1cn ${⊢}1\in ℂ$
12 sq4e2t8 ${⊢}{4}^{2}=2\cdot 8$
13 2cn ${⊢}2\in ℂ$
14 4t2e8 ${⊢}4\cdot 2=8$
15 9 mulid2i ${⊢}1\cdot 8=8$
16 14 15 eqtr4i ${⊢}4\cdot 2=1\cdot 8$
17 3 13 16 mulcomli ${⊢}2\cdot 4=1\cdot 8$
18 12 17 oveq12i ${⊢}{4}^{2}+2\cdot 4=2\cdot 8+1\cdot 8$
19 13 11 9 adddiri ${⊢}\left(2+1\right)\cdot 8=2\cdot 8+1\cdot 8$
20 2p1e3 ${⊢}2+1=3$
21 20 oveq1i ${⊢}\left(2+1\right)\cdot 8=3\cdot 8$
22 18 19 21 3eqtr2i ${⊢}{4}^{2}+2\cdot 4=3\cdot 8$
23 22 oveq1i ${⊢}{4}^{2}+2\cdot 4+1=3\cdot 8+1$
24 10 11 23 mvrraddi ${⊢}\left({4}^{2}+2\cdot 4\right)+1-1=3\cdot 8$
25 7 24 eqtri ${⊢}{5}^{2}-1=3\cdot 8$
26 25 oveq1i ${⊢}\frac{{5}^{2}-1}{8}=\frac{3\cdot 8}{8}$
27 0re ${⊢}0\in ℝ$
28 8pos ${⊢}0<8$
29 27 28 gtneii ${⊢}8\ne 0$
30 8 9 29 divcan4i ${⊢}\frac{3\cdot 8}{8}=3$
31 26 30 eqtri ${⊢}\frac{{5}^{2}-1}{8}=3$