Theorem reglogltb

Description: General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014) (New usage is discouraged.) Use logblt instead.

	Ref	Expression
Assertion	reglogltb	|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( A < B <-> ( ( log ` A ) / ( log ` C ) ) < ( ( log ` B ) / ( log ` C ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		logltb	|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( log ` A ) < ( log ` B ) ) )
2	1	adantr	|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( A < B <-> ( log ` A ) < ( log ` B ) ) )
3		relogcl	|- ( A e. RR+ -> ( log ` A ) e. RR )
4	3	ad2antrr	|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( log ` A ) e. RR )
5		relogcl	|- ( B e. RR+ -> ( log ` B ) e. RR )
6	5	ad2antlr	|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( log ` B ) e. RR )
7		relogcl	|- ( C e. RR+ -> ( log ` C ) e. RR )
8	7	ad2antrl	|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( log ` C ) e. RR )
9		log1	|- ( log ` 1 ) = 0
10		1rp	|- 1 e. RR+
11		logltb	|- ( ( 1 e. RR+ /\ C e. RR+ ) -> ( 1 < C <-> ( log ` 1 ) < ( log ` C ) ) )
12	10 11	mpan	|- ( C e. RR+ -> ( 1 < C <-> ( log ` 1 ) < ( log ` C ) ) )
13	12	biimpa	|- ( ( C e. RR+ /\ 1 < C ) -> ( log ` 1 ) < ( log ` C ) )
14	9 13	eqbrtrrid	|- ( ( C e. RR+ /\ 1 < C ) -> 0 < ( log ` C ) )
15	14	adantl	|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> 0 < ( log ` C ) )
16		ltdiv1	|- ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR /\ ( ( log ` C ) e. RR /\ 0 < ( log ` C ) ) ) -> ( ( log ` A ) < ( log ` B ) <-> ( ( log ` A ) / ( log ` C ) ) < ( ( log ` B ) / ( log ` C ) ) ) )
17	4 6 8 15 16	syl112anc	|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( ( log ` A ) < ( log ` B ) <-> ( ( log ` A ) / ( log ` C ) ) < ( ( log ` B ) / ( log ` C ) ) ) )
18	2 17	bitrd	|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( A < B <-> ( ( log ` A ) / ( log ` C ) ) < ( ( log ` B ) / ( log ` C ) ) ) )