Step | Hyp | Ref
| Expression |
1 | | iftrue 4092 |
. . . . . . . . . . 11
⊢ (𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥)) |
2 | 1 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 ≤ (1 / 4) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(2 · 𝑥))) |
3 | 2 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(2 · 𝑥))) |
4 | | 2cn 11091 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
5 | | 0re 10040 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ |
6 | | 1re 10039 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ |
7 | 5, 6 | elicc2i 12239 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 ≤ 1)) |
8 | 7 | simp1bi 1076 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈
ℝ) |
9 | 8 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈
ℝ) |
10 | 9 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈
ℂ) |
11 | | mulcom 10022 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) = (𝑥 · 2)) |
12 | 4, 10, 11 | sylancr 695 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2
· 𝑥) = (𝑥 · 2)) |
13 | 7 | simp2bi 1077 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0[,]1) → 0 ≤
𝑥) |
14 | 13 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 0 ≤
𝑥) |
15 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 4)) |
16 | | 4nn 11187 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
ℕ |
17 | | nnrecre 11057 |
. . . . . . . . . . . . . . . 16
⊢ (4 ∈
ℕ → (1 / 4) ∈ ℝ) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (1 / 4)
∈ ℝ |
19 | 5, 18 | elicc2i 12239 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0[,](1 / 4)) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥 ∧ 𝑥 ≤ (1 / 4))) |
20 | 9, 14, 15, 19 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ (0[,](1 /
4))) |
21 | | 2rp 11837 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ+ |
22 | 4 | mul02i 10225 |
. . . . . . . . . . . . . 14
⊢ (0
· 2) = 0 |
23 | 18 | recni 10052 |
. . . . . . . . . . . . . . 15
⊢ (1 / 4)
∈ ℂ |
24 | 23 | 2timesi 11147 |
. . . . . . . . . . . . . . . 16
⊢ (2
· (1 / 4)) = ((1 / 4) + (1 / 4)) |
25 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
26 | | recdiv2 10738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) →
((1 / 2) / 2) = (1 / (2 · 2))) |
27 | 4, 25, 4, 25, 26 | mp4an 709 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1 / 2)
/ 2) = (1 / (2 · 2)) |
28 | | 2t2e4 11177 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2
· 2) = 4 |
29 | 28 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 / (2
· 2)) = (1 / 4) |
30 | 27, 29 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 / 2)
/ 2) = (1 / 4) |
31 | 30, 30 | oveq12i 6662 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 / 2)
/ 2) + ((1 / 2) / 2)) = ((1 / 4) + (1 / 4)) |
32 | | halfcn 11247 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 / 2)
∈ ℂ |
33 | | 2halves 11260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 / 2)
∈ ℂ → (((1 / 2) / 2) + ((1 / 2) / 2)) = (1 /
2)) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 / 2)
/ 2) + ((1 / 2) / 2)) = (1 / 2) |
35 | 31, 34 | eqtr3i 2646 |
. . . . . . . . . . . . . . . 16
⊢ ((1 / 4)
+ (1 / 4)) = (1 / 2) |
36 | 24, 35 | eqtri 2644 |
. . . . . . . . . . . . . . 15
⊢ (2
· (1 / 4)) = (1 / 2) |
37 | 4, 23, 36 | mulcomli 10047 |
. . . . . . . . . . . . . 14
⊢ ((1 / 4)
· 2) = (1 / 2) |
38 | 5, 18, 21, 22, 37 | iccdili 12311 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0[,](1 / 4)) →
(𝑥 · 2) ∈
(0[,](1 / 2))) |
39 | 20, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ (0[,](1 /
2))) |
40 | 12, 39 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2
· 𝑥) ∈ (0[,](1
/ 2))) |
41 | | pcoass.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
42 | | pcoass.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
43 | | pcoass.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐽)) |
44 | | pcoass.6 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺‘1) = (𝐻‘0)) |
45 | 42, 43, 44 | pcocn 22817 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺(*𝑝‘𝐽)𝐻) ∈ (II Cn 𝐽)) |
46 | 41, 45 | pcoval1 22813 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) →
((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥)))) |
47 | 41, 42 | pcoval1 22813 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) →
((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥)))) |
48 | 46, 47 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) →
((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
49 | 40, 48 | sylan2 491 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4))) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
50 | 49 | anassrs 680 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
51 | 3, 50 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
52 | 51 | adantlr 751 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
53 | | simplll 798 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝜑) |
54 | 8 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ℝ) |
55 | 54 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ) |
56 | | letric 10137 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ (1 / 4)
∈ ℝ) → (𝑥
≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥)) |
57 | 54, 18, 56 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥)) |
58 | 57 | orcanai 952 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ≤ 𝑥) |
59 | | simplr 792 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 2)) |
60 | | halfre 11246 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℝ |
61 | 18, 60 | elicc2i 12239 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
↔ (𝑥 ∈ ℝ
∧ (1 / 4) ≤ 𝑥 ∧
𝑥 ≤ (1 /
2))) |
62 | 55, 58, 59, 61 | syl3anbrc 1246 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ((1 / 4)[,](1 / 2))) |
63 | 61 | simp1bi 1076 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ 𝑥 ∈
ℝ) |
64 | | readdcl 10019 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ (1 / 4)
∈ ℝ) → (𝑥 +
(1 / 4)) ∈ ℝ) |
65 | 63, 18, 64 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (𝑥 + (1 / 4)) ∈
ℝ) |
66 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (1 / 4) ∈ ℝ) |
67 | 61 | simp2bi 1077 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (1 / 4) ≤ 𝑥) |
68 | 66, 63, 66, 67 | leadd1dd 10641 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ ((1 / 4) + (1 / 4)) ≤ (𝑥 + (1 / 4))) |
69 | 35, 68 | syl5eqbrr 4689 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (1 / 2) ≤ (𝑥 + (1
/ 4))) |
70 | 60 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (1 / 2) ∈ ℝ) |
71 | 61 | simp3bi 1078 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ 𝑥 ≤ (1 /
2)) |
72 | | 2lt4 11198 |
. . . . . . . . . . . . . . . . 17
⊢ 2 <
4 |
73 | | 2re 11090 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
74 | | 4re 11097 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℝ |
75 | | 2pos 11112 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
2 |
76 | | 4pos 11116 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
4 |
77 | 73, 74, 75, 76 | ltrecii 10940 |
. . . . . . . . . . . . . . . . 17
⊢ (2 < 4
↔ (1 / 4) < (1 / 2)) |
78 | 72, 77 | mpbi 220 |
. . . . . . . . . . . . . . . 16
⊢ (1 / 4)
< (1 / 2) |
79 | 18, 60, 78 | ltleii 10160 |
. . . . . . . . . . . . . . 15
⊢ (1 / 4)
≤ (1 / 2) |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (1 / 4) ≤ (1 / 2)) |
81 | 63, 66, 70, 70, 71, 80 | le2addd 10646 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (𝑥 + (1 / 4)) ≤
((1 / 2) + (1 / 2))) |
82 | | ax-1cn 9994 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
83 | | 2halves 11260 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℂ → ((1 / 2) + (1 / 2)) = 1) |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((1 / 2)
+ (1 / 2)) = 1 |
85 | 81, 84 | syl6breq 4694 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (𝑥 + (1 / 4)) ≤
1) |
86 | 60, 6 | elicc2i 12239 |
. . . . . . . . . . . 12
⊢ ((𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)
↔ ((𝑥 + (1 / 4))
∈ ℝ ∧ (1 / 2) ≤ (𝑥 + (1 / 4)) ∧ (𝑥 + (1 / 4)) ≤ 1)) |
87 | 65, 69, 85, 86 | syl3anbrc 1246 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (𝑥 + (1 / 4)) ∈
((1 / 2)[,]1)) |
88 | 62, 87 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝑥 + (1 / 4)) ∈ ((1 /
2)[,]1)) |
89 | | pcoass.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) |
90 | 42, 43 | pco0 22814 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺(*𝑝‘𝐽)𝐻)‘0) = (𝐺‘0)) |
91 | 89, 90 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘1) = ((𝐺(*𝑝‘𝐽)𝐻)‘0)) |
92 | 41, 45, 91 | pcoval2 22816 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)) →
((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1))) |
93 | 53, 88, 92 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1))) |
94 | 84 | oveq2i 6661 |
. . . . . . . . . . . 12
⊢ ((2
· (𝑥 + (1 / 4)))
− ((1 / 2) + (1 / 2))) = ((2 · (𝑥 + (1 / 4))) − 1) |
95 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 2 ∈
ℂ) |
96 | 55 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ) |
97 | 23 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ∈
ℂ) |
98 | 95, 96, 97 | adddid 10064 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 ·
𝑥) + (2 · (1 /
4)))) |
99 | 36 | oveq2i 6661 |
. . . . . . . . . . . . . 14
⊢ ((2
· 𝑥) + (2 ·
(1 / 4))) = ((2 · 𝑥)
+ (1 / 2)) |
100 | 98, 99 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 ·
𝑥) + (1 /
2))) |
101 | 100 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − ((1 / 2) +
(1 / 2))) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 /
2)))) |
102 | 94, 101 | syl5eqr 2670 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = (((2
· 𝑥) + (1 / 2))
− ((1 / 2) + (1 / 2)))) |
103 | | remulcl 10021 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ ∧ 𝑥
∈ ℝ) → (2 · 𝑥) ∈ ℝ) |
104 | 73, 55, 103 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈
ℝ) |
105 | 104 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈
ℂ) |
106 | 32 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 2) ∈
ℂ) |
107 | 105, 106,
106 | pnpcan2d 10430 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (((2 · 𝑥) + (1 / 2)) − ((1 / 2) +
(1 / 2))) = ((2 · 𝑥)
− (1 / 2))) |
108 | 102, 107 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = ((2
· 𝑥) − (1 /
2))) |
109 | 108 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)) = ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2)))) |
110 | 4, 96, 11 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2)) |
111 | 82, 4, 25 | divcan1i 10769 |
. . . . . . . . . . . . . . 15
⊢ ((1 / 2)
· 2) = 1 |
112 | 18, 60, 21, 37, 111 | iccdili 12311 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (𝑥 · 2)
∈ ((1 / 2)[,]1)) |
113 | 62, 112 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ ((1 /
2)[,]1)) |
114 | 110, 113 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ((1 /
2)[,]1)) |
115 | 32 | subidi 10352 |
. . . . . . . . . . . . 13
⊢ ((1 / 2)
− (1 / 2)) = 0 |
116 | | 1mhlfehlf 11251 |
. . . . . . . . . . . . 13
⊢ (1
− (1 / 2)) = (1 / 2) |
117 | 60, 6, 60, 115, 116 | iccshftli 12309 |
. . . . . . . . . . . 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 | 42, 43 | pcoval1 22813 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((2 · 𝑥) − (1 / 2)) ∈
(0[,](1 / 2))) → ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 /
2))))) |
120 | 53, 118, 119 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 /
2))))) |
121 | 95, 105, 106 | subdid 10486 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2
· 𝑥) − (1 /
2))) = ((2 · (2 · 𝑥)) − (2 · (1 /
2)))) |
122 | 4, 25 | recidi 10756 |
. . . . . . . . . . . . 13
⊢ (2
· (1 / 2)) = 1 |
123 | 122 | oveq2i 6661 |
. . . . . . . . . . . 12
⊢ ((2
· (2 · 𝑥))
− (2 · (1 / 2))) = ((2 · (2 · 𝑥)) − 1) |
124 | 121, 123 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2
· 𝑥) − (1 /
2))) = ((2 · (2 · 𝑥)) − 1)) |
125 | 124 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))) = (𝐺‘((2 · (2 ·
𝑥)) −
1))) |
126 | 120, 125 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘((2 · (2 · 𝑥)) − 1))) |
127 | 93, 109, 126 | 3eqtrd 2660 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = (𝐺‘((2 · (2 · 𝑥)) − 1))) |
128 | | iffalse 4095 |
. . . . . . . . . 10
⊢ (¬
𝑥 ≤ (1 / 4) →
if(𝑥 ≤ (1 / 4), (2
· 𝑥), (𝑥 + (1 / 4))) = (𝑥 + (1 / 4))) |
129 | 128 | fveq2d 6195 |
. . . . . . . . 9
⊢ (¬
𝑥 ≤ (1 / 4) →
((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4)))) |
130 | 129 | adantl 482 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4)))) |
131 | 41, 42, 89 | pcoval2 22816 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (2 · 𝑥) ∈ ((1 / 2)[,]1)) →
((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1))) |
132 | 53, 114, 131 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1))) |
133 | 127, 130,
132 | 3eqtr4d 2666 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
134 | 52, 133 | pm2.61dan 832 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
135 | | iftrue 4092 |
. . . . . . . 8
⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) |
136 | 135 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑥 ≤ (1 / 2) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))) |
137 | 136 | adantl 482 |
. . . . . 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 4092 |
. . . . . . 7
⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
139 | 138 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥))) |
140 | 134, 137,
139 | 3eqtr4d 2666 |
. . . . 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 22735 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 ≤ (1 / 2)) →
𝑥 ∈ ((1 /
2)[,]1)) |
142 | | halfgt0 11248 |
. . . . . . . . . . . . . . 15
⊢ 0 < (1
/ 2) |
143 | 5, 60, 142 | ltleii 10160 |
. . . . . . . . . . . . . 14
⊢ 0 ≤ (1
/ 2) |
144 | | halflt1 11250 |
. . . . . . . . . . . . . . 15
⊢ (1 / 2)
< 1 |
145 | 60, 6, 144 | ltleii 10160 |
. . . . . . . . . . . . . 14
⊢ (1 / 2)
≤ 1 |
146 | 5, 6 | elicc2i 12239 |
. . . . . . . . . . . . . 14
⊢ ((1 / 2)
∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 /
2) ≤ 1)) |
147 | 60, 143, 145, 146 | mpbir3an 1244 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ (0[,]1) |
148 | | 1elunit 12291 |
. . . . . . . . . . . . 13
⊢ 1 ∈
(0[,]1) |
149 | | iccss2 12244 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → ((1 / 2)[,]1) ⊆
(0[,]1)) |
150 | 147, 148,
149 | mp2an 708 |
. . . . . . . . . . . 12
⊢ ((1 /
2)[,]1) ⊆ (0[,]1) |
151 | 150 | sseli 3599 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
𝑥 ∈
(0[,]1)) |
152 | 4, 25 | div0i 10759 |
. . . . . . . . . . . 12
⊢ (0 / 2) =
0 |
153 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (1 / 2) =
(1 / 2) |
154 | 5, 6, 21, 152, 153 | icccntri 12313 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]1) → (𝑥 / 2) ∈ (0[,](1 /
2))) |
155 | 32 | addid2i 10224 |
. . . . . . . . . . . 12
⊢ (0 + (1 /
2)) = (1 / 2) |
156 | 5, 60, 60, 155, 84 | iccshftri 12307 |
. . . . . . . . . . 11
⊢ ((𝑥 / 2) ∈ (0[,](1 / 2))
→ ((𝑥 / 2) + (1 / 2))
∈ ((1 / 2)[,]1)) |
157 | 151, 154,
156 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
((𝑥 / 2) + (1 / 2)) ∈
((1 / 2)[,]1)) |
158 | 41, 45, 91 | pcoval2 22816 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1)) →
((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) −
1))) |
159 | 157, 158 | sylan2 491 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) −
1))) |
160 | 60, 6 | elicc2i 12239 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ((1 / 2)[,]1) ↔
(𝑥 ∈ ℝ ∧ (1
/ 2) ≤ 𝑥 ∧ 𝑥 ≤ 1)) |
161 | 160 | simp1bi 1076 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
𝑥 ∈
ℝ) |
162 | 161 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
𝑥 ∈
ℂ) |
163 | 82 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((1 / 2)[,]1) → 1
∈ ℂ) |
164 | | 2cnd 11093 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2
∈ ℂ) |
165 | 25 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2
≠ 0) |
166 | 162, 163,
164, 165 | divdird 10839 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
((𝑥 + 1) / 2) = ((𝑥 / 2) + (1 /
2))) |
167 | 166 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2
· ((𝑥 + 1) / 2)) =
(2 · ((𝑥 / 2) + (1 /
2)))) |
168 | | peano2cn 10208 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (𝑥 + 1) ∈
ℂ) |
169 | 162, 168 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
(𝑥 + 1) ∈
ℂ) |
170 | 169, 164,
165 | divcan2d 10803 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2
· ((𝑥 + 1) / 2)) =
(𝑥 + 1)) |
171 | 167, 170 | eqtr3d 2658 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2
· ((𝑥 / 2) + (1 /
2))) = (𝑥 +
1)) |
172 | 171 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((2
· ((𝑥 / 2) + (1 /
2))) − 1) = ((𝑥 + 1)
− 1)) |
173 | | pncan 10287 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑥 + 1)
− 1) = 𝑥) |
174 | 162, 82, 173 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
((𝑥 + 1) − 1) = 𝑥) |
175 | 172, 174 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((2
· ((𝑥 / 2) + (1 /
2))) − 1) = 𝑥) |
176 | 175 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
((𝐺(*𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(*𝑝‘𝐽)𝐻)‘𝑥)) |
177 | 176 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(*𝑝‘𝐽)𝐻)‘𝑥)) |
178 | 42, 43, 44 | pcoval2 22816 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝‘𝐽)𝐻)‘𝑥) = (𝐻‘((2 · 𝑥) − 1))) |
179 | 159, 177,
178 | 3eqtrd 2660 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1))) |
180 | 141, 179 | sylan2 491 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2))) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1))) |
181 | 180 | anassrs 680 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1))) |
182 | | iffalse 4095 |
. . . . . . . 8
⊢ (¬
𝑥 ≤ (1 / 2) →
if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2))) |
183 | 182 | fveq2d 6195 |
. . . . . . 7
⊢ (¬
𝑥 ≤ (1 / 2) →
((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2)))) |
184 | 183 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2)))) |
185 | | iffalse 4095 |
. . . . . . 7
⊢ (¬
𝑥 ≤ (1 / 2) →
if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1))) |
186 | 185 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1))) |
187 | 181, 184,
186 | 3eqtr4d 2666 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))) |
188 | 140, 187 | pm2.61dan 832 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))) |
189 | 188 | mpteq2dva 4744 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))) |
190 | | pcoass.7 |
. . . . . . 7
⊢ 𝑃 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) |
191 | | iitopon 22682 |
. . . . . . . . 9
⊢ II ∈
(TopOn‘(0[,]1)) |
192 | 191 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
193 | 192 | cnmptid 21464 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II)) |
194 | | 0elunit 12290 |
. . . . . . . . . 10
⊢ 0 ∈
(0[,]1) |
195 | 194 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
(0[,]1)) |
196 | 192, 192,
195 | cnmptc 21465 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn
II)) |
197 | | eqid 2622 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
198 | | eqid 2622 |
. . . . . . . . 9
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) =
((topGen‘ran (,)) ↾t (0[,](1 / 2))) |
199 | | eqid 2622 |
. . . . . . . . 9
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) =
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) |
200 | | dfii2 22685 |
. . . . . . . . 9
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
201 | | 0red 10041 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
202 | | 1red 10055 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ) |
203 | 147 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 2) ∈
(0[,]1)) |
204 | | simprl 794 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2)) |
205 | 204 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 2) + (1 /
4))) |
206 | 32, 23 | addcomi 10227 |
. . . . . . . . . . 11
⊢ ((1 / 2)
+ (1 / 4)) = ((1 / 4) + (1 / 2)) |
207 | 205, 206 | syl6eq 2672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 /
2))) |
208 | 18, 60 | ltnlei 10158 |
. . . . . . . . . . . . 13
⊢ ((1 / 4)
< (1 / 2) ↔ ¬ (1 / 2) ≤ (1 / 4)) |
209 | 78, 208 | mpbi 220 |
. . . . . . . . . . . 12
⊢ ¬ (1
/ 2) ≤ (1 / 4) |
210 | 204 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 ≤ (1 / 4) ↔ (1 / 2) ≤ (1 /
4))) |
211 | 209, 210 | mtbiri 317 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ¬ 𝑦 ≤ (1 / 4)) |
212 | 211 | iffalsed 4097 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = (𝑦 + (1 / 4))) |
213 | 204 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = ((1 / 2) / 2)) |
214 | 213, 30 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = (1 / 4)) |
215 | 214 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((𝑦 / 2) + (1 / 2)) = ((1 / 4) + (1 /
2))) |
216 | 207, 212,
215 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = ((𝑦 / 2) + (1 / 2))) |
217 | | eqid 2622 |
. . . . . . . . . 10
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 4))) =
((topGen‘ran (,)) ↾t (0[,](1 / 4))) |
218 | | eqid 2622 |
. . . . . . . . . 10
⊢
((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) =
((topGen‘ran (,)) ↾t ((1 / 4)[,](1 /
2))) |
219 | 60 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
220 | 74, 76 | recgt0ii 10929 |
. . . . . . . . . . . . 13
⊢ 0 < (1
/ 4) |
221 | 5, 18, 220 | ltleii 10160 |
. . . . . . . . . . . 12
⊢ 0 ≤ (1
/ 4) |
222 | 5, 60 | elicc2i 12239 |
. . . . . . . . . . . 12
⊢ ((1 / 4)
∈ (0[,](1 / 2)) ↔ ((1 / 4) ∈ ℝ ∧ 0 ≤ (1 / 4) ∧
(1 / 4) ≤ (1 / 2))) |
223 | 18, 221, 79, 222 | mpbir3an 1244 |
. . . . . . . . . . 11
⊢ (1 / 4)
∈ (0[,](1 / 2)) |
224 | 223 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / 4) ∈ (0[,](1 /
2))) |
225 | | simprl 794 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 4)) |
226 | 225 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 /
4))) |
227 | 225 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 /
4))) |
228 | 24, 226, 227 | 3eqtr4a 2682 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (𝑦 + (1 / 4))) |
229 | | retopon 22567 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
230 | | 0xr 10086 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ* |
231 | 60 | rexri 10097 |
. . . . . . . . . . . . . . . 16
⊢ (1 / 2)
∈ ℝ* |
232 | | lbicc2 12288 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ* ∧ (1 / 2) ∈ ℝ* ∧ 0
≤ (1 / 2)) → 0 ∈ (0[,](1 / 2))) |
233 | 230, 231,
143, 232 | mp3an 1424 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
(0[,](1 / 2)) |
234 | | iccss2 12244 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ (0[,](1 / 2)) ∧ (1 / 4) ∈ (0[,](1 / 2))) → (0[,](1 / 4))
⊆ (0[,](1 / 2))) |
235 | 233, 223,
234 | mp2an 708 |
. . . . . . . . . . . . . 14
⊢ (0[,](1 /
4)) ⊆ (0[,](1 / 2)) |
236 | | iccssre 12255 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆
ℝ) |
237 | 5, 60, 236 | mp2an 708 |
. . . . . . . . . . . . . 14
⊢ (0[,](1 /
2)) ⊆ ℝ |
238 | 235, 237 | sstri 3612 |
. . . . . . . . . . . . 13
⊢ (0[,](1 /
4)) ⊆ ℝ |
239 | | resttopon 20965 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
4)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 4))) ∈ (TopOn‘(0[,](1 / 4)))) |
240 | 229, 238,
239 | mp2an 708 |
. . . . . . . . . . . 12
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 4))) ∈
(TopOn‘(0[,](1 / 4))) |
241 | 240 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ((topGen‘ran (,))
↾t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 /
4)))) |
242 | 241, 192 | cnmpt1st 21471 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 4))) ×t II) Cn
((topGen‘ran (,)) ↾t (0[,](1 / 4))))) |
243 | | retop 22565 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ Top |
244 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ (0[,](1 /
2)) ∈ V |
245 | | restabs 20969 |
. . . . . . . . . . . . . 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)))) |
246 | 243, 235,
244, 245 | mp3an 1424 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ↾t (0[,](1 / 2)))
↾t (0[,](1 / 4))) = ((topGen‘ran (,))
↾t (0[,](1 / 4))) |
247 | 246 | eqcomi 2631 |
. . . . . . . . . . . 12
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 4))) =
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) ↾t
(0[,](1 / 4))) |
248 | | resttopon 20965 |
. . . . . . . . . . . . . 14
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 2))) ∈ (TopOn‘(0[,](1 / 2)))) |
249 | 229, 237,
248 | mp2an 708 |
. . . . . . . . . . . . 13
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈
(TopOn‘(0[,](1 / 2))) |
250 | 249 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((topGen‘ran (,))
↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 /
2)))) |
251 | 235 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0[,](1 / 4)) ⊆
(0[,](1 / 2))) |
252 | 198 | iihalf1cn 22731 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2
· 𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II) |
253 | 252 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)) ↦ (2 ·
𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II)) |
254 | 247, 250,
251, 253 | cnmpt1res 21479 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 4)) ↦ (2 ·
𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 4))) Cn
II)) |
255 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦)) |
256 | 241, 192,
242, 241, 254, 255 | cnmpt21 21474 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 4))) ×t II) Cn
II)) |
257 | | iccssre 12255 |
. . . . . . . . . . . . . 14
⊢ (((1 / 4)
∈ ℝ ∧ (1 / 2) ∈ ℝ) → ((1 / 4)[,](1 / 2)) ⊆
ℝ) |
258 | 18, 60, 257 | mp2an 708 |
. . . . . . . . . . . . 13
⊢ ((1 /
4)[,](1 / 2)) ⊆ ℝ |
259 | | resttopon 20965 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
4)[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,))
↾t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 /
2)))) |
260 | 229, 258,
259 | mp2an 708 |
. . . . . . . . . . . 12
⊢
((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ∈
(TopOn‘((1 / 4)[,](1 / 2))) |
261 | 260 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 /
2)))) |
262 | 261, 192 | cnmpt1st 21471 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ ((1 / 4)[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran
(,)) ↾t ((1 / 4)[,](1 / 2))) ×t II) Cn
((topGen‘ran (,)) ↾t ((1 / 4)[,](1 /
2))))) |
263 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
264 | 258 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 / 4)[,](1 / 2))
⊆ ℝ) |
265 | | unitssre 12319 |
. . . . . . . . . . . . 13
⊢ (0[,]1)
⊆ ℝ |
266 | 265 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0[,]1) ⊆
ℝ) |
267 | 150, 87 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2))
→ (𝑥 + (1 / 4)) ∈
(0[,]1)) |
268 | 267 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 4)[,](1 / 2))) → (𝑥 + (1 / 4)) ∈
(0[,]1)) |
269 | 263 | cnfldtopon 22586 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
270 | 269 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
271 | 270 | cnmptid 21464 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝑥) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
272 | 18 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 / 4) ∈
ℝ) |
273 | 272 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 / 4) ∈
ℂ) |
274 | 270, 270,
273 | cnmptc 21465 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 4)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
275 | 263 | addcn 22668 |
. . . . . . . . . . . . . 14
⊢ + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
276 | 275 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
277 | 270, 271,
274, 276 | cnmpt12f 21469 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 + (1 / 4))) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
278 | 263, 218,
200, 264, 266, 268, 277 | cnmptre 22726 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↦ (𝑥 + (1 / 4))) ∈
(((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) Cn
II)) |
279 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 + (1 / 4)) = (𝑦 + (1 / 4))) |
280 | 261, 192,
262, 261, 278, 279 | cnmpt21 21474 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ((1 / 4)[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ (𝑦 + (1 / 4))) ∈
((((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2)))
×t II) Cn II)) |
281 | 197, 217,
218, 198, 201, 219, 224, 192, 228, 256, 280 | cnmpt2pc 22727 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 2))) ×t II) Cn
II)) |
282 | | iccssre 12255 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆
ℝ) |
283 | 60, 6, 282 | mp2an 708 |
. . . . . . . . . . . 12
⊢ ((1 /
2)[,]1) ⊆ ℝ |
284 | | resttopon 20965 |
. . . . . . . . . . . 12
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1
/ 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))) |
285 | 229, 283,
284 | mp2an 708 |
. . . . . . . . . . 11
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈
(TopOn‘((1 / 2)[,]1)) |
286 | 285 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 /
2)[,]1))) |
287 | 286, 192 | cnmpt1st 21471 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)))) |
288 | 283 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1 / 2)[,]1) ⊆
ℝ) |
289 | 150, 157 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((1 / 2)[,]1) →
((𝑥 / 2) + (1 / 2)) ∈
(0[,]1)) |
290 | 289 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝑥 / 2) + (1 / 2)) ∈
(0[,]1)) |
291 | 263 | divccn 22676 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
292 | 4, 25, 291 | mp2an 708 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
293 | 292 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
294 | 32 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / 2) ∈
ℂ) |
295 | 270, 270,
294 | cnmptc 21465 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 2)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
296 | 270, 293,
295, 276 | cnmpt12f 21469 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥 / 2) + (1 / 2))) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
297 | 263, 199,
200, 288, 266, 290, 296 | cnmptre 22726 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((𝑥 / 2) + (1 / 2))) ∈
(((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II)) |
298 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2)) |
299 | 298 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 / 2) + (1 / 2)) = ((𝑦 / 2) + (1 / 2))) |
300 | 286, 192,
287, 286, 297, 299 | cnmpt21 21474 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ ((𝑦 / 2) + (1 / 2))) ∈ ((((topGen‘ran
(,)) ↾t ((1 / 2)[,]1)) ×t II) Cn
II)) |
301 | 197, 198,
199, 200, 201, 202, 203, 192, 216, 281, 300 | cnmpt2pc 22727 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) ∈ ((II
×t II) Cn II)) |
302 | | breq1 4656 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2))) |
303 | | breq1 4656 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 4) ↔ 𝑦 ≤ (1 / 4))) |
304 | 303, 255,
279 | ifbieq12d 4113 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) |
305 | 302, 304,
299 | ifbieq12d 4113 |
. . . . . . . . . . 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)))) |
306 | 305 | equcoms 1947 |
. . . . . . . . . 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)))) |
307 | 306 | adantr 481 |
. . . . . . . . 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)))) |
308 | 307 | eqcomd 2628 |
. . . . . . . 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)))) |
309 | 192, 193,
196, 192, 192, 301, 308 | cnmpt12 21470 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) ∈ (II Cn
II)) |
310 | 190, 309 | syl5eqel 2705 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ (II Cn II)) |
311 | | iiuni 22684 |
. . . . . . 7
⊢ (0[,]1) =
∪ II |
312 | 311, 311 | cnf 21050 |
. . . . . 6
⊢ (𝑃 ∈ (II Cn II) → 𝑃:(0[,]1)⟶(0[,]1)) |
313 | 310, 312 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃:(0[,]1)⟶(0[,]1)) |
314 | 190 | fmpt 6381 |
. . . . 5
⊢
(∀𝑥 ∈
(0[,]1)if(𝑥 ≤ (1 / 2),
if(𝑥 ≤ (1 / 4), (2
· 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈ (0[,]1)
↔ 𝑃:(0[,]1)⟶(0[,]1)) |
315 | 313, 314 | sylibr 224 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈
(0[,]1)) |
316 | 190 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑃 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))) |
317 | 41, 45, 91 | pcocn 22817 |
. . . . . 6
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽)) |
318 | | eqid 2622 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
319 | 311, 318 | cnf 21050 |
. . . . . 6
⊢ ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽) → (𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽) |
320 | 317, 319 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽) |
321 | 320 | feqmptd 6249 |
. . . 4
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) = (𝑦 ∈ (0[,]1) ↦ ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘𝑦))) |
322 | | fveq2 6191 |
. . . 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))))) |
323 | 315, 316,
321, 322 | fmptcof 6397 |
. . 3
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) ∘ 𝑃) = (𝑥 ∈ (0[,]1) ↦ ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))))) |
324 | 41, 42, 89 | pcocn 22817 |
. . . 4
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽)) |
325 | 324, 43 | pcoval 22811 |
. . 3
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)(*𝑝‘𝐽)𝐻) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))) |
326 | 189, 323,
325 | 3eqtr4rd 2667 |
. 2
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)(*𝑝‘𝐽)𝐻) = ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) ∘ 𝑃)) |
327 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = 0 → 𝑥 = 0) |
328 | 327, 143 | syl6eqbr 4692 |
. . . . . . 7
⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 2)) |
329 | 328 | iftrued 4094 |
. . . . . 6
⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) |
330 | 327, 221 | syl6eqbr 4692 |
. . . . . . 7
⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 4)) |
331 | 330 | iftrued 4094 |
. . . . . 6
⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥)) |
332 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = 0 → (2 · 𝑥) = (2 ·
0)) |
333 | | 2t0e0 11183 |
. . . . . . 7
⊢ (2
· 0) = 0 |
334 | 332, 333 | syl6eq 2672 |
. . . . . 6
⊢ (𝑥 = 0 → (2 · 𝑥) = 0) |
335 | 329, 331,
334 | 3eqtrd 2660 |
. . . . 5
⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 0) |
336 | | c0ex 10034 |
. . . . 5
⊢ 0 ∈
V |
337 | 335, 190,
336 | fvmpt 6282 |
. . . 4
⊢ (0 ∈
(0[,]1) → (𝑃‘0)
= 0) |
338 | 195, 337 | syl 17 |
. . 3
⊢ (𝜑 → (𝑃‘0) = 0) |
339 | 148 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 ∈
(0[,]1)) |
340 | 60, 6 | ltnlei 10158 |
. . . . . . . . 9
⊢ ((1 / 2)
< 1 ↔ ¬ 1 ≤ (1 / 2)) |
341 | 144, 340 | mpbi 220 |
. . . . . . . 8
⊢ ¬ 1
≤ (1 / 2) |
342 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 /
2))) |
343 | 341, 342 | mtbiri 317 |
. . . . . . 7
⊢ (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2)) |
344 | 343 | iffalsed 4097 |
. . . . . 6
⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2))) |
345 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝑥 / 2) = (1 / 2)) |
346 | 345 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = ((1 / 2) + (1 /
2))) |
347 | 346, 84 | syl6eq 2672 |
. . . . . 6
⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = 1) |
348 | 344, 347 | eqtrd 2656 |
. . . . 5
⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 1) |
349 | | 1ex 10035 |
. . . . 5
⊢ 1 ∈
V |
350 | 348, 190,
349 | fvmpt 6282 |
. . . 4
⊢ (1 ∈
(0[,]1) → (𝑃‘1)
= 1) |
351 | 339, 350 | syl 17 |
. . 3
⊢ (𝜑 → (𝑃‘1) = 1) |
352 | 317, 310,
338, 351 | reparpht 22798 |
. 2
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻)) ∘ 𝑃)( ≃ph‘𝐽)(𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))) |
353 | 326, 352 | eqbrtrd 4675 |
1
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)(𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))) |