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 ) ∈ ℤ

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 ) ∈ ℤ