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

Metamath Proof Explorer

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 )