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

Metamath Proof Explorer

Theorem divge1

Description: The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Assertion divge1 ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 1 ≤ ( 𝐵 / 𝐴 ) )

Proof

Step Hyp Ref Expression
1 rpgecl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ+ )
2 rpcn ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
3 rpne0 ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
4 2 3 dividd ⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 / 𝐵 ) = 1 )
5 4 eqcomd ⊢ ( 𝐵 ∈ ℝ+ → 1 = ( 𝐵 / 𝐵 ) )
6 1 5 syl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 1 = ( 𝐵 / 𝐵 ) )
7 simp3 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
8 simp1 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ+ )
9 8 1 1 lediv2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐵 / 𝐵 ) ≤ ( 𝐵 / 𝐴 ) ) )
10 7 9 mpbid ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 / 𝐵 ) ≤ ( 𝐵 / 𝐴 ) )
11 6 10 eqbrtrd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 1 ≤ ( 𝐵 / 𝐴 ) )