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 \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to (A \leq B \leftrightarrow \frac{A}{B} \in [0, 1])$

Proof

Step	Hyp	Ref	Expression
1		elunitrn	$⊢ A \in [0, 1] \to A \in ℝ$
2	1	3ad2ant1	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to A \in ℝ$
3		elunitrn	$⊢ B \in [0, 1] \to B \in ℝ$
4	3	3ad2ant2	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to B \in ℝ$
5		simp3	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to B \neq 0$
6	2 4 5	redivcld	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to \frac{A}{B} \in ℝ$
7	6	adantr	$⊢ ((A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \land A \leq B) \to \frac{A}{B} \in ℝ$
8		elunitge0	$⊢ A \in [0, 1] \to 0 \leq A$
9	8	3ad2ant1	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to 0 \leq A$
10		elunitge0	$⊢ B \in [0, 1] \to 0 \leq B$
11	10	adantr	$⊢ (B \in [0, 1] \land B \neq 0) \to 0 \leq B$
12		0re	$⊢ 0 \in ℝ$
13		ltlen	$⊢ (0 \in ℝ \land B \in ℝ) \to (0 < B \leftrightarrow (0 \leq B \land B \neq 0))$
14	12 3 13	sylancr	$⊢ B \in [0, 1] \to (0 < B \leftrightarrow (0 \leq B \land B \neq 0))$
15	14	biimpar	$⊢ (B \in [0, 1] \land (0 \leq B \land B \neq 0)) \to 0 < B$
16	15	3impb	$⊢ (B \in [0, 1] \land 0 \leq B \land B \neq 0) \to 0 < B$
17	16	3com23	$⊢ (B \in [0, 1] \land B \neq 0 \land 0 \leq B) \to 0 < B$
18	11 17	mpd3an3	$⊢ (B \in [0, 1] \land B \neq 0) \to 0 < B$
19	18	3adant1	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to 0 < B$
20		divge0	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 < B)) \to 0 \leq \frac{A}{B}$
21	2 9 4 19 20	syl22anc	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to 0 \leq \frac{A}{B}$
22	21	adantr	$⊢ ((A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \land A \leq B) \to 0 \leq \frac{A}{B}$
23		1red	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to 1 \in ℝ$
24		ledivmul	$⊢ (A \in ℝ \land 1 \in ℝ \land (B \in ℝ \land 0 < B)) \to (\frac{A}{B} \leq 1 \leftrightarrow A \leq B \cdot 1)$
25	2 23 4 19 24	syl112anc	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to (\frac{A}{B} \leq 1 \leftrightarrow A \leq B \cdot 1)$
26		ax-1rid	$⊢ B \in ℝ \to B \cdot 1 = B$
27	26	breq2d	$⊢ B \in ℝ \to (A \leq B \cdot 1 \leftrightarrow A \leq B)$
28	4 27	syl	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to (A \leq B \cdot 1 \leftrightarrow A \leq B)$
29	25 28	bitr2d	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to (A \leq B \leftrightarrow \frac{A}{B} \leq 1)$
30	29	biimpa	$⊢ ((A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \land A \leq B) \to \frac{A}{B} \leq 1$
31	7 22 30	3jca	$⊢ ((A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \land A \leq B) \to (\frac{A}{B} \in ℝ \land 0 \leq \frac{A}{B} \land \frac{A}{B} \leq 1)$
32	31	ex	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to (A \leq B \to (\frac{A}{B} \in ℝ \land 0 \leq \frac{A}{B} \land \frac{A}{B} \leq 1))$
33		simp3	$⊢ (\frac{A}{B} \in ℝ \land 0 \leq \frac{A}{B} \land \frac{A}{B} \leq 1) \to \frac{A}{B} \leq 1$
34	33 29	imbitrrid	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to ((\frac{A}{B} \in ℝ \land 0 \leq \frac{A}{B} \land \frac{A}{B} \leq 1) \to A \leq B)$
35	32 34	impbid	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to (A \leq B \leftrightarrow (\frac{A}{B} \in ℝ \land 0 \leq \frac{A}{B} \land \frac{A}{B} \leq 1))$
36		elicc01	$⊢ \frac{A}{B} \in [0, 1] \leftrightarrow (\frac{A}{B} \in ℝ \land 0 \leq \frac{A}{B} \land \frac{A}{B} \leq 1)$
37	35 36	bitr4di	$⊢ (A \in [0, 1] \land B \in [0, 1] \land B \neq 0) \to (A \leq B \leftrightarrow \frac{A}{B} \in [0, 1])$

Metamath Proof Explorer

Theorem unitdivcld

Proof