Theorem 3halfnz

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

	Ref	Expression
Assertion	3halfnz	⊢ ¬ ( 3 / 2 ) ∈ ℤ

Proof

Step	Hyp	Ref	Expression
1		1z	⊢ 1 ∈ ℤ
2		2cn	⊢ 2 ∈ ℂ
3	2	mullidi	⊢ ( 1 · 2 ) = 2
4		2lt3	⊢ 2 < 3
5	3 4	eqbrtri	⊢ ( 1 · 2 ) < 3
6		1re	⊢ 1 ∈ ℝ
7		3re	⊢ 3 ∈ ℝ
8		2re	⊢ 2 ∈ ℝ
9		2pos	⊢ 0 < 2
10	8 9	pm3.2i	⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
11		ltmuldiv	⊢ ( ( 1 ∈ ℝ ∧ 3 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 1 · 2 ) < 3 ↔ 1 < ( 3 / 2 ) ) )
12	6 7 10 11	mp3an	⊢ ( ( 1 · 2 ) < 3 ↔ 1 < ( 3 / 2 ) )
13	5 12	mpbi	⊢ 1 < ( 3 / 2 )
14		3lt4	⊢ 3 < 4
15		2t2e4	⊢ ( 2 · 2 ) = 4
16	15	breq2i	⊢ ( 3 < ( 2 · 2 ) ↔ 3 < 4 )
17	14 16	mpbir	⊢ 3 < ( 2 · 2 )
18		1p1e2	⊢ ( 1 + 1 ) = 2
19	18	breq2i	⊢ ( ( 3 / 2 ) < ( 1 + 1 ) ↔ ( 3 / 2 ) < 2 )
20		ltdivmul	⊢ ( ( 3 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 3 / 2 ) < 2 ↔ 3 < ( 2 · 2 ) ) )
21	7 8 10 20	mp3an	⊢ ( ( 3 / 2 ) < 2 ↔ 3 < ( 2 · 2 ) )
22	19 21	bitri	⊢ ( ( 3 / 2 ) < ( 1 + 1 ) ↔ 3 < ( 2 · 2 ) )
23	17 22	mpbir	⊢ ( 3 / 2 ) < ( 1 + 1 )
24		btwnnz	⊢ ( ( 1 ∈ ℤ ∧ 1 < ( 3 / 2 ) ∧ ( 3 / 2 ) < ( 1 + 1 ) ) → ¬ ( 3 / 2 ) ∈ ℤ )
25	1 13 23 24	mp3an	⊢ ¬ ( 3 / 2 ) ∈ ℤ