Proof of Theorem pcoval2
Step | Hyp | Ref
| Expression |
1 | | 0re 10040 |
. . . . 5
⊢ 0 ∈
ℝ |
2 | | 1re 10039 |
. . . . 5
⊢ 1 ∈
ℝ |
3 | | halfre 11246 |
. . . . . 6
⊢ (1 / 2)
∈ ℝ |
4 | | halfgt0 11248 |
. . . . . 6
⊢ 0 < (1
/ 2) |
5 | 1, 3, 4 | ltleii 10160 |
. . . . 5
⊢ 0 ≤ (1
/ 2) |
6 | | 1le1 10655 |
. . . . 5
⊢ 1 ≤
1 |
7 | | iccss 12241 |
. . . . 5
⊢ (((0
∈ ℝ ∧ 1 ∈ ℝ) ∧ (0 ≤ (1 / 2) ∧ 1 ≤ 1))
→ ((1 / 2)[,]1) ⊆ (0[,]1)) |
8 | 1, 2, 5, 6, 7 | mp4an 709 |
. . . 4
⊢ ((1 /
2)[,]1) ⊆ (0[,]1) |
9 | 8 | sseli 3599 |
. . 3
⊢ (𝑋 ∈ ((1 / 2)[,]1) →
𝑋 ∈
(0[,]1)) |
10 | | pcoval.2 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
11 | | pcoval.3 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
12 | 10, 11 | pcovalg 22812 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑋) = if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1)))) |
13 | 9, 12 | sylan2 491 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑋) = if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1)))) |
14 | | pcoval2.4 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) |
15 | 14 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (𝐹‘1) = (𝐺‘0)) |
16 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → 𝑋 ≤ (1 / 2)) |
17 | 3, 2 | elicc2i 12239 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ((1 / 2)[,]1) ↔
(𝑋 ∈ ℝ ∧ (1
/ 2) ≤ 𝑋 ∧ 𝑋 ≤ 1)) |
18 | 17 | simp2bi 1077 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ((1 / 2)[,]1) → (1
/ 2) ≤ 𝑋) |
19 | 18 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (1 / 2)
≤ 𝑋) |
20 | 17 | simp1bi 1076 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ((1 / 2)[,]1) →
𝑋 ∈
ℝ) |
21 | 20 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → 𝑋 ∈
ℝ) |
22 | | letri3 10123 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℝ ∧ (1 / 2)
∈ ℝ) → (𝑋 =
(1 / 2) ↔ (𝑋 ≤ (1 /
2) ∧ (1 / 2) ≤ 𝑋))) |
23 | 21, 3, 22 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (𝑋 = (1 / 2) ↔ (𝑋 ≤ (1 / 2) ∧ (1 / 2) ≤
𝑋))) |
24 | 16, 19, 23 | mpbir2and 957 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → 𝑋 = (1 / 2)) |
25 | 24 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (2
· 𝑋) = (2 ·
(1 / 2))) |
26 | | 2cn 11091 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
27 | | 2ne0 11113 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
28 | 26, 27 | recidi 10756 |
. . . . . . . . 9
⊢ (2
· (1 / 2)) = 1 |
29 | 25, 28 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (2
· 𝑋) =
1) |
30 | 29 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (𝐹‘(2 · 𝑋)) = (𝐹‘1)) |
31 | 29 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → ((2
· 𝑋) − 1) = (1
− 1)) |
32 | | 1m1e0 11089 |
. . . . . . . . 9
⊢ (1
− 1) = 0 |
33 | 31, 32 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → ((2
· 𝑋) − 1) =
0) |
34 | 33 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (𝐺‘((2 · 𝑋) − 1)) = (𝐺‘0)) |
35 | 15, 30, 34 | 3eqtr4d 2666 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → (𝐹‘(2 · 𝑋)) = (𝐺‘((2 · 𝑋) − 1))) |
36 | 35 | ifeq1d 4104 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1))) = if(𝑋 ≤ (1 / 2), (𝐺‘((2 · 𝑋) − 1)), (𝐺‘((2 · 𝑋) − 1)))) |
37 | | ifid 4125 |
. . . . 5
⊢ if(𝑋 ≤ (1 / 2), (𝐺‘((2 · 𝑋) − 1)), (𝐺‘((2 · 𝑋) − 1))) = (𝐺‘((2 · 𝑋) − 1)) |
38 | 36, 37 | syl6eq 2672 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ ((1 / 2)[,]1) ∧ 𝑋 ≤ (1 / 2))) → if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1))) = (𝐺‘((2 · 𝑋) − 1))) |
39 | 38 | expr 643 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ((1 / 2)[,]1)) → (𝑋 ≤ (1 / 2) → if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1))) = (𝐺‘((2 · 𝑋) − 1)))) |
40 | | iffalse 4095 |
. . 3
⊢ (¬
𝑋 ≤ (1 / 2) →
if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1))) = (𝐺‘((2 · 𝑋) − 1))) |
41 | 39, 40 | pm2.61d1 171 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ ((1 / 2)[,]1)) → if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1))) = (𝐺‘((2 · 𝑋) − 1))) |
42 | 13, 41 | eqtrd 2656 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑋) = (𝐺‘((2 · 𝑋) − 1))) |