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

Metamath Proof Explorer

Theorem divelunit

Description: A condition for a ratio to be a member of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion divelunit ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) ∈ ( 0 [,] 1 ) ↔ 𝐴 ≤ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elicc01 ⊢ ( ( 𝐴 / 𝐵 ) ∈ ( 0 [,] 1 ) ↔ ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ∧ ( 𝐴 / 𝐵 ) ≤ 1 ) )
2 df-3an ⊢ ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ∧ ( 𝐴 / 𝐵 ) ≤ 1 ) ↔ ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ) ∧ ( 𝐴 / 𝐵 ) ≤ 1 ) )
3 1 2 bitri ⊢ ( ( 𝐴 / 𝐵 ) ∈ ( 0 [,] 1 ) ↔ ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ) ∧ ( 𝐴 / 𝐵 ) ≤ 1 ) )
4 1re ⊢ 1 ∈ ℝ
5 ledivmul ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) ≤ 1 ↔ 𝐴 ≤ ( 𝐵 · 1 ) ) )
6 4 5 mp3an2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) ≤ 1 ↔ 𝐴 ≤ ( 𝐵 · 1 ) ) )
7 6 adantlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) ≤ 1 ↔ 𝐴 ≤ ( 𝐵 · 1 ) ) )
8 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 𝐴 ∈ ℝ )
9 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 𝐵 ∈ ℝ )
10 gt0ne0 ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ≠ 0 )
11 10 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 𝐵 ≠ 0 )
12 8 9 11 redivcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
13 divge0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 ≤ ( 𝐴 / 𝐵 ) )
14 12 13 jca ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ) )
15 14 biantrurd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) ≤ 1 ↔ ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ) ∧ ( 𝐴 / 𝐵 ) ≤ 1 ) ) )
16 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
17 16 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 𝐵 ∈ ℂ )
18 17 mulridd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐵 · 1 ) = 𝐵 )
19 18 breq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐴 ≤ ( 𝐵 · 1 ) ↔ 𝐴 ≤ 𝐵 ) )
20 7 15 19 3bitr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ) ∧ ( 𝐴 / 𝐵 ) ≤ 1 ) ↔ 𝐴 ≤ 𝐵 ) )
21 3 20 bitrid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) ∈ ( 0 [,] 1 ) ↔ 𝐴 ≤ 𝐵 ) )