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	imbitrrid	⊢ ( ( 𝐴 ∈ ( 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 ) ) )