Metamath Proof Explorer

Theorem unitdivcld

Description: Necessary conditions for a quotient to be in the closed unit interval. (somewhat too strong, it would be sufficient that A and B are in RR+) (Contributed by Thierry Arnoux, 20-Dec-2016)

Ref Expression
Assertion unitdivcld ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 / 𝐵 ) ∈ ( 0 [,] 1 ) ) )

Proof

Step Hyp Ref Expression
1 elunitrn ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) → 𝐴 ∈ ℝ )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → 𝐴 ∈ ℝ )
3 elunitrn ⊢ ( 𝐵 ∈ ( 0 [,] 1 ) → 𝐵 ∈ ℝ )
4 3 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℝ )
5 simp3 ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → 𝐵 ≠ 0 )
6 2 4 5 redivcld ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
7 6 adantr ⊢ ( ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
8 elunitge0 ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) → 0 ≤ 𝐴 )
9 8 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → 0 ≤ 𝐴 )
10 elunitge0 ⊢ ( 𝐵 ∈ ( 0 [,] 1 ) → 0 ≤ 𝐵 )
11 10 adantr ⊢ ( ( 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → 0 ≤ 𝐵 )
12 0re ⊢ 0 ∈ ℝ
13 ltlen ⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐵 ↔ ( 0 ≤ 𝐵 ∧ 𝐵 ≠ 0 ) ) )
14 12 3 13 sylancr ⊢ ( 𝐵 ∈ ( 0 [,] 1 ) → ( 0 < 𝐵 ↔ ( 0 ≤ 𝐵 ∧ 𝐵 ≠ 0 ) ) )
15 14 biimpar ⊢ ( ( 𝐵 ∈ ( 0 [,] 1 ) ∧ ( 0 ≤ 𝐵 ∧ 𝐵 ≠ 0 ) ) → 0 < 𝐵 )
16 15 3impb ⊢ ( ( 𝐵 ∈ ( 0 [,] 1 ) ∧ 0 ≤ 𝐵 ∧ 𝐵 ≠ 0 ) → 0 < 𝐵 )
17 16 3com23 ⊢ ( ( 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ∧ 0 ≤ 𝐵 ) → 0 < 𝐵 )
18 11 17 mpd3an3 ⊢ ( ( 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → 0 < 𝐵 )
19 18 3adant1 ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → 0 < 𝐵 )
20 divge0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 ≤ ( 𝐴 / 𝐵 ) )
21 2 9 4 19 20 syl22anc ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → 0 ≤ ( 𝐴 / 𝐵 ) )
22 21 adantr ⊢ ( ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≤ 𝐵 ) → 0 ≤ ( 𝐴 / 𝐵 ) )
23 1red ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → 1 ∈ ℝ )
24 ledivmul ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) ≤ 1 ↔ 𝐴 ≤ ( 𝐵 · 1 ) ) )
25 2 23 4 19 24 syl112anc ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) ≤ 1 ↔ 𝐴 ≤ ( 𝐵 · 1 ) ) )
26 ax-1rid ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 1 ) = 𝐵 )
27 26 breq2d ⊢ ( 𝐵 ∈ ℝ → ( 𝐴 ≤ ( 𝐵 · 1 ) ↔ 𝐴 ≤ 𝐵 ) )
28 4 27 syl ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → ( 𝐴 ≤ ( 𝐵 · 1 ) ↔ 𝐴 ≤ 𝐵 ) )
29 25 28 bitr2d ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 / 𝐵 ) ≤ 1 ) )
30 29 biimpa ⊢ ( ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 / 𝐵 ) ≤ 1 )
31 7 22 30 3jca ⊢ ( ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ∧ ( 𝐴 / 𝐵 ) ≤ 1 ) )
32 31 ex ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → ( 𝐴 ≤ 𝐵 → ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ∧ ( 𝐴 / 𝐵 ) ≤ 1 ) ) )
33 simp3 ⊢ ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ∧ ( 𝐴 / 𝐵 ) ≤ 1 ) → ( 𝐴 / 𝐵 ) ≤ 1 )
34 33 29 syl5ibr ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ∧ ( 𝐴 / 𝐵 ) ≤ 1 ) → 𝐴 ≤ 𝐵 ) )
35 32 34 impbid ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → ( 𝐴 ≤ 𝐵 ↔ ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ∧ ( 𝐴 / 𝐵 ) ≤ 1 ) ) )
36 elicc01 ⊢ ( ( 𝐴 / 𝐵 ) ∈ ( 0 [,] 1 ) ↔ ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ∧ ( 𝐴 / 𝐵 ) ≤ 1 ) )
37 35 36 bitr4di ⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ∧ 𝐵 ≠ 0 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 / 𝐵 ) ∈ ( 0 [,] 1 ) ) )