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

Metamath Proof Explorer

Theorem logltb

Description: The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007)

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

Proof

Step	Hyp	Ref	Expression
1		relogiso	\|- ( log \|` RR+ ) Isom < , < ( RR+ , RR )
2		df-isom	\|- ( ( log \|` RR+ ) Isom < , < ( RR+ , RR ) <-> ( ( log \|` RR+ ) : RR+ -1-1-onto-> RR /\ A. x e. RR+ A. y e. RR+ ( x < y <-> ( ( log \|` RR+ ) ` x ) < ( ( log \|` RR+ ) ` y ) ) ) )
3	1 2	mpbi	\|- ( ( log \|` RR+ ) : RR+ -1-1-onto-> RR /\ A. x e. RR+ A. y e. RR+ ( x < y <-> ( ( log \|` RR+ ) ` x ) < ( ( log \|` RR+ ) ` y ) ) )
4	3	simpri	\|- A. x e. RR+ A. y e. RR+ ( x < y <-> ( ( log \|` RR+ ) ` x ) < ( ( log \|` RR+ ) ` y ) )
5		breq1	\|- ( x = A -> ( x < y <-> A < y ) )
6		fveq2	\|- ( x = A -> ( ( log \|` RR+ ) ` x ) = ( ( log \|` RR+ ) ` A ) )
7	6	breq1d	\|- ( x = A -> ( ( ( log \|` RR+ ) ` x ) < ( ( log \|` RR+ ) ` y ) <-> ( ( log \|` RR+ ) ` A ) < ( ( log \|` RR+ ) ` y ) ) )
8	5 7	bibi12d	\|- ( x = A -> ( ( x < y <-> ( ( log \|` RR+ ) ` x ) < ( ( log \|` RR+ ) ` y ) ) <-> ( A < y <-> ( ( log \|` RR+ ) ` A ) < ( ( log \|` RR+ ) ` y ) ) ) )
9		breq2	\|- ( y = B -> ( A < y <-> A < B ) )
10		fveq2	\|- ( y = B -> ( ( log \|` RR+ ) ` y ) = ( ( log \|` RR+ ) ` B ) )
11	10	breq2d	\|- ( y = B -> ( ( ( log \|` RR+ ) ` A ) < ( ( log \|` RR+ ) ` y ) <-> ( ( log \|` RR+ ) ` A ) < ( ( log \|` RR+ ) ` B ) ) )
12	9 11	bibi12d	\|- ( y = B -> ( ( A < y <-> ( ( log \|` RR+ ) ` A ) < ( ( log \|` RR+ ) ` y ) ) <-> ( A < B <-> ( ( log \|` RR+ ) ` A ) < ( ( log \|` RR+ ) ` B ) ) ) )
13	8 12	rspc2v	\|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A. x e. RR+ A. y e. RR+ ( x < y <-> ( ( log \|` RR+ ) ` x ) < ( ( log \|` RR+ ) ` y ) ) -> ( A < B <-> ( ( log \|` RR+ ) ` A ) < ( ( log \|` RR+ ) ` B ) ) ) )
14	4 13	mpi	\|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( ( log \|` RR+ ) ` A ) < ( ( log \|` RR+ ) ` B ) ) )
15		fvres	\|- ( A e. RR+ -> ( ( log \|` RR+ ) ` A ) = ( log ` A ) )
16		fvres	\|- ( B e. RR+ -> ( ( log \|` RR+ ) ` B ) = ( log ` B ) )
17	15 16	breqan12d	\|- ( ( A e. RR+ /\ B e. RR+ ) -> ( ( ( log \|` RR+ ) ` A ) < ( ( log \|` RR+ ) ` B ) <-> ( log ` A ) < ( log ` B ) ) )
18	14 17	bitrd	\|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( log ` A ) < ( log ` B ) ) )