Theorem 41prothprmlem1

Description: Lemma 1 for 41prothprm . (Contributed by AV, 4-Jul-2020)

	Ref	Expression
Hypothesis	41prothprm.p	$$⊢P=41$$
Assertion	41prothprmlem1	$$⊢\frac{P-1}{2}=20$$

Proof

Step	Hyp	Ref	Expression
1		41prothprm.p	$$⊢P=41$$
2		dfdec10	$$⊢41=10\cdot 4+1$$
3	1 2	eqtri	$$⊢P=10\cdot 4+1$$
4	3	oveq1i	$$⊢P-1=10\cdot 4+1-1$$
5		10nn	$$⊢10\in \mathbb{N}$$
6	5	nncni	$$⊢10\in ℂ$$
7		4cn	$$⊢4\in ℂ$$
8	6 7	mulcli	$$⊢10\cdot 4\in ℂ$$
9		pncan1	$$⊢10\cdot 4\in ℂ\to 10\cdot 4+1-1=10\cdot 4$$
10	8 9	ax-mp	$$⊢10\cdot 4+1-1=10\cdot 4$$
11	4 10	eqtri	$$⊢P-1=10\cdot 4$$
12	11	oveq1i	$$⊢\frac{P-1}{2}=\frac{10\cdot 4}{2}$$
13		2cn	$$⊢2\in ℂ$$
14		2ne0	$$⊢2\ne 0$$
15	6 7 13 14	divassi	$$⊢\frac{10\cdot 4}{2}=10\left(\frac{4}{2}\right)$$
16		4div2e2	$$⊢\frac{4}{2}=2$$
17	16	oveq2i	$$⊢10\left(\frac{4}{2}\right)=10\cdot 2$$
18		2nn0	$$⊢2\in {\mathbb{N}}_0$$
19	18	dec0u	$$⊢10\cdot 2=20$$
20	17 19	eqtri	$$⊢10\left(\frac{4}{2}\right)=20$$
21	15 20	eqtri	$$⊢\frac{10\cdot 4}{2}=20$$
22	12 21	eqtri	$$⊢\frac{P-1}{2}=20$$