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

Metamath Proof Explorer

Theorem remulg

Description: The multiplication (group power) operation of the group of reals. (Contributed by Thierry Arnoux, 1-Nov-2017)

Ref Expression
Assertion remulg 
|- ( ( N e. ZZ /\ A e. RR ) -> ( N ( .g ` RRfld ) A ) = ( N x. A ) )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( x e. RR -> x e. CC )
2 readdcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
3 renegcl 
 |-  ( x e. RR -> -u x e. RR )
4 1re 
 |-  1 e. RR
5 1 2 3 4 cnsubglem 
 |-  RR e. ( SubGrp ` CCfld )
6 eqid 
 |-  ( .g ` CCfld ) = ( .g ` CCfld )
7 df-refld 
 |-  RRfld = ( CCfld |`s RR )
8 eqid 
 |-  ( .g ` RRfld ) = ( .g ` RRfld )
9 6 7 8 subgmulg 
 |-  ( ( RR e. ( SubGrp ` CCfld ) /\ N e. ZZ /\ A e. RR ) -> ( N ( .g ` CCfld ) A ) = ( N ( .g ` RRfld ) A ) )
10 5 9 mp3an1 
 |-  ( ( N e. ZZ /\ A e. RR ) -> ( N ( .g ` CCfld ) A ) = ( N ( .g ` RRfld ) A ) )
11 simpr 
 |-  ( ( N e. ZZ /\ A e. RR ) -> A e. RR )
12 11 recnd 
 |-  ( ( N e. ZZ /\ A e. RR ) -> A e. CC )
13 cnfldmulg 
 |-  ( ( N e. ZZ /\ A e. CC ) -> ( N ( .g ` CCfld ) A ) = ( N x. A ) )
14 12 13 syldan 
 |-  ( ( N e. ZZ /\ A e. RR ) -> ( N ( .g ` CCfld ) A ) = ( N x. A ) )
15 10 14 eqtr3d 
 |-  ( ( N e. ZZ /\ A e. RR ) -> ( N ( .g ` RRfld ) A ) = ( N x. A ) )