Step |
Hyp |
Ref |
Expression |
1 |
|
ftc1anc.g |
⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
2 |
|
ftc1anc.a |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
3 |
|
ftc1anc.b |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
4 |
|
ftc1anc.le |
⊢ ( 𝜑 → 𝐴 ≤ 𝐵 ) |
5 |
|
ftc1anc.s |
⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 ) |
6 |
|
ftc1anc.d |
⊢ ( 𝜑 → 𝐷 ⊆ ℝ ) |
7 |
|
ftc1anc.i |
⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 ) |
8 |
|
ftc1anc.f |
⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ ) |
9 |
|
ftc1anc.t |
⊢ ( 𝜑 → ∀ 𝑠 ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ( abs ‘ ∫ 𝑠 ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
10 |
1 2 3 4 5 6 7 8
|
ftc1lem2 |
⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ) |
11 |
|
rphalfcl |
⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ+ ) |
12 |
1 2 3 4 5 6 7 8
|
ftc1anclem6 |
⊢ ( ( 𝜑 ∧ ( 𝑦 / 2 ) ∈ ℝ+ ) → ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) |
13 |
11 12
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) |
14 |
13
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) → ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) |
15 |
11
|
ad2antll |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) → ( 𝑦 / 2 ) ∈ ℝ+ ) |
16 |
|
2rp |
⊢ 2 ∈ ℝ+ |
17 |
|
i1ff |
⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 : ℝ ⟶ ℝ ) |
18 |
17
|
frnd |
⊢ ( 𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ ) |
19 |
18
|
adantr |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ran 𝑓 ⊆ ℝ ) |
20 |
|
i1ff |
⊢ ( 𝑔 ∈ dom ∫1 → 𝑔 : ℝ ⟶ ℝ ) |
21 |
20
|
frnd |
⊢ ( 𝑔 ∈ dom ∫1 → ran 𝑔 ⊆ ℝ ) |
22 |
21
|
adantl |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ran 𝑔 ⊆ ℝ ) |
23 |
19 22
|
unssd |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℝ ) |
24 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
25 |
23 24
|
sstrdi |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ) |
26 |
|
i1f0rn |
⊢ ( 𝑓 ∈ dom ∫1 → 0 ∈ ran 𝑓 ) |
27 |
|
elun1 |
⊢ ( 0 ∈ ran 𝑓 → 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) |
28 |
26 27
|
syl |
⊢ ( 𝑓 ∈ dom ∫1 → 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) |
29 |
28
|
adantr |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) |
30 |
|
absf |
⊢ abs : ℂ ⟶ ℝ |
31 |
|
ffn |
⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ ) |
32 |
30 31
|
ax-mp |
⊢ abs Fn ℂ |
33 |
|
fnfvima |
⊢ ( ( abs Fn ℂ ∧ ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 0 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ) |
34 |
32 33
|
mp3an1 |
⊢ ( ( ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ 0 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 0 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ) |
35 |
25 29 34
|
syl2anc |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs ‘ 0 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ) |
36 |
35
|
ne0d |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ) |
37 |
|
imassrn |
⊢ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ran abs |
38 |
|
frn |
⊢ ( abs : ℂ ⟶ ℝ → ran abs ⊆ ℝ ) |
39 |
30 38
|
ax-mp |
⊢ ran abs ⊆ ℝ |
40 |
37 39
|
sstri |
⊢ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ |
41 |
|
ffun |
⊢ ( abs : ℂ ⟶ ℝ → Fun abs ) |
42 |
30 41
|
ax-mp |
⊢ Fun abs |
43 |
|
i1frn |
⊢ ( 𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin ) |
44 |
|
i1frn |
⊢ ( 𝑔 ∈ dom ∫1 → ran 𝑔 ∈ Fin ) |
45 |
|
unfi |
⊢ ( ( ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin ) → ( ran 𝑓 ∪ ran 𝑔 ) ∈ Fin ) |
46 |
43 44 45
|
syl2an |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ran 𝑓 ∪ ran 𝑔 ) ∈ Fin ) |
47 |
|
imafi |
⊢ ( ( Fun abs ∧ ( ran 𝑓 ∪ ran 𝑔 ) ∈ Fin ) → ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ∈ Fin ) |
48 |
42 46 47
|
sylancr |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ∈ Fin ) |
49 |
|
fimaxre2 |
⊢ ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) |
50 |
40 48 49
|
sylancr |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) |
51 |
|
suprcl |
⊢ ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ ) |
52 |
40 51
|
mp3an1 |
⊢ ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ ) |
53 |
36 50 52
|
syl2anc |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ ) |
54 |
53
|
adantr |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ ) |
55 |
|
0red |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → 0 ∈ ℝ ) |
56 |
25
|
sselda |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → 𝑟 ∈ ℂ ) |
57 |
56
|
abscld |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ∈ ℝ ) |
58 |
57
|
adantrr |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → ( abs ‘ 𝑟 ) ∈ ℝ ) |
59 |
53
|
adantr |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ ) |
60 |
|
absgt0 |
⊢ ( 𝑟 ∈ ℂ → ( 𝑟 ≠ 0 ↔ 0 < ( abs ‘ 𝑟 ) ) ) |
61 |
56 60
|
syl |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( 𝑟 ≠ 0 ↔ 0 < ( abs ‘ 𝑟 ) ) ) |
62 |
61
|
biimpd |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( 𝑟 ≠ 0 → 0 < ( abs ‘ 𝑟 ) ) ) |
63 |
62
|
impr |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → 0 < ( abs ‘ 𝑟 ) ) |
64 |
40
|
a1i |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ) |
65 |
64 36 50
|
3jca |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) ) |
66 |
65
|
adantr |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) ) |
67 |
|
fnfvima |
⊢ ( ( abs Fn ℂ ∧ ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ) |
68 |
32 67
|
mp3an1 |
⊢ ( ( ( ran 𝑓 ∪ ran 𝑔 ) ⊆ ℂ ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ) |
69 |
25 68
|
sylan |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ) |
70 |
|
suprub |
⊢ ( ( ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ⊆ ℝ ∧ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) 𝑦 ≤ 𝑥 ) ∧ ( abs ‘ 𝑟 ) ∈ ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) ) → ( abs ‘ 𝑟 ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) |
71 |
66 69 70
|
syl2anc |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) → ( abs ‘ 𝑟 ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) |
72 |
71
|
adantrr |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → ( abs ‘ 𝑟 ) ≤ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) |
73 |
55 58 59 63 72
|
ltletrd |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ 𝑟 ≠ 0 ) ) → 0 < sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) |
74 |
73
|
rexlimdvaa |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 → 0 < sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) |
75 |
74
|
imp |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → 0 < sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) |
76 |
54 75
|
elrpd |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ+ ) |
77 |
|
rpmulcl |
⊢ ( ( 2 ∈ ℝ+ ∧ sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ∈ ℝ+ ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ ) |
78 |
16 76 77
|
sylancr |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ ) |
79 |
|
rpdivcl |
⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ∈ ℝ+ ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ+ ) |
80 |
15 78 79
|
syl2an |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ+ ) |
81 |
80
|
anassrs |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ+ ) |
82 |
81
|
adantlr |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ+ ) |
83 |
|
ancom |
⊢ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ↔ ( 𝑦 ∈ ℝ+ ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ) |
84 |
83
|
anbi2i |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ) ) |
85 |
|
an32 |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ↔ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ) |
86 |
85
|
anbi1i |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ↔ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ) |
87 |
|
an32 |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ↔ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ) |
88 |
86 87
|
bitri |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ↔ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ) |
89 |
88
|
anbi1i |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ) |
90 |
|
an32 |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ) |
91 |
89 90
|
bitri |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ) |
92 |
|
anass |
⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ) ) |
93 |
84 91 92
|
3bitr4i |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ↔ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ) |
94 |
|
oveq12 |
⊢ ( ( 𝑏 = 𝑤 ∧ 𝑎 = 𝑢 ) → ( 𝑏 − 𝑎 ) = ( 𝑤 − 𝑢 ) ) |
95 |
94
|
ancoms |
⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑤 ) → ( 𝑏 − 𝑎 ) = ( 𝑤 − 𝑢 ) ) |
96 |
95
|
fveq2d |
⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑤 ) → ( abs ‘ ( 𝑏 − 𝑎 ) ) = ( abs ‘ ( 𝑤 − 𝑢 ) ) ) |
97 |
96
|
breq1d |
⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑤 ) → ( ( abs ‘ ( 𝑏 − 𝑎 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ↔ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) ) |
98 |
|
fveq2 |
⊢ ( 𝑏 = 𝑤 → ( 𝐺 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑤 ) ) |
99 |
|
fveq2 |
⊢ ( 𝑎 = 𝑢 → ( 𝐺 ‘ 𝑎 ) = ( 𝐺 ‘ 𝑢 ) ) |
100 |
98 99
|
oveqan12rd |
⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑤 ) → ( ( 𝐺 ‘ 𝑏 ) − ( 𝐺 ‘ 𝑎 ) ) = ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) |
101 |
100
|
fveq2d |
⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑏 ) − ( 𝐺 ‘ 𝑎 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ) |
102 |
101
|
breq1d |
⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑤 ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑏 ) − ( 𝐺 ‘ 𝑎 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
103 |
97 102
|
imbi12d |
⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑤 ) → ( ( ( abs ‘ ( 𝑏 − 𝑎 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑏 ) − ( 𝐺 ‘ 𝑎 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) ) |
104 |
|
oveq12 |
⊢ ( ( 𝑏 = 𝑢 ∧ 𝑎 = 𝑤 ) → ( 𝑏 − 𝑎 ) = ( 𝑢 − 𝑤 ) ) |
105 |
104
|
ancoms |
⊢ ( ( 𝑎 = 𝑤 ∧ 𝑏 = 𝑢 ) → ( 𝑏 − 𝑎 ) = ( 𝑢 − 𝑤 ) ) |
106 |
105
|
fveq2d |
⊢ ( ( 𝑎 = 𝑤 ∧ 𝑏 = 𝑢 ) → ( abs ‘ ( 𝑏 − 𝑎 ) ) = ( abs ‘ ( 𝑢 − 𝑤 ) ) ) |
107 |
106
|
breq1d |
⊢ ( ( 𝑎 = 𝑤 ∧ 𝑏 = 𝑢 ) → ( ( abs ‘ ( 𝑏 − 𝑎 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ↔ ( abs ‘ ( 𝑢 − 𝑤 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) ) |
108 |
|
fveq2 |
⊢ ( 𝑏 = 𝑢 → ( 𝐺 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑢 ) ) |
109 |
|
fveq2 |
⊢ ( 𝑎 = 𝑤 → ( 𝐺 ‘ 𝑎 ) = ( 𝐺 ‘ 𝑤 ) ) |
110 |
108 109
|
oveqan12rd |
⊢ ( ( 𝑎 = 𝑤 ∧ 𝑏 = 𝑢 ) → ( ( 𝐺 ‘ 𝑏 ) − ( 𝐺 ‘ 𝑎 ) ) = ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) |
111 |
110
|
fveq2d |
⊢ ( ( 𝑎 = 𝑤 ∧ 𝑏 = 𝑢 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑏 ) − ( 𝐺 ‘ 𝑎 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) |
112 |
111
|
breq1d |
⊢ ( ( 𝑎 = 𝑤 ∧ 𝑏 = 𝑢 ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑏 ) − ( 𝐺 ‘ 𝑎 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) < 𝑦 ) ) |
113 |
107 112
|
imbi12d |
⊢ ( ( 𝑎 = 𝑤 ∧ 𝑏 = 𝑢 ) → ( ( ( abs ‘ ( 𝑏 − 𝑎 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑏 ) − ( 𝐺 ‘ 𝑎 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑢 − 𝑤 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) < 𝑦 ) ) ) |
114 |
|
iccssre |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) |
115 |
2 3 114
|
syl2anc |
⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) |
116 |
115
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) |
117 |
|
simp-4l |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → 𝜑 ) |
118 |
115 24
|
sstrdi |
⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ ) |
119 |
118
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑤 ∈ ℂ ) |
120 |
118
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑢 ∈ ℂ ) |
121 |
|
abssub |
⊢ ( ( 𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ ) → ( abs ‘ ( 𝑤 − 𝑢 ) ) = ( abs ‘ ( 𝑢 − 𝑤 ) ) ) |
122 |
119 120 121
|
syl2anr |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( 𝑤 − 𝑢 ) ) = ( abs ‘ ( 𝑢 − 𝑤 ) ) ) |
123 |
122
|
anandis |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( 𝑤 − 𝑢 ) ) = ( abs ‘ ( 𝑢 − 𝑤 ) ) ) |
124 |
123
|
breq1d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ↔ ( abs ‘ ( 𝑢 − 𝑤 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) ) |
125 |
10
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺 ‘ 𝑤 ) ∈ ℂ ) |
126 |
10
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺 ‘ 𝑢 ) ∈ ℂ ) |
127 |
|
abssub |
⊢ ( ( ( 𝐺 ‘ 𝑤 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑢 ) ∈ ℂ ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) |
128 |
125 126 127
|
syl2anr |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) |
129 |
128
|
anandis |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) |
130 |
129
|
breq1d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) < 𝑦 ) ) |
131 |
124 130
|
imbi12d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑢 − 𝑤 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) < 𝑦 ) ) ) |
132 |
117 131
|
sylan |
⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑢 − 𝑤 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) < 𝑦 ) ) ) |
133 |
2
|
rexrd |
⊢ ( 𝜑 → 𝐴 ∈ ℝ* ) |
134 |
3
|
rexrd |
⊢ ( 𝜑 → 𝐵 ∈ ℝ* ) |
135 |
133 134
|
jca |
⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ) |
136 |
|
df-icc |
⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑡 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦 ) } ) |
137 |
136
|
elixx3g |
⊢ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑢 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵 ) ) ) |
138 |
137
|
simprbi |
⊢ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵 ) ) |
139 |
138
|
simpld |
⊢ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) → 𝐴 ≤ 𝑢 ) |
140 |
136
|
elixx3g |
⊢ ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵 ) ) ) |
141 |
140
|
simprbi |
⊢ ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵 ) ) |
142 |
141
|
simprd |
⊢ ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) → 𝑤 ≤ 𝐵 ) |
143 |
139 142
|
anim12i |
⊢ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵 ) ) |
144 |
|
ioossioo |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵 ) ) → ( 𝑢 (,) 𝑤 ) ⊆ ( 𝐴 (,) 𝐵 ) ) |
145 |
135 143 144
|
syl2an |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑢 (,) 𝑤 ) ⊆ ( 𝐴 (,) 𝐵 ) ) |
146 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 ) |
147 |
145 146
|
sstrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑢 (,) 𝑤 ) ⊆ 𝐷 ) |
148 |
147
|
sselda |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 𝑡 ∈ 𝐷 ) |
149 |
8
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ ) |
150 |
149
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ ) |
151 |
150
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ* ) |
152 |
149
|
absge0d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) |
153 |
|
elxrge0 |
⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) |
154 |
151 152 153
|
sylanbrc |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 0 [,] +∞ ) ) |
155 |
154
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 0 [,] +∞ ) ) |
156 |
148 155
|
syldan |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ( 0 [,] +∞ ) ) |
157 |
|
0e0iccpnf |
⊢ 0 ∈ ( 0 [,] +∞ ) |
158 |
157
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ∈ ( 0 [,] +∞ ) ) |
159 |
156 158
|
ifclda |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
160 |
159
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
161 |
160
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
162 |
|
itg2cl |
⊢ ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ* ) |
163 |
161 162
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ* ) |
164 |
163
|
3adantr3 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ* ) |
165 |
117 164
|
sylan |
⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ* ) |
166 |
165
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ* ) |
167 |
|
simplll |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ) |
168 |
149
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ ) |
169 |
148 168
|
syldan |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ ) |
170 |
169
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ ) |
171 |
|
elioore |
⊢ ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → 𝑡 ∈ ℝ ) |
172 |
17
|
ffvelrnda |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℝ ) |
173 |
172
|
recnd |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℂ ) |
174 |
|
ax-icn |
⊢ i ∈ ℂ |
175 |
20
|
ffvelrnda |
⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ℝ ) |
176 |
175
|
recnd |
⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ℂ ) |
177 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℂ ) → ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) |
178 |
174 176 177
|
sylancr |
⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) |
179 |
|
addcl |
⊢ ( ( ( 𝑓 ‘ 𝑡 ) ∈ ℂ ∧ ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ ) |
180 |
173 178 179
|
syl2an |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ ) |
181 |
180
|
anandirs |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ ) |
182 |
171 181
|
sylan2 |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ ) |
183 |
182
|
adantll |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ ) |
184 |
183
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ ) |
185 |
170 184
|
subcld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℂ ) |
186 |
185
|
abscld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ) |
187 |
182
|
abscld |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ ) |
188 |
187
|
adantll |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ ) |
189 |
188
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ ) |
190 |
186 189
|
readdcld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ) |
191 |
190
|
rexrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* ) |
192 |
185
|
absge0d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) |
193 |
181
|
absge0d |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) |
194 |
171 193
|
sylan2 |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) |
195 |
194
|
adantll |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) |
196 |
195
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) |
197 |
186 189 192 196
|
addge0d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) |
198 |
|
elxrge0 |
⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* ∧ 0 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) |
199 |
191 197 198
|
sylanbrc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ) |
200 |
157
|
a1i |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ∈ ( 0 [,] +∞ ) ) |
201 |
199 200
|
ifclda |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
202 |
201
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
203 |
202
|
fmpttd |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
204 |
|
itg2cl |
⊢ ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* ) |
205 |
203 204
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* ) |
206 |
205
|
3adantr3 |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* ) |
207 |
167 206
|
sylan |
⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* ) |
208 |
207
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ* ) |
209 |
|
rpxr |
⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ* ) |
210 |
209
|
ad3antlr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → 𝑦 ∈ ℝ* ) |
211 |
159
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
212 |
211
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
213 |
212
|
fmpttd |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
214 |
170 184
|
npcand |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 𝐹 ‘ 𝑡 ) ) |
215 |
214
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) |
216 |
185 184
|
abstrid |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) |
217 |
215 216
|
eqbrtrrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) |
218 |
|
iftrue |
⊢ ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) = ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) |
219 |
218
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) = ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) |
220 |
|
iftrue |
⊢ ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) |
221 |
220
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) |
222 |
217 219 221
|
3brtr4d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) |
223 |
222
|
ex |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) |
224 |
|
0le0 |
⊢ 0 ≤ 0 |
225 |
224
|
a1i |
⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → 0 ≤ 0 ) |
226 |
|
iffalse |
⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) = 0 ) |
227 |
|
iffalse |
⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) = 0 ) |
228 |
225 226 227
|
3brtr4d |
⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) |
229 |
223 228
|
pm2.61d1 |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) |
230 |
229
|
ralrimivw |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) |
231 |
|
reex |
⊢ ℝ ∈ V |
232 |
231
|
a1i |
⊢ ( 𝜑 → ℝ ∈ V ) |
233 |
|
fvex |
⊢ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ V |
234 |
|
c0ex |
⊢ 0 ∈ V |
235 |
233 234
|
ifex |
⊢ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ V |
236 |
235
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ V ) |
237 |
|
ovex |
⊢ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ V |
238 |
237 234
|
ifex |
⊢ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ V |
239 |
238
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ V ) |
240 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) |
241 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) |
242 |
232 236 239 240 241
|
ofrfval2 |
⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) |
243 |
242
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) |
244 |
230 243
|
mpbird |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) |
245 |
|
itg2le |
⊢ ( ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ) |
246 |
213 203 244 245
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ) |
247 |
246
|
3adantr3 |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ) |
248 |
167 247
|
sylan |
⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ) |
249 |
248
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ) |
250 |
1 2 3 4 5 6 7 8
|
ftc1anclem8 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) < 𝑦 ) |
251 |
166 208 210 249 250
|
xrlelttrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < 𝑦 ) |
252 |
|
simplll |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → 𝜑 ) |
253 |
|
simpr2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) |
254 |
|
oveq2 |
⊢ ( 𝑥 = 𝑤 → ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑤 ) ) |
255 |
|
itgeq1 |
⊢ ( ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑤 ) → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
256 |
254 255
|
syl |
⊢ ( 𝑥 = 𝑤 → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
257 |
|
itgex |
⊢ ∫ ( 𝐴 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ V |
258 |
256 1 257
|
fvmpt |
⊢ ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐺 ‘ 𝑤 ) = ∫ ( 𝐴 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
259 |
253 258
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( 𝐺 ‘ 𝑤 ) = ∫ ( 𝐴 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
260 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → 𝐴 ∈ ℝ ) |
261 |
115
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑤 ∈ ℝ ) |
262 |
261
|
3ad2antr2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → 𝑤 ∈ ℝ ) |
263 |
115
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑢 ∈ ℝ ) |
264 |
263
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑢 ∈ ℝ* ) |
265 |
264
|
3ad2antr1 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → 𝑢 ∈ ℝ* ) |
266 |
|
elicc1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵 ) ) ) |
267 |
133 134 266
|
syl2anc |
⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵 ) ) ) |
268 |
267
|
biimpa |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵 ) ) |
269 |
268
|
simp2d |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑢 ) |
270 |
269
|
3ad2antr1 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → 𝐴 ≤ 𝑢 ) |
271 |
|
simpr3 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → 𝑢 ≤ 𝑤 ) |
272 |
133
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ* ) |
273 |
261
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑤 ∈ ℝ* ) |
274 |
|
elicc1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝑢 ∈ ( 𝐴 [,] 𝑤 ) ↔ ( 𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤 ) ) ) |
275 |
272 273 274
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑢 ∈ ( 𝐴 [,] 𝑤 ) ↔ ( 𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤 ) ) ) |
276 |
275
|
3ad2antr2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( 𝑢 ∈ ( 𝐴 [,] 𝑤 ) ↔ ( 𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤 ) ) ) |
277 |
265 270 271 276
|
mpbir3and |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → 𝑢 ∈ ( 𝐴 [,] 𝑤 ) ) |
278 |
|
iooss2 |
⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑤 ≤ 𝐵 ) → ( 𝐴 (,) 𝑤 ) ⊆ ( 𝐴 (,) 𝐵 ) ) |
279 |
134 142 278
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑤 ) ⊆ ( 𝐴 (,) 𝐵 ) ) |
280 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 ) |
281 |
279 280
|
sstrd |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑤 ) ⊆ 𝐷 ) |
282 |
281
|
3ad2antr2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( 𝐴 (,) 𝑤 ) ⊆ 𝐷 ) |
283 |
282
|
sselda |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑤 ) ) → 𝑡 ∈ 𝐷 ) |
284 |
149
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ ) |
285 |
283 284
|
syldan |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑤 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ ) |
286 |
|
eleq1w |
⊢ ( 𝑤 = 𝑢 → ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ↔ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ) |
287 |
286
|
anbi2d |
⊢ ( 𝑤 = 𝑢 → ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ) ) |
288 |
|
oveq2 |
⊢ ( 𝑤 = 𝑢 → ( 𝐴 (,) 𝑤 ) = ( 𝐴 (,) 𝑢 ) ) |
289 |
288
|
mpteq1d |
⊢ ( 𝑤 = 𝑢 → ( 𝑡 ∈ ( 𝐴 (,) 𝑤 ) ↦ ( 𝐹 ‘ 𝑡 ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝑢 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ) |
290 |
289
|
eleq1d |
⊢ ( 𝑤 = 𝑢 → ( ( 𝑡 ∈ ( 𝐴 (,) 𝑤 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 ↔ ( 𝑡 ∈ ( 𝐴 (,) 𝑢 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 ) ) |
291 |
287 290
|
imbi12d |
⊢ ( 𝑤 = 𝑢 → ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑤 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 ) ↔ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑢 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 ) ) ) |
292 |
|
ioombl |
⊢ ( 𝐴 (,) 𝑤 ) ∈ dom vol |
293 |
292
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑤 ) ∈ dom vol ) |
294 |
149
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ ) |
295 |
8
|
feqmptd |
⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ) |
296 |
295 7
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 ) |
297 |
296
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 ) |
298 |
281 293 294 297
|
iblss |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑤 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 ) |
299 |
291 298
|
chvarvv |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑢 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 ) |
300 |
299
|
3ad2antr1 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑢 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 ) |
301 |
|
ioombl |
⊢ ( 𝑢 (,) 𝑤 ) ∈ dom vol |
302 |
301
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑢 (,) 𝑤 ) ∈ dom vol ) |
303 |
|
fvexd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ V ) |
304 |
296
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 ) |
305 |
147 302 303 304
|
iblss |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 ) |
306 |
305
|
3adantr3 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 ) |
307 |
260 262 277 285 300 306
|
itgsplitioo |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ∫ ( 𝐴 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ( ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ) |
308 |
259 307
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( 𝐺 ‘ 𝑤 ) = ( ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ) |
309 |
|
simpr1 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) |
310 |
|
oveq2 |
⊢ ( 𝑥 = 𝑢 → ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑢 ) ) |
311 |
|
itgeq1 |
⊢ ( ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑢 ) → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
312 |
310 311
|
syl |
⊢ ( 𝑥 = 𝑢 → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
313 |
|
itgex |
⊢ ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ V |
314 |
312 1 313
|
fvmpt |
⊢ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐺 ‘ 𝑢 ) = ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
315 |
309 314
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( 𝐺 ‘ 𝑢 ) = ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
316 |
308 315
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) = ( ( ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) − ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ) |
317 |
|
fvexd |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑢 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ V ) |
318 |
317 299
|
itgcl |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ ℂ ) |
319 |
318
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ ℂ ) |
320 |
|
fvexd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ V ) |
321 |
320 305
|
itgcl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ ℂ ) |
322 |
319 321
|
pncan2d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) − ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) = ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
323 |
322
|
3adantr3 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ( ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) − ∫ ( 𝐴 (,) 𝑢 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) = ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
324 |
316 323
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) = ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
325 |
324
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) = ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ) |
326 |
|
df-ov |
⊢ ( 𝑢 (,) 𝑤 ) = ( (,) ‘ 〈 𝑢 , 𝑤 〉 ) |
327 |
|
opelxpi |
⊢ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 〈 𝑢 , 𝑤 〉 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) |
328 |
|
ioof |
⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ |
329 |
|
ffn |
⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) ) |
330 |
328 329
|
ax-mp |
⊢ (,) Fn ( ℝ* × ℝ* ) |
331 |
|
iccssxr |
⊢ ( 𝐴 [,] 𝐵 ) ⊆ ℝ* |
332 |
|
xpss12 |
⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ* ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ⊆ ( ℝ* × ℝ* ) ) |
333 |
331 331 332
|
mp2an |
⊢ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ⊆ ( ℝ* × ℝ* ) |
334 |
|
fnfvima |
⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ⊆ ( ℝ* × ℝ* ) ∧ 〈 𝑢 , 𝑤 〉 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( (,) ‘ 〈 𝑢 , 𝑤 〉 ) ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) |
335 |
330 333 334
|
mp3an12 |
⊢ ( 〈 𝑢 , 𝑤 〉 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) → ( (,) ‘ 〈 𝑢 , 𝑤 〉 ) ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) |
336 |
327 335
|
syl |
⊢ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( (,) ‘ 〈 𝑢 , 𝑤 〉 ) ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) |
337 |
326 336
|
eqeltrid |
⊢ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑢 (,) 𝑤 ) ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) |
338 |
|
itgeq1 |
⊢ ( 𝑠 = ( 𝑢 (,) 𝑤 ) → ∫ 𝑠 ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) |
339 |
338
|
fveq2d |
⊢ ( 𝑠 = ( 𝑢 (,) 𝑤 ) → ( abs ‘ ∫ 𝑠 ( 𝐹 ‘ 𝑡 ) d 𝑡 ) = ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ) |
340 |
|
eleq2 |
⊢ ( 𝑠 = ( 𝑢 (,) 𝑤 ) → ( 𝑡 ∈ 𝑠 ↔ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) ) |
341 |
340
|
ifbid |
⊢ ( 𝑠 = ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) |
342 |
341
|
mpteq2dv |
⊢ ( 𝑠 = ( 𝑢 (,) 𝑤 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) |
343 |
342
|
fveq2d |
⊢ ( 𝑠 = ( 𝑢 (,) 𝑤 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
344 |
339 343
|
breq12d |
⊢ ( 𝑠 = ( 𝑢 (,) 𝑤 ) → ( ( abs ‘ ∫ 𝑠 ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ↔ ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) ) |
345 |
344
|
rspccva |
⊢ ( ( ∀ 𝑠 ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ( abs ‘ ∫ 𝑠 ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∧ ( 𝑢 (,) 𝑤 ) ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
346 |
9 337 345
|
syl2an |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
347 |
346
|
3adantr3 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
348 |
325 347
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
349 |
348
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
350 |
|
subcl |
⊢ ( ( ( 𝐺 ‘ 𝑤 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑢 ) ∈ ℂ ) → ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ∈ ℂ ) |
351 |
125 126 350
|
syl2anr |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ∈ ℂ ) |
352 |
351
|
anandis |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ∈ ℂ ) |
353 |
352
|
abscld |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ∈ ℝ ) |
354 |
353
|
rexrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ∈ ℝ* ) |
355 |
354
|
3adantr3 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ∈ ℝ* ) |
356 |
355
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ∈ ℝ* ) |
357 |
164
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ* ) |
358 |
209
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → 𝑦 ∈ ℝ* ) |
359 |
|
xrlelttr |
⊢ ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ∈ ℝ* ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
360 |
356 357 358 359
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
361 |
349 360
|
mpand |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
362 |
252 361
|
sylanl1 |
⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
363 |
362
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
364 |
251 363
|
mpd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) |
365 |
364
|
ex |
⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
366 |
103 113 116 132 365
|
wlogle |
⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
367 |
366
|
anassrs |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
368 |
93 367
|
sylanb |
⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
369 |
368
|
ralrimiva |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
370 |
|
breq2 |
⊢ ( 𝑧 = ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) ) |
371 |
370
|
rspceaimv |
⊢ ( ( ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
372 |
82 369 371
|
syl2anc |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
373 |
|
ralnex |
⊢ ( ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ¬ 𝑟 ≠ 0 ↔ ¬ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) |
374 |
|
nne |
⊢ ( ¬ 𝑟 ≠ 0 ↔ 𝑟 = 0 ) |
375 |
374
|
ralbii |
⊢ ( ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) ¬ 𝑟 ≠ 0 ↔ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) |
376 |
373 375
|
bitr3i |
⊢ ( ¬ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ↔ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) |
377 |
17
|
ffnd |
⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 Fn ℝ ) |
378 |
|
fnfvelrn |
⊢ ( ( 𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ran 𝑓 ) |
379 |
377 378
|
sylan |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ran 𝑓 ) |
380 |
|
elun1 |
⊢ ( ( 𝑓 ‘ 𝑡 ) ∈ ran 𝑓 → ( 𝑓 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) |
381 |
379 380
|
syl |
⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) |
382 |
|
eqeq1 |
⊢ ( 𝑟 = ( 𝑓 ‘ 𝑡 ) → ( 𝑟 = 0 ↔ ( 𝑓 ‘ 𝑡 ) = 0 ) ) |
383 |
382
|
rspcva |
⊢ ( ( ( 𝑓 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( 𝑓 ‘ 𝑡 ) = 0 ) |
384 |
381 383
|
sylan |
⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( 𝑓 ‘ 𝑡 ) = 0 ) |
385 |
384
|
adantllr |
⊢ ( ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( 𝑓 ‘ 𝑡 ) = 0 ) |
386 |
20
|
ffnd |
⊢ ( 𝑔 ∈ dom ∫1 → 𝑔 Fn ℝ ) |
387 |
|
fnfvelrn |
⊢ ( ( 𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ran 𝑔 ) |
388 |
386 387
|
sylan |
⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ran 𝑔 ) |
389 |
|
elun2 |
⊢ ( ( 𝑔 ‘ 𝑡 ) ∈ ran 𝑔 → ( 𝑔 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) |
390 |
388 389
|
syl |
⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ) |
391 |
|
eqeq1 |
⊢ ( 𝑟 = ( 𝑔 ‘ 𝑡 ) → ( 𝑟 = 0 ↔ ( 𝑔 ‘ 𝑡 ) = 0 ) ) |
392 |
391
|
rspcva |
⊢ ( ( ( 𝑔 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( 𝑔 ‘ 𝑡 ) = 0 ) |
393 |
392
|
oveq2d |
⊢ ( ( ( 𝑔 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( i · ( 𝑔 ‘ 𝑡 ) ) = ( i · 0 ) ) |
394 |
|
it0e0 |
⊢ ( i · 0 ) = 0 |
395 |
393 394
|
eqtrdi |
⊢ ( ( ( 𝑔 ‘ 𝑡 ) ∈ ( ran 𝑓 ∪ ran 𝑔 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( i · ( 𝑔 ‘ 𝑡 ) ) = 0 ) |
396 |
390 395
|
sylan |
⊢ ( ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( i · ( 𝑔 ‘ 𝑡 ) ) = 0 ) |
397 |
396
|
adantlll |
⊢ ( ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( i · ( 𝑔 ‘ 𝑡 ) ) = 0 ) |
398 |
385 397
|
oveq12d |
⊢ ( ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) = ( 0 + 0 ) ) |
399 |
398
|
an32s |
⊢ ( ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) = ( 0 + 0 ) ) |
400 |
|
00id |
⊢ ( 0 + 0 ) = 0 |
401 |
399 400
|
eqtrdi |
⊢ ( ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) = 0 ) |
402 |
401
|
adantlll |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) = 0 ) |
403 |
402
|
oveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − 0 ) ) |
404 |
|
0cnd |
⊢ ( ( 𝜑 ∧ ¬ 𝑡 ∈ 𝐷 ) → 0 ∈ ℂ ) |
405 |
149 404
|
ifclda |
⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ∈ ℂ ) |
406 |
405
|
subid1d |
⊢ ( 𝜑 → ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − 0 ) = if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) |
407 |
406
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − 0 ) = if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) |
408 |
403 407
|
eqtrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) |
409 |
408
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( abs ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) ) |
410 |
|
fvif |
⊢ ( abs ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , ( abs ‘ 0 ) ) |
411 |
|
abs0 |
⊢ ( abs ‘ 0 ) = 0 |
412 |
|
ifeq2 |
⊢ ( ( abs ‘ 0 ) = 0 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , ( abs ‘ 0 ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) |
413 |
411 412
|
ax-mp |
⊢ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , ( abs ‘ 0 ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) |
414 |
410 413
|
eqtri |
⊢ ( abs ‘ if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) |
415 |
409 414
|
eqtrdi |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) |
416 |
415
|
mpteq2dva |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) |
417 |
416
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) = ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
418 |
417
|
breq1d |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ↔ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ) |
419 |
418
|
biimpd |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ) |
420 |
419
|
ex |
⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ) ) |
421 |
420
|
com23 |
⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) → ( ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ) ) |
422 |
421
|
imp32 |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) |
423 |
422
|
anasss |
⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) |
424 |
423
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) |
425 |
|
1rp |
⊢ 1 ∈ ℝ+ |
426 |
425
|
ne0ii |
⊢ ℝ+ ≠ ∅ |
427 |
352
|
anassrs |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ∈ ℂ ) |
428 |
427
|
abscld |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ∈ ℝ ) |
429 |
428
|
adantlrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ∈ ℝ ) |
430 |
429
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ∈ ℝ ) |
431 |
|
rpre |
⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ ) |
432 |
431
|
rehalfcld |
⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ ) |
433 |
432
|
adantl |
⊢ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) ∈ ℝ ) |
434 |
433
|
ad3antlr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 / 2 ) ∈ ℝ ) |
435 |
431
|
adantl |
⊢ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ ) |
436 |
435
|
ad3antlr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑦 ∈ ℝ ) |
437 |
430
|
rexrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ∈ ℝ* ) |
438 |
157
|
a1i |
⊢ ( ( 𝜑 ∧ ¬ 𝑡 ∈ 𝐷 ) → 0 ∈ ( 0 [,] +∞ ) ) |
439 |
154 438
|
ifclda |
⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
440 |
439
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
441 |
440
|
fmpttd |
⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
442 |
|
itg2cl |
⊢ ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ* ) |
443 |
441 442
|
syl |
⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ* ) |
444 |
443
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ* ) |
445 |
434
|
rexrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 / 2 ) ∈ ℝ* ) |
446 |
109 108
|
oveqan12rd |
⊢ ( ( 𝑏 = 𝑢 ∧ 𝑎 = 𝑤 ) → ( ( 𝐺 ‘ 𝑎 ) − ( 𝐺 ‘ 𝑏 ) ) = ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) |
447 |
446
|
fveq2d |
⊢ ( ( 𝑏 = 𝑢 ∧ 𝑎 = 𝑤 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑎 ) − ( 𝐺 ‘ 𝑏 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ) |
448 |
447
|
breq1d |
⊢ ( ( 𝑏 = 𝑢 ∧ 𝑎 = 𝑤 ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑎 ) − ( 𝐺 ‘ 𝑏 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) ) |
449 |
99 98
|
oveqan12rd |
⊢ ( ( 𝑏 = 𝑤 ∧ 𝑎 = 𝑢 ) → ( ( 𝐺 ‘ 𝑎 ) − ( 𝐺 ‘ 𝑏 ) ) = ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) |
450 |
449
|
fveq2d |
⊢ ( ( 𝑏 = 𝑤 ∧ 𝑎 = 𝑢 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑎 ) − ( 𝐺 ‘ 𝑏 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) |
451 |
450
|
breq1d |
⊢ ( ( 𝑏 = 𝑤 ∧ 𝑎 = 𝑢 ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑎 ) − ( 𝐺 ‘ 𝑏 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) ) |
452 |
129
|
breq1d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑢 ) − ( 𝐺 ‘ 𝑤 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) ) |
453 |
321
|
abscld |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ∈ ℝ ) |
454 |
453
|
rexrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ∈ ℝ* ) |
455 |
443
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ ℝ* ) |
456 |
441
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
457 |
|
breq2 |
⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) → ( if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) |
458 |
|
breq2 |
⊢ ( 0 = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) → ( if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ 0 ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) |
459 |
150
|
leidd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) |
460 |
|
breq1 |
⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) |
461 |
|
breq1 |
⊢ ( 0 = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) → ( 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) |
462 |
460 461
|
ifboth |
⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∧ 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) |
463 |
459 152 462
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) |
464 |
463
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ 𝐷 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) |
465 |
147
|
ssneld |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ¬ 𝑡 ∈ 𝐷 → ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) ) |
466 |
465
|
imp |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡 ∈ 𝐷 ) → ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) |
467 |
226 224
|
eqbrtrdi |
⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ 0 ) |
468 |
466 467
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡 ∈ 𝐷 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ 0 ) |
469 |
457 458 464 468
|
ifbothda |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) |
470 |
469
|
ralrimivw |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) |
471 |
233 234
|
ifex |
⊢ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ V |
472 |
471
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ V ) |
473 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) |
474 |
232 236 472 240 473
|
ofrfval2 |
⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) |
475 |
474
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) |
476 |
470 475
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) |
477 |
|
itg2le |
⊢ ( ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
478 |
161 456 476 477
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
479 |
454 163 455 346 478
|
xrletrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
480 |
479
|
3adantr3 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( abs ‘ ∫ ( 𝑢 (,) 𝑤 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
481 |
325 480
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
482 |
448 451 115 452 481
|
wlogle |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
483 |
482
|
anassrs |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
484 |
483
|
adantlrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
485 |
484
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ) |
486 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) |
487 |
437 444 445 485 486
|
xrlelttrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < ( 𝑦 / 2 ) ) |
488 |
|
rphalflt |
⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) < 𝑦 ) |
489 |
488
|
adantl |
⊢ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) < 𝑦 ) |
490 |
489
|
ad3antlr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 / 2 ) < 𝑦 ) |
491 |
430 434 436 487 490
|
lttrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) |
492 |
491
|
a1d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
493 |
492
|
ralrimiva |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) → ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
494 |
493
|
ralrimivw |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) → ∀ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
495 |
|
r19.2z |
⊢ ( ( ℝ+ ≠ ∅ ∧ ∀ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
496 |
426 494 495
|
sylancr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) < ( 𝑦 / 2 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
497 |
424 496
|
syldan |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
498 |
497
|
anassrs |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
499 |
498
|
anassrs |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∀ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 = 0 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
500 |
376 499
|
sylan2b |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ¬ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
501 |
372 500
|
pm2.61dan |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
502 |
501
|
ex |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) ) |
503 |
502
|
rexlimdvva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) → ( ∃ 𝑓 ∈ dom ∫1 ∃ 𝑔 ∈ dom ∫1 ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) ) |
504 |
14 503
|
mpd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ℝ+ ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
505 |
504
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) |
506 |
|
ssid |
⊢ ℂ ⊆ ℂ |
507 |
|
elcncf2 |
⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ↔ ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) ) ) |
508 |
118 506 507
|
sylancl |
⊢ ( 𝜑 → ( 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ↔ ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ∀ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑤 − 𝑢 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑢 ) ) ) < 𝑦 ) ) ) ) |
509 |
10 505 508
|
mpbir2and |
⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) |