Theorem iihalf2

Description: Map the second half of II into II . (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	iihalf2	⊢ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 2 · 𝑋 ) − 1 ) ∈ ( 0 [,] 1 ) )

Proof

Step	Hyp	Ref	Expression
1		2re	⊢ 2 ∈ ℝ
2		remulcl	⊢ ( ( 2 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 2 · 𝑋 ) ∈ ℝ )
3	1 2	mpan	⊢ ( 𝑋 ∈ ℝ → ( 2 · 𝑋 ) ∈ ℝ )
4		1re	⊢ 1 ∈ ℝ
5		resubcl	⊢ ( ( ( 2 · 𝑋 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 2 · 𝑋 ) − 1 ) ∈ ℝ )
6	3 4 5	sylancl	⊢ ( 𝑋 ∈ ℝ → ( ( 2 · 𝑋 ) − 1 ) ∈ ℝ )
7	6	3ad2ant1	⊢ ( ( 𝑋 ∈ ℝ ∧ ( 1 / 2 ) ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → ( ( 2 · 𝑋 ) − 1 ) ∈ ℝ )
8		subge0	⊢ ( ( ( 2 · 𝑋 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 ≤ ( ( 2 · 𝑋 ) − 1 ) ↔ 1 ≤ ( 2 · 𝑋 ) ) )
9	3 4 8	sylancl	⊢ ( 𝑋 ∈ ℝ → ( 0 ≤ ( ( 2 · 𝑋 ) − 1 ) ↔ 1 ≤ ( 2 · 𝑋 ) ) )
10		2pos	⊢ 0 < 2
11	1 10	pm3.2i	⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
12		ledivmul	⊢ ( ( 1 ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 1 / 2 ) ≤ 𝑋 ↔ 1 ≤ ( 2 · 𝑋 ) ) )
13	4 11 12	mp3an13	⊢ ( 𝑋 ∈ ℝ → ( ( 1 / 2 ) ≤ 𝑋 ↔ 1 ≤ ( 2 · 𝑋 ) ) )
14	9 13	bitr4d	⊢ ( 𝑋 ∈ ℝ → ( 0 ≤ ( ( 2 · 𝑋 ) − 1 ) ↔ ( 1 / 2 ) ≤ 𝑋 ) )
15	14	biimpar	⊢ ( ( 𝑋 ∈ ℝ ∧ ( 1 / 2 ) ≤ 𝑋 ) → 0 ≤ ( ( 2 · 𝑋 ) − 1 ) )
16	15	3adant3	⊢ ( ( 𝑋 ∈ ℝ ∧ ( 1 / 2 ) ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → 0 ≤ ( ( 2 · 𝑋 ) − 1 ) )
17		ax-1cn	⊢ 1 ∈ ℂ
18	17	2timesi	⊢ ( 2 · 1 ) = ( 1 + 1 )
19	18	a1i	⊢ ( 𝑋 ∈ ℝ → ( 2 · 1 ) = ( 1 + 1 ) )
20	19	breq2d	⊢ ( 𝑋 ∈ ℝ → ( ( 2 · 𝑋 ) ≤ ( 2 · 1 ) ↔ ( 2 · 𝑋 ) ≤ ( 1 + 1 ) ) )
21		lemul2	⊢ ( ( 𝑋 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝑋 ≤ 1 ↔ ( 2 · 𝑋 ) ≤ ( 2 · 1 ) ) )
22	4 11 21	mp3an23	⊢ ( 𝑋 ∈ ℝ → ( 𝑋 ≤ 1 ↔ ( 2 · 𝑋 ) ≤ ( 2 · 1 ) ) )
23		lesubadd	⊢ ( ( ( 2 · 𝑋 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( 2 · 𝑋 ) − 1 ) ≤ 1 ↔ ( 2 · 𝑋 ) ≤ ( 1 + 1 ) ) )
24	4 4 23	mp3an23	⊢ ( ( 2 · 𝑋 ) ∈ ℝ → ( ( ( 2 · 𝑋 ) − 1 ) ≤ 1 ↔ ( 2 · 𝑋 ) ≤ ( 1 + 1 ) ) )
25	3 24	syl	⊢ ( 𝑋 ∈ ℝ → ( ( ( 2 · 𝑋 ) − 1 ) ≤ 1 ↔ ( 2 · 𝑋 ) ≤ ( 1 + 1 ) ) )
26	20 22 25	3bitr4d	⊢ ( 𝑋 ∈ ℝ → ( 𝑋 ≤ 1 ↔ ( ( 2 · 𝑋 ) − 1 ) ≤ 1 ) )
27	26	biimpa	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑋 ≤ 1 ) → ( ( 2 · 𝑋 ) − 1 ) ≤ 1 )
28	27	3adant2	⊢ ( ( 𝑋 ∈ ℝ ∧ ( 1 / 2 ) ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → ( ( 2 · 𝑋 ) − 1 ) ≤ 1 )
29	7 16 28	3jca	⊢ ( ( 𝑋 ∈ ℝ ∧ ( 1 / 2 ) ≤ 𝑋 ∧ 𝑋 ≤ 1 ) → ( ( ( 2 · 𝑋 ) − 1 ) ∈ ℝ ∧ 0 ≤ ( ( 2 · 𝑋 ) − 1 ) ∧ ( ( 2 · 𝑋 ) − 1 ) ≤ 1 ) )
30		halfre	⊢ ( 1 / 2 ) ∈ ℝ
31	30 4	elicc2i	⊢ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) ↔ ( 𝑋 ∈ ℝ ∧ ( 1 / 2 ) ≤ 𝑋 ∧ 𝑋 ≤ 1 ) )
32		elicc01	⊢ ( ( ( 2 · 𝑋 ) − 1 ) ∈ ( 0 [,] 1 ) ↔ ( ( ( 2 · 𝑋 ) − 1 ) ∈ ℝ ∧ 0 ≤ ( ( 2 · 𝑋 ) − 1 ) ∧ ( ( 2 · 𝑋 ) − 1 ) ≤ 1 ) )
33	29 31 32	3imtr4i	⊢ ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 2 · 𝑋 ) − 1 ) ∈ ( 0 [,] 1 ) )