Theorem 3halfnz

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

	Ref	Expression
Assertion	3halfnz	|- -. ( 3 / 2 ) e. ZZ

Proof

Step	Hyp	Ref	Expression
1		1z	|- 1 e. ZZ
2		2cn	|- 2 e. CC
3	2	mullidi	|- ( 1 x. 2 ) = 2
4		2lt3	|- 2 < 3
5	3 4	eqbrtri	|- ( 1 x. 2 ) < 3
6		1re	|- 1 e. RR
7		3re	|- 3 e. RR
8		2re	|- 2 e. RR
9		2pos	|- 0 < 2
10	8 9	pm3.2i	|- ( 2 e. RR /\ 0 < 2 )
11		ltmuldiv	|- ( ( 1 e. RR /\ 3 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 1 x. 2 ) < 3 <-> 1 < ( 3 / 2 ) ) )
12	6 7 10 11	mp3an	|- ( ( 1 x. 2 ) < 3 <-> 1 < ( 3 / 2 ) )
13	5 12	mpbi	|- 1 < ( 3 / 2 )
14		3lt4	|- 3 < 4
15		2t2e4	|- ( 2 x. 2 ) = 4
16	15	breq2i	|- ( 3 < ( 2 x. 2 ) <-> 3 < 4 )
17	14 16	mpbir	|- 3 < ( 2 x. 2 )
18		1p1e2	|- ( 1 + 1 ) = 2
19	18	breq2i	|- ( ( 3 / 2 ) < ( 1 + 1 ) <-> ( 3 / 2 ) < 2 )
20		ltdivmul	|- ( ( 3 e. RR /\ 2 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 3 / 2 ) < 2 <-> 3 < ( 2 x. 2 ) ) )
21	7 8 10 20	mp3an	|- ( ( 3 / 2 ) < 2 <-> 3 < ( 2 x. 2 ) )
22	19 21	bitri	|- ( ( 3 / 2 ) < ( 1 + 1 ) <-> 3 < ( 2 x. 2 ) )
23	17 22	mpbir	|- ( 3 / 2 ) < ( 1 + 1 )
24		btwnnz	|- ( ( 1 e. ZZ /\ 1 < ( 3 / 2 ) /\ ( 3 / 2 ) < ( 1 + 1 ) ) -> -. ( 3 / 2 ) e. ZZ )
25	1 13 23 24	mp3an	|- -. ( 3 / 2 ) e. ZZ