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 ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 < 𝐵 ↔ ( log ‘ 𝐴 ) < ( log ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 relogiso ⊢ ( log ↾ ℝ+ ) Isom < , < ( ℝ+ , ℝ )
2 df-isom ⊢ ( ( log ↾ ℝ+ ) Isom < , < ( ℝ+ , ℝ ) ↔ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ ∧ ∀ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℝ+ ( 𝑥 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) ) )
3 1 2 mpbi ⊢ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ ∧ ∀ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℝ+ ( 𝑥 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) )
4 3 simpri ⊢ ∀ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℝ+ ( 𝑥 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) )
5 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 < 𝑦 ↔ 𝐴 < 𝑦 ) )
6 fveq2 ⊢ ( 𝑥 = 𝐴 → ( ( log ↾ ℝ+ ) ‘ 𝑥 ) = ( ( log ↾ ℝ+ ) ‘ 𝐴 ) )
7 6 breq1d ⊢ ( 𝑥 = 𝐴 → ( ( ( log ↾ ℝ+ ) ‘ 𝑥 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) )
8 5 7 bibi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) ↔ ( 𝐴 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) ) )
9 breq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 < 𝑦 ↔ 𝐴 < 𝐵 ) )
10 fveq2 ⊢ ( 𝑦 = 𝐵 → ( ( log ↾ ℝ+ ) ‘ 𝑦 ) = ( ( log ↾ ℝ+ ) ‘ 𝐵 ) )
11 10 breq2d ⊢ ( 𝑦 = 𝐵 → ( ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝐵 ) ) )
12 9 11 bibi12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) ↔ ( 𝐴 < 𝐵 ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝐵 ) ) ) )
13 8 12 rspc2v ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℝ+ ( 𝑥 < 𝑦 ↔ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) < ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) → ( 𝐴 < 𝐵 ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝐵 ) ) ) )
14 4 13 mpi ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 < 𝐵 ↔ ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝐵 ) ) )
15 fvres ⊢ ( 𝐴 ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ 𝐴 ) = ( log ‘ 𝐴 ) )
16 fvres ⊢ ( 𝐵 ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ 𝐵 ) = ( log ‘ 𝐵 ) )
17 15 16 breqan12d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( log ↾ ℝ+ ) ‘ 𝐴 ) < ( ( log ↾ ℝ+ ) ‘ 𝐵 ) ↔ ( log ‘ 𝐴 ) < ( log ‘ 𝐵 ) ) )
18 14 17 bitrd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 < 𝐵 ↔ ( log ‘ 𝐴 ) < ( log ‘ 𝐵 ) ) )