Step | Hyp | Ref
| Expression |
1 | | 0xr 9965 |
. . . 4
⊢ 0 ∈
ℝ* |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 0 ∈
ℝ*) |
3 | | imassrn 5396 |
. . . . 5
⊢ (𝐹 “ (𝑋(,)𝑌)) ⊆ ran 𝐹 |
4 | | itg2gt0cn.3 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
5 | | frn 5966 |
. . . . . . 7
⊢ (𝐹:ℝ⟶(0[,)+∞)
→ ran 𝐹 ⊆
(0[,)+∞)) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 ⊆ (0[,)+∞)) |
7 | | icossxr 12129 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℝ* |
8 | 6, 7 | syl6ss 3580 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆
ℝ*) |
9 | 3, 8 | syl5ss 3579 |
. . . 4
⊢ (𝜑 → (𝐹 “ (𝑋(,)𝑌)) ⊆
ℝ*) |
10 | | supxrcl 12017 |
. . . 4
⊢ ((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* →
sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈
ℝ*) |
11 | 9, 10 | syl 17 |
. . 3
⊢ (𝜑 → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈
ℝ*) |
12 | | itg2gt0cn.2 |
. . . . . 6
⊢ (𝜑 → 𝑋 < 𝑌) |
13 | | ltrelxr 9978 |
. . . . . . . . . 10
⊢ <
⊆ (ℝ* × ℝ*) |
14 | 13 | ssbri 4627 |
. . . . . . . . 9
⊢ (𝑋 < 𝑌 → 𝑋(ℝ* ×
ℝ*)𝑌) |
15 | 12, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋(ℝ* ×
ℝ*)𝑌) |
16 | | brxp 5071 |
. . . . . . . 8
⊢ (𝑋(ℝ* ×
ℝ*)𝑌
↔ (𝑋 ∈
ℝ* ∧ 𝑌
∈ ℝ*)) |
17 | 15, 16 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∈ ℝ* ∧ 𝑌 ∈
ℝ*)) |
18 | | ioon0 12072 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ*) → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌)) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌)) |
20 | 12, 19 | mpbird 246 |
. . . . 5
⊢ (𝜑 → (𝑋(,)𝑌) ≠ ∅) |
21 | | itg2gt0cn.5 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹‘𝑥)) |
22 | 21 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥)) |
23 | | r19.2z 4012 |
. . . . 5
⊢ (((𝑋(,)𝑌) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥)) → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥)) |
24 | 20, 22, 23 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥)) |
25 | | supxrlub 12027 |
. . . . . 6
⊢ (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* ∧ 0
∈ ℝ*) → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔
∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦)) |
26 | 9, 1, 25 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔
∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦)) |
27 | | ffn 5958 |
. . . . . . 7
⊢ (𝐹:ℝ⟶(0[,)+∞)
→ 𝐹 Fn
ℝ) |
28 | 4, 27 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn ℝ) |
29 | | ioossre 12106 |
. . . . . 6
⊢ (𝑋(,)𝑌) ⊆ ℝ |
30 | | breq2 4587 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑥) → (0 < 𝑦 ↔ 0 < (𝐹‘𝑥))) |
31 | 30 | rexima 6401 |
. . . . . 6
⊢ ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥))) |
32 | 28, 29, 31 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥))) |
33 | 26, 32 | bitrd 267 |
. . . 4
⊢ (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔
∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥))) |
34 | 24, 33 | mpbird 246 |
. . 3
⊢ (𝜑 → 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, <
)) |
35 | | qbtwnxr 11905 |
. . 3
⊢ ((0
∈ ℝ* ∧ sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈
ℝ* ∧ 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
∃𝑦 ∈ ℚ (0
< 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, <
))) |
36 | 2, 11, 34, 35 | syl3anc 1318 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ ℚ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, <
))) |
37 | | qre 11669 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℚ → 𝑦 ∈
ℝ) |
38 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℚ ∧ 0 <
𝑦) → 𝑦 ∈
ℝ) |
39 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℚ ∧ 0 <
𝑦) → 0 < 𝑦) |
40 | 38, 39 | elrpd 11745 |
. . . . . . 7
⊢ ((𝑦 ∈ ℚ ∧ 0 <
𝑦) → 𝑦 ∈
ℝ+) |
41 | 40 | anim1i 590 |
. . . . . 6
⊢ (((𝑦 ∈ ℚ ∧ 0 <
𝑦) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(𝑦 ∈
ℝ+ ∧ 𝑦
< sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, <
))) |
42 | 41 | anasss 677 |
. . . . 5
⊢ ((𝑦 ∈ ℚ ∧ (0 <
𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) →
(𝑦 ∈
ℝ+ ∧ 𝑦
< sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, <
))) |
43 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
𝑦 ∈
ℝ+) |
44 | | rpxr 11716 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ*) |
45 | | supxrlub 12027 |
. . . . . . . . . . 11
⊢ (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* ∧ 𝑦 ∈ ℝ*)
→ (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔
∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧)) |
46 | 9, 44, 45 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔
∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧)) |
47 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐹‘𝑥) → (𝑦 < 𝑧 ↔ 𝑦 < (𝐹‘𝑥))) |
48 | 47 | rexima 6401 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥))) |
49 | 28, 29, 48 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥))) |
50 | 49 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥))) |
51 | 46, 50 | bitrd 267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔
∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥))) |
52 | 1 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 0 ∈
ℝ*) |
53 | | ioorp 12122 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0(,)+∞) = ℝ+ |
54 | | ioossicc 12130 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0(,)+∞) ⊆ (0[,]+∞) |
55 | 53, 54 | eqsstr3i 3599 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℝ+ ⊆ (0[,]+∞) |
56 | 55 | sseli 3564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
(0[,]+∞)) |
57 | | 0e0iccpnf 12154 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
(0[,]+∞) |
58 | | ifcl 4080 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (0[,]+∞) ∧ 0
∈ (0[,]+∞)) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞)) |
59 | 56, 57, 58 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ+
→ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞)) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ 𝑤 ∈ ℝ)
→ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞)) |
61 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) |
62 | 60, 61 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ+
→ (𝑤 ∈ ℝ
↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦,
0)):ℝ⟶(0[,]+∞)) |
63 | | itg2cl 23305 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈
ℝ*) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
→ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈
ℝ*) |
65 | 64 | ad5antlr 767 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈
ℝ*) |
66 | | ifcl 4080 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (0[,]+∞) ∧ 0
∈ (0[,]+∞)) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞)) |
67 | 56, 57, 66 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ+
→ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞)) |
68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ 𝑤 ∈ ℝ)
→ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞)) |
69 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) |
70 | 68, 69 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ+
→ (𝑤 ∈ ℝ
↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦,
0)):ℝ⟶(0[,]+∞)) |
71 | | itg2cl 23305 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈
ℝ*) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
→ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈
ℝ*) |
73 | 72 | ad5antlr 767 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈
ℝ*) |
74 | | rpre 11715 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
75 | 74 | ad4antlr 765 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈
ℝ) |
76 | | ioombl 23140 |
. . . . . . . . . . . . . . . . . . 19
⊢ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol |
77 | | mblvol 23105 |
. . . . . . . . . . . . . . . . . . 19
⊢
((if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol →
(vol‘(if(𝑋 ≤
(𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))) |
78 | 76, 77 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(vol‘(if(𝑋
≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) |
79 | | elioore 12076 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ ℝ) |
80 | 79 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈
ℝ) |
81 | | rpre 11715 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ∈
ℝ) |
82 | 81 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈
ℝ) |
83 | 80, 82 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) ∈ ℝ) |
84 | 83 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑋 ≤ (𝑥 − 𝑧)) → (𝑥 − 𝑧) ∈ ℝ) |
85 | 83 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) ∈
ℝ*) |
86 | 85 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑋 ≤ (𝑥 − 𝑧)) → (𝑥 − 𝑧) ∈
ℝ*) |
87 | 17 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
88 | 87 | ad5antr 766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑋 ≤ (𝑥 − 𝑧)) → 𝑋 ∈
ℝ*) |
89 | 17 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
90 | 89 | ad5antr 766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑋 ≤ (𝑥 − 𝑧)) → 𝑌 ∈
ℝ*) |
91 | 87 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 ∈
ℝ*) |
92 | | xrltnle 9984 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 − 𝑧) ∈ ℝ* ∧ 𝑋 ∈ ℝ*)
→ ((𝑥 − 𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥 − 𝑧))) |
93 | 85, 91, 92 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑥 − 𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥 − 𝑧))) |
94 | 93 | biimpar 501 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑋 ≤ (𝑥 − 𝑧)) → (𝑥 − 𝑧) < 𝑋) |
95 | 12 | ad5antr 766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑋 ≤ (𝑥 − 𝑧)) → 𝑋 < 𝑌) |
96 | | xrre2 11875 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑥 − 𝑧) ∈ ℝ* ∧ 𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ*) ∧ ((𝑥 − 𝑧) < 𝑋 ∧ 𝑋 < 𝑌)) → 𝑋 ∈ ℝ) |
97 | 86, 88, 90, 94, 95, 96 | syl32anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑋 ≤ (𝑥 − 𝑧)) → 𝑋 ∈ ℝ) |
98 | 84, 97 | ifclda 4070 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) ∈ ℝ) |
99 | 89 | ad5antr 766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈
ℝ*) |
100 | 82, 80 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ) |
102 | | mnfxr 9975 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ -∞
∈ ℝ* |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → -∞ ∈
ℝ*) |
104 | | mnfle 11845 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑋 ∈ ℝ*
→ -∞ ≤ 𝑋) |
105 | 87, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → -∞ ≤ 𝑋) |
106 | 103, 87, 89, 105, 12 | xrlelttrd 11867 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → -∞ < 𝑌) |
107 | 106 | ad5antr 766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → -∞ < 𝑌) |
108 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ≤ (𝑧 + 𝑥)) |
109 | | xrre 11874 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑌 ∈ ℝ*
∧ (𝑧 + 𝑥) ∈ ℝ) ∧
(-∞ < 𝑌 ∧
𝑌 ≤ (𝑧 + 𝑥))) → 𝑌 ∈ ℝ) |
110 | 99, 101, 107, 108, 109 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ) |
111 | 100 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ) |
112 | 110, 111 | ifclda 4070 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ) |
113 | 80 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈
ℝ*) |
114 | 89 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑌 ∈
ℝ*) |
115 | | rpgt0 11720 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ ℝ+
→ 0 < 𝑧) |
116 | 115 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 <
𝑧) |
117 | 82, 80 | ltsubposd 10492 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 <
𝑧 ↔ (𝑥 − 𝑧) < 𝑥)) |
118 | 116, 117 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) < 𝑥) |
119 | | eliooord 12104 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ (𝑋(,)𝑌) → (𝑋 < 𝑥 ∧ 𝑥 < 𝑌)) |
120 | 119 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 < 𝑌) |
121 | 120 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < 𝑌) |
122 | 85, 113, 114, 118, 121 | xrlttrd 11866 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) < 𝑌) |
123 | 82, 80 | ltaddpos2d 10491 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 <
𝑧 ↔ 𝑥 < (𝑧 + 𝑥))) |
124 | 116, 123 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < (𝑧 + 𝑥)) |
125 | 83, 80, 100, 118, 124 | lttrd 10077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) < (𝑧 + 𝑥)) |
126 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥 − 𝑧) < 𝑌 ↔ (𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) |
127 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥 − 𝑧) < (𝑧 + 𝑥) ↔ (𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) |
128 | 126, 127 | ifboth 4074 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 − 𝑧) < 𝑌 ∧ (𝑥 − 𝑧) < (𝑧 + 𝑥)) → (𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) |
129 | 122, 125,
128 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) |
130 | 12 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑌) |
131 | 100 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈
ℝ*) |
132 | 119 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑋 < 𝑥) |
133 | 132 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑥) |
134 | 91, 113, 131, 133, 124 | xrlttrd 11866 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < (𝑧 + 𝑥)) |
135 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < 𝑌 ↔ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) |
136 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < (𝑧 + 𝑥) ↔ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) |
137 | 135, 136 | ifboth 4074 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 < 𝑌 ∧ 𝑋 < (𝑧 + 𝑥)) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) |
138 | 130, 134,
137 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) |
139 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 − 𝑧) = if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) → ((𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) |
140 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑋 = if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) → (𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) |
141 | 139, 140 | ifboth 4074 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∧ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) |
142 | 129, 138,
141 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) |
143 | 98, 112, 142 | ltled 10064 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) |
144 | | ovolioo 23143 |
. . . . . . . . . . . . . . . . . . 19
⊢
((if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) ∈ ℝ ∧ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ ∧ if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → (vol*‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋))) |
145 | 98, 112, 143, 144 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) →
(vol*‘(if(𝑋 ≤
(𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋))) |
146 | 78, 145 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) →
(vol‘(if(𝑋 ≤
(𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋))) |
147 | 112, 98 | resubcld 10337 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)) ∈ ℝ) |
148 | 146, 147 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) →
(vol‘(if(𝑋 ≤
(𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ) |
149 | | rpgt0 11720 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ+
→ 0 < 𝑦) |
150 | 149 | ad4antlr 765 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 <
𝑦) |
151 | 98, 112 | posdifd 10493 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)))) |
152 | 142, 151 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 <
(if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋))) |
153 | 152, 146 | breqtrrd 4611 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 <
(vol‘(if(𝑋 ≤
(𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))) |
154 | 75, 148, 150, 153 | mulgt0d 10071 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 <
(𝑦 ·
(vol‘(if(𝑋 ≤
(𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))) |
155 | | iooin 12080 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ*) ∧ ((𝑥 − 𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*)) → ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) |
156 | 91, 114, 85, 131, 155 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) |
157 | 156 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) ↔ 𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))) |
158 | 157 | ifbid 4058 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0)) |
159 | 158 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) |
160 | 159 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0)))) |
161 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol) |
162 | | rpge0 11721 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 0 ≤ 𝑦) |
163 | | elrege0 12149 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (0[,)+∞) ↔
(𝑦 ∈ ℝ ∧ 0
≤ 𝑦)) |
164 | 74, 162, 163 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
(0[,)+∞)) |
165 | 164 | ad4antlr 765 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈
(0[,)+∞)) |
166 | | itg2const 23313 |
. . . . . . . . . . . . . . . . 17
⊢
(((if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol ∧ (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ ∧ 𝑦 ∈ (0[,)+∞)) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))) |
167 | 161, 148,
165, 166 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))) |
168 | 160, 167 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))) |
169 | 154, 168 | breqtrrd 4611 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)))) |
170 | 169 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)))) |
171 | 62 | ad5antlr 767 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦,
0)):ℝ⟶(0[,]+∞)) |
172 | 70 | ad5antlr 767 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦,
0)):ℝ⟶(0[,]+∞)) |
173 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 = 𝑤 → (𝑢 − 𝑥) = (𝑤 − 𝑥)) |
174 | 173 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = 𝑤 → (abs‘(𝑢 − 𝑥)) = (abs‘(𝑤 − 𝑥))) |
175 | 174 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 = 𝑤 → ((abs‘(𝑢 − 𝑥)) < 𝑧 ↔ (abs‘(𝑤 − 𝑥)) < 𝑧)) |
176 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 = 𝑤 → (𝐹‘𝑢) = (𝐹‘𝑤)) |
177 | 176 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 = 𝑤 → ((𝐹‘𝑢) − (𝐹‘𝑥)) = ((𝐹‘𝑤) − (𝐹‘𝑥))) |
178 | 177 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) = (abs‘((𝐹‘𝑤) − (𝐹‘𝑥)))) |
179 | 178 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 = 𝑤 → ((abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦) ↔ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) |
180 | 175, 179 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑤 → (((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ↔ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))) |
181 | 180 | rspccva 3281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑢 ∈
(𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) |
182 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (𝑦 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))) |
183 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0 =
if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))) |
184 | 74 | leidd 10473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≤ 𝑦) |
185 | 184 | ad6antlr 769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ 𝑦) |
186 | 79 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 𝑥 ∈ ℝ) |
187 | 81 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 𝑧 ∈ ℝ) |
188 | 186, 187 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑥 − 𝑧) ∈ ℝ) |
189 | 188 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑥 − 𝑧) ∈
ℝ*) |
190 | 187, 186 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ) |
191 | 190 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈
ℝ*) |
192 | | elioo2 12087 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 − 𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*) → (𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)))) |
193 | 189, 191,
192 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)))) |
194 | | 3anass 1035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑤 ∈ ℝ ∧ (𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)))) |
195 | 193, 194 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥))))) |
196 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ) |
197 | 79 | ad5antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℝ) |
198 | 196, 197 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑤 − 𝑥) ∈ ℝ) |
199 | 81 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℝ) |
200 | 198, 199 | absltd 14016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤 − 𝑥)) < 𝑧 ↔ (-𝑧 < (𝑤 − 𝑥) ∧ (𝑤 − 𝑥) < 𝑧))) |
201 | 199 | renegcld 10336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → -𝑧 ∈ ℝ) |
202 | 197, 201,
196 | ltaddsub2d 10507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ -𝑧 < (𝑤 − 𝑥))) |
203 | 197 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℂ) |
204 | 199 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℂ) |
205 | 203, 204 | negsubd 10277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑥 + -𝑧) = (𝑥 − 𝑧)) |
206 | 205 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ (𝑥 − 𝑧) < 𝑤)) |
207 | 202, 206 | bitr3d 269 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (-𝑧 < (𝑤 − 𝑥) ↔ (𝑥 − 𝑧) < 𝑤)) |
208 | 196, 197,
199 | ltsubaddd 10502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑤 − 𝑥) < 𝑧 ↔ 𝑤 < (𝑧 + 𝑥))) |
209 | 207, 208 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((-𝑧 < (𝑤 − 𝑥) ∧ (𝑤 − 𝑥) < 𝑧) ↔ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)))) |
210 | 200, 209 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤 − 𝑥)) < 𝑧 ↔ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)))) |
211 | 210 | pm5.32da 671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ∧ (abs‘(𝑤 − 𝑥)) < 𝑧) ↔ (𝑤 ∈ ℝ ∧ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥))))) |
212 | 195, 211 | bitr4d 270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (abs‘(𝑤 − 𝑥)) < 𝑧))) |
213 | 212 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → (𝑤 ∈ ℝ ∧ (abs‘(𝑤 − 𝑥)) < 𝑧)) |
214 | | pm3.35 609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((abs‘(𝑤
− 𝑥)) < 𝑧 ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) |
215 | 214 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((abs‘(𝑤
− 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ∧ (abs‘(𝑤 − 𝑥)) < 𝑧) → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) |
216 | 74 | ad6antlr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → 𝑦 ∈ ℝ) |
217 | | rge0ssre 12151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(0[,)+∞) ⊆ ℝ |
218 | 4 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞)) |
219 | 218 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑤) ∈ (0[,)+∞)) |
220 | 217, 219 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑤) ∈ ℝ) |
221 | 220 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → (𝐹‘𝑤) ∈ ℝ) |
222 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞)) |
223 | 222 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
224 | 217, 223 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
225 | 79, 224 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹‘𝑥) ∈ ℝ) |
226 | 225 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
227 | 220, 226 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹‘𝑤) − (𝐹‘𝑥)) ∈ ℝ) |
228 | 74 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ) |
229 | 225, 228 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹‘𝑥) − 𝑦) ∈ ℝ) |
230 | 229 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹‘𝑥) − 𝑦) ∈ ℝ) |
231 | 227, 230 | absltd 14016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) →
((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦) ↔ (-((𝐹‘𝑥) − 𝑦) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ∧ ((𝐹‘𝑤) − (𝐹‘𝑥)) < ((𝐹‘𝑥) − 𝑦)))) |
232 | 225 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹‘𝑥) ∈ ℂ) |
233 | | rpcn 11717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
234 | 233 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ) |
235 | 232, 234 | negsubdi2d 10287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → -((𝐹‘𝑥) − 𝑦) = (𝑦 − (𝐹‘𝑥))) |
236 | 235 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → -((𝐹‘𝑥) − 𝑦) = (𝑦 − (𝐹‘𝑥))) |
237 | 236 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) →
(-((𝐹‘𝑥) − 𝑦) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ↔ (𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥)))) |
238 | 237 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) →
((-((𝐹‘𝑥) − 𝑦) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ∧ ((𝐹‘𝑤) − (𝐹‘𝑥)) < ((𝐹‘𝑥) − 𝑦)) ↔ ((𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ∧ ((𝐹‘𝑤) − (𝐹‘𝑥)) < ((𝐹‘𝑥) − 𝑦)))) |
239 | 231, 238 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) →
((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦) ↔ ((𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ∧ ((𝐹‘𝑤) − (𝐹‘𝑥)) < ((𝐹‘𝑥) − 𝑦)))) |
240 | 239 | simprbda 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → (𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥))) |
241 | 225 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → (𝐹‘𝑥) ∈ ℝ) |
242 | 216, 221,
241 | ltsub1d 10515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → (𝑦 < (𝐹‘𝑤) ↔ (𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥)))) |
243 | 240, 242 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → 𝑦 < (𝐹‘𝑤)) |
244 | 216, 221,
243 | ltled 10064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → 𝑦 ≤ (𝐹‘𝑤)) |
245 | 215, 244 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ∧ (abs‘(𝑤 − 𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹‘𝑤)) |
246 | 245 | an4s 865 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ (𝑤 ∈ ℝ ∧ (abs‘(𝑤 − 𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹‘𝑤)) |
247 | 213, 246 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ (𝐹‘𝑤)) |
248 | 247 | iftrued 4044 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) = 𝑦) |
249 | 185, 248 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) |
250 | | 0le0 10987 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ≤
0 |
251 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) → (0 ≤ 𝑦 ↔ 0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))) |
252 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 =
if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))) |
253 | 251, 252 | ifboth 4074 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((0 ≤
𝑦 ∧ 0 ≤ 0) → 0
≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) |
254 | 162, 250,
253 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ+
→ 0 ≤ if(𝑦 ≤
(𝐹‘𝑤), 𝑦, 0)) |
255 | 254 | ad6antlr 769 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ ¬ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → 0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) |
256 | 182, 183,
249, 255 | ifbothda 4073 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) |
257 | 181, 256 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
(∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌))) → if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) |
258 | 257 | anassrs 678 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) |
259 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0)) |
260 | 259 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0)) |
261 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) |
262 | 261 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) |
263 | 258, 260,
262 | 3brtr4d 4615 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0)) |
264 | 263 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0))) |
265 | 250 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑤 ∈ (𝑋(,)𝑌) → 0 ≤ 0) |
266 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = 0) |
267 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) = 0) |
268 | 265, 266,
267 | 3brtr4d 4615 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0)) |
269 | 264, 268 | pm2.61d1 170 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0)) |
270 | | elin 3758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)))) |
271 | | ifbi 4057 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) |
272 | 270, 271 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) |
273 | | ifan 4084 |
. . . . . . . . . . . . . . . . . 18
⊢ if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) |
274 | 272, 273 | eqtri 2632 |
. . . . . . . . . . . . . . . . 17
⊢ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) |
275 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = 𝑤 → (𝐹‘𝑣) = (𝐹‘𝑤)) |
276 | 275 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = 𝑤 → (𝑦 ≤ (𝐹‘𝑣) ↔ 𝑦 ≤ (𝐹‘𝑤))) |
277 | 276 | elrab 3331 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤))) |
278 | | ifbi 4057 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤))) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤)), 𝑦, 0)) |
279 | 277, 278 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤)), 𝑦, 0) |
280 | | ifan 4084 |
. . . . . . . . . . . . . . . . . 18
⊢ if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤)), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) |
281 | 279, 280 | eqtri 2632 |
. . . . . . . . . . . . . . . . 17
⊢ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) |
282 | 269, 274,
281 | 3brtr4g 4617 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) |
283 | 282 | ralrimivw 2950 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) |
284 | | reex 9906 |
. . . . . . . . . . . . . . . . 17
⊢ ℝ
∈ V |
285 | 284 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → ℝ ∈ V) |
286 | 59 | ad6antlr 769 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞)) |
287 | 67 | ad6antlr 769 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞)) |
288 | | eqidd 2611 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) |
289 | | eqidd 2611 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) |
290 | 285, 286,
287, 288, 289 | ofrfval2 6813 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) |
291 | 283, 290 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) |
292 | | itg2le 23312 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) ∧
(𝑤 ∈ ℝ ↦
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧
(𝑤 ∈ ℝ ↦
if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘𝑟 ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))) |
293 | 171, 172,
291, 292 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))) |
294 | 52, 65, 73, 170, 293 | xrltletrd 11868 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))) |
295 | | itg2gt0cn.cn |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
296 | 295 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
297 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 𝑥 ∈ (𝑋(,)𝑌)) |
298 | | fssres 5983 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (𝑋(,)𝑌) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞)) |
299 | 29, 298 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:ℝ⟶(0[,)+∞)
→ (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞)) |
300 | | fss 5969 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) ∧ (0[,)+∞)
⊆ ℝ) → (𝐹
↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ) |
301 | 217, 300 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ) |
302 | 4, 299, 301 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ) |
303 | 302 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ) |
304 | 303 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ∈ ℝ) |
305 | 304, 228 | resubcld 10337 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ) |
306 | 305 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ) |
307 | 228, 304 | posdifd 10493 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))) |
308 | 307 | biimpa 500 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) |
309 | 306, 308 | elrpd 11745 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈
ℝ+) |
310 | | cncfi 22505 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ 𝑥 ∈ (𝑋(,)𝑌) ∧ (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))) |
311 | 296, 297,
309, 310 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))) |
312 | 311 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))) |
313 | | fvres 6117 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹‘𝑥)) |
314 | 313 | breq2d 4595 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑋(,)𝑌) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹‘𝑥))) |
315 | 314 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹‘𝑥))) |
316 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹‘𝑢)) |
317 | 316 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹‘𝑢)) |
318 | 313 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹‘𝑥)) |
319 | 317, 318 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) = ((𝐹‘𝑢) − (𝐹‘𝑥))) |
320 | 319 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) = (abs‘((𝐹‘𝑢) − (𝐹‘𝑥)))) |
321 | 313 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝑋(,)𝑌) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹‘𝑥) − 𝑦)) |
322 | 321 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹‘𝑥) − 𝑦)) |
323 | 320, 322 | breq12d 4596 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ↔ (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) |
324 | 323 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))) |
325 | 324 | ralbidva 2968 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))) |
326 | 325 | rexbidv 3034 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))) |
327 | 312, 315,
326 | 3imtr3d 281 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < (𝐹‘𝑥) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))) |
328 | 327 | imp 444 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) |
329 | 294, 328 | r19.29a 3060 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) → 0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))) |
330 | 329 | ex 449 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < (𝐹‘𝑥) → 0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))))) |
331 | 330 | rexlimdva 3013 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥) → 0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))))) |
332 | 51, 331 | sylbid 229 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) → 0
< (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))))) |
333 | 332 | imp 444 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0
< (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))) |
334 | 70 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(𝑤 ∈ ℝ ↦
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦,
0)):ℝ⟶(0[,]+∞)) |
335 | | icossicc 12131 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
336 | | fss 5969 |
. . . . . . . . . 10
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞)) |
337 | 4, 335, 336 | sylancl 693 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) |
338 | 337 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
𝐹:ℝ⟶(0[,]+∞)) |
339 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (𝑦 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) → (𝑦 ≤ (𝐹‘𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤))) |
340 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (0 =
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) → (0 ≤ (𝐹‘𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤))) |
341 | 277 | simprbi 479 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)} → 𝑦 ≤ (𝐹‘𝑤)) |
342 | 341 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}) → 𝑦 ≤ (𝐹‘𝑤)) |
343 | 4 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑤) ∈ (0[,)+∞)) |
344 | | elrege0 12149 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑤) ∈ (0[,)+∞) ↔ ((𝐹‘𝑤) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑤))) |
345 | 343, 344 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → ((𝐹‘𝑤) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑤))) |
346 | 345 | simprd 478 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → 0 ≤ (𝐹‘𝑤)) |
347 | 346 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ¬ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}) → 0 ≤ (𝐹‘𝑤)) |
348 | 339, 340,
342, 347 | ifbothda 4073 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤)) |
349 | 348 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤)) |
350 | 349 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
∀𝑤 ∈ ℝ
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤)) |
351 | 284 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
ℝ ∈ V) |
352 | 67 | ad3antlr 763 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞)) |
353 | | fvex 6113 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑤) ∈ V |
354 | 353 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑤) ∈ V) |
355 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(𝑤 ∈ ℝ ↦
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) |
356 | 4 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑤 ∈ ℝ ↦ (𝐹‘𝑤))) |
357 | 356 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
𝐹 = (𝑤 ∈ ℝ ↦ (𝐹‘𝑤))) |
358 | 351, 352,
354, 355, 357 | ofrfval2 6813 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
((𝑤 ∈ ℝ ↦
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) ∘𝑟 ≤ 𝐹 ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤))) |
359 | 350, 358 | mpbird 246 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(𝑤 ∈ ℝ ↦
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) ∘𝑟 ≤ 𝐹) |
360 | | itg2le 23312 |
. . . . . . . 8
⊢ (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧
𝐹:ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) ∘𝑟 ≤ 𝐹) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) |
361 | 334, 338,
359, 360 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) |
362 | 43, 333, 361 | jca32 556 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(𝑦 ∈
ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)))) |
363 | 362 | expl 646 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ ℝ+ ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(𝑦 ∈
ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹))))) |
364 | 42, 363 | syl5 33 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ ℚ ∧ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) →
(𝑦 ∈
ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹))))) |
365 | 364 | reximdv2 2997 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
∃𝑦 ∈
ℝ+ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)))) |
366 | 1 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 0 ∈
ℝ*) |
367 | 72 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈
ℝ*) |
368 | | itg2cl 23305 |
. . . . . . 7
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ (∫2‘𝐹) ∈
ℝ*) |
369 | 337, 368 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ*) |
370 | 369 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∫2‘𝐹)
∈ ℝ*) |
371 | | xrltletr 11864 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈ ℝ* ∧
(∫2‘𝐹)
∈ ℝ*) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) → 0 <
(∫2‘𝐹))) |
372 | 366, 367,
370, 371 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ((0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) → 0 <
(∫2‘𝐹))) |
373 | 372 | rexlimdva 3013 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ ℝ+ (0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) → 0 <
(∫2‘𝐹))) |
374 | 365, 373 | syld 46 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0
< (∫2‘𝐹))) |
375 | 36, 374 | mpd 15 |
1
⊢ (𝜑 → 0 <
(∫2‘𝐹)) |