Step |
Hyp |
Ref |
Expression |
1 |
|
1red |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 1 ∈ ℝ ) |
2 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 𝐴 ∈ ℝ ) |
3 |
|
remulcl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ ) |
4 |
3
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → ( 𝐴 · 𝐵 ) ∈ ℝ ) |
5 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 1 < 𝐴 ) |
6 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 1 < 𝐵 ) |
7 |
|
0red |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 0 ∈ ℝ ) |
8 |
|
0lt1 |
⊢ 0 < 1 |
9 |
8
|
a1i |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 0 < 1 ) |
10 |
7 1 2 9 5
|
lttrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 0 < 𝐴 ) |
11 |
|
ltmulgt11 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 < 𝐵 ↔ 𝐴 < ( 𝐴 · 𝐵 ) ) ) |
12 |
11
|
3expa |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < 𝐴 ) → ( 1 < 𝐵 ↔ 𝐴 < ( 𝐴 · 𝐵 ) ) ) |
13 |
10 12
|
syldan |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → ( 1 < 𝐵 ↔ 𝐴 < ( 𝐴 · 𝐵 ) ) ) |
14 |
6 13
|
mpbid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 𝐴 < ( 𝐴 · 𝐵 ) ) |
15 |
1 2 4 5 14
|
lttrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 1 < ( 𝐴 · 𝐵 ) ) |