| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0xr 11308 | . . 3
⊢ 0 ∈
ℝ* | 
| 2 |  | imassrn 6089 | . . . . 5
⊢ (𝐹 “ (𝑋(,)𝑌)) ⊆ ran 𝐹 | 
| 3 |  | itg2gt0cn.3 | . . . . . . 7
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) | 
| 4 | 3 | frnd 6744 | . . . . . 6
⊢ (𝜑 → ran 𝐹 ⊆ (0[,)+∞)) | 
| 5 |  | icossxr 13472 | . . . . . 6
⊢
(0[,)+∞) ⊆ ℝ* | 
| 6 | 4, 5 | sstrdi 3996 | . . . . 5
⊢ (𝜑 → ran 𝐹 ⊆
ℝ*) | 
| 7 | 2, 6 | sstrid 3995 | . . . 4
⊢ (𝜑 → (𝐹 “ (𝑋(,)𝑌)) ⊆
ℝ*) | 
| 8 |  | supxrcl 13357 | . . . 4
⊢ ((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* →
sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈
ℝ*) | 
| 9 | 7, 8 | syl 17 | . . 3
⊢ (𝜑 → sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈
ℝ*) | 
| 10 |  | itg2gt0cn.2 | . . . . . 6
⊢ (𝜑 → 𝑋 < 𝑌) | 
| 11 |  | ltrelxr 11322 | . . . . . . . . . 10
⊢  <
⊆ (ℝ* × ℝ*) | 
| 12 | 11 | ssbri 5188 | . . . . . . . . 9
⊢ (𝑋 < 𝑌 → 𝑋(ℝ* ×
ℝ*)𝑌) | 
| 13 | 10, 12 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑋(ℝ* ×
ℝ*)𝑌) | 
| 14 |  | brxp 5734 | . . . . . . . 8
⊢ (𝑋(ℝ* ×
ℝ*)𝑌
↔ (𝑋 ∈
ℝ* ∧ 𝑌
∈ ℝ*)) | 
| 15 | 13, 14 | sylib 218 | . . . . . . 7
⊢ (𝜑 → (𝑋 ∈ ℝ* ∧ 𝑌 ∈
ℝ*)) | 
| 16 |  | ioon0 13413 | . . . . . . 7
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ*) → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌)) | 
| 17 | 15, 16 | syl 17 | . . . . . 6
⊢ (𝜑 → ((𝑋(,)𝑌) ≠ ∅ ↔ 𝑋 < 𝑌)) | 
| 18 | 10, 17 | mpbird 257 | . . . . 5
⊢ (𝜑 → (𝑋(,)𝑌) ≠ ∅) | 
| 19 |  | itg2gt0cn.5 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 0 < (𝐹‘𝑥)) | 
| 20 | 19 | ralrimiva 3146 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥)) | 
| 21 |  | r19.2z 4495 | . . . . 5
⊢ (((𝑋(,)𝑌) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥)) → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥)) | 
| 22 | 18, 20, 21 | syl2anc 584 | . . . 4
⊢ (𝜑 → ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥)) | 
| 23 |  | supxrlub 13367 | . . . . . 6
⊢ (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* ∧ 0
∈ ℝ*) → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔
∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦)) | 
| 24 | 7, 1, 23 | sylancl 586 | . . . . 5
⊢ (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔
∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦)) | 
| 25 | 3 | ffnd 6737 | . . . . . 6
⊢ (𝜑 → 𝐹 Fn ℝ) | 
| 26 |  | ioossre 13448 | . . . . . 6
⊢ (𝑋(,)𝑌) ⊆ ℝ | 
| 27 |  | breq2 5147 | . . . . . . 7
⊢ (𝑦 = (𝐹‘𝑥) → (0 < 𝑦 ↔ 0 < (𝐹‘𝑥))) | 
| 28 | 27 | rexima 7258 | . . . . . 6
⊢ ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥))) | 
| 29 | 25, 26, 28 | sylancl 586 | . . . . 5
⊢ (𝜑 → (∃𝑦 ∈ (𝐹 “ (𝑋(,)𝑌))0 < 𝑦 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥))) | 
| 30 | 24, 29 | bitrd 279 | . . . 4
⊢ (𝜑 → (0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔
∃𝑥 ∈ (𝑋(,)𝑌)0 < (𝐹‘𝑥))) | 
| 31 | 22, 30 | mpbird 257 | . . 3
⊢ (𝜑 → 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, <
)) | 
| 32 |  | qbtwnxr 13242 | . . 3
⊢ ((0
∈ ℝ* ∧ sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ∈
ℝ* ∧ 0 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
∃𝑦 ∈ ℚ (0
< 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, <
))) | 
| 33 | 1, 9, 31, 32 | mp3an2i 1468 | . 2
⊢ (𝜑 → ∃𝑦 ∈ ℚ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, <
))) | 
| 34 |  | qre 12995 | . . . . . . . . 9
⊢ (𝑦 ∈ ℚ → 𝑦 ∈
ℝ) | 
| 35 | 34 | adantr 480 | . . . . . . . 8
⊢ ((𝑦 ∈ ℚ ∧ 0 <
𝑦) → 𝑦 ∈
ℝ) | 
| 36 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑦 ∈ ℚ ∧ 0 <
𝑦) → 0 < 𝑦) | 
| 37 | 35, 36 | elrpd 13074 | . . . . . . 7
⊢ ((𝑦 ∈ ℚ ∧ 0 <
𝑦) → 𝑦 ∈
ℝ+) | 
| 38 | 37 | anim1i 615 | . . . . . 6
⊢ (((𝑦 ∈ ℚ ∧ 0 <
𝑦) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(𝑦 ∈
ℝ+ ∧ 𝑦
< sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, <
))) | 
| 39 | 38 | anasss 466 | . . . . 5
⊢ ((𝑦 ∈ ℚ ∧ (0 <
𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) →
(𝑦 ∈
ℝ+ ∧ 𝑦
< sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, <
))) | 
| 40 |  | simplr 769 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
𝑦 ∈
ℝ+) | 
| 41 |  | rpxr 13044 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ*) | 
| 42 |  | supxrlub 13367 | . . . . . . . . . . 11
⊢ (((𝐹 “ (𝑋(,)𝑌)) ⊆ ℝ* ∧ 𝑦 ∈ ℝ*)
→ (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔
∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧)) | 
| 43 | 7, 41, 42 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔
∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧)) | 
| 44 |  | breq2 5147 | . . . . . . . . . . . . 13
⊢ (𝑧 = (𝐹‘𝑥) → (𝑦 < 𝑧 ↔ 𝑦 < (𝐹‘𝑥))) | 
| 45 | 44 | rexima 7258 | . . . . . . . . . . . 12
⊢ ((𝐹 Fn ℝ ∧ (𝑋(,)𝑌) ⊆ ℝ) → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥))) | 
| 46 | 25, 26, 45 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝜑 → (∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥))) | 
| 47 | 46 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∃𝑧 ∈ (𝐹 “ (𝑋(,)𝑌))𝑦 < 𝑧 ↔ ∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥))) | 
| 48 | 43, 47 | bitrd 279 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) ↔
∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥))) | 
| 49 | 1 | a1i 11 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 0 ∈
ℝ*) | 
| 50 |  | ioorp 13465 | . . . . . . . . . . . . . . . . . . 19
⊢
(0(,)+∞) = ℝ+ | 
| 51 |  | ioossicc 13473 | . . . . . . . . . . . . . . . . . . 19
⊢
(0(,)+∞) ⊆ (0[,]+∞) | 
| 52 | 50, 51 | eqsstrri 4031 | . . . . . . . . . . . . . . . . . 18
⊢
ℝ+ ⊆ (0[,]+∞) | 
| 53 | 52 | sseli 3979 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
(0[,]+∞)) | 
| 54 |  | 0e0iccpnf 13499 | . . . . . . . . . . . . . . . . 17
⊢ 0 ∈
(0[,]+∞) | 
| 55 |  | ifcl 4571 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ (0[,]+∞) ∧ 0
∈ (0[,]+∞)) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞)) | 
| 56 | 53, 54, 55 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞)) | 
| 57 | 56 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ+
∧ 𝑤 ∈ ℝ)
→ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞)) | 
| 58 | 57 | fmpttd 7135 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
→ (𝑤 ∈ ℝ
↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦,
0)):ℝ⟶(0[,]+∞)) | 
| 59 |  | itg2cl 25767 | . . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈
ℝ*) | 
| 60 | 58, 59 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ+
→ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈
ℝ*) | 
| 61 | 60 | ad5antlr 735 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ∈
ℝ*) | 
| 62 |  | ifcl 4571 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ (0[,]+∞) ∧ 0
∈ (0[,]+∞)) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞)) | 
| 63 | 53, 54, 62 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞)) | 
| 64 | 63 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ+
∧ 𝑤 ∈ ℝ)
→ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞)) | 
| 65 | 64 | fmpttd 7135 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
→ (𝑤 ∈ ℝ
↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦,
0)):ℝ⟶(0[,]+∞)) | 
| 66 |  | itg2cl 25767 | . . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈
ℝ*) | 
| 67 | 65, 66 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ+
→ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈
ℝ*) | 
| 68 | 67 | ad5antlr 735 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈
ℝ*) | 
| 69 |  | rpre 13043 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) | 
| 70 | 69 | ad4antlr 733 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈
ℝ) | 
| 71 |  | ioombl 25600 | . . . . . . . . . . . . . . . . . 18
⊢ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol | 
| 72 |  | mblvol 25565 | . . . . . . . . . . . . . . . . . 18
⊢
((if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol →
(vol‘(if(𝑋 ≤
(𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))) | 
| 73 | 71, 72 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢
(vol‘(if(𝑋
≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (vol*‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) | 
| 74 |  | elioore 13417 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ ℝ) | 
| 75 | 74 | ad3antlr 731 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈
ℝ) | 
| 76 |  | rpre 13043 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ∈
ℝ) | 
| 77 | 76 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈
ℝ) | 
| 78 | 75, 77 | resubcld 11691 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) ∈ ℝ) | 
| 79 | 78 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑋 ≤ (𝑥 − 𝑧)) → (𝑥 − 𝑧) ∈ ℝ) | 
| 80 | 78 | rexrd 11311 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) ∈
ℝ*) | 
| 81 | 80 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑋 ≤ (𝑥 − 𝑧)) → (𝑥 − 𝑧) ∈
ℝ*) | 
| 82 | 15 | simpld 494 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑋 ∈
ℝ*) | 
| 83 | 82 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑋 ≤ (𝑥 − 𝑧)) → 𝑋 ∈
ℝ*) | 
| 84 | 15 | simprd 495 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑌 ∈
ℝ*) | 
| 85 | 84 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑋 ≤ (𝑥 − 𝑧)) → 𝑌 ∈
ℝ*) | 
| 86 | 82 | ad4antr 732 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 ∈
ℝ*) | 
| 87 |  | xrltnle 11328 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 − 𝑧) ∈ ℝ* ∧ 𝑋 ∈ ℝ*)
→ ((𝑥 − 𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥 − 𝑧))) | 
| 88 | 80, 86, 87 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑥 − 𝑧) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑥 − 𝑧))) | 
| 89 | 88 | biimpar 477 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑋 ≤ (𝑥 − 𝑧)) → (𝑥 − 𝑧) < 𝑋) | 
| 90 | 10 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑋 ≤ (𝑥 − 𝑧)) → 𝑋 < 𝑌) | 
| 91 |  | xrre2 13212 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 − 𝑧) ∈ ℝ* ∧ 𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ*) ∧ ((𝑥 − 𝑧) < 𝑋 ∧ 𝑋 < 𝑌)) → 𝑋 ∈ ℝ) | 
| 92 | 81, 83, 85, 89, 90, 91 | syl32anc 1380 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑋 ≤ (𝑥 − 𝑧)) → 𝑋 ∈ ℝ) | 
| 93 | 79, 92 | ifclda 4561 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) ∈ ℝ) | 
| 94 | 84 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈
ℝ*) | 
| 95 | 77, 75 | readdcld 11290 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈ ℝ) | 
| 96 | 95 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ) | 
| 97 |  | mnfxr 11318 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ -∞
∈ ℝ* | 
| 98 | 97 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → -∞ ∈
ℝ*) | 
| 99 |  | mnfle 13177 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑋 ∈ ℝ*
→ -∞ ≤ 𝑋) | 
| 100 | 82, 99 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → -∞ ≤ 𝑋) | 
| 101 | 98, 82, 84, 100, 10 | xrlelttrd 13202 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → -∞ < 𝑌) | 
| 102 | 101 | ad5antr 734 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → -∞ < 𝑌) | 
| 103 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ≤ (𝑧 + 𝑥)) | 
| 104 |  | xrre 13211 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑌 ∈ ℝ*
∧ (𝑧 + 𝑥) ∈ ℝ) ∧
(-∞ < 𝑌 ∧
𝑌 ≤ (𝑧 + 𝑥))) → 𝑌 ∈ ℝ) | 
| 105 | 94, 96, 102, 103, 104 | syl22anc 839 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑌 ≤ (𝑧 + 𝑥)) → 𝑌 ∈ ℝ) | 
| 106 | 95 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ ¬
𝑌 ≤ (𝑧 + 𝑥)) → (𝑧 + 𝑥) ∈ ℝ) | 
| 107 | 105, 106 | ifclda 4561 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ) | 
| 108 | 75 | rexrd 11311 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈
ℝ*) | 
| 109 | 84 | ad4antr 732 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑌 ∈
ℝ*) | 
| 110 |  | rpgt0 13047 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ ℝ+
→ 0 < 𝑧) | 
| 111 | 110 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 <
𝑧) | 
| 112 | 77, 75 | ltsubposd 11849 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 <
𝑧 ↔ (𝑥 − 𝑧) < 𝑥)) | 
| 113 | 111, 112 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) < 𝑥) | 
| 114 |  | eliooord 13446 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ (𝑋(,)𝑌) → (𝑋 < 𝑥 ∧ 𝑥 < 𝑌)) | 
| 115 | 114 | simprd 495 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 < 𝑌) | 
| 116 | 115 | ad3antlr 731 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < 𝑌) | 
| 117 | 80, 108, 109, 113, 116 | xrlttrd 13201 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) < 𝑌) | 
| 118 | 77, 75 | ltaddpos2d 11848 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (0 <
𝑧 ↔ 𝑥 < (𝑧 + 𝑥))) | 
| 119 | 111, 118 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑥 < (𝑧 + 𝑥)) | 
| 120 | 78, 75, 95, 113, 119 | lttrd 11422 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) < (𝑧 + 𝑥)) | 
| 121 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥 − 𝑧) < 𝑌 ↔ (𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) | 
| 122 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → ((𝑥 − 𝑧) < (𝑧 + 𝑥) ↔ (𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) | 
| 123 | 121, 122 | ifboth 4565 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 − 𝑧) < 𝑌 ∧ (𝑥 − 𝑧) < (𝑧 + 𝑥)) → (𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) | 
| 124 | 117, 120,
123 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) | 
| 125 | 10 | ad4antr 732 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑌) | 
| 126 | 95 | rexrd 11311 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑧 + 𝑥) ∈
ℝ*) | 
| 127 | 114 | simpld 494 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑋 < 𝑥) | 
| 128 | 127 | ad3antlr 731 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < 𝑥) | 
| 129 | 86, 108, 126, 128, 119 | xrlttrd 13201 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < (𝑧 + 𝑥)) | 
| 130 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑌 = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < 𝑌 ↔ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) | 
| 131 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 + 𝑥) = if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) → (𝑋 < (𝑧 + 𝑥) ↔ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) | 
| 132 | 130, 131 | ifboth 4565 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 < 𝑌 ∧ 𝑋 < (𝑧 + 𝑥)) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) | 
| 133 | 125, 129,
132 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) | 
| 134 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 − 𝑧) = if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) → ((𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) | 
| 135 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑋 = if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) → (𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) | 
| 136 | 134, 135 | ifboth 4565 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 − 𝑧) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∧ 𝑋 < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) | 
| 137 | 124, 133,
136 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) | 
| 138 | 93, 107, 137 | ltled 11409 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) | 
| 139 |  | ovolioo 25603 | . . . . . . . . . . . . . . . . . 18
⊢
((if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) ∈ ℝ ∧ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ∈ ℝ ∧ if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) ≤ if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) → (vol*‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋))) | 
| 140 | 93, 107, 138, 139 | syl3anc 1373 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) →
(vol*‘(if(𝑋 ≤
(𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋))) | 
| 141 | 73, 140 | eqtrid 2789 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) →
(vol‘(if(𝑋 ≤
(𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) = (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋))) | 
| 142 | 107, 93 | resubcld 11691 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)) ∈ ℝ) | 
| 143 | 141, 142 | eqeltrd 2841 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) →
(vol‘(if(𝑋 ≤
(𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ) | 
| 144 |  | rpgt0 13047 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ 0 < 𝑦) | 
| 145 | 144 | ad4antlr 733 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 <
𝑦) | 
| 146 | 93, 107 | posdifd 11850 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋) < if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) ↔ 0 < (if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)))) | 
| 147 | 137, 146 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 <
(if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)) − if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋))) | 
| 148 | 147, 141 | breqtrrd 5171 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 <
(vol‘(if(𝑋 ≤
(𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))) | 
| 149 | 70, 143, 145, 148 | mulgt0d 11416 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 <
(𝑦 ·
(vol‘(if(𝑋 ≤
(𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))) | 
| 150 |  | iooin 13421 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ*) ∧ ((𝑥 − 𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*)) → ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) | 
| 151 | 86, 109, 80, 126, 150 | syl22anc 839 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) = (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) | 
| 152 | 151 | eleq2d 2827 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) ↔ 𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))))) | 
| 153 | 152 | ifbid 4549 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0)) | 
| 154 | 153 | mpteq2dv 5244 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) | 
| 155 | 154 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0)))) | 
| 156 |  | rpge0 13048 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ 0 ≤ 𝑦) | 
| 157 |  | elrege0 13494 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (0[,)+∞) ↔
(𝑦 ∈ ℝ ∧ 0
≤ 𝑦)) | 
| 158 | 69, 156, 157 | sylanbrc 583 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
(0[,)+∞)) | 
| 159 | 158 | ad4antlr 733 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝑦 ∈
(0[,)+∞)) | 
| 160 |  | itg2const 25775 | . . . . . . . . . . . . . . . 16
⊢
(((if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))) ∈ dom vol ∧ (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))) ∈ ℝ ∧ 𝑦 ∈ (0[,)+∞)) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))) | 
| 161 | 71, 143, 159, 160 | mp3an2i 1468 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ (if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))) | 
| 162 | 155, 161 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) = (𝑦 · (vol‘(if(𝑋 ≤ (𝑥 − 𝑧), (𝑥 − 𝑧), 𝑋)(,)if(𝑌 ≤ (𝑧 + 𝑥), 𝑌, (𝑧 + 𝑥)))))) | 
| 163 | 149, 162 | breqtrrd 5171 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)))) | 
| 164 | 163 | adantr 480 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)))) | 
| 165 | 58 | ad5antlr 735 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦,
0)):ℝ⟶(0[,]+∞)) | 
| 166 | 65 | ad5antlr 735 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦,
0)):ℝ⟶(0[,]+∞)) | 
| 167 |  | fvoveq1 7454 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 = 𝑤 → (abs‘(𝑢 − 𝑥)) = (abs‘(𝑤 − 𝑥))) | 
| 168 | 167 | breq1d 5153 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑤 → ((abs‘(𝑢 − 𝑥)) < 𝑧 ↔ (abs‘(𝑤 − 𝑥)) < 𝑧)) | 
| 169 | 168 | imbrov2fvoveq 7456 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑤 → (((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ↔ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))) | 
| 170 | 169 | rspccva 3621 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑢 ∈
(𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) | 
| 171 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (𝑦 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))) | 
| 172 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 =
if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) → (0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) ↔ if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))) | 
| 173 | 69 | leidd 11829 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≤ 𝑦) | 
| 174 | 173 | ad6antlr 737 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ 𝑦) | 
| 175 | 74 | ad4antlr 733 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 𝑥 ∈ ℝ) | 
| 176 | 76 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 𝑧 ∈ ℝ) | 
| 177 | 175, 176 | resubcld 11691 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑥 − 𝑧) ∈ ℝ) | 
| 178 | 177 | rexrd 11311 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑥 − 𝑧) ∈
ℝ*) | 
| 179 | 176, 175 | readdcld 11290 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈ ℝ) | 
| 180 | 179 | rexrd 11311 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑧 + 𝑥) ∈
ℝ*) | 
| 181 |  | elioo2 13428 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 − 𝑧) ∈ ℝ* ∧ (𝑧 + 𝑥) ∈ ℝ*) → (𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)))) | 
| 182 | 178, 180,
181 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)))) | 
| 183 |  | 3anass 1095 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑤 ∈ ℝ ∧ (𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)))) | 
| 184 | 182, 183 | bitrdi 287 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥))))) | 
| 185 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ) | 
| 186 | 74 | ad5antlr 735 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℝ) | 
| 187 | 185, 186 | resubcld 11691 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑤 − 𝑥) ∈ ℝ) | 
| 188 | 76 | ad3antlr 731 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℝ) | 
| 189 | 187, 188 | absltd 15468 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤 − 𝑥)) < 𝑧 ↔ (-𝑧 < (𝑤 − 𝑥) ∧ (𝑤 − 𝑥) < 𝑧))) | 
| 190 | 188 | renegcld 11690 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → -𝑧 ∈ ℝ) | 
| 191 | 186, 190,
185 | ltaddsub2d 11864 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ -𝑧 < (𝑤 − 𝑥))) | 
| 192 | 186 | recnd 11289 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑥 ∈ ℂ) | 
| 193 | 188 | recnd 11289 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → 𝑧 ∈ ℂ) | 
| 194 | 192, 193 | negsubd 11626 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (𝑥 + -𝑧) = (𝑥 − 𝑧)) | 
| 195 | 194 | breq1d 5153 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑥 + -𝑧) < 𝑤 ↔ (𝑥 − 𝑧) < 𝑤)) | 
| 196 | 191, 195 | bitr3d 281 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → (-𝑧 < (𝑤 − 𝑥) ↔ (𝑥 − 𝑧) < 𝑤)) | 
| 197 | 185, 186,
188 | ltsubaddd 11859 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((𝑤 − 𝑥) < 𝑧 ↔ 𝑤 < (𝑧 + 𝑥))) | 
| 198 | 196, 197 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((-𝑧 < (𝑤 − 𝑥) ∧ (𝑤 − 𝑥) < 𝑧) ↔ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)))) | 
| 199 | 189, 198 | bitrd 279 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → ((abs‘(𝑤 − 𝑥)) < 𝑧 ↔ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥)))) | 
| 200 | 199 | pm5.32da 579 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ∧ (abs‘(𝑤 − 𝑥)) < 𝑧) ↔ (𝑤 ∈ ℝ ∧ ((𝑥 − 𝑧) < 𝑤 ∧ 𝑤 < (𝑧 + 𝑥))))) | 
| 201 | 184, 200 | bitr4d 282 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)) ↔ (𝑤 ∈ ℝ ∧ (abs‘(𝑤 − 𝑥)) < 𝑧))) | 
| 202 | 201 | biimpa 476 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → (𝑤 ∈ ℝ ∧ (abs‘(𝑤 − 𝑥)) < 𝑧)) | 
| 203 |  | pm3.35 803 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((abs‘(𝑤
− 𝑥)) < 𝑧 ∧ ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) | 
| 204 | 203 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((abs‘(𝑤
− 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ∧ (abs‘(𝑤 − 𝑥)) < 𝑧) → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) | 
| 205 | 69 | ad6antlr 737 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → 𝑦 ∈ ℝ) | 
| 206 |  | rge0ssre 13496 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(0[,)+∞) ⊆ ℝ | 
| 207 | 3 | ad4antr 732 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞)) | 
| 208 | 207 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑤) ∈ (0[,)+∞)) | 
| 209 | 206, 208 | sselid 3981 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑤) ∈ ℝ) | 
| 210 | 209 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → (𝐹‘𝑤) ∈ ℝ) | 
| 211 | 3 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞)) | 
| 212 | 211 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) | 
| 213 | 206, 212 | sselid 3981 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) | 
| 214 | 74, 213 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹‘𝑥) ∈ ℝ) | 
| 215 | 214 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) | 
| 216 | 209, 215 | resubcld 11691 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹‘𝑤) − (𝐹‘𝑥)) ∈ ℝ) | 
| 217 | 69 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ) | 
| 218 | 214, 217 | resubcld 11691 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹‘𝑥) − 𝑦) ∈ ℝ) | 
| 219 | 218 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → ((𝐹‘𝑥) − 𝑦) ∈ ℝ) | 
| 220 | 216, 219 | absltd 15468 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) →
((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦) ↔ (-((𝐹‘𝑥) − 𝑦) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ∧ ((𝐹‘𝑤) − (𝐹‘𝑥)) < ((𝐹‘𝑥) − 𝑦)))) | 
| 221 | 214 | recnd 11289 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐹‘𝑥) ∈ ℂ) | 
| 222 |  | rpcn 13045 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) | 
| 223 | 222 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ) | 
| 224 | 221, 223 | negsubdi2d 11636 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → -((𝐹‘𝑥) − 𝑦) = (𝑦 − (𝐹‘𝑥))) | 
| 225 | 224 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) → -((𝐹‘𝑥) − 𝑦) = (𝑦 − (𝐹‘𝑥))) | 
| 226 | 225 | breq1d 5153 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) →
(-((𝐹‘𝑥) − 𝑦) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ↔ (𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥)))) | 
| 227 | 226 | anbi1d 631 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) →
((-((𝐹‘𝑥) − 𝑦) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ∧ ((𝐹‘𝑤) − (𝐹‘𝑥)) < ((𝐹‘𝑥) − 𝑦)) ↔ ((𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ∧ ((𝐹‘𝑤) − (𝐹‘𝑥)) < ((𝐹‘𝑥) − 𝑦)))) | 
| 228 | 220, 227 | bitrd 279 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) →
((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦) ↔ ((𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥)) ∧ ((𝐹‘𝑤) − (𝐹‘𝑥)) < ((𝐹‘𝑥) − 𝑦)))) | 
| 229 | 228 | simprbda 498 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → (𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥))) | 
| 230 | 214 | ad4antr 732 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → (𝐹‘𝑥) ∈ ℝ) | 
| 231 | 205, 210,
230 | ltsub1d 11872 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → (𝑦 < (𝐹‘𝑤) ↔ (𝑦 − (𝐹‘𝑥)) < ((𝐹‘𝑤) − (𝐹‘𝑥)))) | 
| 232 | 229, 231 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → 𝑦 < (𝐹‘𝑤)) | 
| 233 | 205, 210,
232 | ltled 11409 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) → 𝑦 ≤ (𝐹‘𝑤)) | 
| 234 | 204, 233 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℝ) ∧
(((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ∧ (abs‘(𝑤 − 𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹‘𝑤)) | 
| 235 | 234 | an4s 660 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ (𝑤 ∈ ℝ ∧ (abs‘(𝑤 − 𝑥)) < 𝑧)) → 𝑦 ≤ (𝐹‘𝑤)) | 
| 236 | 202, 235 | syldan 591 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ (𝐹‘𝑤)) | 
| 237 | 236 | iftrued 4533 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) = 𝑦) | 
| 238 | 174, 237 | breqtrrd 5171 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → 𝑦 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) | 
| 239 |  | 0le0 12367 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ≤
0 | 
| 240 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) → (0 ≤ 𝑦 ↔ 0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))) | 
| 241 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 =
if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0))) | 
| 242 | 240, 241 | ifboth 4565 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0 ≤
𝑦 ∧ 0 ≤ 0) → 0
≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) | 
| 243 | 156, 239,
242 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℝ+
→ 0 ≤ if(𝑦 ≤
(𝐹‘𝑤), 𝑦, 0)) | 
| 244 | 243 | ad6antlr 737 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ ¬ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) → 0 ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) | 
| 245 | 171, 172,
238, 244 | ifbothda 4564 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
((abs‘(𝑤 −
𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) | 
| 246 | 170, 245 | sylan2 593 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
(∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)) ∧ 𝑤 ∈ (𝑋(,)𝑌))) → if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) | 
| 247 | 246 | anassrs 467 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0) ≤ if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) | 
| 248 |  | iftrue 4531 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0)) | 
| 249 | 248 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0)) | 
| 250 |  | iftrue 4531 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) | 
| 251 | 250 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) = if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0)) | 
| 252 | 247, 249,
251 | 3brtr4d 5175 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ (𝑋(,)𝑌)) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0)) | 
| 253 | 252 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0))) | 
| 254 | 239 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑤 ∈ (𝑋(,)𝑌) → 0 ≤ 0) | 
| 255 |  | iffalse 4534 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) = 0) | 
| 256 |  | iffalse 4534 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) = 0) | 
| 257 | 254, 255,
256 | 3brtr4d 5175 | . . . . . . . . . . . . . . . . 17
⊢ (¬
𝑤 ∈ (𝑋(,)𝑌) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0)) | 
| 258 | 253, 257 | pm2.61d1 180 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) ≤ if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0)) | 
| 259 |  | elin 3967 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)))) | 
| 260 |  | ifbi 4548 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))) ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) | 
| 261 | 259, 260 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) | 
| 262 |  | ifan 4579 | . . . . . . . . . . . . . . . . 17
⊢ if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) | 
| 263 | 261, 262 | eqtri 2765 | . . . . . . . . . . . . . . . 16
⊢ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑤 ∈ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥)), 𝑦, 0), 0) | 
| 264 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = 𝑤 → (𝐹‘𝑣) = (𝐹‘𝑤)) | 
| 265 | 264 | breq2d 5155 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑤 → (𝑦 ≤ (𝐹‘𝑣) ↔ 𝑦 ≤ (𝐹‘𝑤))) | 
| 266 | 265 | elrab 3692 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤))) | 
| 267 |  | ifbi 4548 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)} ↔ (𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤))) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤)), 𝑦, 0)) | 
| 268 | 266, 267 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) = if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤)), 𝑦, 0) | 
| 269 |  | ifan 4579 | . . . . . . . . . . . . . . . . 17
⊢ if((𝑤 ∈ (𝑋(,)𝑌) ∧ 𝑦 ≤ (𝐹‘𝑤)), 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) | 
| 270 | 268, 269 | eqtri 2765 | . . . . . . . . . . . . . . . 16
⊢ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) = if(𝑤 ∈ (𝑋(,)𝑌), if(𝑦 ≤ (𝐹‘𝑤), 𝑦, 0), 0) | 
| 271 | 258, 263,
270 | 3brtr4g 5177 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) | 
| 272 | 271 | ralrimivw 3150 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) | 
| 273 |  | reex 11246 | . . . . . . . . . . . . . . . 16
⊢ ℝ
∈ V | 
| 274 | 273 | a1i 11 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → ℝ ∈ V) | 
| 275 | 56 | ad6antlr 737 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ∈ (0[,]+∞)) | 
| 276 | 63 | ad6antlr 737 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞)) | 
| 277 |  | eqidd 2738 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) | 
| 278 |  | eqidd 2738 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) | 
| 279 | 274, 275,
276, 277, 278 | ofrfval2 7718 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → ((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘r ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0) ≤ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) | 
| 280 | 272, 279 | mpbird 257 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘r ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) | 
| 281 |  | itg2le 25774 | . . . . . . . . . . . . 13
⊢ (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)):ℝ⟶(0[,]+∞) ∧
(𝑤 ∈ ℝ ↦
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧
(𝑤 ∈ ℝ ↦
if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0)) ∘r ≤ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))) | 
| 282 | 165, 166,
280, 281 | syl3anc 1373 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ ((𝑋(,)𝑌) ∩ ((𝑥 − 𝑧)(,)(𝑧 + 𝑥))), 𝑦, 0))) ≤ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))) | 
| 283 | 49, 61, 68, 164, 282 | xrltletrd 13203 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) ∧ 𝑧 ∈ ℝ+) ∧
∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) → 0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))) | 
| 284 |  | itg2gt0cn.cn | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) | 
| 285 | 284 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) | 
| 286 |  | simplr 769 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 𝑥 ∈ (𝑋(,)𝑌)) | 
| 287 |  | fssres 6774 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (𝑋(,)𝑌) ⊆ ℝ) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞)) | 
| 288 | 26, 287 | mpan2 691 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹:ℝ⟶(0[,)+∞)
→ (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞)) | 
| 289 |  | fss 6752 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) ∧ (0[,)+∞)
⊆ ℝ) → (𝐹
↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ) | 
| 290 | 206, 289 | mpan2 691 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶(0[,)+∞) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ) | 
| 291 | 3, 288, 290 | 3syl 18 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ) | 
| 292 | 291 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝐹 ↾ (𝑋(,)𝑌)):(𝑋(,)𝑌)⟶ℝ) | 
| 293 | 292 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ∈ ℝ) | 
| 294 | 293, 217 | resubcld 11691 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ) | 
| 295 | 294 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ) | 
| 296 | 217, 293 | posdifd 11850 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))) | 
| 297 | 296 | biimpa 476 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → 0 < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) | 
| 298 | 295, 297 | elrpd 13074 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈
ℝ+) | 
| 299 |  | cncfi 24920 | . . . . . . . . . . . . . . 15
⊢ (((𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ 𝑥 ∈ (𝑋(,)𝑌) ∧ (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))) | 
| 300 | 285, 286,
298, 299 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦))) | 
| 301 | 300 | ex 412 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)))) | 
| 302 |  | fvres 6925 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹‘𝑥)) | 
| 303 | 302 | breq2d 5155 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑋(,)𝑌) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹‘𝑥))) | 
| 304 | 303 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) ↔ 𝑦 < (𝐹‘𝑥))) | 
| 305 |  | fvres 6925 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ (𝑋(,)𝑌) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹‘𝑢)) | 
| 306 | 305 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) = (𝐹‘𝑢)) | 
| 307 | 302 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) = (𝐹‘𝑥)) | 
| 308 | 306, 307 | oveq12d 7449 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥)) = ((𝐹‘𝑢) − (𝐹‘𝑥))) | 
| 309 | 308 | fveq2d 6910 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) = (abs‘((𝐹‘𝑢) − (𝐹‘𝑥)))) | 
| 310 | 302 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝑋(,)𝑌) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹‘𝑥) − 𝑦)) | 
| 311 | 310 | ad2antlr 727 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) = ((𝐹‘𝑥) − 𝑦)) | 
| 312 | 309, 311 | breq12d 5156 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → ((abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦) ↔ (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) | 
| 313 | 312 | imbi2d 340 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑢 ∈ (𝑋(,)𝑌)) → (((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))) | 
| 314 | 313 | ralbidva 3176 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))) | 
| 315 | 314 | rexbidv 3179 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘(((𝐹 ↾ (𝑋(,)𝑌))‘𝑢) − ((𝐹 ↾ (𝑋(,)𝑌))‘𝑥))) < (((𝐹 ↾ (𝑋(,)𝑌))‘𝑥) − 𝑦)) ↔ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))) | 
| 316 | 301, 304,
315 | 3imtr3d 293 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝑦 < (𝐹‘𝑥) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦)))) | 
| 317 | 316 | imp 406 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ (𝑋(,)𝑌)((abs‘(𝑢 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑥))) < ((𝐹‘𝑥) − 𝑦))) | 
| 318 | 283, 317 | r19.29a 3162 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ (𝑋(,)𝑌)) ∧ 𝑦 < (𝐹‘𝑥)) → 0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))) | 
| 319 | 318 | rexlimdva2 3157 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∃𝑥 ∈ (𝑋(,)𝑌)𝑦 < (𝐹‘𝑥) → 0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))))) | 
| 320 | 48, 319 | sylbid 240 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ) → 0
< (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))))) | 
| 321 | 320 | imp 406 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0
< (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)))) | 
| 322 | 65 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(𝑤 ∈ ℝ ↦
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦,
0)):ℝ⟶(0[,]+∞)) | 
| 323 |  | icossicc 13476 | . . . . . . . . . 10
⊢
(0[,)+∞) ⊆ (0[,]+∞) | 
| 324 |  | fss 6752 | . . . . . . . . . 10
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞)) | 
| 325 | 3, 323, 324 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) | 
| 326 | 325 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
𝐹:ℝ⟶(0[,]+∞)) | 
| 327 |  | breq1 5146 | . . . . . . . . . . . 12
⊢ (𝑦 = if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) → (𝑦 ≤ (𝐹‘𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤))) | 
| 328 |  | breq1 5146 | . . . . . . . . . . . 12
⊢ (0 =
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) → (0 ≤ (𝐹‘𝑤) ↔ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤))) | 
| 329 | 266 | simprbi 496 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)} → 𝑦 ≤ (𝐹‘𝑤)) | 
| 330 | 329 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}) → 𝑦 ≤ (𝐹‘𝑤)) | 
| 331 | 3 | ffvelcdmda 7104 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑤) ∈ (0[,)+∞)) | 
| 332 |  | elrege0 13494 | . . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑤) ∈ (0[,)+∞) ↔ ((𝐹‘𝑤) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑤))) | 
| 333 | 331, 332 | sylib 218 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → ((𝐹‘𝑤) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑤))) | 
| 334 | 333 | simprd 495 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → 0 ≤ (𝐹‘𝑤)) | 
| 335 | 334 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ¬ 𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}) → 0 ≤ (𝐹‘𝑤)) | 
| 336 | 327, 328,
330, 335 | ifbothda 4564 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤)) | 
| 337 | 336 | ralrimiva 3146 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤)) | 
| 338 | 337 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
∀𝑤 ∈ ℝ
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤)) | 
| 339 | 273 | a1i 11 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
ℝ ∈ V) | 
| 340 | 63 | ad3antlr 731 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ∈ (0[,]+∞)) | 
| 341 |  | fvexd 6921 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) ∧ 𝑤 ∈ ℝ) → (𝐹‘𝑤) ∈ V) | 
| 342 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(𝑤 ∈ ℝ ↦
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) = (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) | 
| 343 | 3 | feqmptd 6977 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑤 ∈ ℝ ↦ (𝐹‘𝑤))) | 
| 344 | 343 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
𝐹 = (𝑤 ∈ ℝ ↦ (𝐹‘𝑤))) | 
| 345 | 339, 340,
341, 342, 344 | ofrfval2 7718 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
((𝑤 ∈ ℝ ↦
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) ∘r ≤ 𝐹 ↔ ∀𝑤 ∈ ℝ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0) ≤ (𝐹‘𝑤))) | 
| 346 | 338, 345 | mpbird 257 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(𝑤 ∈ ℝ ↦
if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) ∘r ≤ 𝐹) | 
| 347 |  | itg2le 25774 | . . . . . . . 8
⊢ (((𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)):ℝ⟶(0[,]+∞) ∧
𝐹:ℝ⟶(0[,]+∞) ∧ (𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0)) ∘r ≤ 𝐹) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) | 
| 348 | 322, 326,
346, 347 | syl3anc 1373 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) | 
| 349 | 40, 321, 348 | jca32 515 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(𝑦 ∈
ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)))) | 
| 350 | 349 | expl 457 | . . . . 5
⊢ (𝜑 → ((𝑦 ∈ ℝ+ ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
(𝑦 ∈
ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹))))) | 
| 351 | 39, 350 | syl5 34 | . . . 4
⊢ (𝜑 → ((𝑦 ∈ ℚ ∧ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < ))) →
(𝑦 ∈
ℝ+ ∧ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹))))) | 
| 352 | 351 | reximdv2 3164 | . . 3
⊢ (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) →
∃𝑦 ∈
ℝ+ (0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)))) | 
| 353 | 67 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈
ℝ*) | 
| 354 |  | itg2cl 25767 | . . . . . . 7
⊢ (𝐹:ℝ⟶(0[,]+∞)
→ (∫2‘𝐹) ∈
ℝ*) | 
| 355 | 325, 354 | syl 17 | . . . . . 6
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ*) | 
| 356 | 355 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∫2‘𝐹)
∈ ℝ*) | 
| 357 |  | xrltletr 13199 | . . . . 5
⊢ ((0
∈ ℝ* ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∈ ℝ* ∧
(∫2‘𝐹)
∈ ℝ*) → ((0 < (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) → 0 <
(∫2‘𝐹))) | 
| 358 | 1, 353, 356, 357 | mp3an2i 1468 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ((0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) → 0 <
(∫2‘𝐹))) | 
| 359 | 358 | rexlimdva 3155 | . . 3
⊢ (𝜑 → (∃𝑦 ∈ ℝ+ (0 <
(∫2‘(𝑤
∈ ℝ ↦ if(𝑤
∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ∧ (∫2‘(𝑤 ∈ ℝ ↦ if(𝑤 ∈ {𝑣 ∈ (𝑋(,)𝑌) ∣ 𝑦 ≤ (𝐹‘𝑣)}, 𝑦, 0))) ≤ (∫2‘𝐹)) → 0 <
(∫2‘𝐹))) | 
| 360 | 352, 359 | syld 47 | . 2
⊢ (𝜑 → (∃𝑦 ∈ ℚ (0 < 𝑦 ∧ 𝑦 < sup((𝐹 “ (𝑋(,)𝑌)), ℝ*, < )) → 0
< (∫2‘𝐹))) | 
| 361 | 33, 360 | mpd 15 | 1
⊢ (𝜑 → 0 <
(∫2‘𝐹)) |