This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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