Theorem iimulcl

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

	Ref	Expression
Assertion	iimulcl	⊢ ( ( 𝐴 ∈ ( 0 [,] 1 ) ∧ 𝐵 ∈ ( 0 [,] 1 ) ) → ( 𝐴 · 𝐵 ) ∈ ( 0 [,] 1 ) )

Proof

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