Metamath Proof Explorer

Theorem iimulcl

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

Ref Expression
Assertion iimulcl ⊢ A ∈ 0 1 ∧ B ∈ 0 1 → A ⁢ B ∈ 0 1

Proof

Step Hyp Ref Expression
1 remulcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⁢ B ∈ ℝ
2 1 3ad2antr1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ B ∧ B ≤ 1 → A ⁢ B ∈ ℝ
3 2 3ad2antl1 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ A ≤ 1 ∧ B ∈ ℝ ∧ 0 ≤ B ∧ B ≤ 1 → A ⁢ B ∈ ℝ
4 mulge0 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → 0 ≤ A ⁢ B
5 4 3adantr3 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ B ≤ 1 → 0 ≤ A ⁢ B
6 5 3adantl3 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ A ≤ 1 ∧ B ∈ ℝ ∧ 0 ≤ B ∧ B ≤ 1 → 0 ≤ A ⁢ B
7 an6 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ A ≤ 1 ∧ B ∈ ℝ ∧ 0 ≤ B ∧ B ≤ 1 ↔ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ∧ 0 ≤ B ∧ A ≤ 1 ∧ B ≤ 1
8 1re ⊢ 1 ∈ ℝ
9 lemul12a ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ 1 ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ B ∧ 1 ∈ ℝ → A ≤ 1 ∧ B ≤ 1 → A ⁢ B ≤ 1 ⋅ 1
10 8 9 mpanr2 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ 1 ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ 1 ∧ B ≤ 1 → A ⁢ B ≤ 1 ⋅ 1
11 8 10 mpanl2 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ 1 ∧ B ≤ 1 → A ⁢ B ≤ 1 ⋅ 1
12 11 an4s ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ∧ 0 ≤ B → A ≤ 1 ∧ B ≤ 1 → A ⁢ B ≤ 1 ⋅ 1
13 12 3impia ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ∧ 0 ≤ B ∧ A ≤ 1 ∧ B ≤ 1 → A ⁢ B ≤ 1 ⋅ 1
14 7 13 sylbi ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ A ≤ 1 ∧ B ∈ ℝ ∧ 0 ≤ B ∧ B ≤ 1 → A ⁢ B ≤ 1 ⋅ 1
15 1t1e1 ⊢ 1 ⋅ 1 = 1
16 14 15 breqtrdi ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ A ≤ 1 ∧ B ∈ ℝ ∧ 0 ≤ B ∧ B ≤ 1 → A ⁢ B ≤ 1
17 3 6 16 3jca ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ A ≤ 1 ∧ B ∈ ℝ ∧ 0 ≤ B ∧ B ≤ 1 → A ⁢ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ A ⁢ B ≤ 1
18 elicc01 ⊢ A ∈ 0 1 ↔ A ∈ ℝ ∧ 0 ≤ A ∧ A ≤ 1
19 elicc01 ⊢ B ∈ 0 1 ↔ B ∈ ℝ ∧ 0 ≤ B ∧ B ≤ 1
20 18 19 anbi12i ⊢ A ∈ 0 1 ∧ B ∈ 0 1 ↔ A ∈ ℝ ∧ 0 ≤ A ∧ A ≤ 1 ∧ B ∈ ℝ ∧ 0 ≤ B ∧ B ≤ 1
21 elicc01 ⊢ A ⁢ B ∈ 0 1 ↔ A ⁢ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ A ⁢ B ≤ 1
22 17 20 21 3imtr4i ⊢ A ∈ 0 1 ∧ B ∈ 0 1 → A ⁢ B ∈ 0 1