3halfnz

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

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

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
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	$⊢ (2 \in ℝ \land 0 < 2)$
11		ltmuldiv	$⊢ (1 \in ℝ \land 3 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (1 \cdot 2 < 3 \leftrightarrow 1 < \frac{3}{2})$
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	$⊢ (3 \in ℝ \land 2 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\frac{3}{2} < 2 \leftrightarrow 3 < 2 \cdot 2)$
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	$⊢ (1 \in ℤ \land 1 < \frac{3}{2} \land \frac{3}{2} < 1 + 1) \to \neg \frac{3}{2} \in ℤ$
25	1 13 23 24	mp3an	$⊢ \neg \frac{3}{2} \in ℤ$

Metamath Proof Explorer