dec2dvds

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

	Ref	Expression
Hypotheses	dec2dvds.1	$⊢ A \in ℕ_{0}$
	dec2dvds.2	$⊢ B \in ℕ_{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 ℕ_{0}$
2		dec2dvds.2	$⊢ B \in ℕ_{0}$
3		dec2dvds.3	$⊢ B \cdot 2 = C$
4		dec2dvds.4	$⊢ D = C + 1$
5		5nn0	$⊢ 5 \in ℕ_{0}$
6	5	nn0zi	$⊢ 5 \in ℤ$
7		2z	$⊢ 2 \in ℤ$
8		dvdsmul2	$⊢ (5 \in ℤ \land 2 \in ℤ) \to 2 ∥ 5 \cdot 2$
9	6 7 8	mp2an	$⊢ 2 ∥ 5 \cdot 2$
10		5t2e10	$⊢ 5 \cdot 2 = 10$
11	9 10	breqtri	$⊢ 2 ∥ 10$
12		10nn0	$⊢ 10 \in ℕ_{0}$
13	12	nn0zi	$⊢ 10 \in ℤ$
14	1	nn0zi	$⊢ A \in ℤ$
15		dvdsmultr1	$⊢ (2 \in ℤ \land 10 \in ℤ \land A \in ℤ) \to (2 ∥ 10 \to 2 ∥ 10 A)$
16	7 13 14 15	mp3an	$⊢ 2 ∥ 10 \to 2 ∥ 10 A$
17	11 16	ax-mp	$⊢ 2 ∥ 10 A$
18	2	nn0zi	$⊢ B \in ℤ$
19		dvdsmul2	$⊢ (B \in ℤ \land 2 \in ℤ) \to 2 ∥ B \cdot 2$
20	18 7 19	mp2an	$⊢ 2 ∥ B \cdot 2$
21	20 3	breqtri	$⊢ 2 ∥ C$
22	12 1	nn0mulcli	$⊢ 10 A \in ℕ_{0}$
23	22	nn0zi	$⊢ 10 A \in ℤ$
24		2nn0	$⊢ 2 \in ℕ_{0}$
25	2 24	nn0mulcli	$⊢ B \cdot 2 \in ℕ_{0}$
26	3 25	eqeltrri	$⊢ C \in ℕ_{0}$
27	26	nn0zi	$⊢ C \in ℤ$
28		dvds2add	$⊢ (2 \in ℤ \land 10 A \in ℤ \land C \in ℤ) \to ((2 ∥ 10 A \land 2 ∥ C) \to 2 ∥ (10 A + C))$
29	7 23 27 28	mp3an	$⊢ (2 ∥ 10 A \land 2 ∥ C) \to 2 ∥ (10 A + C)$
30	17 21 29	mp2an	$⊢ 2 ∥ (10 A + C)$
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 ℕ$
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 \|-

Metamath Proof Explorer

Theorem dec2dvds

Proof