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 e. RR
2 2re 
 |-  2 e. RR
3 2ne0 
 |-  2 =/= 0
4 1 2 3 redivcli 
 |-  ( 3 / 2 ) e. RR
5 4 recni 
 |-  ( 3 / 2 ) e. CC
6 1nn0 
 |-  1 e. NN0
7 5re 
 |-  5 e. RR
8 dpcl 
 |-  ( ( 1 e. NN0 /\ 5 e. RR ) -> ( 1 . 5 ) e. RR )
9 6 7 8 mp2an 
 |-  ( 1 . 5 ) e. RR
10 9 recni 
 |-  ( 1 . 5 ) e. CC
11 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
12 5 10 11 3pm3.2i 
 |-  ( ( 3 / 2 ) e. CC /\ ( 1 . 5 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) )
13 5nn0 
 |-  5 e. NN0
14 3nn0 
 |-  3 e. NN0
15 0nn0 
 |-  0 e. NN0
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 ) x. 2 ) = ( ( 1 . 5 ) + ( 1 . 5 ) )
27 1 recni 
 |-  3 e. CC
28 11 simpli 
 |-  2 e. CC
29 27 28 3 divcan1i 
 |-  ( ( 3 / 2 ) x. 2 ) = 3
30 25 26 29 3eqtr4ri 
 |-  ( ( 3 / 2 ) x. 2 ) = ( ( 1 . 5 ) x. 2 )
31 mulcan2 
 |-  ( ( ( 3 / 2 ) e. CC /\ ( 1 . 5 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( 3 / 2 ) x. 2 ) = ( ( 1 . 5 ) x. 2 ) <-> ( 3 / 2 ) = ( 1 . 5 ) ) )
32 31 biimpa 
 |-  ( ( ( ( 3 / 2 ) e. CC /\ ( 1 . 5 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) /\ ( ( 3 / 2 ) x. 2 ) = ( ( 1 . 5 ) x. 2 ) ) -> ( 3 / 2 ) = ( 1 . 5 ) )
33 12 30 32 mp2an 
 |-  ( 3 / 2 ) = ( 1 . 5 )