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 23799 |
. 2
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
10 | | rphalfcl 11858 |
. . . . . 6
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ+) |
11 | 1, 2, 3, 4, 5, 6, 7, 8 | ftc1anclem6 33490 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 / 2) ∈ ℝ+) →
∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) |
12 | 10, 11 | sylan2 491 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) |
13 | 12 | adantrl 752 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) →
∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) |
14 | 10 | ad2antll 765 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (𝑦 / 2) ∈
ℝ+) |
15 | | 2rp 11837 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ+ |
16 | | i1ff 23443 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
17 | | frn 6053 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:ℝ⟶ℝ →
ran 𝑓 ⊆
ℝ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ dom ∫1
→ ran 𝑓 ⊆
ℝ) |
19 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ran 𝑓 ⊆ ℝ) |
20 | | i1ff 23443 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 ∈ dom ∫1
→ 𝑔:ℝ⟶ℝ) |
21 | | frn 6053 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔:ℝ⟶ℝ →
ran 𝑔 ⊆
ℝ) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 ∈ dom ∫1
→ ran 𝑔 ⊆
ℝ) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ran 𝑔 ⊆ ℝ) |
24 | 19, 23 | unssd 3789 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℝ) |
25 | | ax-resscn 9993 |
. . . . . . . . . . . . . . . . . 18
⊢ ℝ
⊆ ℂ |
26 | 24, 25 | syl6ss 3615 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ) |
27 | | i1f0rn 23449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ 0 ∈ ran 𝑓) |
28 | | elun1 3780 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
ran 𝑓 → 0 ∈ (ran
𝑓 ∪ ran 𝑔)) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ dom ∫1
→ 0 ∈ (ran 𝑓
∪ ran 𝑔)) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 0 ∈ (ran 𝑓 ∪ ran 𝑔)) |
31 | | absf 14077 |
. . . . . . . . . . . . . . . . . . 19
⊢
abs:ℂ⟶ℝ |
32 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ abs Fn
ℂ |
34 | | fnfvima 6496 |
. . . . . . . . . . . . . . . . . 18
⊢ ((abs Fn
ℂ ∧ (ran 𝑓 ∪
ran 𝑔) ⊆ ℂ
∧ 0 ∈ (ran 𝑓 ∪
ran 𝑔)) →
(abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
35 | 33, 34 | mp3an1 1411 |
. . . . . . . . . . . . . . . . 17
⊢ (((ran
𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈
(ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈
(abs “ (ran 𝑓 ∪
ran 𝑔))) |
36 | 26, 30, 35 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
37 | | ne0i 3921 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅) |
39 | | imassrn 5477 |
. . . . . . . . . . . . . . . . 17
⊢ (abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ran
abs |
40 | | frn 6053 |
. . . . . . . . . . . . . . . . . 18
⊢
(abs:ℂ⟶ℝ → ran abs ⊆
ℝ) |
41 | 31, 40 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ran abs
⊆ ℝ |
42 | 39, 41 | sstri 3612 |
. . . . . . . . . . . . . . . 16
⊢ (abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆
ℝ |
43 | | ffun 6048 |
. . . . . . . . . . . . . . . . . 18
⊢
(abs:ℂ⟶ℝ → Fun abs) |
44 | 31, 43 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ Fun
abs |
45 | | i1frn 23444 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ dom ∫1
→ ran 𝑓 ∈
Fin) |
46 | | i1frn 23444 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 ∈ dom ∫1
→ ran 𝑔 ∈
Fin) |
47 | | unfi 8227 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ran
𝑓 ∈ Fin ∧ ran
𝑔 ∈ Fin) → (ran
𝑓 ∪ ran 𝑔) ∈ Fin) |
48 | 45, 46, 47 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin) |
49 | | imafi 8259 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun abs
∧ (ran 𝑓 ∪ ran
𝑔) ∈ Fin) → (abs
“ (ran 𝑓 ∪ ran
𝑔)) ∈
Fin) |
50 | 44, 48, 49 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin) |
51 | | fimaxre2 10969 |
. . . . . . . . . . . . . . . 16
⊢ (((abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ℝ ∧
(abs “ (ran 𝑓 ∪
ran 𝑔)) ∈ Fin) →
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) |
52 | 42, 50, 51 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥) |
53 | | suprcl 10983 |
. . . . . . . . . . . . . . . 16
⊢ (((abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ℝ ∧
(abs “ (ran 𝑓 ∪
ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
54 | 42, 53 | mp3an1 1411 |
. . . . . . . . . . . . . . 15
⊢ (((abs
“ (ran 𝑓 ∪ ran
𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
55 | 38, 52, 54 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
56 | 55 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
57 | | 0red 10041 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → 0 ∈
ℝ) |
58 | 26 | sselda 3603 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → 𝑟 ∈
ℂ) |
59 | 58 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (abs‘𝑟) ∈
ℝ) |
60 | 59 | adantrr 753 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ∈
ℝ) |
61 | 55 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
62 | | absgt0 14064 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ℂ → (𝑟 ≠ 0 ↔ 0 <
(abs‘𝑟))) |
63 | 58, 62 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (𝑟 ≠ 0 ↔ 0 <
(abs‘𝑟))) |
64 | 63 | biimpd 219 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (𝑟 ≠ 0 → 0 <
(abs‘𝑟))) |
65 | 64 | impr 649 |
. . . . . . . . . . . . . . . 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 1242 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran
𝑓 ∪ ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥)) |
68 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → ((abs “
(ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs
“ (ran 𝑓 ∪ ran
𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥)) |
69 | | fnfvima 6496 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((abs Fn
ℂ ∧ (ran 𝑓 ∪
ran 𝑔) ⊆ ℂ
∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
70 | 33, 69 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((ran
𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
71 | 26, 70 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
72 | | suprub 10984 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ℝ ∧
(abs “ (ran 𝑓 ∪
ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) ∧ (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) |
73 | 68, 71, 72 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (abs‘𝑟) ≤ sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)) |
74 | 73 | adantrr 753 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ≤ sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)) |
75 | 57, 60, 61, 65, 74 | ltletrd 10197 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → 0 < sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)) |
76 | 75 | rexlimdvaa 3032 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 → 0 < sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))) |
77 | 76 | imp 445 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 0 < sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)) |
78 | 56, 77 | elrpd 11869 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ+) |
79 | | rpmulcl 11855 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ+ ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) |
80 | 15, 78, 79 | sylancr 695 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) |
81 | | rpdivcl 11856 |
. . . . . . . . . . 11
⊢ (((𝑦 / 2) ∈ ℝ+
∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ+) |
82 | 14, 80, 81 | syl2an 494 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)) → ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ+) |
83 | 82 | anassrs 680 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ+) |
84 | 83 | adantlr 751 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ+) |
85 | | ancom 466 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) ↔ (𝑦 ∈ ℝ+
∧ 𝑢 ∈ (𝐴[,]𝐵))) |
86 | 85 | anbi2i 730 |
. . . . . . . . . . 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 839 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ↔ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈
ℝ+))) |
88 | 87 | anbi1i 731 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2))) |
89 | | an32 839 |
. . . . . . . . . . . . . 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 264 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈
ℝ+))) |
91 | 90 | anbi1i 731 |
. . . . . . . . . . . 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 839 |
. . . . . . . . . . . 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 264 |
. . . . . . . . . . 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 681 |
. . . . . . . . . . 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 292 |
. . . . . . . . . 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 6659 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → (𝑏 − 𝑎) = (𝑤 − 𝑢)) |
97 | 96 | ancoms 469 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (𝑏 − 𝑎) = (𝑤 − 𝑢)) |
98 | 97 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (abs‘(𝑏 − 𝑎)) = (abs‘(𝑤 − 𝑢))) |
99 | 98 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔
(abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))))) |
100 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑤 → (𝐺‘𝑏) = (𝐺‘𝑤)) |
101 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑢 → (𝐺‘𝑎) = (𝐺‘𝑢)) |
102 | 100, 101 | oveqan12rd 6670 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((𝐺‘𝑏) − (𝐺‘𝑎)) = ((𝐺‘𝑤) − (𝐺‘𝑢))) |
103 | 102 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) = (abs‘((𝐺‘𝑤) − (𝐺‘𝑢)))) |
104 | 103 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦 ↔ (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
105 | 99, 104 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦) ↔ ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))) |
106 | | oveq12 6659 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → (𝑏 − 𝑎) = (𝑢 − 𝑤)) |
107 | 106 | ancoms 469 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (𝑏 − 𝑎) = (𝑢 − 𝑤)) |
108 | 107 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (abs‘(𝑏 − 𝑎)) = (abs‘(𝑢 − 𝑤))) |
109 | 108 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔
(abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))))) |
110 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑢 → (𝐺‘𝑏) = (𝐺‘𝑢)) |
111 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑤 → (𝐺‘𝑎) = (𝐺‘𝑤)) |
112 | 110, 111 | oveqan12rd 6670 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((𝐺‘𝑏) − (𝐺‘𝑎)) = ((𝐺‘𝑢) − (𝐺‘𝑤))) |
113 | 112 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤)))) |
114 | 113 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦 ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦)) |
115 | 109, 114 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦) ↔ ((abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦))) |
116 | | iccssre 12255 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
117 | 2, 3, 116 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
118 | 117 | ad4antr 768 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝐴[,]𝐵) ⊆ ℝ) |
119 | | simp-4l 806 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → 𝜑) |
120 | 117, 25 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
121 | 120 | sselda 3603 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℂ) |
122 | 120 | sselda 3603 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℂ) |
123 | | abssub 14066 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ) →
(abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤))) |
124 | 121, 122,
123 | syl2anr 495 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤))) |
125 | 124 | anandis 873 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤))) |
126 | 125 | breq1d 4663 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔
(abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))))) |
127 | 9 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑤) ∈ ℂ) |
128 | 9 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑢) ∈ ℂ) |
129 | | abssub 14066 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺‘𝑤) ∈ ℂ ∧ (𝐺‘𝑢) ∈ ℂ) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤)))) |
130 | 127, 128,
129 | syl2anr 495 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤)))) |
131 | 130 | anandis 873 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤)))) |
132 | 131 | breq1d 4663 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦 ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦)) |
133 | 126, 132 | imbi12d 334 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) ↔ ((abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦))) |
134 | 119, 133 | sylan 488 |
. . . . . . . . . . . 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 10089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
136 | 3 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
137 | 135, 136 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
138 | | df-icc 12182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ [,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦)}) |
139 | 138 | elixx3g 12188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑢 ∈
ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))) |
140 | 139 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)) |
141 | 140 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑢) |
142 | 138 | elixx3g 12188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) ∧ (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵))) |
143 | 142 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵)) |
144 | 143 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ≤ 𝐵) |
145 | 141, 144 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) |
146 | | ioossioo 12265 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵)) |
147 | 137, 145,
146 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵)) |
148 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷) |
149 | 147, 148 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷) |
150 | 149 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷) |
151 | 8 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
152 | 151 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ ℝ) |
153 | 152 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈
ℝ*) |
154 | 151 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(𝐹‘𝑡))) |
155 | | elxrge0 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((abs‘(𝐹‘𝑡)) ∈ (0[,]+∞) ↔
((abs‘(𝐹‘𝑡)) ∈ ℝ*
∧ 0 ≤ (abs‘(𝐹‘𝑡)))) |
156 | 153, 154,
155 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞)) |
157 | 156 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞)) |
158 | 150, 157 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞)) |
159 | | 0e0iccpnf 12283 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
(0[,]+∞) |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈
(0[,]+∞)) |
161 | 158, 160 | ifclda 4120 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈
(0[,]+∞)) |
162 | 161 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈
(0[,]+∞)) |
163 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) |
164 | 162, 163 | fmptd 6385 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)),
0)):ℝ⟶(0[,]+∞)) |
165 | | itg2cl 23499 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
167 | 166 | 3adantr3 1222 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
168 | 119, 167 | sylan 488 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
169 | 168 | adantr 481 |
. . . . . . . . . . . . . . 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 798 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom
∫1))) |
171 | 151 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
172 | 150, 171 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ) |
173 | 172 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ) |
174 | | elioore 12205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ) |
175 | 16 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈
ℝ) |
176 | 175 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈
ℂ) |
177 | | ax-icn 9995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ i ∈
ℂ |
178 | 20 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℝ) |
179 | 178 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℂ) |
180 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((i
∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ) |
181 | 177, 179,
180 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (i · (𝑔‘𝑡)) ∈ ℂ) |
182 | | addcl 10018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
183 | 176, 181,
182 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝑔 ∈ dom
∫1 ∧ 𝑡
∈ ℝ)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
184 | 183 | anandirs 874 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
185 | 174, 184 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
186 | 185 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
187 | 186 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
188 | 173, 187 | subcld 10392 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ) |
189 | 188 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ) |
190 | 185 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ) |
191 | 190 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ) |
192 | 191 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ) |
193 | 189, 192 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ) |
194 | 193 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈
ℝ*) |
195 | 188 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
196 | 184 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
197 | 174, 196 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → 0 ≤
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
198 | 197 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
199 | 198 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
200 | 189, 192,
195, 199 | addge0d 10603 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
201 | | elxrge0 12281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔
(((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
202 | 194, 200,
201 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . 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 4120 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
(0[,]+∞)) |
205 | 204 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
(0[,]+∞)) |
206 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
207 | 205, 206 | fmptd 6385 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))),
0)):ℝ⟶(0[,]+∞)) |
208 | | itg2cl 23499 |
. . . . . . . . . . . . . . . . . . 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 1222 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈
ℝ*) |
211 | 170, 210 | sylan 488 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈
ℝ*) |
212 | 211 | adantr 481 |
. . . . . . . . . . . . . . 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 11840 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ*) |
214 | 213 | ad3antlr 767 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
𝑦 ∈
ℝ*) |
215 | 161 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈
(0[,]+∞)) |
216 | 215 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈
(0[,]+∞)) |
217 | 216, 163 | fmptd 6385 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)),
0)):ℝ⟶(0[,]+∞)) |
218 | 173, 187 | npcand 10396 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (𝐹‘𝑡)) |
219 | 218 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘(𝐹‘𝑡))) |
220 | 188, 187 | abstrid 14195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
221 | 219, 220 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹‘𝑡)) ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
222 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = (abs‘(𝐹‘𝑡))) |
223 | 222 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = (abs‘(𝐹‘𝑡))) |
224 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
225 | 224 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
226 | 221, 223,
225 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
227 | 226 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
228 | | 0le0 11110 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ≤
0 |
229 | 228 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → 0 ≤ 0) |
230 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = 0) |
231 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0) |
232 | 229, 230,
231 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
233 | 227, 232 | pm2.61d1 171 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
234 | 233 | ralrimivw 2967 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
235 | | reex 10027 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℝ
∈ V |
236 | 235 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ℝ ∈
V) |
237 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(abs‘(𝐹‘𝑡)) ∈ V |
238 | | c0ex 10034 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
V |
239 | 237, 238 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ V |
240 | 239 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ V) |
241 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V |
242 | 241, 238 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V |
243 | 242 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V) |
244 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) |
245 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
246 | 236, 240,
243, 244, 245 | ofrfval2 6915 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
247 | 246 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 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 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
249 | | itg2le 23506 |
. . . . . . . . . . . . . . . . . . 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 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) |
251 | 250 | 3adantr3 1222 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) |
252 | 170, 251 | sylan 488 |
. . . . . . . . . . . . . . . 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 481 |
. . . . . . . . . . . . . . 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 33492 |
. . . . . . . . . . . . . . 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 11991 |
. . . . . . . . . . . . . 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 798 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 𝜑) |
257 | | simpr2 1068 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑤 ∈ (𝐴[,]𝐵)) |
258 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑤 → (𝐴(,)𝑥) = (𝐴(,)𝑤)) |
259 | | itgeq1 23539 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴(,)𝑥) = (𝐴(,)𝑤) → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡) |
260 | 258, 259 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑤 → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡) |
261 | | itgex 23537 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡 ∈ V |
262 | 260, 1, 261 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐺‘𝑤) = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡) |
263 | 257, 262 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑤) = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡) |
264 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝐴 ∈ ℝ) |
265 | 117 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ) |
266 | 265 | 3ad2antr2 1227 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑤 ∈ ℝ) |
267 | 117 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ) |
268 | 267 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ*) |
269 | 268 | 3ad2antr1 1226 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ ℝ*) |
270 | | elicc1 12219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))) |
271 | 135, 136,
270 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))) |
272 | 271 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)) |
273 | 272 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑢) |
274 | 273 | 3ad2antr1 1226 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝐴 ≤ 𝑢) |
275 | | simpr3 1069 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ≤ 𝑤) |
276 | 135 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝐴 ∈
ℝ*) |
277 | 265 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ*) |
278 | | elicc1 12219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤))) |
279 | 276, 277,
278 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤))) |
280 | 279 | 3ad2antr2 1227 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤))) |
281 | 269, 274,
275, 280 | mpbir3and 1245 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ (𝐴[,]𝑤)) |
282 | | iooss2 12211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐵 ∈ ℝ*
∧ 𝑤 ≤ 𝐵) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵)) |
283 | 136, 144,
282 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵)) |
284 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝐵) ⊆ 𝐷) |
285 | 283, 284 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ 𝐷) |
286 | 285 | 3ad2antr2 1227 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐴(,)𝑤) ⊆ 𝐷) |
287 | 286 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → 𝑡 ∈ 𝐷) |
288 | 151 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
289 | 287, 288 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ) |
290 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 = 𝑢 → (𝑤 ∈ (𝐴[,]𝐵) ↔ 𝑢 ∈ (𝐴[,]𝐵))) |
291 | 290 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = 𝑢 → ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)))) |
292 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 = 𝑢 → (𝐴(,)𝑤) = (𝐴(,)𝑢)) |
293 | 292 | mpteq1d 4738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 = 𝑢 → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) = (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡))) |
294 | 293 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = 𝑢 → ((𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔ (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈
𝐿1)) |
295 | 291, 294 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = 𝑢 → (((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1) ↔
((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈
𝐿1))) |
296 | | ioombl 23333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴(,)𝑤) ∈ dom vol |
297 | 296 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ∈ dom vol) |
298 | 151 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
299 | 8 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))) |
300 | 299, 7 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
301 | 300 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
302 | 285, 297,
298, 301 | iblss 23571 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
303 | 295, 302 | chvarv 2263 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
304 | 303 | 3ad2antr1 1226 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
305 | | ioombl 23333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢(,)𝑤) ∈ dom vol |
306 | 305 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ∈ dom vol) |
307 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ V) |
308 | 300 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
309 | 149, 306,
307, 308 | iblss 23571 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
310 | 309 | 3adantr3 1222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
311 | 264, 266,
281, 289, 304, 310 | itgsplitioo 23604 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡 = (∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)) |
312 | 263, 311 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑤) = (∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)) |
313 | | simpr1 1067 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ (𝐴[,]𝐵)) |
314 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑢 → (𝐴(,)𝑥) = (𝐴(,)𝑢)) |
315 | | itgeq1 23539 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴(,)𝑥) = (𝐴(,)𝑢) → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) |
316 | 314, 315 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑢 → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) |
317 | | itgex 23537 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ V |
318 | 316, 1, 317 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐺‘𝑢) = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) |
319 | 313, 318 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑢) = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) |
320 | 312, 319 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) = ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)) |
321 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑢)) → (𝐹‘𝑡) ∈ V) |
322 | 321, 303 | itgcl 23550 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ ℂ) |
323 | 322 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ ℂ) |
324 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ V) |
325 | 324, 309 | itgcl 23550 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡 ∈ ℂ) |
326 | 323, 325 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) |
327 | 326 | 3adantr3 1222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) |
328 | 320, 327 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) |
329 | 328 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)) |
330 | | ftc1anc.t |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0)))) |
331 | | df-ov 6653 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢(,)𝑤) = ((,)‘〈𝑢, 𝑤〉) |
332 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 〈𝑢, 𝑤〉 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) |
333 | | ioof 12271 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
334 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
335 | 333, 334 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (,) Fn
(ℝ* × ℝ*) |
336 | | iccssxr 12256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴[,]𝐵) ⊆
ℝ* |
337 | | xpss12 5225 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴[,]𝐵) ⊆ ℝ* ∧ (𝐴[,]𝐵) ⊆ ℝ*) →
((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* ×
ℝ*)) |
338 | 336, 336,
337 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* ×
ℝ*) |
339 | | fnfvima 6496 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* ×
ℝ*) ∧ 〈𝑢, 𝑤〉 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((,)‘〈𝑢, 𝑤〉) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) |
340 | 335, 338,
339 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑢, 𝑤〉 ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘〈𝑢, 𝑤〉) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) |
341 | 332, 340 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((,)‘〈𝑢, 𝑤〉) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) |
342 | 331, 341 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) |
343 | | itgeq1 23539 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 = (𝑢(,)𝑤) → ∫𝑠(𝐹‘𝑡) d𝑡 = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) |
344 | 343 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 = (𝑢(,)𝑤) → (abs‘∫𝑠(𝐹‘𝑡) d𝑡) = (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)) |
345 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ 𝑠 ↔ 𝑡 ∈ (𝑢(,)𝑤))) |
346 | 345 | ifbid 4108 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑠 = (𝑢(,)𝑤) → if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) |
347 | 346 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) |
348 | 347 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 = (𝑢(,)𝑤) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))) |
349 | 344, 348 | breq12d 4666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = (𝑢(,)𝑤) → ((abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))) |
350 | 349 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑠 ∈
((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) ∧ (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))) |
351 | 330, 342,
350 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))) |
352 | 351 | 3adantr3 1222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))) |
353 | 329, 352 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))) |
354 | 353 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))) |
355 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺‘𝑤) ∈ ℂ ∧ (𝐺‘𝑢) ∈ ℂ) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ) |
356 | 127, 128,
355 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ) |
357 | 356 | anandis 873 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ) |
358 | 357 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ) |
359 | 358 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈
ℝ*) |
360 | 359 | 3adantr3 1222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈
ℝ*) |
361 | 360 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈
ℝ*) |
362 | 167 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
363 | 213 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑦 ∈ ℝ*) |
364 | | xrlelttr 11987 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ* ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ* ∧
𝑦 ∈
ℝ*) → (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
365 | 361, 362,
363, 364 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
366 | 354, 365 | mpand 711 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
367 | 256, 366 | sylanl1 682 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
368 | 367 | adantr 481 |
. . . . . . . . . . . . . 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‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
369 | 255, 368 | mpd 15 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) |
370 | 369 | ex 450 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
371 | 105, 115,
118, 134, 370 | wlogle 10561 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
372 | 371 | anassrs 680 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
373 | 95, 372 | sylanb 489 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
374 | 373 | ralrimiva 2966 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
375 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑧 = ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
((abs‘(𝑤 −
𝑢)) < 𝑧 ↔ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))))) |
376 | 375 | imbi1d 331 |
. . . . . . . . . 10
⊢ (𝑧 = ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(((abs‘(𝑤 −
𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) ↔ ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))) |
377 | 376 | ralbidv 2986 |
. . . . . . . . 9
⊢ (𝑧 = ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) ↔ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))) |
378 | 377 | rspcev 3309 |
. . . . . . . 8
⊢ ((((𝑦 / 2) / (2 · sup((abs
“ (ran 𝑓 ∪ ran
𝑔)), ℝ, < )))
∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) →
(abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
379 | 84, 374, 378 | syl2anc 693 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
380 | | ralnex 2992 |
. . . . . . . . 9
⊢
(∀𝑟 ∈
(ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) |
381 | | nne 2798 |
. . . . . . . . . 10
⊢ (¬
𝑟 ≠ 0 ↔ 𝑟 = 0) |
382 | 381 | ralbii 2980 |
. . . . . . . . 9
⊢
(∀𝑟 ∈
(ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) |
383 | 380, 382 | bitr3i 266 |
. . . . . . . 8
⊢ (¬
∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) |
384 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓:ℝ⟶ℝ →
𝑓 Fn
ℝ) |
385 | 16, 384 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓 ∈ dom ∫1
→ 𝑓 Fn
ℝ) |
386 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ran 𝑓) |
387 | 385, 386 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈ ran 𝑓) |
388 | | elun1 3780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑓‘𝑡) ∈ ran 𝑓 → (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
389 | 387, 388 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
390 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑟 = (𝑓‘𝑡) → (𝑟 = 0 ↔ (𝑓‘𝑡) = 0)) |
391 | 390 | rspcva 3307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0) |
392 | 389, 391 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0) |
393 | 392 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0) |
394 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑔:ℝ⟶ℝ →
𝑔 Fn
ℝ) |
395 | 20, 394 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑔 ∈ dom ∫1
→ 𝑔 Fn
ℝ) |
396 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ran 𝑔) |
397 | 395, 396 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈ ran 𝑔) |
398 | | elun2 3781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑔‘𝑡) ∈ ran 𝑔 → (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
399 | 397, 398 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
400 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑟 = (𝑔‘𝑡) → (𝑟 = 0 ↔ (𝑔‘𝑡) = 0)) |
401 | 400 | rspcva 3307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑔‘𝑡) = 0) |
402 | 401 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = (i · 0)) |
403 | | it0e0 11254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (i
· 0) = 0 |
404 | 402, 403 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0) |
405 | 399, 404 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0) |
406 | 405 | adantlll 754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0) |
407 | 393, 406 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = (0 + 0)) |
408 | 407 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = (0 + 0)) |
409 | | 00id 10211 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 + 0) =
0 |
410 | 408, 409 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = 0) |
411 | 410 | adantlll 754 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = 0) |
412 | 411 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0)) |
413 | | 0cnd 10033 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ) |
414 | 151, 413 | ifclda 4120 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ) |
415 | 414 | subid1d 10381 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) |
416 | 415 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) |
417 | 412, 416 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) |
418 | 417 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
419 | | fvif 6204 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(abs‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), (abs‘0)) |
420 | | abs0 14025 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(abs‘0) = 0 |
421 | | ifeq2 4091 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((abs‘0) = 0 → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), (abs‘0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) |
422 | 420, 421 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), (abs‘0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) |
423 | 419, 422 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(abs‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) |
424 | 418, 423 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) |
425 | 424 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
426 | 425 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
427 | 426 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))) |
428 | 427 | biimpd 219 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∀𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))) |
429 | 428 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∀𝑟 ∈
(ran 𝑓 ∪ ran 𝑔)𝑟 = 0 → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)))) |
430 | 429 | com23 86 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)))) |
431 | 430 | imp32 449 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) |
432 | 431 | anasss 679 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)
∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) |
433 | 432 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) |
434 | | 1rp 11836 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
435 | 434 | ne0ii 3923 |
. . . . . . . . . . . 12
⊢
ℝ+ ≠ ∅ |
436 | 357 | anassrs 680 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ) |
437 | 436 | abscld 14175 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ) |
438 | 437 | adantlrr 757 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ) |
439 | 438 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ) |
440 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
441 | 440 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ) |
442 | 441 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈
ℝ) |
443 | 442 | ad3antlr 767 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ) |
444 | 440 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ) |
445 | 444 | ad3antlr 767 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ) |
446 | 439 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈
ℝ*) |
447 | 159 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈
(0[,]+∞)) |
448 | 156, 447 | ifclda 4120 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈
(0[,]+∞)) |
449 | 448 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈
(0[,]+∞)) |
450 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) |
451 | 449, 450 | fmptd 6385 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)),
0)):ℝ⟶(0[,]+∞)) |
452 | | itg2cl 23499 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
453 | 451, 452 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
454 | 453 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
455 | 443 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈
ℝ*) |
456 | 111, 110 | oveqan12rd 6670 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → ((𝐺‘𝑎) − (𝐺‘𝑏)) = ((𝐺‘𝑤) − (𝐺‘𝑢))) |
457 | 456 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → (abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) = (abs‘((𝐺‘𝑤) − (𝐺‘𝑢)))) |
458 | 457 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → ((abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))) |
459 | 101, 100 | oveqan12rd 6670 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → ((𝐺‘𝑎) − (𝐺‘𝑏)) = ((𝐺‘𝑢) − (𝐺‘𝑤))) |
460 | 459 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → (abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤)))) |
461 | 460 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → ((abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))) |
462 | 131 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))) |
463 | 325 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ∈ ℝ) |
464 | 463 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ∈
ℝ*) |
465 | 453 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈
ℝ*) |
466 | 451 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)),
0)):ℝ⟶(0[,]+∞)) |
467 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((abs‘(𝐹‘𝑡)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
468 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (0 =
if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0 ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
469 | 152 | leidd 10594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡))) |
470 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((abs‘(𝐹‘𝑡)) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) → ((abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))) |
471 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (0 =
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) → (0 ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))) |
472 | 470, 471 | ifboth 4124 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)) ∧ 0 ≤ (abs‘(𝐹‘𝑡))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡))) |
473 | 469, 154,
472 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡))) |
474 | 473 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡))) |
475 | 149 | ssneld 3605 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (¬ 𝑡 ∈ 𝐷 → ¬ 𝑡 ∈ (𝑢(,)𝑤))) |
476 | 475 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ 𝐷) → ¬ 𝑡 ∈ (𝑢(,)𝑤)) |
477 | 230, 228 | syl6eqbr 4692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0) |
478 | 476, 477 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0) |
479 | 467, 468,
474, 478 | ifbothda 4123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) |
480 | 479 | ralrimivw 2967 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) |
481 | 237, 238 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ V |
482 | 481 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ V) |
483 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
484 | 236, 240,
482, 244, 483 | ofrfval2 6915 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
485 | 484 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
486 | 480, 485 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) |
487 | | itg2le 23506 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
488 | 164, 466,
486, 487 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
489 | 464, 166,
465, 351, 488 | xrletrd 11993 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
490 | 489 | 3adantr3 1222 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
491 | 329, 490 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
492 | 458, 461,
117, 462, 491 | wlogle 10561 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
493 | 492 | anassrs 680 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
494 | 493 | adantlrr 757 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
495 | 494 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))) |
496 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) |
497 | 446, 454,
455, 495, 496 | xrlelttrd 11991 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < (𝑦 / 2)) |
498 | | rphalflt 11860 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) < 𝑦) |
499 | 498 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) < 𝑦) |
500 | 499 | ad3antlr 767 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) < 𝑦) |
501 | 439, 443,
445, 497, 500 | lttrd 10198 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) |
502 | 501 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
503 | 502 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
504 | 503 | ralrimivw 2967 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∀𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
505 | | r19.2z 4060 |
. . . . . . . . . . . 12
⊢
((ℝ+ ≠ ∅ ∧ ∀𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
506 | 435, 504,
505 | sylancr 695 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
507 | 433, 506 | syldan 487 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
508 | 507 | anassrs 680 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
509 | 508 | anassrs 680 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
510 | 383, 509 | sylan2b 492 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
511 | 379, 510 | pm2.61dan 832 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
512 | 511 | ex 450 |
. . . . 5
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))) |
513 | 512 | rexlimdvva 3038 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) →
(∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))) |
514 | 13, 513 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
515 | 514 | ralrimivva 2971 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) |
516 | | ssid 3624 |
. . 3
⊢ ℂ
⊆ ℂ |
517 | | elcncf2 22693 |
. . 3
⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝐺 ∈
((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)))) |
518 | 120, 516,
517 | sylancl 694 |
. 2
⊢ (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)))) |
519 | 9, 515, 518 | mpbir2and 957 |
1
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |