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 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 < B → A B ∈ 0 1 ↔ A ≤ B

Proof

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