| Step | Hyp | Ref
| Expression |
| 1 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥)) |
| 2 | 1 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑥 ≤ (1 / 4) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(2 · 𝑥))) |
| 3 | 2 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(2 · 𝑥))) |
| 4 | | 2cn 12341 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
| 5 | | elicc01 13506 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 ≤ 1)) |
| 6 | 5 | simp1bi 1146 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈
ℝ) |
| 7 | 6 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈
ℝ) |
| 8 | 7 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈
ℂ) |
| 9 | | mulcom 11241 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) = (𝑥 · 2)) |
| 10 | 4, 8, 9 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2
· 𝑥) = (𝑥 · 2)) |
| 11 | 5 | simp2bi 1147 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0[,]1) → 0 ≤
𝑥) |
| 12 | 11 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 0 ≤
𝑥) |
| 13 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 4)) |
| 14 | | 0re 11263 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
| 15 | | 4nn 12349 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
ℕ |
| 16 | | nnrecre 12308 |
. . . . . . . . . . . . . . . 16
⊢ (4 ∈
ℕ → (1 / 4) ∈ ℝ) |
| 17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (1 / 4)
∈ ℝ |
| 18 | 14, 17 | elicc2i 13453 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0[,](1 / 4)) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥 ∧ 𝑥 ≤ (1 / 4))) |
| 19 | 7, 12, 13, 18 | syl3anbrc 1344 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ (0[,](1 /
4))) |
| 20 | | 2rp 13039 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ+ |
| 21 | 4 | mul02i 11450 |
. . . . . . . . . . . . . 14
⊢ (0
· 2) = 0 |
| 22 | 17 | recni 11275 |
. . . . . . . . . . . . . . 15
⊢ (1 / 4)
∈ ℂ |
| 23 | 22 | 2timesi 12404 |
. . . . . . . . . . . . . . . 16
⊢ (2
· (1 / 4)) = ((1 / 4) + (1 / 4)) |
| 24 | | 2ne0 12370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
| 25 | | recdiv2 11980 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) →
((1 / 2) / 2) = (1 / (2 · 2))) |
| 26 | 4, 24, 4, 24, 25 | mp4an 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1 / 2)
/ 2) = (1 / (2 · 2)) |
| 27 | | 2t2e4 12430 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2
· 2) = 4 |
| 28 | 27 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 / (2
· 2)) = (1 / 4) |
| 29 | 26, 28 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 / 2)
/ 2) = (1 / 4) |
| 30 | 29, 29 | oveq12i 7443 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 / 2)
/ 2) + ((1 / 2) / 2)) = ((1 / 4) + (1 / 4)) |
| 31 | | halfcn 12481 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 / 2)
∈ ℂ |
| 32 | | 2halves 12494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 / 2)
∈ ℂ → (((1 / 2) / 2) + ((1 / 2) / 2)) = (1 /
2)) |
| 33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 / 2)
/ 2) + ((1 / 2) / 2)) = (1 / 2) |
| 34 | 30, 33 | eqtr3i 2767 |
. . . . . . . . . . . . . . . 16
⊢ ((1 / 4)
+ (1 / 4)) = (1 / 2) |
| 35 | 23, 34 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ (2
· (1 / 4)) = (1 / 2) |
| 36 | 4, 22, 35 | mulcomli 11270 |
. . . . . . . . . . . . . 14
⊢ ((1 / 4)
· 2) = (1 / 2) |
| 37 | 14, 17, 20, 21, 36 | iccdili 13531 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0[,](1 / 4)) →
(𝑥 · 2) ∈
(0[,](1 / 2))) |
| 38 | 19, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ (0[,](1 /
2))) |
| 39 | 10, 38 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2
· 𝑥) ∈ (0[,](1
/ 2))) |
| 40 | | pcoass.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
| 41 | | pcoass.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
| 42 | | pcoass.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐽)) |
| 43 | | pcoass.6 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺‘1) = (𝐻‘0)) |
| 44 | 41, 42, 43 | pcocn 25050 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺(*𝑝‘𝐽)𝐻) ∈ (II Cn 𝐽)) |
| 45 | 40, 44 | pcoval1 25046 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) →
((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥)))) |
| 46 | 40, 41 | pcoval1 25046 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) →
((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥)))) |
| 47 | 45, 46 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) →
((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
| 48 | 39, 47 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4))) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
| 49 | 48 | anassrs 467 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
| 50 | 3, 49 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
| 51 | 50 | adantlr 715 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
| 52 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝜑) |
| 53 | 6 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ℝ) |
| 54 | 53 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ) |
| 55 | | letric 11361 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ (1 / 4)
∈ ℝ) → (𝑥
≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥)) |
| 56 | 53, 17, 55 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥)) |
| 57 | 56 | orcanai 1005 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ≤ 𝑥) |
| 58 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 2)) |
| 59 | | halfre 12480 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℝ |
| 60 | 17, 59 | elicc2i 13453 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
↔ (𝑥 ∈ ℝ
∧ (1 / 4) ≤ 𝑥 ∧
𝑥 ≤ (1 /
2))) |
| 61 | 54, 57, 58, 60 | syl3anbrc 1344 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ((1 / 4)[,](1 / 2))) |
| 62 | 60 | simp1bi 1146 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ 𝑥 ∈
ℝ) |
| 63 | | readdcl 11238 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ (1 / 4)
∈ ℝ) → (𝑥 +
(1 / 4)) ∈ ℝ) |
| 64 | 62, 17, 63 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (𝑥 + (1 / 4)) ∈
ℝ) |
| 65 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (1 / 4) ∈ ℝ) |
| 66 | 60 | simp2bi 1147 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (1 / 4) ≤ 𝑥) |
| 67 | 65, 62, 65, 66 | leadd1dd 11877 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ ((1 / 4) + (1 / 4)) ≤ (𝑥 + (1 / 4))) |
| 68 | 34, 67 | eqbrtrrid 5179 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (1 / 2) ≤ (𝑥 + (1
/ 4))) |
| 69 | 59 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (1 / 2) ∈ ℝ) |
| 70 | 60 | simp3bi 1148 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ 𝑥 ≤ (1 /
2)) |
| 71 | | 2lt4 12441 |
. . . . . . . . . . . . . . . . 17
⊢ 2 <
4 |
| 72 | | 2re 12340 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
| 73 | | 4re 12350 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℝ |
| 74 | | 2pos 12369 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
2 |
| 75 | | 4pos 12373 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
4 |
| 76 | 72, 73, 74, 75 | ltrecii 12184 |
. . . . . . . . . . . . . . . . 17
⊢ (2 < 4
↔ (1 / 4) < (1 / 2)) |
| 77 | 71, 76 | mpbi 230 |
. . . . . . . . . . . . . . . 16
⊢ (1 / 4)
< (1 / 2) |
| 78 | 17, 59, 77 | ltleii 11384 |
. . . . . . . . . . . . . . 15
⊢ (1 / 4)
≤ (1 / 2) |
| 79 | 78 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (1 / 4) ≤ (1 / 2)) |
| 80 | 62, 65, 69, 69, 70, 79 | le2addd 11882 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (𝑥 + (1 / 4)) ≤
((1 / 2) + (1 / 2))) |
| 81 | | ax-1cn 11213 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
| 82 | | 2halves 12494 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℂ → ((1 / 2) + (1 / 2)) = 1) |
| 83 | 81, 82 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((1 / 2)
+ (1 / 2)) = 1 |
| 84 | 80, 83 | breqtrdi 5184 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (𝑥 + (1 / 4)) ≤
1) |
| 85 | | 1re 11261 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
| 86 | 59, 85 | elicc2i 13453 |
. . . . . . . . . . . 12
⊢ ((𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)
↔ ((𝑥 + (1 / 4))
∈ ℝ ∧ (1 / 2) ≤ (𝑥 + (1 / 4)) ∧ (𝑥 + (1 / 4)) ≤ 1)) |
| 87 | 64, 68, 84, 86 | syl3anbrc 1344 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (𝑥 + (1 / 4)) ∈
((1 / 2)[,]1)) |
| 88 | 61, 87 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝑥 + (1 / 4)) ∈ ((1 /
2)[,]1)) |
| 89 | | pcoass.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) |
| 90 | 41, 42 | pco0 25047 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺(*𝑝‘𝐽)𝐻)‘0) = (𝐺‘0)) |
| 91 | 89, 90 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘1) = ((𝐺(*𝑝‘𝐽)𝐻)‘0)) |
| 92 | 40, 44, 91 | pcoval2 25049 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)) →
((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1))) |
| 93 | 52, 88, 92 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1))) |
| 94 | 83 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ ((2
· (𝑥 + (1 / 4)))
− ((1 / 2) + (1 / 2))) = ((2 · (𝑥 + (1 / 4))) − 1) |
| 95 | | 2cnd 12344 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 2 ∈
ℂ) |
| 96 | 54 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ) |
| 97 | 22 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ∈
ℂ) |
| 98 | 95, 96, 97 | adddid 11285 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 ·
𝑥) + (2 · (1 /
4)))) |
| 99 | 35 | oveq2i 7442 |
. . . . . . . . . . . . . 14
⊢ ((2
· 𝑥) + (2 ·
(1 / 4))) = ((2 · 𝑥)
+ (1 / 2)) |
| 100 | 98, 99 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 ·
𝑥) + (1 /
2))) |
| 101 | 100 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − ((1 / 2) +
(1 / 2))) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 /
2)))) |
| 102 | 94, 101 | eqtr3id 2791 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = (((2
· 𝑥) + (1 / 2))
− ((1 / 2) + (1 / 2)))) |
| 103 | | remulcl 11240 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ ∧ 𝑥
∈ ℝ) → (2 · 𝑥) ∈ ℝ) |
| 104 | 72, 54, 103 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈
ℝ) |
| 105 | 104 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈
ℂ) |
| 106 | 31 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 2) ∈
ℂ) |
| 107 | 105, 106,
106 | pnpcan2d 11658 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (((2 · 𝑥) + (1 / 2)) − ((1 / 2) +
(1 / 2))) = ((2 · 𝑥)
− (1 / 2))) |
| 108 | 102, 107 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = ((2
· 𝑥) − (1 /
2))) |
| 109 | 108 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)) = ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2)))) |
| 110 | 4, 96, 9 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2)) |
| 111 | 81, 4, 24 | divcan1i 12011 |
. . . . . . . . . . . . . . 15
⊢ ((1 / 2)
· 2) = 1 |
| 112 | 17, 59, 20, 36, 111 | iccdili 13531 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (𝑥 · 2)
∈ ((1 / 2)[,]1)) |
| 113 | 61, 112 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ ((1 /
2)[,]1)) |
| 114 | 110, 113 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ((1 /
2)[,]1)) |
| 115 | 31 | subidi 11580 |
. . . . . . . . . . . . 13
⊢ ((1 / 2)
− (1 / 2)) = 0 |
| 116 | | 1mhlfehlf 12485 |
. . . . . . . . . . . . 13
⊢ (1
− (1 / 2)) = (1 / 2) |
| 117 | 59, 85, 59, 115, 116 | iccshftli 13529 |
. . . . . . . . . . . 12
⊢ ((2
· 𝑥) ∈ ((1 /
2)[,]1) → ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 /
2))) |
| 118 | 114, 117 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · 𝑥) − (1 / 2)) ∈
(0[,](1 / 2))) |
| 119 | 41, 42 | pcoval1 25046 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((2 · 𝑥) − (1 / 2)) ∈
(0[,](1 / 2))) → ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 /
2))))) |
| 120 | 52, 118, 119 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 /
2))))) |
| 121 | 95, 105, 106 | subdid 11719 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2
· 𝑥) − (1 /
2))) = ((2 · (2 · 𝑥)) − (2 · (1 /
2)))) |
| 122 | 4, 24 | recidi 11998 |
. . . . . . . . . . . . 13
⊢ (2
· (1 / 2)) = 1 |
| 123 | 122 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ ((2
· (2 · 𝑥))
− (2 · (1 / 2))) = ((2 · (2 · 𝑥)) − 1) |
| 124 | 121, 123 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2
· 𝑥) − (1 /
2))) = ((2 · (2 · 𝑥)) − 1)) |
| 125 | 124 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))) = (𝐺‘((2 · (2 ·
𝑥)) −
1))) |
| 126 | 120, 125 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘((2 · (2 · 𝑥)) − 1))) |
| 127 | 93, 109, 126 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = (𝐺‘((2 · (2 · 𝑥)) − 1))) |
| 128 | | iffalse 4534 |
. . . . . . . . . 10
⊢ (¬
𝑥 ≤ (1 / 4) →
if(𝑥 ≤ (1 / 4), (2
· 𝑥), (𝑥 + (1 / 4))) = (𝑥 + (1 / 4))) |
| 129 | 128 | fveq2d 6910 |
. . . . . . . . 9
⊢ (¬
𝑥 ≤ (1 / 4) →
((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4)))) |
| 130 | 129 | adantl 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4)))) |
| 131 | 40, 41, 89 | pcoval2 25049 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (2 · 𝑥) ∈ ((1 / 2)[,]1)) →
((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1))) |
| 132 | 52, 114, 131 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1))) |
| 133 | 127, 130,
132 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
| 134 | 51, 133 | pm2.61dan 813 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
| 135 | | iftrue 4531 |
. . . . . . . 8
⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) |
| 136 | 135 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑥 ≤ (1 / 2) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))) |
| 137 | 136 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))) |
| 138 | | iftrue 4531 |
. . . . . . 7
⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
| 139 | 138 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
| 140 | 134, 137,
139 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))) |
| 141 | | elii2 24965 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 ≤ (1 / 2)) →
𝑥 ∈ ((1 /
2)[,]1)) |
| 142 | | halfge0 12483 |
. . . . . . . . . . . . . 14
⊢ 0 ≤ (1
/ 2) |
| 143 | | halflt1 12484 |
. . . . . . . . . . . . . . 15
⊢ (1 / 2)
< 1 |
| 144 | 59, 85, 143 | ltleii 11384 |
. . . . . . . . . . . . . 14
⊢ (1 / 2)
≤ 1 |
| 145 | | elicc01 13506 |
. . . . . . . . . . . . . 14
⊢ ((1 / 2)
∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 /
2) ≤ 1)) |
| 146 | 59, 142, 144, 145 | mpbir3an 1342 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ (0[,]1) |
| 147 | | 1elunit 13510 |
. . . . . . . . . . . . 13
⊢ 1 ∈
(0[,]1) |
| 148 | | iccss2 13458 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → ((1 / 2)[,]1) ⊆
(0[,]1)) |
| 149 | 146, 147,
148 | mp2an 692 |
. . . . . . . . . . . 12
⊢ ((1 /
2)[,]1) ⊆ (0[,]1) |
| 150 | 149 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
𝑥 ∈
(0[,]1)) |
| 151 | 4, 24 | div0i 12001 |
. . . . . . . . . . . 12
⊢ (0 / 2) =
0 |
| 152 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (1 / 2) =
(1 / 2) |
| 153 | 14, 85, 20, 151, 152 | icccntri 13533 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]1) → (𝑥 / 2) ∈ (0[,](1 /
2))) |
| 154 | 31 | addlidi 11449 |
. . . . . . . . . . . 12
⊢ (0 + (1 /
2)) = (1 / 2) |
| 155 | 14, 59, 59, 154, 83 | iccshftri 13527 |
. . . . . . . . . . 11
⊢ ((𝑥 / 2) ∈ (0[,](1 / 2))
→ ((𝑥 / 2) + (1 / 2))
∈ ((1 / 2)[,]1)) |
| 156 | 150, 153,
155 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
((𝑥 / 2) + (1 / 2)) ∈
((1 / 2)[,]1)) |
| 157 | 40, 44, 91 | pcoval2 25049 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1)) →
((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) −
1))) |
| 158 | 156, 157 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) −
1))) |
| 159 | 59, 85 | elicc2i 13453 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 2)[,]1) ↔
(𝑥 ∈ ℝ ∧ (1
/ 2) ≤ 𝑥 ∧ 𝑥 ≤ 1)) |
| 160 | 159 | simp1bi 1146 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
𝑥 ∈
ℝ) |
| 161 | 160 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
𝑥 ∈
ℂ) |
| 162 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 2)[,]1) → 1
∈ ℂ) |
| 163 | | 2cnd 12344 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2
∈ ℂ) |
| 164 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2
≠ 0) |
| 165 | 161, 162,
163, 164 | divdird 12081 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
((𝑥 + 1) / 2) = ((𝑥 / 2) + (1 /
2))) |
| 166 | 165 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2
· ((𝑥 + 1) / 2)) =
(2 · ((𝑥 / 2) + (1 /
2)))) |
| 167 | | peano2cn 11433 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (𝑥 + 1) ∈
ℂ) |
| 168 | 161, 167 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
(𝑥 + 1) ∈
ℂ) |
| 169 | 168, 163,
164 | divcan2d 12045 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2
· ((𝑥 + 1) / 2)) =
(𝑥 + 1)) |
| 170 | 166, 169 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2
· ((𝑥 / 2) + (1 /
2))) = (𝑥 +
1)) |
| 171 | 161, 162,
170 | mvrraddd 11675 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((2
· ((𝑥 / 2) + (1 /
2))) − 1) = 𝑥) |
| 172 | 171 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
((𝐺(*𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(*𝑝‘𝐽)𝐻)‘𝑥)) |
| 173 | 172 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(*𝑝‘𝐽)𝐻)‘𝑥)) |
| 174 | 41, 42, 43 | pcoval2 25049 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝‘𝐽)𝐻)‘𝑥) = (𝐻‘((2 · 𝑥) − 1))) |
| 175 | 158, 173,
174 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1))) |
| 176 | 141, 175 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2))) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1))) |
| 177 | 176 | anassrs 467 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1))) |
| 178 | | iffalse 4534 |
. . . . . . . 8
⊢ (¬
𝑥 ≤ (1 / 2) →
if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2))) |
| 179 | 178 | fveq2d 6910 |
. . . . . . 7
⊢ (¬
𝑥 ≤ (1 / 2) →
((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2)))) |
| 180 | 179 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2)))) |
| 181 | | iffalse 4534 |
. . . . . . 7
⊢ (¬
𝑥 ≤ (1 / 2) →
if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1))) |
| 182 | 181 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1))) |
| 183 | 177, 180,
182 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))) |
| 184 | 140, 183 | pm2.61dan 813 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))) |
| 185 | 184 | mpteq2dva 5242 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))) |
| 186 | | pcoass.7 |
. . . . . . 7
⊢ 𝑃 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) |
| 187 | | iitopon 24905 |
. . . . . . . . 9
⊢ II ∈
(TopOn‘(0[,]1)) |
| 188 | 187 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
| 189 | 188 | cnmptid 23669 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II)) |
| 190 | | 0elunit 13509 |
. . . . . . . . . 10
⊢ 0 ∈
(0[,]1) |
| 191 | 190 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
(0[,]1)) |
| 192 | 188, 188,
191 | cnmptc 23670 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn
II)) |
| 193 | | eqid 2737 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 194 | | eqid 2737 |
. . . . . . . . 9
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) =
((topGen‘ran (,)) ↾t (0[,](1 / 2))) |
| 195 | | eqid 2737 |
. . . . . . . . 9
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) =
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) |
| 196 | | dfii2 24908 |
. . . . . . . . 9
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
| 197 | | 0red 11264 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
| 198 | | 1red 11262 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ) |
| 199 | 146 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 2) ∈
(0[,]1)) |
| 200 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2)) |
| 201 | 200 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 2) + (1 /
4))) |
| 202 | 31, 22 | addcomi 11452 |
. . . . . . . . . . 11
⊢ ((1 / 2)
+ (1 / 4)) = ((1 / 4) + (1 / 2)) |
| 203 | 201, 202 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 /
2))) |
| 204 | 17, 59 | ltnlei 11382 |
. . . . . . . . . . . . 13
⊢ ((1 / 4)
< (1 / 2) ↔ ¬ (1 / 2) ≤ (1 / 4)) |
| 205 | 77, 204 | mpbi 230 |
. . . . . . . . . . . 12
⊢ ¬ (1
/ 2) ≤ (1 / 4) |
| 206 | 200 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 ≤ (1 / 4) ↔ (1 / 2) ≤ (1 /
4))) |
| 207 | 205, 206 | mtbiri 327 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ¬ 𝑦 ≤ (1 / 4)) |
| 208 | 207 | iffalsed 4536 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = (𝑦 + (1 / 4))) |
| 209 | 200 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = ((1 / 2) / 2)) |
| 210 | 209, 29 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = (1 / 4)) |
| 211 | 210 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((𝑦 / 2) + (1 / 2)) = ((1 / 4) + (1 /
2))) |
| 212 | 203, 208,
211 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = ((𝑦 / 2) + (1 / 2))) |
| 213 | | eqid 2737 |
. . . . . . . . . 10
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 4))) =
((topGen‘ran (,)) ↾t (0[,](1 / 4))) |
| 214 | | eqid 2737 |
. . . . . . . . . 10
⊢
((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) =
((topGen‘ran (,)) ↾t ((1 / 4)[,](1 /
2))) |
| 215 | 59 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
| 216 | 73, 75 | recgt0ii 12174 |
. . . . . . . . . . . . 13
⊢ 0 < (1
/ 4) |
| 217 | 14, 17, 216 | ltleii 11384 |
. . . . . . . . . . . 12
⊢ 0 ≤ (1
/ 4) |
| 218 | 14, 59 | elicc2i 13453 |
. . . . . . . . . . . 12
⊢ ((1 / 4)
∈ (0[,](1 / 2)) ↔ ((1 / 4) ∈ ℝ ∧ 0 ≤ (1 / 4) ∧
(1 / 4) ≤ (1 / 2))) |
| 219 | 17, 217, 78, 218 | mpbir3an 1342 |
. . . . . . . . . . 11
⊢ (1 / 4)
∈ (0[,](1 / 2)) |
| 220 | 219 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / 4) ∈ (0[,](1 /
2))) |
| 221 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 4)) |
| 222 | 221 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 /
4))) |
| 223 | 221 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 /
4))) |
| 224 | 23, 222, 223 | 3eqtr4a 2803 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (𝑦 + (1 / 4))) |
| 225 | | retopon 24784 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
| 226 | | 0xr 11308 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ* |
| 227 | 59 | rexri 11319 |
. . . . . . . . . . . . . . . 16
⊢ (1 / 2)
∈ ℝ* |
| 228 | | lbicc2 13504 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ* ∧ (1 / 2) ∈ ℝ* ∧ 0
≤ (1 / 2)) → 0 ∈ (0[,](1 / 2))) |
| 229 | 226, 227,
142, 228 | mp3an 1463 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
(0[,](1 / 2)) |
| 230 | | iccss2 13458 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ (0[,](1 / 2)) ∧ (1 / 4) ∈ (0[,](1 / 2))) → (0[,](1 / 4))
⊆ (0[,](1 / 2))) |
| 231 | 229, 219,
230 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (0[,](1 /
4)) ⊆ (0[,](1 / 2)) |
| 232 | | iccssre 13469 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆
ℝ) |
| 233 | 14, 59, 232 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (0[,](1 /
2)) ⊆ ℝ |
| 234 | 231, 233 | sstri 3993 |
. . . . . . . . . . . . 13
⊢ (0[,](1 /
4)) ⊆ ℝ |
| 235 | | resttopon 23169 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
4)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 4))) ∈ (TopOn‘(0[,](1 / 4)))) |
| 236 | 225, 234,
235 | mp2an 692 |
. . . . . . . . . . . 12
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 4))) ∈
(TopOn‘(0[,](1 / 4))) |
| 237 | 236 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ((topGen‘ran (,))
↾t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 /
4)))) |
| 238 | 237, 188 | cnmpt1st 23676 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 4))) ×t II) Cn
((topGen‘ran (,)) ↾t (0[,](1 / 4))))) |
| 239 | | retop 24782 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ Top |
| 240 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢ (0[,](1 /
2)) ∈ V |
| 241 | | restabs 23173 |
. . . . . . . . . . . . . 14
⊢
(((topGen‘ran (,)) ∈ Top ∧ (0[,](1 / 4)) ⊆ (0[,](1
/ 2)) ∧ (0[,](1 / 2)) ∈ V) → (((topGen‘ran (,))
↾t (0[,](1 / 2))) ↾t (0[,](1 / 4))) =
((topGen‘ran (,)) ↾t (0[,](1 / 4)))) |
| 242 | 239, 231,
240, 241 | mp3an 1463 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ↾t (0[,](1 / 2)))
↾t (0[,](1 / 4))) = ((topGen‘ran (,))
↾t (0[,](1 / 4))) |
| 243 | 242 | eqcomi 2746 |
. . . . . . . . . . . 12
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 4))) =
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) ↾t
(0[,](1 / 4))) |
| 244 | | resttopon 23169 |
. . . . . . . . . . . . . 14
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 2))) ∈ (TopOn‘(0[,](1 / 2)))) |
| 245 | 225, 233,
244 | mp2an 692 |
. . . . . . . . . . . . 13
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈
(TopOn‘(0[,](1 / 2))) |
| 246 | 245 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((topGen‘ran (,))
↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 /
2)))) |
| 247 | 231 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0[,](1 / 4)) ⊆
(0[,](1 / 2))) |
| 248 | 194 | iihalf1cn 24959 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2
· 𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II) |
| 249 | 248 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)) ↦ (2 ·
𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II)) |
| 250 | 243, 246,
247, 249 | cnmpt1res 23684 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 4)) ↦ (2 ·
𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 4))) Cn
II)) |
| 251 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦)) |
| 252 | 237, 188,
238, 237, 250, 251 | cnmpt21 23679 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 4))) ×t II) Cn
II)) |
| 253 | | iccssre 13469 |
. . . . . . . . . . . . . 14
⊢ (((1 / 4)
∈ ℝ ∧ (1 / 2) ∈ ℝ) → ((1 / 4)[,](1 / 2)) ⊆
ℝ) |
| 254 | 17, 59, 253 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ ((1 /
4)[,](1 / 2)) ⊆ ℝ |
| 255 | | resttopon 23169 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
4)[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,))
↾t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 /
2)))) |
| 256 | 225, 254,
255 | mp2an 692 |
. . . . . . . . . . . 12
⊢
((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ∈
(TopOn‘((1 / 4)[,](1 / 2))) |
| 257 | 256 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 /
2)))) |
| 258 | 257, 188 | cnmpt1st 23676 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ ((1 / 4)[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran
(,)) ↾t ((1 / 4)[,](1 / 2))) ×t II) Cn
((topGen‘ran (,)) ↾t ((1 / 4)[,](1 /
2))))) |
| 259 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 260 | 254 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 / 4)[,](1 / 2))
⊆ ℝ) |
| 261 | | unitssre 13539 |
. . . . . . . . . . . . 13
⊢ (0[,]1)
⊆ ℝ |
| 262 | 261 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0[,]1) ⊆
ℝ) |
| 263 | 149, 87 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (𝑥 + (1 / 4)) ∈
(0[,]1)) |
| 264 | 263 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 4)[,](1 / 2))) → (𝑥 + (1 / 4)) ∈
(0[,]1)) |
| 265 | 259 | cnfldtopon 24803 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 266 | 265 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
| 267 | 266 | cnmptid 23669 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝑥) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
| 268 | 17 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 / 4) ∈
ℝ) |
| 269 | 268 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 / 4) ∈
ℂ) |
| 270 | 266, 266,
269 | cnmptc 23670 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 4)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
| 271 | 259 | addcn 24887 |
. . . . . . . . . . . . . 14
⊢ + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
| 272 | 271 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
| 273 | 266, 267,
270, 272 | cnmpt12f 23674 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 + (1 / 4))) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
| 274 | 259, 214,
196, 260, 262, 264, 273 | cnmptre 24954 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↦ (𝑥 + (1 / 4))) ∈
(((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) Cn
II)) |
| 275 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 + (1 / 4)) = (𝑦 + (1 / 4))) |
| 276 | 257, 188,
258, 257, 274, 275 | cnmpt21 23679 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ((1 / 4)[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ (𝑦 + (1 / 4))) ∈
((((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2)))
×t II) Cn II)) |
| 277 | 193, 213,
214, 194, 197, 215, 220, 188, 224, 252, 276 | cnmpopc 24955 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 2))) ×t II) Cn
II)) |
| 278 | | iccssre 13469 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆
ℝ) |
| 279 | 59, 85, 278 | mp2an 692 |
. . . . . . . . . . . 12
⊢ ((1 /
2)[,]1) ⊆ ℝ |
| 280 | | resttopon 23169 |
. . . . . . . . . . . 12
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1
/ 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))) |
| 281 | 225, 279,
280 | mp2an 692 |
. . . . . . . . . . 11
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈
(TopOn‘((1 / 2)[,]1)) |
| 282 | 281 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 /
2)[,]1))) |
| 283 | 282, 188 | cnmpt1st 23676 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)))) |
| 284 | 279 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1 / 2)[,]1) ⊆
ℝ) |
| 285 | 149, 156 | sselid 3981 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
((𝑥 / 2) + (1 / 2)) ∈
(0[,]1)) |
| 286 | 285 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝑥 / 2) + (1 / 2)) ∈
(0[,]1)) |
| 287 | 259 | divccn 24897 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
| 288 | 4, 24, 287 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
| 289 | 288 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
| 290 | 31 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / 2) ∈
ℂ) |
| 291 | 266, 266,
290 | cnmptc 23670 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 2)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
| 292 | 266, 289,
291, 272 | cnmpt12f 23674 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥 / 2) + (1 / 2))) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
| 293 | 259, 195,
196, 284, 262, 286, 292 | cnmptre 24954 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((𝑥 / 2) + (1 / 2))) ∈
(((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II)) |
| 294 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2)) |
| 295 | 294 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 / 2) + (1 / 2)) = ((𝑦 / 2) + (1 / 2))) |
| 296 | 282, 188,
283, 282, 293, 295 | cnmpt21 23679 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ ((𝑦 / 2) + (1 / 2))) ∈ ((((topGen‘ran
(,)) ↾t ((1 / 2)[,]1)) ×t II) Cn
II)) |
| 297 | 193, 194,
195, 196, 197, 198, 199, 188, 212, 277, 296 | cnmpopc 24955 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) ∈ ((II
×t II) Cn II)) |
| 298 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2))) |
| 299 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 4) ↔ 𝑦 ≤ (1 / 4))) |
| 300 | 299, 251,
275 | ifbieq12d 4554 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) |
| 301 | 298, 300,
295 | ifbieq12d 4554 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) |
| 302 | 301 | equcoms 2019 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) |
| 303 | 302 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑥 ∧ 𝑧 = 0) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) |
| 304 | 303 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝑦 = 𝑥 ∧ 𝑧 = 0) → if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) |
| 305 | 188, 189,
192, 188, 188, 297, 304 | cnmpt12 23675 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) ∈ (II Cn
II)) |
| 306 | 186, 305 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ (II Cn II)) |
| 307 | | iiuni 24907 |
. . . . . . 7
⊢ (0[,]1) =
∪ II |
| 308 | 307, 307 | cnf 23254 |
. . . . . 6
⊢ (𝑃 ∈ (II Cn II) → 𝑃:(0[,]1)⟶(0[,]1)) |
| 309 | 306, 308 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃:(0[,]1)⟶(0[,]1)) |
| 310 | 186 | fmpt 7130 |
. . . . 5
⊢
(∀𝑥 ∈
(0[,]1)if(𝑥 ≤ (1 / 2),
if(𝑥 ≤ (1 / 4), (2
· 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈ (0[,]1)
↔ 𝑃:(0[,]1)⟶(0[,]1)) |
| 311 | 309, 310 | sylibr 234 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈
(0[,]1)) |
| 312 | 186 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑃 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))) |
| 313 | 40, 44, 91 | pcocn 25050 |
. . . . . 6
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽)) |
| 314 | | eqid 2737 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 315 | 307, 314 | cnf 23254 |
. . . . . 6
⊢ ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽) → (𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽) |
| 316 | 313, 315 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽) |
| 317 | 316 | feqmptd 6977 |
. . . 4
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) = (𝑦 ∈ (0[,]1) ↦ ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘𝑦))) |
| 318 | | fveq2 6906 |
. . . 4
⊢ (𝑦 = if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘𝑦) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))) |
| 319 | 311, 312,
317, 318 | fmptcof 7150 |
. . 3
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) ∘ 𝑃) = (𝑥 ∈ (0[,]1) ↦ ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))))) |
| 320 | 40, 41, 89 | pcocn 25050 |
. . . 4
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽)) |
| 321 | 320, 42 | pcoval 25044 |
. . 3
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)(*𝑝‘𝐽)𝐻) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))) |
| 322 | 185, 319,
321 | 3eqtr4rd 2788 |
. 2
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)(*𝑝‘𝐽)𝐻) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) ∘ 𝑃)) |
| 323 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = 0 → 𝑥 = 0) |
| 324 | 323, 142 | eqbrtrdi 5182 |
. . . . . . 7
⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 2)) |
| 325 | 324 | iftrued 4533 |
. . . . . 6
⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) |
| 326 | 323, 217 | eqbrtrdi 5182 |
. . . . . . 7
⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 4)) |
| 327 | 326 | iftrued 4533 |
. . . . . 6
⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥)) |
| 328 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑥 = 0 → (2 · 𝑥) = (2 ·
0)) |
| 329 | | 2t0e0 12435 |
. . . . . . 7
⊢ (2
· 0) = 0 |
| 330 | 328, 329 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑥 = 0 → (2 · 𝑥) = 0) |
| 331 | 325, 327,
330 | 3eqtrd 2781 |
. . . . 5
⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 0) |
| 332 | | c0ex 11255 |
. . . . 5
⊢ 0 ∈
V |
| 333 | 331, 186,
332 | fvmpt 7016 |
. . . 4
⊢ (0 ∈
(0[,]1) → (𝑃‘0)
= 0) |
| 334 | 191, 333 | syl 17 |
. . 3
⊢ (𝜑 → (𝑃‘0) = 0) |
| 335 | 147 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 ∈
(0[,]1)) |
| 336 | 59, 85 | ltnlei 11382 |
. . . . . . . . 9
⊢ ((1 / 2)
< 1 ↔ ¬ 1 ≤ (1 / 2)) |
| 337 | 143, 336 | mpbi 230 |
. . . . . . . 8
⊢ ¬ 1
≤ (1 / 2) |
| 338 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 /
2))) |
| 339 | 337, 338 | mtbiri 327 |
. . . . . . 7
⊢ (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2)) |
| 340 | 339 | iffalsed 4536 |
. . . . . 6
⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2))) |
| 341 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝑥 / 2) = (1 / 2)) |
| 342 | 341 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = ((1 / 2) + (1 /
2))) |
| 343 | 342, 83 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = 1) |
| 344 | 340, 343 | eqtrd 2777 |
. . . . 5
⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 1) |
| 345 | | 1ex 11257 |
. . . . 5
⊢ 1 ∈
V |
| 346 | 344, 186,
345 | fvmpt 7016 |
. . . 4
⊢ (1 ∈
(0[,]1) → (𝑃‘1)
= 1) |
| 347 | 335, 346 | syl 17 |
. . 3
⊢ (𝜑 → (𝑃‘1) = 1) |
| 348 | 313, 306,
334, 347 | reparpht 25031 |
. 2
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) ∘ 𝑃)( ≃ph‘𝐽)(𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))) |
| 349 | 322, 348 | eqbrtrd 5165 |
1
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)(𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))) |