Step |
Hyp |
Ref |
Expression |
1 |
|
pcoval.2 |
⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) ) |
2 |
|
pcoval.3 |
⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) ) |
3 |
|
0re |
⊢ 0 ∈ ℝ |
4 |
|
1re |
⊢ 1 ∈ ℝ |
5 |
|
0le0 |
⊢ 0 ≤ 0 |
6 |
|
halfre |
⊢ ( 1 / 2 ) ∈ ℝ |
7 |
|
halflt1 |
⊢ ( 1 / 2 ) < 1 |
8 |
6 4 7
|
ltleii |
⊢ ( 1 / 2 ) ≤ 1 |
9 |
|
iccss |
⊢ ( ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ 0 ∧ ( 1 / 2 ) ≤ 1 ) ) → ( 0 [,] ( 1 / 2 ) ) ⊆ ( 0 [,] 1 ) ) |
10 |
3 4 5 8 9
|
mp4an |
⊢ ( 0 [,] ( 1 / 2 ) ) ⊆ ( 0 [,] 1 ) |
11 |
10
|
sseli |
⊢ ( 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) → 𝑋 ∈ ( 0 [,] 1 ) ) |
12 |
1 2
|
pcovalg |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 𝑋 ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) ) |
13 |
11 12
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 𝑋 ) = if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) ) |
14 |
|
elii1 |
⊢ ( 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) ↔ ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑋 ≤ ( 1 / 2 ) ) ) |
15 |
14
|
simprbi |
⊢ ( 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) → 𝑋 ≤ ( 1 / 2 ) ) |
16 |
15
|
iftrued |
⊢ ( 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) → if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) = ( 𝐹 ‘ ( 2 · 𝑋 ) ) ) |
17 |
16
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) ) → if ( 𝑋 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑋 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑋 ) − 1 ) ) ) = ( 𝐹 ‘ ( 2 · 𝑋 ) ) ) |
18 |
13 17
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 2 · 𝑋 ) ) ) |