Proof of Theorem pcoval2
Step | Hyp | Ref
| Expression |
1 | | 0re 9919 |
. . . . 5
⊢ 0 ∈
ℝ |
2 | | 1re 9918 |
. . . . 5
⊢ 1 ∈
ℝ |
3 | | halfre 11123 |
. . . . . 6
⊢ (1 / 2)
∈ ℝ |
4 | | halfgt0 11125 |
. . . . . 6
⊢ 0 < (1
/ 2) |
5 | 1, 3, 4 | ltleii 10039 |
. . . . 5
⊢ 0 ≤ (1
/ 2) |
6 | | 1le1 10534 |
. . . . 5
⊢ 1 ≤
1 |
7 | | iccss 12112 |
. . . . 5
⊢ (((0
∈ ℝ ∧ 1 ∈ ℝ) ∧ (0 ≤ (1 / 2) ∧ 1 ≤ 1))
→ ((1 / 2)[,]1) ⊆ (0[,]1)) |
8 | 1, 2, 5, 6, 7 | mp4an 705 |
. . . 4
⊢ ((1 /
2)[,]1) ⊆ (0[,]1) |
9 | 8 | sseli 3564 |
. . 3
⊢ (𝑋 ∈ ((1 / 2)[,]1) →
𝑋 ∈
(0[,]1)) |
10 | | pcoval.2 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
11 | | pcoval.3 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
12 | 10, 11 | pcovalg 22620 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑋) = if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1)))) |
13 | 9, 12 | sylan2 490 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑋) = if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1)))) |
14 | | pcoval2.4 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (𝐹‘1) = (𝐺‘0)) |
16 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → 𝑋 ≤ (1 / 2)) |
17 | 3, 2 | elicc2i 12110 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ((1 / 2)[,]1) ↔
(𝑋 ∈ ℝ ∧ (1
/ 2) ≤ 𝑋 ∧ 𝑋 ≤ 1)) |
18 | 17 | simp2bi 1070 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ((1 / 2)[,]1) → (1
/ 2) ≤ 𝑋) |
19 | 18 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (1 / 2)
≤ 𝑋) |
20 | 17 | simp1bi 1069 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ((1 / 2)[,]1) →
𝑋 ∈
ℝ) |
21 | 20 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → 𝑋 ∈
ℝ) |
22 | | letri3 10002 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℝ ∧ (1 / 2)
∈ ℝ) → (𝑋 =
(1 / 2) ↔ (𝑋 ≤ (1 /
2) ∧ (1 / 2) ≤ 𝑋))) |
23 | 21, 3, 22 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (𝑋 = (1 / 2) ↔ (𝑋 ≤ (1 / 2) ∧ (1 / 2) ≤
𝑋))) |
24 | 16, 19, 23 | mpbir2and 959 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → 𝑋 = (1 / 2)) |
25 | 24 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (2
· 𝑋) = (2 ·
(1 / 2))) |
26 | | 2cn 10968 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
27 | | 2ne0 10990 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
28 | 26, 27 | recidi 10635 |
. . . . . . . . 9
⊢ (2
· (1 / 2)) = 1 |
29 | 25, 28 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (2
· 𝑋) =
1) |
30 | 29 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (𝐹‘(2 · 𝑋)) = (𝐹‘1)) |
31 | 29 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → ((2
· 𝑋) − 1) = (1
− 1)) |
32 | | 1m1e0 10966 |
. . . . . . . . 9
⊢ (1
− 1) = 0 |
33 | 31, 32 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → ((2
· 𝑋) − 1) =
0) |
34 | 33 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (𝐺‘((2 · 𝑋) − 1)) = (𝐺‘0)) |
35 | 15, 30, 34 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (𝐹‘(2 · 𝑋)) = (𝐺‘((2 · 𝑋) − 1))) |
36 | 35 | ifeq1d 4054 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1))) = if(𝑋 ≤ (1 / 2), (𝐺‘((2 · 𝑋) − 1)), (𝐺‘((2 · 𝑋) − 1)))) |
37 | | ifid 4075 |
. . . . 5
⊢ if(𝑋 ≤ (1 / 2), (𝐺‘((2 · 𝑋) − 1)), (𝐺‘((2 · 𝑋) − 1))) = (𝐺‘((2 · 𝑋) − 1)) |
38 | 36, 37 | syl6eq 2660 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1))) = (𝐺‘((2 · 𝑋) − 1))) |
39 | 38 | expr 641 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ((1 / 2)[,]1)) → (𝑋 ≤ (1 / 2) → if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1))) = (𝐺‘((2 · 𝑋) − 1)))) |
40 | | iffalse 4045 |
. . 3
⊢ (¬
𝑋 ≤ (1 / 2) →
if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1))) = (𝐺‘((2 · 𝑋) − 1))) |
41 | 39, 40 | pm2.61d1 170 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ ((1 / 2)[,]1)) → if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1))) = (𝐺‘((2 · 𝑋) − 1))) |
42 | 13, 41 | eqtrd 2644 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑋) = (𝐺‘((2 · 𝑋) − 1))) |