# Metamath Proof Explorer

## Theorem threehalves

Description: Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021)

Ref Expression
Assertion threehalves ${⊢}\frac{3}{2}=1.5$

### Proof

Step Hyp Ref Expression
1 3re ${⊢}3\in ℝ$
2 2re ${⊢}2\in ℝ$
3 2ne0 ${⊢}2\ne 0$
4 1 2 3 redivcli ${⊢}\frac{3}{2}\in ℝ$
5 4 recni ${⊢}\frac{3}{2}\in ℂ$
6 1nn0 ${⊢}1\in {ℕ}_{0}$
7 5re ${⊢}5\in ℝ$
8 dpcl ${⊢}\left(1\in {ℕ}_{0}\wedge 5\in ℝ\right)\to 1.5\in ℝ$
9 6 7 8 mp2an ${⊢}1.5\in ℝ$
10 9 recni ${⊢}1.5\in ℂ$
11 2cnne0 ${⊢}\left(2\in ℂ\wedge 2\ne 0\right)$
12 5 10 11 3pm3.2i ${⊢}\left(\frac{3}{2}\in ℂ\wedge 1.5\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)$
13 5nn0 ${⊢}5\in {ℕ}_{0}$
14 3nn0 ${⊢}3\in {ℕ}_{0}$
15 0nn0 ${⊢}0\in {ℕ}_{0}$
16 eqid ${⊢}15=15$
17 df-2 ${⊢}2=1+1$
18 17 oveq1i ${⊢}2+1=1+1+1$
19 2p1e3 ${⊢}2+1=3$
20 18 19 eqtr3i ${⊢}1+1+1=3$
21 5p5e10 ${⊢}5+5=10$
22 6 13 6 13 16 16 20 15 21 decaddc ${⊢}15+15=30$
23 6 13 6 13 14 15 22 dpadd ${⊢}1.5+1.5=3.0$
24 14 dp0u ${⊢}3.0=3$
25 23 24 eqtri ${⊢}1.5+1.5=3$
26 10 times2i ${⊢}1.5\cdot 2=1.5+1.5$
27 1 recni ${⊢}3\in ℂ$
28 11 simpli ${⊢}2\in ℂ$
29 27 28 3 divcan1i ${⊢}\left(\frac{3}{2}\right)\cdot 2=3$
30 25 26 29 3eqtr4ri ${⊢}\left(\frac{3}{2}\right)\cdot 2=1.5\cdot 2$
31 mulcan2 ${⊢}\left(\frac{3}{2}\in ℂ\wedge 1.5\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \left(\left(\frac{3}{2}\right)\cdot 2=1.5\cdot 2↔\frac{3}{2}=1.5\right)$
32 31 biimpa ${⊢}\left(\left(\frac{3}{2}\in ℂ\wedge 1.5\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\wedge \left(\frac{3}{2}\right)\cdot 2=1.5\cdot 2\right)\to \frac{3}{2}=1.5$
33 12 30 32 mp2an ${⊢}\frac{3}{2}=1.5$