Step | Hyp | Ref
| Expression |
1 | | ftc1anc.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) |
2 | | ftc1anc.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | | ftc1anc.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | | ftc1anc.le |
. . 3
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
5 | | ftc1anc.s |
. . 3
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) |
6 | | ftc1anc.d |
. . 3
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
7 | | ftc1anc.i |
. . 3
⊢ (𝜑 → 𝐹 ∈
𝐿1) |
8 | | ftc1anc.f |
. . 3
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | ftc1lem2 23603 |
. 2
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
10 | | rphalfcl 11734 |
. . . . . 6
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ+) |
11 | 1, 2, 3, 4, 5, 6, 7, 8 | ftc1anclem6 32660 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 / 2) ∈ ℝ+) →
∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) |
12 | 10, 11 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) |
13 | 12 | adantrl 748 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) →
∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) |
14 | 10 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (𝑦 / 2) ∈
ℝ+) |
15 | | 2rp 11713 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ+ |
16 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
17 | | frn 5966 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:ℝ⟶ℝ →
ran 𝑓 ⊆
ℝ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ dom ∫1
→ ran 𝑓 ⊆
ℝ) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ran 𝑓 ⊆ ℝ) |
20 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 ∈ dom ∫1
→ 𝑔:ℝ⟶ℝ) |
21 | | frn 5966 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔:ℝ⟶ℝ →
ran 𝑔 ⊆
ℝ) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 ∈ dom ∫1
→ ran 𝑔 ⊆
ℝ) |
23 | 22 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ran 𝑔 ⊆ ℝ) |
24 | 19, 23 | unssd 3751 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℝ) |
25 | | ax-resscn 9872 |
. . . . . . . . . . . . . . . . . 18
⊢ ℝ
⊆ ℂ |
26 | 24, 25 | syl6ss 3580 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ) |
27 | | i1f0rn 23255 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ 0 ∈ ran 𝑓) |
28 | | elun1 3742 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
ran 𝑓 → 0 ∈ (ran
𝑓 ∪ ran 𝑔)) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ dom ∫1
→ 0 ∈ (ran 𝑓
∪ ran 𝑔)) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 0 ∈ (ran 𝑓 ∪ ran 𝑔)) |
31 | | absf 13925 |
. . . . . . . . . . . . . . . . . . 19
⊢
abs:ℂ⟶ℝ |
32 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ abs Fn
ℂ |
34 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . . 18
⊢ ((abs Fn
ℂ ∧ (ran 𝑓 ∪
ran 𝑔) ⊆ ℂ
∧ 0 ∈ (ran 𝑓 ∪
ran 𝑔)) →
(abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
35 | 33, 34 | mp3an1 1403 |
. . . . . . . . . . . . . . . . 17
⊢ (((ran
𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈
(ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈
(abs “ (ran 𝑓 ∪
ran 𝑔))) |
36 | 26, 30, 35 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
37 | | ne0i 3880 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅) |
39 | | imassrn 5396 |
. . . . . . . . . . . . . . . . 17
⊢ (abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ran
abs |
40 | | frn 5966 |
. . . . . . . . . . . . . . . . . 18
⊢
(abs:ℂ⟶ℝ → ran abs ⊆
ℝ) |
41 | 31, 40 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ran abs
⊆ ℝ |
42 | 39, 41 | sstri 3577 |
. . . . . . . . . . . . . . . 16
⊢ (abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆
ℝ |
43 | | ffun 5961 |
. . . . . . . . . . . . . . . . . 18
⊢
(abs:ℂ⟶ℝ → Fun abs) |
44 | 31, 43 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ Fun
abs |
45 | | i1frn 23250 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ dom ∫1
→ ran 𝑓 ∈
Fin) |
46 | | i1frn 23250 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 ∈ dom ∫1
→ ran 𝑔 ∈
Fin) |
47 | | unfi 8112 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ran
𝑓 ∈ Fin ∧ ran
𝑔 ∈ Fin) → (ran
𝑓 ∪ ran 𝑔) ∈ Fin) |
48 | 45, 46, 47 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin) |
49 | | imafi 8142 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun abs
∧ (ran 𝑓 ∪ ran
𝑔) ∈ Fin) → (abs
“ (ran 𝑓 ∪ ran
𝑔)) ∈
Fin) |
50 | 44, 48, 49 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin) |
51 | | fimaxre2 10848 |
. . . . . . . . . . . . . . . 16
⊢ (((abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ℝ ∧
(abs “ (ran 𝑓 ∪
ran 𝑔)) ∈ Fin) →
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) |
52 | 42, 50, 51 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥) |
53 | | suprcl 10862 |
. . . . . . . . . . . . . . . 16
⊢ (((abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ℝ ∧
(abs “ (ran 𝑓 ∪
ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
54 | 42, 53 | mp3an1 1403 |
. . . . . . . . . . . . . . 15
⊢ (((abs
“ (ran 𝑓 ∪ ran
𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
55 | 38, 52, 54 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
56 | 55 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
57 | | 0red 9920 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → 0 ∈
ℝ) |
58 | 26 | sselda 3568 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → 𝑟 ∈
ℂ) |
59 | 58 | abscld 14023 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (abs‘𝑟) ∈
ℝ) |
60 | 59 | adantrr 749 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ∈
ℝ) |
61 | 55 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
62 | | absgt0 13912 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ℂ → (𝑟 ≠ 0 ↔ 0 <
(abs‘𝑟))) |
63 | 58, 62 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (𝑟 ≠ 0 ↔ 0 <
(abs‘𝑟))) |
64 | 63 | biimpd 218 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (𝑟 ≠ 0 → 0 <
(abs‘𝑟))) |
65 | 64 | impr 647 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → 0 < (abs‘𝑟)) |
66 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ) |
67 | 66, 38, 52 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran
𝑓 ∪ ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥)) |
68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → ((abs “
(ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs
“ (ran 𝑓 ∪ ran
𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥)) |
69 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((abs Fn
ℂ ∧ (ran 𝑓 ∪
ran 𝑔) ⊆ ℂ
∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
70 | 33, 69 | mp3an1 1403 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((ran
𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
71 | 26, 70 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
72 | | suprub 10863 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ℝ ∧
(abs “ (ran 𝑓 ∪
ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) ∧ (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) |
73 | 68, 71, 72 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (abs‘𝑟) ≤ sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)) |
74 | 73 | adantrr 749 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ≤ sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)) |
75 | 57, 60, 61, 65, 74 | ltletrd 10076 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → 0 < sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)) |
76 | 75 | rexlimdvaa 3014 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 → 0 < sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))) |
77 | 76 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 0 < sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)) |
78 | 56, 77 | elrpd 11745 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ+) |
79 | | rpmulcl 11731 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ+ ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) |
80 | 15, 78, 79 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) |
81 | | rpdivcl 11732 |
. . . . . . . . . . 11
⊢ (((𝑦 / 2) ∈ ℝ+
∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ+) |
82 | 14, 80, 81 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)) → ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ+) |
83 | 82 | anassrs 678 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ+) |
84 | 83 | adantlr 747 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ+) |
85 | | ancom 465 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) ↔ (𝑦 ∈ ℝ+
∧ 𝑢 ∈ (𝐴[,]𝐵))) |
86 | 85 | anbi2i 726 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑓 ∈ 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) ∧ (𝑦 ∈ ℝ+ ∧ 𝑢 ∈ (𝐴[,]𝐵)))) |
87 | | an32 835 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ↔ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈
ℝ+))) |
88 | 87 | anbi1i 727 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2))) |
89 | | an32 835 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈
ℝ+))) |
90 | 88, 89 | bitri 263 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈
ℝ+))) |
91 | 90 | anbi1i 727 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ 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 | | an32 835 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓 ∈ 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 | 91, 92 | bitri 263 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ 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 | | anass 679 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑓 ∈ 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) ∧ (𝑦 ∈ ℝ+ ∧ 𝑢 ∈ (𝐴[,]𝐵)))) |
95 | 86, 93, 94 | 3bitr4i 291 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ 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) ∧ 𝑦 ∈ ℝ+) ∧ 𝑢 ∈ (𝐴[,]𝐵))) |
96 | | oveq12 6558 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → (𝑏 − 𝑎) = (𝑤 − 𝑢)) |
97 | 96 | ancoms 468 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (𝑏 − 𝑎) = (𝑤 − 𝑢)) |
98 | 97 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (abs‘(𝑏 − 𝑎)) = (abs‘(𝑤 − 𝑢))) |
99 | 98 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔
(abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))))) |
100 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑤 → (𝐺‘𝑏) = (𝐺‘𝑤)) |
101 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑢 → (𝐺‘𝑎) = (𝐺‘𝑢)) |
102 | 100, 101 | oveqan12rd 6569 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((𝐺‘𝑏) − (𝐺‘𝑎)) = ((𝐺‘𝑤) − (𝐺‘𝑢))) |
103 | 102 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) = (abs‘((𝐺‘𝑤) − (𝐺‘𝑢)))) |
104 | 103 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦 ↔ (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
105 | 99, 104 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦) ↔ ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))) |
106 | | oveq12 6558 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → (𝑏 − 𝑎) = (𝑢 − 𝑤)) |
107 | 106 | ancoms 468 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (𝑏 − 𝑎) = (𝑢 − 𝑤)) |
108 | 107 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (abs‘(𝑏 − 𝑎)) = (abs‘(𝑢 − 𝑤))) |
109 | 108 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔
(abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))))) |
110 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑢 → (𝐺‘𝑏) = (𝐺‘𝑢)) |
111 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑤 → (𝐺‘𝑎) = (𝐺‘𝑤)) |
112 | 110, 111 | oveqan12rd 6569 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((𝐺‘𝑏) − (𝐺‘𝑎)) = ((𝐺‘𝑢) − (𝐺‘𝑤))) |
113 | 112 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤)))) |
114 | 113 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦 ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦)) |
115 | 109, 114 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦) ↔ ((abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦))) |
116 | | iccssre 12126 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
117 | 2, 3, 116 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
118 | 117 | ad4antr 764 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝐴[,]𝐵) ⊆ ℝ) |
119 | | simp-4l 802 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → 𝜑) |
120 | 117, 25 | syl6ss 3580 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
121 | 120 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℂ) |
122 | 120 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℂ) |
123 | | abssub 13914 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ) →
(abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤))) |
124 | 121, 122,
123 | syl2anr 494 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤))) |
125 | 124 | anandis 869 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤))) |
126 | 125 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔
(abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))))) |
127 | 9 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑤) ∈ ℂ) |
128 | 9 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑢) ∈ ℂ) |
129 | | abssub 13914 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺‘𝑤) ∈ ℂ ∧ (𝐺‘𝑢) ∈ ℂ) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤)))) |
130 | 127, 128,
129 | syl2anr 494 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤)))) |
131 | 130 | anandis 869 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤)))) |
132 | 131 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦 ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦)) |
133 | 126, 132 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) ↔ ((abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦))) |
134 | 119, 133 | sylan 487 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑓 ∈ 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‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦))) |
135 | 2 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
136 | 3 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
137 | 135, 136 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
138 | | df-icc 12053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ [,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦)}) |
139 | 138 | elixx3g 12059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑢 ∈
ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))) |
140 | 139 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)) |
141 | 140 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑢) |
142 | 138 | elixx3g 12059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) ∧ (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵))) |
143 | 142 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵)) |
144 | 143 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ≤ 𝐵) |
145 | 141, 144 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) |
146 | | ioossioo 12136 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵)) |
147 | 137, 145,
146 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵)) |
148 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷) |
149 | 147, 148 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷) |
150 | 149 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷) |
151 | 8 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
152 | 151 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ ℝ) |
153 | 152 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈
ℝ*) |
154 | 151 | absge0d 14031 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(𝐹‘𝑡))) |
155 | | elxrge0 12152 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((abs‘(𝐹‘𝑡)) ∈ (0[,]+∞) ↔
((abs‘(𝐹‘𝑡)) ∈ ℝ*
∧ 0 ≤ (abs‘(𝐹‘𝑡)))) |
156 | 153, 154,
155 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞)) |
157 | 156 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞)) |
158 | 150, 157 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞)) |
159 | | 0e0iccpnf 12154 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
(0[,]+∞) |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈
(0[,]+∞)) |
161 | 158, 160 | ifclda 4070 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈
(0[,]+∞)) |
162 | 161 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈
(0[,]+∞)) |
163 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) |
164 | 162, 163 | fmptd 6292 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)),
0)):ℝ⟶(0[,]+∞)) |
165 | | itg2cl 23305 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
167 | 166 | 3adantr3 1215 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
168 | 119, 167 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
169 | 168 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
170 | | simplll 794 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom
∫1))) |
171 | 151 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
172 | 150, 171 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ) |
173 | 172 | adantllr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ) |
174 | | elioore 12076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ) |
175 | 16 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈
ℝ) |
176 | 175 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈
ℂ) |
177 | | ax-icn 9874 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ i ∈
ℂ |
178 | 20 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℝ) |
179 | 178 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℂ) |
180 | | mulcl 9899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((i
∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ) |
181 | 177, 179,
180 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (i · (𝑔‘𝑡)) ∈ ℂ) |
182 | | addcl 9897 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
183 | 176, 181,
182 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝑔 ∈ dom
∫1 ∧ 𝑡
∈ ℝ)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
184 | 183 | anandirs 870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
185 | 174, 184 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
186 | 185 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
187 | 186 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
188 | 173, 187 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ) |
189 | 188 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ) |
190 | 185 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ) |
191 | 190 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ) |
192 | 191 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ) |
193 | 189, 192 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ) |
194 | 193 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈
ℝ*) |
195 | 188 | absge0d 14031 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
196 | 184 | absge0d 14031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
197 | 174, 196 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → 0 ≤
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
198 | 197 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
199 | 198 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
200 | 189, 192,
195, 199 | addge0d 10482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
201 | | elxrge0 12152 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔
(((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
202 | 194, 200,
201 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞)) |
203 | 159 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈
(0[,]+∞)) |
204 | 202, 203 | ifclda 4070 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
(0[,]+∞)) |
205 | 204 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
(0[,]+∞)) |
206 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
207 | 205, 206 | fmptd 6292 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))),
0)):ℝ⟶(0[,]+∞)) |
208 | | itg2cl 23305 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞)
→ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈
ℝ*) |
209 | 207, 208 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈
ℝ*) |
210 | 209 | 3adantr3 1215 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈
ℝ*) |
211 | 170, 210 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈
ℝ*) |
212 | 211 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑓 ∈ 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))) ∈
ℝ*) |
213 | | rpxr 11716 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ*) |
214 | 213 | ad3antlr 763 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
𝑦 ∈
ℝ*) |
215 | 161 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈
(0[,]+∞)) |
216 | 215 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈
(0[,]+∞)) |
217 | 216, 163 | fmptd 6292 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)),
0)):ℝ⟶(0[,]+∞)) |
218 | 173, 187 | npcand 10275 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (𝐹‘𝑡)) |
219 | 218 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘(𝐹‘𝑡))) |
220 | 188, 187 | abstrid 14043 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
221 | 219, 220 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹‘𝑡)) ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
222 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = (abs‘(𝐹‘𝑡))) |
223 | 222 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = (abs‘(𝐹‘𝑡))) |
224 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
225 | 224 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
226 | 221, 223,
225 | 3brtr4d 4615 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
227 | 226 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
228 | | 0le0 10987 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ≤
0 |
229 | 228 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → 0 ≤ 0) |
230 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = 0) |
231 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0) |
232 | 229, 230,
231 | 3brtr4d 4615 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
233 | 227, 232 | pm2.61d1 170 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
234 | 233 | ralrimivw 2950 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
235 | | reex 9906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℝ
∈ V |
236 | 235 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ℝ ∈
V) |
237 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(abs‘(𝐹‘𝑡)) ∈ V |
238 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
V |
239 | 237, 238 | ifex 4106 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ V |
240 | 239 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ V) |
241 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V |
242 | 241, 238 | ifex 4106 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V |
243 | 242 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V) |
244 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) |
245 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
246 | 236, 240,
243, 244, 245 | ofrfval2 6813 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
247 | 246 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
248 | 234, 247 | mpbird 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
249 | | itg2le 23312 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞)
∧ (𝑡 ∈ ℝ
↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) |
250 | 217, 207,
248, 249 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) |
251 | 250 | 3adantr3 1215 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) |
252 | 170, 251 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) |
253 | 252 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑓 ∈ 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)))) |
254 | 1, 2, 3, 4, 5, 6, 7, 8 | ftc1anclem8 32662 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑓 ∈ 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))) < 𝑦) |
255 | 169, 212,
214, 253, 254 | xrlelttrd 11867 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦) |
256 | | simplll 794 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 𝜑) |
257 | | simpr2 1061 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑤 ∈ (𝐴[,]𝐵)) |
258 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑤 → (𝐴(,)𝑥) = (𝐴(,)𝑤)) |
259 | | itgeq1 23345 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴(,)𝑥) = (𝐴(,)𝑤) → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡) |
260 | 258, 259 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑤 → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡) |
261 | | itgex 23343 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡 ∈ V |
262 | 260, 1, 261 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐺‘𝑤) = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡) |
263 | 257, 262 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑤) = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡) |
264 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝐴 ∈ ℝ) |
265 | 117 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ) |
266 | 265 | 3ad2antr2 1220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑤 ∈ ℝ) |
267 | 117 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ) |
268 | 267 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ*) |
269 | 268 | 3ad2antr1 1219 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ ℝ*) |
270 | | elicc1 12090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))) |
271 | 135, 136,
270 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))) |
272 | 271 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)) |
273 | 272 | simp2d 1067 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑢) |
274 | 273 | 3ad2antr1 1219 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝐴 ≤ 𝑢) |
275 | | simpr3 1062 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ≤ 𝑤) |
276 | 135 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝐴 ∈
ℝ*) |
277 | 265 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ*) |
278 | | elicc1 12090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤))) |
279 | 276, 277,
278 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤))) |
280 | 279 | 3ad2antr2 1220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤))) |
281 | 269, 274,
275, 280 | mpbir3and 1238 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ (𝐴[,]𝑤)) |
282 | | iooss2 12082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐵 ∈ ℝ*
∧ 𝑤 ≤ 𝐵) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵)) |
283 | 136, 144,
282 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵)) |
284 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝐵) ⊆ 𝐷) |
285 | 283, 284 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ 𝐷) |
286 | 285 | 3ad2antr2 1220 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐴(,)𝑤) ⊆ 𝐷) |
287 | 286 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → 𝑡 ∈ 𝐷) |
288 | 151 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
289 | 287, 288 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ) |
290 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 = 𝑢 → (𝑤 ∈ (𝐴[,]𝐵) ↔ 𝑢 ∈ (𝐴[,]𝐵))) |
291 | 290 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = 𝑢 → ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)))) |
292 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 = 𝑢 → (𝐴(,)𝑤) = (𝐴(,)𝑢)) |
293 | 292 | mpteq1d 4666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 = 𝑢 → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) = (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡))) |
294 | 293 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = 𝑢 → ((𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔ (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈
𝐿1)) |
295 | 291, 294 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = 𝑢 → (((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1) ↔
((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈
𝐿1))) |
296 | | ioombl 23140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴(,)𝑤) ∈ dom vol |
297 | 296 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ∈ dom vol) |
298 | 151 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
299 | 8 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))) |
300 | 299, 7 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
301 | 300 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
302 | 285, 297,
298, 301 | iblss 23377 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
303 | 295, 302 | chvarv 2251 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
304 | 303 | 3ad2antr1 1219 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
305 | | ioombl 23140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢(,)𝑤) ∈ dom vol |
306 | 305 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ∈ dom vol) |
307 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹‘𝑡) ∈ V |
308 | 307 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ V) |
309 | 300 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
310 | 149, 306,
308, 309 | iblss 23377 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
311 | 310 | 3adantr3 1215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
312 | 264, 266,
281, 289, 304, 311 | itgsplitioo 23410 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡 = (∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)) |
313 | 263, 312 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑤) = (∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)) |
314 | | simpr1 1060 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ (𝐴[,]𝐵)) |
315 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑢 → (𝐴(,)𝑥) = (𝐴(,)𝑢)) |
316 | | itgeq1 23345 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴(,)𝑥) = (𝐴(,)𝑢) → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) |
317 | 315, 316 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑢 → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) |
318 | | itgex 23343 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ V |
319 | 317, 1, 318 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐺‘𝑢) = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) |
320 | 314, 319 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑢) = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) |
321 | 313, 320 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) = ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)) |
322 | 307 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑢)) → (𝐹‘𝑡) ∈ V) |
323 | 322, 303 | itgcl 23356 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ ℂ) |
324 | 323 | adantrr 749 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ ℂ) |
325 | 307 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ V) |
326 | 325, 310 | itgcl 23356 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡 ∈ ℂ) |
327 | 324, 326 | pncan2d 10273 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) |
328 | 327 | 3adantr3 1215 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) |
329 | 321, 328 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) |
330 | 329 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)) |
331 | | ftc1anc.t |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0)))) |
332 | | df-ov 6552 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢(,)𝑤) = ((,)‘〈𝑢, 𝑤〉) |
333 | | opelxpi 5072 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 〈𝑢, 𝑤〉 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) |
334 | | ioof 12142 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
335 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
336 | 334, 335 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (,) Fn
(ℝ* × ℝ*) |
337 | | iccssxr 12127 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴[,]𝐵) ⊆
ℝ* |
338 | | xpss12 5148 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴[,]𝐵) ⊆ ℝ* ∧ (𝐴[,]𝐵) ⊆ ℝ*) →
((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* ×
ℝ*)) |
339 | 337, 337,
338 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* ×
ℝ*) |
340 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* ×
ℝ*) ∧ 〈𝑢, 𝑤〉 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((,)‘〈𝑢, 𝑤〉) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) |
341 | 336, 339,
340 | mp3an12 1406 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑢, 𝑤〉 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘〈𝑢, 𝑤〉) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) |
342 | 333, 341 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((,)‘〈𝑢, 𝑤〉) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) |
343 | 332, 342 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) |
344 | | itgeq1 23345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 = (𝑢(,)𝑤) → ∫𝑠(𝐹‘𝑡) d𝑡 = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) |
345 | 344 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 = (𝑢(,)𝑤) → (abs‘∫𝑠(𝐹‘𝑡) d𝑡) = (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)) |
346 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ 𝑠 ↔ 𝑡 ∈ (𝑢(,)𝑤))) |
347 | 346 | ifbid 4058 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑠 = (𝑢(,)𝑤) → if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) |
348 | 347 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) |
349 | 348 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 = (𝑢(,)𝑤) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))) |
350 | 345, 349 | breq12d 4596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = (𝑢(,)𝑤) → ((abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))) |
351 | 350 | rspccva 3281 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑠 ∈
((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) ∧ (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))) |
352 | 331, 343,
351 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))) |
353 | 352 | 3adantr3 1215 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))) |
354 | 330, 353 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))) |
355 | 354 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))) |
356 | | subcl 10159 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺‘𝑤) ∈ ℂ ∧ (𝐺‘𝑢) ∈ ℂ) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ) |
357 | 127, 128,
356 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ) |
358 | 357 | anandis 869 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ) |
359 | 358 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ) |
360 | 359 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈
ℝ*) |
361 | 360 | 3adantr3 1215 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈
ℝ*) |
362 | 361 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈
ℝ*) |
363 | 167 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
364 | 213 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑦 ∈ ℝ*) |
365 | | xrlelttr 11863 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ* ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ* ∧
𝑦 ∈
ℝ*) → (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
366 | 362, 363,
364, 365 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
367 | 355, 366 | mpand 707 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
368 | 256, 367 | sylanl1 680 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
369 | 368 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑓 ∈ 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‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
370 | 255, 369 | mpd 15 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) |
371 | 370 | ex 449 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
372 | 105, 115,
118, 134, 371 | wlogle 10440 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
373 | 372 | anassrs 678 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
374 | 95, 373 | sylanb 488 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
375 | 374 | ralrimiva 2949 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
376 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑧 = ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
((abs‘(𝑤 −
𝑢)) < 𝑧 ↔ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))))) |
377 | 376 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑧 = ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(((abs‘(𝑤 −
𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) ↔ ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))) |
378 | 377 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑧 = ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) ↔ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))) |
379 | 378 | rspcev 3282 |
. . . . . . . 8
⊢ ((((𝑦 / 2) / (2 · sup((abs
“ (ran 𝑓 ∪ ran
𝑔)), ℝ, < )))
∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
380 | 84, 375, 379 | syl2anc 691 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
381 | | ralnex 2975 |
. . . . . . . . 9
⊢
(∀𝑟 ∈
(ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) |
382 | | nne 2786 |
. . . . . . . . . 10
⊢ (¬
𝑟 ≠ 0 ↔ 𝑟 = 0) |
383 | 382 | ralbii 2963 |
. . . . . . . . 9
⊢
(∀𝑟 ∈
(ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) |
384 | 381, 383 | bitr3i 265 |
. . . . . . . 8
⊢ (¬
∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) |
385 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓:ℝ⟶ℝ →
𝑓 Fn
ℝ) |
386 | 16, 385 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓 ∈ dom ∫1
→ 𝑓 Fn
ℝ) |
387 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ran 𝑓) |
388 | 386, 387 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈ ran 𝑓) |
389 | | elun1 3742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑓‘𝑡) ∈ ran 𝑓 → (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
390 | 388, 389 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
391 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑟 = (𝑓‘𝑡) → (𝑟 = 0 ↔ (𝑓‘𝑡) = 0)) |
392 | 391 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0) |
393 | 390, 392 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0) |
394 | 393 | adantllr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0) |
395 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑔:ℝ⟶ℝ →
𝑔 Fn
ℝ) |
396 | 20, 395 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑔 ∈ dom ∫1
→ 𝑔 Fn
ℝ) |
397 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ran 𝑔) |
398 | 396, 397 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈ ran 𝑔) |
399 | | elun2 3743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑔‘𝑡) ∈ ran 𝑔 → (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
400 | 398, 399 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
401 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑟 = (𝑔‘𝑡) → (𝑟 = 0 ↔ (𝑔‘𝑡) = 0)) |
402 | 401 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑔‘𝑡) = 0) |
403 | 402 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = (i · 0)) |
404 | | it0e0 11131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (i
· 0) = 0 |
405 | 403, 404 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0) |
406 | 400, 405 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0) |
407 | 406 | adantlll 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0) |
408 | 394, 407 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = (0 + 0)) |
409 | 408 | an32s 842 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = (0 + 0)) |
410 | | 00id 10090 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 + 0) =
0 |
411 | 409, 410 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = 0) |
412 | 411 | adantlll 750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = 0) |
413 | 412 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0)) |
414 | | 0cnd 9912 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ) |
415 | 151, 414 | ifclda 4070 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ) |
416 | 415 | subid1d 10260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) |
417 | 416 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) |
418 | 413, 417 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) |
419 | 418 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
420 | | fvif 6114 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(abs‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), (abs‘0)) |
421 | | abs0 13873 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(abs‘0) = 0 |
422 | | ifeq2 4041 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((abs‘0) = 0 → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), (abs‘0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) |
423 | 421, 422 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), (abs‘0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) |
424 | 420, 423 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(abs‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) |
425 | 419, 424 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) |
426 | 425 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
427 | 426 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
428 | 427 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))) |
429 | 428 | biimpd 218 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))) |
430 | 429 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∀𝑟 ∈
(ran 𝑓 ∪ ran 𝑔)𝑟 = 0 → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)))) |
431 | 430 | com23 84 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)))) |
432 | 431 | imp32 448 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) |
433 | 432 | anasss 677 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)
∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) |
434 | 433 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) |
435 | | 1rp 11712 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
436 | 435 | ne0ii 3882 |
. . . . . . . . . . . 12
⊢
ℝ+ ≠ ∅ |
437 | 358 | anassrs 678 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ) |
438 | 437 | abscld 14023 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ) |
439 | 438 | adantlrr 753 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ) |
440 | 439 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ) |
441 | | rpre 11715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
442 | 441 | rehalfcld 11156 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ) |
443 | 442 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈
ℝ) |
444 | 443 | ad3antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ) |
445 | 441 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ) |
446 | 445 | ad3antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ) |
447 | 440 | rexrd 9968 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈
ℝ*) |
448 | 159 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈
(0[,]+∞)) |
449 | 156, 448 | ifclda 4070 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈
(0[,]+∞)) |
450 | 449 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈
(0[,]+∞)) |
451 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) |
452 | 450, 451 | fmptd 6292 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)),
0)):ℝ⟶(0[,]+∞)) |
453 | | itg2cl 23305 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
454 | 452, 453 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
455 | 454 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
456 | 444 | rexrd 9968 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈
ℝ*) |
457 | 111, 110 | oveqan12rd 6569 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → ((𝐺‘𝑎) − (𝐺‘𝑏)) = ((𝐺‘𝑤) − (𝐺‘𝑢))) |
458 | 457 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → (abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) = (abs‘((𝐺‘𝑤) − (𝐺‘𝑢)))) |
459 | 458 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → ((abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))) |
460 | 101, 100 | oveqan12rd 6569 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → ((𝐺‘𝑎) − (𝐺‘𝑏)) = ((𝐺‘𝑢) − (𝐺‘𝑤))) |
461 | 460 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → (abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤)))) |
462 | 461 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → ((abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))) |
463 | 131 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))) |
464 | 326 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ∈ ℝ) |
465 | 464 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ∈
ℝ*) |
466 | 454 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
467 | 452 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)),
0)):ℝ⟶(0[,]+∞)) |
468 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((abs‘(𝐹‘𝑡)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
469 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (0 =
if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0 ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
470 | 152 | leidd 10473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡))) |
471 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((abs‘(𝐹‘𝑡)) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) → ((abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))) |
472 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (0 =
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) → (0 ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))) |
473 | 471, 472 | ifboth 4074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)) ∧ 0 ≤ (abs‘(𝐹‘𝑡))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡))) |
474 | 470, 154,
473 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡))) |
475 | 474 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡))) |
476 | 149 | ssneld 3570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (¬ 𝑡 ∈ 𝐷 → ¬ 𝑡 ∈ (𝑢(,)𝑤))) |
477 | 476 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ 𝐷) → ¬ 𝑡 ∈ (𝑢(,)𝑤)) |
478 | 230, 228 | syl6eqbr 4622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0) |
479 | 477, 478 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0) |
480 | 468, 469,
475, 479 | ifbothda 4073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) |
481 | 480 | ralrimivw 2950 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) |
482 | 237, 238 | ifex 4106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ V |
483 | 482 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ V) |
484 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
485 | 236, 240,
483, 244, 484 | ofrfval2 6813 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
486 | 485 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
487 | 481, 486 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
488 | | itg2le 23312 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
489 | 164, 467,
487, 488 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
490 | 465, 166,
466, 352, 489 | xrletrd 11869 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
491 | 490 | 3adantr3 1215 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
492 | 330, 491 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
493 | 459, 462,
117, 463, 492 | wlogle 10440 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
494 | 493 | anassrs 678 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
495 | 494 | adantlrr 753 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
496 | 495 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
497 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) |
498 | 447, 455,
456, 496, 497 | xrlelttrd 11867 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < (𝑦 / 2)) |
499 | | rphalflt 11736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) < 𝑦) |
500 | 499 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) < 𝑦) |
501 | 500 | ad3antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) < 𝑦) |
502 | 440, 444,
446, 498, 501 | lttrd 10077 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) |
503 | 502 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
504 | 503 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
505 | 504 | ralrimivw 2950 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∀𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
506 | | r19.2z 4012 |
. . . . . . . . . . . 12
⊢
((ℝ+ ≠ ∅ ∧ ∀𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
507 | 436, 505,
506 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
508 | 434, 507 | syldan 486 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
509 | 508 | anassrs 678 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
510 | 509 | anassrs 678 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
511 | 384, 510 | sylan2b 491 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
512 | 380, 511 | pm2.61dan 828 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
513 | 512 | ex 449 |
. . . . 5
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))) |
514 | 513 | rexlimdvva 3020 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) →
(∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))) |
515 | 13, 514 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
516 | 515 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
517 | | ssid 3587 |
. . 3
⊢ ℂ
⊆ ℂ |
518 | | elcncf2 22501 |
. . 3
⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝐺 ∈
((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)))) |
519 | 120, 517,
518 | sylancl 693 |
. 2
⊢ (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)))) |
520 | 9, 516, 519 | mpbir2and 959 |
1
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |