Theorem 3halfnz

Description: Three halves is not an integer. (Contributed by AV, 2-Jun-2020)

	Ref	Expression
Assertion	3halfnz	$$⊢\neg \frac{3}{2}\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		2cn	$$⊢2\in ℂ$$
3	2	mullidi	$$⊢1\cdot 2=2$$
4		2lt3	$$⊢2<3$$
5	3 4	eqbrtri	$$⊢1\cdot 2<3$$
6		1re	$$⊢1\in ℝ$$
7		3re	$$⊢3\in ℝ$$
8		2re	$$⊢2\in ℝ$$
9		2pos	$$⊢0<2$$
10	8 9	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
11		ltmuldiv	$$⊢\left(1\in ℝ\wedge 3\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(1\cdot 2<3\leftrightarrow 1<\frac{3}{2}\right)$$
12	6 7 10 11	mp3an	$$⊢1\cdot 2<3\leftrightarrow 1<\frac{3}{2}$$
13	5 12	mpbi	$$⊢1<\frac{3}{2}$$
14		3lt4	$$⊢3<4$$
15		2t2e4	$$⊢2\cdot 2=4$$
16	15	breq2i	$$⊢3<2\cdot 2\leftrightarrow 3<4$$
17	14 16	mpbir	$$⊢3<2\cdot 2$$
18		1p1e2	$$⊢1+1=2$$
19	18	breq2i	$$⊢\frac{3}{2}<1+1\leftrightarrow \frac{3}{2}<2$$
20		ltdivmul	$$⊢\left(3\in ℝ\wedge 2\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\frac{3}{2}<2\leftrightarrow 3<2\cdot 2\right)$$
21	7 8 10 20	mp3an	$$⊢\frac{3}{2}<2\leftrightarrow 3<2\cdot 2$$
22	19 21	bitri	$$⊢\frac{3}{2}<1+1\leftrightarrow 3<2\cdot 2$$
23	17 22	mpbir	$$⊢\frac{3}{2}<1+1$$
24		btwnnz	$$⊢\left(1\in \mathbb{Z}\wedge 1<\frac{3}{2}\wedge \frac{3}{2}<1+1\right)\to \neg \frac{3}{2}\in \mathbb{Z}$$
25	1 13 23 24	mp3an	$$⊢\neg \frac{3}{2}\in \mathbb{Z}$$