Theorem n2dvds3OLD

Description: Obsolete version of n2dvds3 as of 3-May-2023. 2 does not divide 3. That means 3 is odd. (Contributed by AV, 28-Feb-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	n2dvds3OLD	$$⊢\neg 2\parallel 3$$

Proof

Step	Hyp	Ref	Expression
1		2z	$$⊢2\in \mathbb{Z}$$
2		iddvds	$$⊢2\in \mathbb{Z}\to 2\parallel 2$$
3	1 2	ax-mp	$$⊢2\parallel 2$$
4		3m1e2	$$⊢3-1=2$$
5	3 4	breqtrri	$$⊢2\parallel \left(3-1\right)$$
6		3z	$$⊢3\in \mathbb{Z}$$
7		oddm1even	$$⊢3\in \mathbb{Z}\to \left(\neg 2\parallel 3\leftrightarrow 2\parallel \left(3-1\right)\right)$$
8	6 7	ax-mp	$$⊢\neg 2\parallel 3\leftrightarrow 2\parallel \left(3-1\right)$$
9	5 8	mpbir	$$⊢\neg 2\parallel 3$$