Theorem dec2nprm

Description: Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015)

	Ref	Expression
Hypotheses	dec5nprm.1	$$⊢A\in \mathbb{N}$$
	dec2nprm.2	$$⊢B\in {\mathbb{N}}_0$$
	dec2nprm.3	$$⊢B\cdot 2=C$$
Assertion	dec2nprm	Could not format assertion : No typesetting found for |- -. ; A C e. Prime with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dec5nprm.1	$$⊢A\in \mathbb{N}$$
2		dec2nprm.2	$$⊢B\in {\mathbb{N}}_0$$
3		dec2nprm.3	$$⊢B\cdot 2=C$$
4		5nn	$$⊢5\in \mathbb{N}$$
5	4 1	nnmulcli	$$⊢5A\in \mathbb{N}$$
6		nnnn0addcl	$$⊢\left(5A\in \mathbb{N}\wedge B\in {\mathbb{N}}_0\right)\to 5A+B\in \mathbb{N}$$
7	5 2 6	mp2an	$$⊢5A+B\in \mathbb{N}$$
8		2nn	$$⊢2\in \mathbb{N}$$
9		1nn0	$$⊢1\in {\mathbb{N}}_0$$
10		1lt5	$$⊢1<5$$
11	4 1 2 9 10	numlti	$$⊢1<5A+B$$
12		1lt2	$$⊢1<2$$
13	4	nncni	$$⊢5\in ℂ$$
14	1	nncni	$$⊢A\in ℂ$$
15		2cn	$$⊢2\in ℂ$$
16	13 14 15	mul32i	$$⊢5A\cdot 2=5\cdot 2A$$
17		5t2e10	$$⊢5\cdot 2=10$$
18	17	oveq1i	$$⊢5\cdot 2A=10A$$
19	16 18	eqtri	$$⊢5A\cdot 2=10A$$
20	19 3	oveq12i	$$⊢5A\cdot 2+B\cdot 2=10A+C$$
21	5	nncni	$$⊢5A\in ℂ$$
22	2	nn0cni	$$⊢B\in ℂ$$
23	21 22 15	adddiri	$$⊢\left(5A+B\right)\cdot 2=5A\cdot 2+B\cdot 2$$
24		dfdec10	Could not format ; A C = ( ( ; 1 0 x. A ) + C ) : No typesetting found for |- ; A C = ( ( ; 1 0 x. A ) + C ) with typecode |-
25	20 23 24	3eqtr4i	Could not format ( ( ( 5 x. A ) + B ) x. 2 ) = ; A C : No typesetting found for |- ( ( ( 5 x. A ) + B ) x. 2 ) = ; A C with typecode |-
26	7 8 11 12 25	nprmi	Could not format -. ; A C e. Prime : No typesetting found for |- -. ; A C e. Prime with typecode |-