Theorem dec2dvds

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

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

Proof

Step	Hyp	Ref	Expression
1		dec2dvds.1	$$⊢A\in {\mathbb{N}}_0$$
2		dec2dvds.2	$$⊢B\in {\mathbb{N}}_0$$
3		dec2dvds.3	$$⊢B\cdot 2=C$$
4		dec2dvds.4	$$⊢D=C+1$$
5		5nn0	$$⊢5\in {\mathbb{N}}_0$$
6	5	nn0zi	$$⊢5\in \mathbb{Z}$$
7		2z	$$⊢2\in \mathbb{Z}$$
8		dvdsmul2	$$⊢\left(5\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to 2\parallel 5\cdot 2$$
9	6 7 8	mp2an	$$⊢2\parallel 5\cdot 2$$
10		5t2e10	$$⊢5\cdot 2=10$$
11	9 10	breqtri	$$⊢2\parallel 10$$
12		10nn0	$$⊢10\in {\mathbb{N}}_0$$
13	12	nn0zi	$$⊢10\in \mathbb{Z}$$
14	1	nn0zi	$$⊢A\in \mathbb{Z}$$
15		dvdsmultr1	$$⊢\left(2\in \mathbb{Z}\wedge 10\in \mathbb{Z}\wedge A\in \mathbb{Z}\right)\to \left(2\parallel 10\to 2\parallel 10A\right)$$
16	7 13 14 15	mp3an	$$⊢2\parallel 10\to 2\parallel 10A$$
17	11 16	ax-mp	$$⊢2\parallel 10A$$
18	2	nn0zi	$$⊢B\in \mathbb{Z}$$
19		dvdsmul2	$$⊢\left(B\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to 2\parallel B\cdot 2$$
20	18 7 19	mp2an	$$⊢2\parallel B\cdot 2$$
21	20 3	breqtri	$$⊢2\parallel C$$
22	12 1	nn0mulcli	$$⊢10A\in {\mathbb{N}}_0$$
23	22	nn0zi	$$⊢10A\in \mathbb{Z}$$
24		2nn0	$$⊢2\in {\mathbb{N}}_0$$
25	2 24	nn0mulcli	$$⊢B\cdot 2\in {\mathbb{N}}_0$$
26	3 25	eqeltrri	$$⊢C\in {\mathbb{N}}_0$$
27	26	nn0zi	$$⊢C\in \mathbb{Z}$$
28		dvds2add	$$⊢\left(2\in \mathbb{Z}\wedge 10A\in \mathbb{Z}\wedge C\in \mathbb{Z}\right)\to \left(\left(2\parallel 10A\wedge 2\parallel C\right)\to 2\parallel \left(10A+C\right)\right)$$
29	7 23 27 28	mp3an	$$⊢\left(2\parallel 10A\wedge 2\parallel C\right)\to 2\parallel \left(10A+C\right)$$
30	17 21 29	mp2an	$$⊢2\parallel \left(10A+C\right)$$
31		dfdec10	Could not format ; A C = ( ( ; 1 0 x. A ) + C ) : No typesetting found for |- ; A C = ( ( ; 1 0 x. A ) + C ) with typecode |-
32	30 31	breqtrri	Could not format 2 || ; A C : No typesetting found for |- 2 || ; A C with typecode |-
33	1 26	deccl	Could not format ; A C e. NN0 : No typesetting found for |- ; A C e. NN0 with typecode |-
34	33	nn0zi	Could not format ; A C e. ZZ : No typesetting found for |- ; A C e. ZZ with typecode |-
35		2nn	$$⊢2\in \mathbb{N}$$
36		1lt2	$$⊢1<2$$
37		ndvdsp1	Could not format ( ( ; A C e. ZZ /\ 2 e. NN /\ 1 < 2 ) -> ( 2 || ; A C -> -. 2 || ( ; A C + 1 ) ) ) : No typesetting found for |- ( ( ; A C e. ZZ /\ 2 e. NN /\ 1 < 2 ) -> ( 2 || ; A C -> -. 2 || ( ; A C + 1 ) ) ) with typecode |-
38	34 35 36 37	mp3an	Could not format ( 2 || ; A C -> -. 2 || ( ; A C + 1 ) ) : No typesetting found for |- ( 2 || ; A C -> -. 2 || ( ; A C + 1 ) ) with typecode |-
39	32 38	ax-mp	Could not format -. 2 || ( ; A C + 1 ) : No typesetting found for |- -. 2 || ( ; A C + 1 ) with typecode |-
40	4	eqcomi	$$⊢C+1=D$$
41		eqid	Could not format ; A C = ; A C : No typesetting found for |- ; A C = ; A C with typecode |-
42	1 26 40 41	decsuc	Could not format ( ; A C + 1 ) = ; A D : No typesetting found for |- ( ; A C + 1 ) = ; A D with typecode |-
43	42	breq2i	Could not format ( 2 || ( ; A C + 1 ) <-> 2 || ; A D ) : No typesetting found for |- ( 2 || ( ; A C + 1 ) <-> 2 || ; A D ) with typecode |-
44	39 43	mtbi	Could not format -. 2 || ; A D : No typesetting found for |- -. 2 || ; A D with typecode |-