threehalves

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

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

Step	Hyp	Ref	Expression
1		3re	$⊢ 3 \in ℝ$
2		2re	$⊢ 2 \in ℝ$
3		2ne0	$⊢ 2 \neq 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	$⊢ (1 \in ℕ_{0} \land 5 \in ℝ) \to 1.5 \in ℝ$
9	6 7 8	mp2an	$⊢ 1.5 \in ℝ$
10	9	recni	$⊢ 1.5 \in ℂ$
11		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
12	5 10 11	3pm3.2i	$⊢ (\frac{3}{2} \in ℂ \land 1.5 \in ℂ \land (2 \in ℂ \land 2 \neq 0))$
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	$⊢ (\frac{3}{2}) \cdot 2 = 3$
30	25 26 29	3eqtr4ri	$⊢ (\frac{3}{2}) \cdot 2 = 1.5 \cdot 2$
31		mulcan2	$⊢ (\frac{3}{2} \in ℂ \land 1.5 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to ((\frac{3}{2}) \cdot 2 = 1.5 \cdot 2 \leftrightarrow \frac{3}{2} = 1.5)$
32	31	biimpa	$⊢ ((\frac{3}{2} \in ℂ \land 1.5 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \land (\frac{3}{2}) \cdot 2 = 1.5 \cdot 2) \to \frac{3}{2} = 1.5$
33	12 30 32	mp2an	$⊢ \frac{3}{2} = 1.5$

Metamath Proof Explorer