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∈01∧B∈01→A⁢B∈01

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∈01↔A∈ℝ∧0≤A∧A≤1
19 elicc01 ⊢B∈01↔B∈ℝ∧0≤B∧B≤1
20 18 19 anbi12i ⊢A∈01∧B∈01↔A∈ℝ∧0≤A∧A≤1∧B∈ℝ∧0≤B∧B≤1
21 elicc01 ⊢A⁢B∈01↔A⁢B∈ℝ∧0≤A⁢B∧A⁢B≤1
22 17 20 21 3imtr4i ⊢A∈01∧B∈01→A⁢B∈01