Metamath Proof Explorer

Theorem relogoprlem

Description: Lemma for relogmul and relogdiv . Remark of Cohen p. 301 ("The proof of Property 3 is quite similar to the proof given for Property 2"). (Contributed by Steve Rodriguez, 25-Nov-2007)

Ref Expression
Hypotheses relogoprlem.1 
|- ( ( ( log ` A ) e. CC /\ ( log ` B ) e. CC ) -> ( exp ` ( ( log ` A ) F ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) G ( exp ` ( log ` B ) ) ) )
relogoprlem.2 
|- ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( ( log ` A ) F ( log ` B ) ) e. RR )
Assertion relogoprlem 
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A G B ) ) = ( ( log ` A ) F ( log ` B ) ) )

Proof

Step Hyp Ref Expression
1 relogoprlem.1 
 |-  ( ( ( log ` A ) e. CC /\ ( log ` B ) e. CC ) -> ( exp ` ( ( log ` A ) F ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) G ( exp ` ( log ` B ) ) ) )
2 relogoprlem.2 
 |-  ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( ( log ` A ) F ( log ` B ) ) e. RR )
3 reeflog 
 |-  ( A e. RR+ -> ( exp ` ( log ` A ) ) = A )
4 reeflog 
 |-  ( B e. RR+ -> ( exp ` ( log ` B ) ) = B )
5 3 4 oveqan12d 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( ( exp ` ( log ` A ) ) G ( exp ` ( log ` B ) ) ) = ( A G B ) )
6 5 fveq2d 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( ( exp ` ( log ` A ) ) G ( exp ` ( log ` B ) ) ) ) = ( log ` ( A G B ) ) )
7 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
8 relogcl 
 |-  ( B e. RR+ -> ( log ` B ) e. RR )
9 recn 
 |-  ( ( log ` A ) e. RR -> ( log ` A ) e. CC )
10 recn 
 |-  ( ( log ` B ) e. RR -> ( log ` B ) e. CC )
11 1 fveq2d 
 |-  ( ( ( log ` A ) e. CC /\ ( log ` B ) e. CC ) -> ( log ` ( exp ` ( ( log ` A ) F ( log ` B ) ) ) ) = ( log ` ( ( exp ` ( log ` A ) ) G ( exp ` ( log ` B ) ) ) ) )
12 9 10 11 syl2an 
 |-  ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( log ` ( exp ` ( ( log ` A ) F ( log ` B ) ) ) ) = ( log ` ( ( exp ` ( log ` A ) ) G ( exp ` ( log ` B ) ) ) ) )
13 relogef 
 |-  ( ( ( log ` A ) F ( log ` B ) ) e. RR -> ( log ` ( exp ` ( ( log ` A ) F ( log ` B ) ) ) ) = ( ( log ` A ) F ( log ` B ) ) )
14 2 13 syl 
 |-  ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( log ` ( exp ` ( ( log ` A ) F ( log ` B ) ) ) ) = ( ( log ` A ) F ( log ` B ) ) )
15 12 14 eqtr3d 
 |-  ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( log ` ( ( exp ` ( log ` A ) ) G ( exp ` ( log ` B ) ) ) ) = ( ( log ` A ) F ( log ` B ) ) )
16 7 8 15 syl2an 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( ( exp ` ( log ` A ) ) G ( exp ` ( log ` B ) ) ) ) = ( ( log ` A ) F ( log ` B ) ) )
17 6 16 eqtr3d 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A G B ) ) = ( ( log ` A ) F ( log ` B ) ) )