# Metamath Proof Explorer

## Theorem iimulcl

Description: The unit interval is closed under multiplication. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion iimulcl ${⊢}\left({A}\in \left[0,1\right]\wedge {B}\in \left[0,1\right]\right)\to {A}{B}\in \left[0,1\right]$

### Proof

Step Hyp Ref Expression
1 remulcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{B}\in ℝ$
2 1 3ad2antr1 ${⊢}\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0\le {B}\wedge {B}\le 1\right)\right)\to {A}{B}\in ℝ$
3 2 3ad2antl1 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\wedge {A}\le 1\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\wedge {B}\le 1\right)\right)\to {A}{B}\in ℝ$
4 mulge0 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\right)\right)\to 0\le {A}{B}$
5 4 3adantr3 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\wedge {B}\le 1\right)\right)\to 0\le {A}{B}$
6 5 3adantl3 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\wedge {A}\le 1\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\wedge {B}\le 1\right)\right)\to 0\le {A}{B}$
7 an6 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\wedge {A}\le 1\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\wedge {B}\le 1\right)\right)↔\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left(0\le {A}\wedge 0\le {B}\right)\wedge \left({A}\le 1\wedge {B}\le 1\right)\right)$
8 1re ${⊢}1\in ℝ$
9 lemul12a ${⊢}\left(\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge 1\in ℝ\right)\wedge \left(\left({B}\in ℝ\wedge 0\le {B}\right)\wedge 1\in ℝ\right)\right)\to \left(\left({A}\le 1\wedge {B}\le 1\right)\to {A}{B}\le 1\cdot 1\right)$
10 8 9 mpanr2 ${⊢}\left(\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge 1\in ℝ\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\right)\right)\to \left(\left({A}\le 1\wedge {B}\le 1\right)\to {A}{B}\le 1\cdot 1\right)$
11 8 10 mpanl2 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\right)\right)\to \left(\left({A}\le 1\wedge {B}\le 1\right)\to {A}{B}\le 1\cdot 1\right)$
12 11 an4s ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left(0\le {A}\wedge 0\le {B}\right)\right)\to \left(\left({A}\le 1\wedge {B}\le 1\right)\to {A}{B}\le 1\cdot 1\right)$
13 12 3impia ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left(0\le {A}\wedge 0\le {B}\right)\wedge \left({A}\le 1\wedge {B}\le 1\right)\right)\to {A}{B}\le 1\cdot 1$
14 7 13 sylbi ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\wedge {A}\le 1\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\wedge {B}\le 1\right)\right)\to {A}{B}\le 1\cdot 1$
15 1t1e1 ${⊢}1\cdot 1=1$
16 14 15 breqtrdi ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\wedge {A}\le 1\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\wedge {B}\le 1\right)\right)\to {A}{B}\le 1$
17 3 6 16 3jca ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\wedge {A}\le 1\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\wedge {B}\le 1\right)\right)\to \left({A}{B}\in ℝ\wedge 0\le {A}{B}\wedge {A}{B}\le 1\right)$
18 elicc01 ${⊢}{A}\in \left[0,1\right]↔\left({A}\in ℝ\wedge 0\le {A}\wedge {A}\le 1\right)$
19 elicc01 ${⊢}{B}\in \left[0,1\right]↔\left({B}\in ℝ\wedge 0\le {B}\wedge {B}\le 1\right)$
20 18 19 anbi12i ${⊢}\left({A}\in \left[0,1\right]\wedge {B}\in \left[0,1\right]\right)↔\left(\left({A}\in ℝ\wedge 0\le {A}\wedge {A}\le 1\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\wedge {B}\le 1\right)\right)$
21 elicc01 ${⊢}{A}{B}\in \left[0,1\right]↔\left({A}{B}\in ℝ\wedge 0\le {A}{B}\wedge {A}{B}\le 1\right)$
22 17 20 21 3imtr4i ${⊢}\left({A}\in \left[0,1\right]\wedge {B}\in \left[0,1\right]\right)\to {A}{B}\in \left[0,1\right]$