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 ⊢A∈01∧B∈01∧B≠0→A≤B↔AB∈01

Proof

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