Theorem threehalves

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

	Ref	Expression
Assertion	threehalves	⊢ ( 3 / 2 ) = ( 1 . 5 )

Proof

Step	Hyp	Ref	Expression
1		3re	⊢ 3 ∈ ℝ
2		2re	⊢ 2 ∈ ℝ
3		2ne0	⊢ 2 ≠ 0
4	1 2 3	redivcli	⊢ ( 3 / 2 ) ∈ ℝ
5	4	recni	⊢ ( 3 / 2 ) ∈ ℂ
6		1nn0	⊢ 1 ∈ ℕ0
7		5re	⊢ 5 ∈ ℝ
8		dpcl	⊢ ( ( 1 ∈ ℕ0 ∧ 5 ∈ ℝ ) → ( 1 . 5 ) ∈ ℝ )
9	6 7 8	mp2an	⊢ ( 1 . 5 ) ∈ ℝ
10	9	recni	⊢ ( 1 . 5 ) ∈ ℂ
11		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
12	5 10 11	3pm3.2i	⊢ ( ( 3 / 2 ) ∈ ℂ ∧ ( 1 . 5 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
13		5nn0	⊢ 5 ∈ ℕ0
14		3nn0	⊢ 3 ∈ ℕ0
15		0nn0	⊢ 0 ∈ ℕ0
16		eqid	⊢ ; 1 5 = ; 1 5
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 ) = ; 1 0
22	6 13 6 13 16 16 20 15 21	decaddc	⊢ ( ; 1 5 + ; 1 5 ) = ; 3 0
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 ) · 2 ) = ( ( 1 . 5 ) + ( 1 . 5 ) )
27	1	recni	⊢ 3 ∈ ℂ
28	11	simpli	⊢ 2 ∈ ℂ
29	27 28 3	divcan1i	⊢ ( ( 3 / 2 ) · 2 ) = 3
30	25 26 29	3eqtr4ri	⊢ ( ( 3 / 2 ) · 2 ) = ( ( 1 . 5 ) · 2 )
31		mulcan2	⊢ ( ( ( 3 / 2 ) ∈ ℂ ∧ ( 1 . 5 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 3 / 2 ) · 2 ) = ( ( 1 . 5 ) · 2 ) ↔ ( 3 / 2 ) = ( 1 . 5 ) ) )
32	31	biimpa	⊢ ( ( ( ( 3 / 2 ) ∈ ℂ ∧ ( 1 . 5 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) ∧ ( ( 3 / 2 ) · 2 ) = ( ( 1 . 5 ) · 2 ) ) → ( 3 / 2 ) = ( 1 . 5 ) )
33	12 30 32	mp2an	⊢ ( 3 / 2 ) = ( 1 . 5 )