Metamath Proof Explorer

Theorem itg2gt0cn

Description: itg2gt0 holds on functions continuous on an open interval in the absence of ax-cc . The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017)

Ref Expression
Hypotheses itg2gt0cn.2 ⊢ ( 𝜑 → 𝑋 < 𝑌 )
itg2gt0cn.3 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
itg2gt0cn.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 0 < ( 𝐹 ‘ 𝑥 ) )
itg2gt0cn.cn ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
Assertion itg2gt0cn ( 𝜑 → 0 < ( ∫2 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 itg2gt0cn.2 ⊢ ( 𝜑 → 𝑋 < 𝑌 )
2 itg2gt0cn.3 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
3 itg2gt0cn.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 0 < ( 𝐹 ‘ 𝑥 ) )
4 itg2gt0cn.cn ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
5 0xr ⊢ 0 ∈ ℝ*
6 imassrn ⊢ ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) ⊆ ran 𝐹
7 2 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 0 [,) +∞ ) )
8 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
9 7 8 sstrdi ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ* )
10 6 9 sstrid ⊢ ( 𝜑 → ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) ⊆ ℝ* )
11 supxrcl ⊢ ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) ⊆ ℝ* → sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ∈ ℝ* )
12 10 11 syl ⊢ ( 𝜑 → sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ∈ ℝ* )
13 ltrelxr ⊢ < ⊆ ( ℝ* × ℝ* )
14 13 ssbri ⊢ ( 𝑋 < 𝑌 → 𝑋 ( ℝ* × ℝ* ) 𝑌 )
15 1 14 syl ⊢ ( 𝜑 → 𝑋 ( ℝ* × ℝ* ) 𝑌 )
16 brxp ⊢ ( 𝑋 ( ℝ* × ℝ* ) 𝑌 ↔ ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ) )
17 15 16 sylib ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ) )
18 ioon0 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ) → ( ( 𝑋 (,) 𝑌 ) ≠ ∅ ↔ 𝑋 < 𝑌 ) )
19 17 18 syl ⊢ ( 𝜑 → ( ( 𝑋 (,) 𝑌 ) ≠ ∅ ↔ 𝑋 < 𝑌 ) )
20 1 19 mpbird ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ≠ ∅ )
21 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 0 < ( 𝐹 ‘ 𝑥 ) )
22 r19.2z ⊢ ( ( ( 𝑋 (,) 𝑌 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 0 < ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 0 < ( 𝐹 ‘ 𝑥 ) )
23 20 21 22 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 0 < ( 𝐹 ‘ 𝑥 ) )
24 supxrlub ⊢ ( ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) ⊆ ℝ* ∧ 0 ∈ ℝ* ) → ( 0 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ↔ ∃ 𝑦 ∈ ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) 0 < 𝑦 ) )
25 10 5 24 sylancl ⊢ ( 𝜑 → ( 0 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ↔ ∃ 𝑦 ∈ ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) 0 < 𝑦 ) )
26 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℝ )
27 ioossre ⊢ ( 𝑋 (,) 𝑌 ) ⊆ ℝ
28 breq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 0 < 𝑦 ↔ 0 < ( 𝐹 ‘ 𝑥 ) ) )
29 28 rexima ⊢ ( ( 𝐹 Fn ℝ ∧ ( 𝑋 (,) 𝑌 ) ⊆ ℝ ) → ( ∃ 𝑦 ∈ ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) 0 < 𝑦 ↔ ∃ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 0 < ( 𝐹 ‘ 𝑥 ) ) )
30 26 27 29 sylancl ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) 0 < 𝑦 ↔ ∃ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 0 < ( 𝐹 ‘ 𝑥 ) ) )
31 25 30 bitrd ⊢ ( 𝜑 → ( 0 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ↔ ∃ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 0 < ( 𝐹 ‘ 𝑥 ) ) )
32 23 31 mpbird ⊢ ( 𝜑 → 0 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) )
33 qbtwnxr ⊢ ( ( 0 ∈ ℝ* ∧ sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ∈ ℝ* ∧ 0 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → ∃ 𝑦 ∈ ℚ ( 0 < 𝑦 ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) )
34 5 12 32 33 mp3an2i ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℚ ( 0 < 𝑦 ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) )
35 qre ⊢ ( 𝑦 ∈ ℚ → 𝑦 ∈ ℝ )
36 35 adantr ⊢ ( ( 𝑦 ∈ ℚ ∧ 0 < 𝑦 ) → 𝑦 ∈ ℝ )
37 simpr ⊢ ( ( 𝑦 ∈ ℚ ∧ 0 < 𝑦 ) → 0 < 𝑦 )
38 36 37 elrpd ⊢ ( ( 𝑦 ∈ ℚ ∧ 0 < 𝑦 ) → 𝑦 ∈ ℝ+ )
39 38 anim1i ⊢ ( ( ( 𝑦 ∈ ℚ ∧ 0 < 𝑦 ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → ( 𝑦 ∈ ℝ+ ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) )
40 39 anasss ⊢ ( ( 𝑦 ∈ ℚ ∧ ( 0 < 𝑦 ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) ) → ( 𝑦 ∈ ℝ+ ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) )
41 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → 𝑦 ∈ ℝ+ )
42 rpxr ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ* )
43 supxrlub ⊢ ( ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) ⊆ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ↔ ∃ 𝑧 ∈ ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) 𝑦 < 𝑧 ) )
44 10 42 43 syl2an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ↔ ∃ 𝑧 ∈ ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) 𝑦 < 𝑧 ) )
45 breq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 < 𝑧 ↔ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) )
46 45 rexima ⊢ ( ( 𝐹 Fn ℝ ∧ ( 𝑋 (,) 𝑌 ) ⊆ ℝ ) → ( ∃ 𝑧 ∈ ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) 𝑦 < 𝑧 ↔ ∃ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 𝑦 < ( 𝐹 ‘ 𝑥 ) ) )
47 26 27 46 sylancl ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) 𝑦 < 𝑧 ↔ ∃ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 𝑦 < ( 𝐹 ‘ 𝑥 ) ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) 𝑦 < 𝑧 ↔ ∃ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 𝑦 < ( 𝐹 ‘ 𝑥 ) ) )
49 44 48 bitrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ↔ ∃ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 𝑦 < ( 𝐹 ‘ 𝑥 ) ) )
50 5 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → 0 ∈ ℝ* )
51 ioorp ⊢ ( 0 (,) +∞ ) = ℝ+
52 ioossicc ⊢ ( 0 (,) +∞ ) ⊆ ( 0 [,] +∞ )
53 51 52 eqsstrri ⊢ ℝ+ ⊆ ( 0 [,] +∞ )
54 53 sseli ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ( 0 [,] +∞ ) )
55 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
56 ifcl ⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ∈ ( 0 [,] +∞ ) )
57 54 55 56 sylancl ⊢ ( 𝑦 ∈ ℝ+ → if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ∈ ( 0 [,] +∞ ) )
58 57 adantr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑤 ∈ ℝ ) → if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ∈ ( 0 [,] +∞ ) )
59 58 fmpttd ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
60 itg2cl ⊢ ( ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ) ∈ ℝ* )
61 59 60 syl ⊢ ( 𝑦 ∈ ℝ+ → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ) ∈ ℝ* )
62 61 ad5antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ) ∈ ℝ* )
63 ifcl ⊢ ( ( 𝑦 ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ∈ ( 0 [,] +∞ ) )
64 54 55 63 sylancl ⊢ ( 𝑦 ∈ ℝ+ → if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ∈ ( 0 [,] +∞ ) )
65 64 adantr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑤 ∈ ℝ ) → if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ∈ ( 0 [,] +∞ ) )
66 65 fmpttd ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
67 itg2cl ⊢ ( ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ∈ ℝ* )
68 66 67 syl ⊢ ( 𝑦 ∈ ℝ+ → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ∈ ℝ* )
69 68 ad5antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ∈ ℝ* )
70 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
71 70 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑦 ∈ ℝ )
72 ioombl ⊢ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ∈ dom vol
73 mblvol ⊢ ( ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ∈ dom vol → ( vol ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) = ( vol* ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) )
74 72 73 ax-mp ⊢ ( vol ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) = ( vol* ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) )
75 elioore ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → 𝑥 ∈ ℝ )
76 75 ad3antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
77 rpre ⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ )
78 77 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑧 ∈ ℝ )
79 76 78 resubcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑥 − 𝑧 ) ∈ ℝ )
80 79 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑋 ≤ ( 𝑥 − 𝑧 ) ) → ( 𝑥 − 𝑧 ) ∈ ℝ )
81 79 rexrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑥 − 𝑧 ) ∈ ℝ* )
82 81 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ¬ 𝑋 ≤ ( 𝑥 − 𝑧 ) ) → ( 𝑥 − 𝑧 ) ∈ ℝ* )
83 17 simpld ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
84 83 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ¬ 𝑋 ≤ ( 𝑥 − 𝑧 ) ) → 𝑋 ∈ ℝ* )
85 17 simprd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
86 85 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ¬ 𝑋 ≤ ( 𝑥 − 𝑧 ) ) → 𝑌 ∈ ℝ* )
87 83 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑋 ∈ ℝ* )
88 xrltnle ⊢ ( ( ( 𝑥 − 𝑧 ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑥 − 𝑧 ) < 𝑋 ↔ ¬ 𝑋 ≤ ( 𝑥 − 𝑧 ) ) )
89 81 87 88 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝑥 − 𝑧 ) < 𝑋 ↔ ¬ 𝑋 ≤ ( 𝑥 − 𝑧 ) ) )
90 89 biimpar ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ¬ 𝑋 ≤ ( 𝑥 − 𝑧 ) ) → ( 𝑥 − 𝑧 ) < 𝑋 )
91 1 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ¬ 𝑋 ≤ ( 𝑥 − 𝑧 ) ) → 𝑋 < 𝑌 )
92 xrre2 ⊢ ( ( ( ( 𝑥 − 𝑧 ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ) ∧ ( ( 𝑥 − 𝑧 ) < 𝑋 ∧ 𝑋 < 𝑌 ) ) → 𝑋 ∈ ℝ )
93 82 84 86 90 91 92 syl32anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ¬ 𝑋 ≤ ( 𝑥 − 𝑧 ) ) → 𝑋 ∈ ℝ )
94 80 93 ifclda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) ∈ ℝ )
95 85 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑌 ≤ ( 𝑧 + 𝑥 ) ) → 𝑌 ∈ ℝ* )
96 78 76 readdcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑧 + 𝑥 ) ∈ ℝ )
97 96 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑌 ≤ ( 𝑧 + 𝑥 ) ) → ( 𝑧 + 𝑥 ) ∈ ℝ )
98 mnfxr ⊢ -∞ ∈ ℝ*
99 98 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
100 mnfle ⊢ ( 𝑋 ∈ ℝ* → -∞ ≤ 𝑋 )
101 83 100 syl ⊢ ( 𝜑 → -∞ ≤ 𝑋 )
102 99 83 85 101 1 xrlelttrd ⊢ ( 𝜑 → -∞ < 𝑌 )
103 102 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑌 ≤ ( 𝑧 + 𝑥 ) ) → -∞ < 𝑌 )
104 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑌 ≤ ( 𝑧 + 𝑥 ) ) → 𝑌 ≤ ( 𝑧 + 𝑥 ) )
105 xrre ⊢ ( ( ( 𝑌 ∈ ℝ* ∧ ( 𝑧 + 𝑥 ) ∈ ℝ ) ∧ ( -∞ < 𝑌 ∧ 𝑌 ≤ ( 𝑧 + 𝑥 ) ) ) → 𝑌 ∈ ℝ )
106 95 97 103 104 105 syl22anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑌 ≤ ( 𝑧 + 𝑥 ) ) → 𝑌 ∈ ℝ )
107 96 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ¬ 𝑌 ≤ ( 𝑧 + 𝑥 ) ) → ( 𝑧 + 𝑥 ) ∈ ℝ )
108 106 107 ifclda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ∈ ℝ )
109 76 rexrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑥 ∈ ℝ* )
110 85 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑌 ∈ ℝ* )
111 rpgt0 ⊢ ( 𝑧 ∈ ℝ+ → 0 < 𝑧 )
112 111 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 0 < 𝑧 )
113 78 76 ltsubposd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 0 < 𝑧 ↔ ( 𝑥 − 𝑧 ) < 𝑥 ) )
114 112 113 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑥 − 𝑧 ) < 𝑥 )
115 eliooord ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → ( 𝑋 < 𝑥 ∧ 𝑥 < 𝑌 ) )
116 115 simprd ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → 𝑥 < 𝑌 )
117 116 ad3antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑥 < 𝑌 )
118 81 109 110 114 117 xrlttrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑥 − 𝑧 ) < 𝑌 )
119 78 76 ltaddpos2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 0 < 𝑧 ↔ 𝑥 < ( 𝑧 + 𝑥 ) ) )
120 112 119 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑥 < ( 𝑧 + 𝑥 ) )
121 79 76 96 114 120 lttrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑥 − 𝑧 ) < ( 𝑧 + 𝑥 ) )
122 breq2 ⊢ ( 𝑌 = if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) → ( ( 𝑥 − 𝑧 ) < 𝑌 ↔ ( 𝑥 − 𝑧 ) < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) )
123 breq2 ⊢ ( ( 𝑧 + 𝑥 ) = if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) → ( ( 𝑥 − 𝑧 ) < ( 𝑧 + 𝑥 ) ↔ ( 𝑥 − 𝑧 ) < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) )
124 122 123 ifboth ⊢ ( ( ( 𝑥 − 𝑧 ) < 𝑌 ∧ ( 𝑥 − 𝑧 ) < ( 𝑧 + 𝑥 ) ) → ( 𝑥 − 𝑧 ) < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) )
125 118 121 124 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑥 − 𝑧 ) < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) )
126 1 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑋 < 𝑌 )
127 96 rexrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑧 + 𝑥 ) ∈ ℝ* )
128 115 simpld ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → 𝑋 < 𝑥 )
129 128 ad3antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑋 < 𝑥 )
130 87 109 127 129 120 xrlttrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑋 < ( 𝑧 + 𝑥 ) )
131 breq2 ⊢ ( 𝑌 = if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) → ( 𝑋 < 𝑌 ↔ 𝑋 < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) )
132 breq2 ⊢ ( ( 𝑧 + 𝑥 ) = if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) → ( 𝑋 < ( 𝑧 + 𝑥 ) ↔ 𝑋 < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) )
133 131 132 ifboth ⊢ ( ( 𝑋 < 𝑌 ∧ 𝑋 < ( 𝑧 + 𝑥 ) ) → 𝑋 < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) )
134 126 130 133 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑋 < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) )
135 breq1 ⊢ ( ( 𝑥 − 𝑧 ) = if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) → ( ( 𝑥 − 𝑧 ) < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ↔ if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) )
136 breq1 ⊢ ( 𝑋 = if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) → ( 𝑋 < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ↔ if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) )
137 135 136 ifboth ⊢ ( ( ( 𝑥 − 𝑧 ) < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ∧ 𝑋 < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) → if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) )
138 125 134 137 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) )
139 94 108 138 ltled ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) ≤ if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) )
140 ovolioo ⊢ ( ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) ∈ ℝ ∧ if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ∈ ℝ ∧ if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) ≤ if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) → ( vol* ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) = ( if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) − if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) ) )
141 94 108 139 140 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( vol* ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) = ( if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) − if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) ) )
142 74 141 syl5eq ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( vol ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) = ( if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) − if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) ) )
143 108 94 resubcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) − if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) ) ∈ ℝ )
144 142 143 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( vol ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) ∈ ℝ )
145 rpgt0 ⊢ ( 𝑦 ∈ ℝ+ → 0 < 𝑦 )
146 145 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 0 < 𝑦 )
147 94 108 posdifd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) < if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ↔ 0 < ( if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) − if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) ) ) )
148 138 147 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 0 < ( if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) − if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) ) )
149 148 142 breqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 0 < ( vol ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) )
150 71 144 146 149 mulgt0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 0 < ( 𝑦 · ( vol ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) ) )
151 iooin ⊢ ( ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ) ∧ ( ( 𝑥 − 𝑧 ) ∈ ℝ* ∧ ( 𝑧 + 𝑥 ) ∈ ℝ* ) ) → ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) = ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) )
152 87 110 81 127 151 syl22anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) = ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) )
153 152 eleq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) ↔ 𝑤 ∈ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) )
154 153 ifbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) = if ( 𝑤 ∈ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) )
155 154 mpteq2dv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) = ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) )
156 155 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ) = ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ) )
157 rpge0 ⊢ ( 𝑦 ∈ ℝ+ → 0 ≤ 𝑦 )
158 elrege0 ⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ) )
159 70 157 158 sylanbrc ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ( 0 [,) +∞ ) )
160 159 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑦 ∈ ( 0 [,) +∞ ) )
161 itg2const ⊢ ( ( ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ∈ dom vol ∧ ( vol ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) ∈ ℝ ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ) = ( 𝑦 · ( vol ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) ) )
162 72 144 160 161 mp3an2i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ) = ( 𝑦 · ( vol ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) ) )
163 156 162 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ) = ( 𝑦 · ( vol ‘ ( if ( 𝑋 ≤ ( 𝑥 − 𝑧 ) , ( 𝑥 − 𝑧 ) , 𝑋 ) (,) if ( 𝑌 ≤ ( 𝑧 + 𝑥 ) , 𝑌 , ( 𝑧 + 𝑥 ) ) ) ) ) )
164 150 163 breqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ) )
165 164 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ) )
166 59 ad5antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
167 66 ad5antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
168 fvoveq1 ⊢ ( 𝑢 = 𝑤 → ( abs ‘ ( 𝑢 − 𝑥 ) ) = ( abs ‘ ( 𝑤 − 𝑥 ) ) )
169 168 breq1d ⊢ ( 𝑢 = 𝑤 → ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 ) )
170 169 imbrov2fvoveq ⊢ ( 𝑢 = 𝑤 → ( ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ↔ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) )
171 170 rspccva ⊢ ( ( ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ∧ 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) )
172 breq1 ⊢ ( 𝑦 = if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) → ( 𝑦 ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) ↔ if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) ) )
173 breq1 ⊢ ( 0 = if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) → ( 0 ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) ↔ if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) ) )
174 70 leidd ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ≤ 𝑦 )
175 174 ad6antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) → 𝑦 ≤ 𝑦 )
176 75 ad4antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → 𝑥 ∈ ℝ )
177 77 ad2antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → 𝑧 ∈ ℝ )
178 176 177 resubcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑥 − 𝑧 ) ∈ ℝ )
179 178 rexrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑥 − 𝑧 ) ∈ ℝ* )
180 177 176 readdcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑧 + 𝑥 ) ∈ ℝ )
181 180 rexrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑧 + 𝑥 ) ∈ ℝ* )
182 elioo2 ⊢ ( ( ( 𝑥 − 𝑧 ) ∈ ℝ* ∧ ( 𝑧 + 𝑥 ) ∈ ℝ* ) → ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ↔ ( 𝑤 ∈ ℝ ∧ ( 𝑥 − 𝑧 ) < 𝑤 ∧ 𝑤 < ( 𝑧 + 𝑥 ) ) ) )
183 179 181 182 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ↔ ( 𝑤 ∈ ℝ ∧ ( 𝑥 − 𝑧 ) < 𝑤 ∧ 𝑤 < ( 𝑧 + 𝑥 ) ) ) )
184 3anass ⊢ ( ( 𝑤 ∈ ℝ ∧ ( 𝑥 − 𝑧 ) < 𝑤 ∧ 𝑤 < ( 𝑧 + 𝑥 ) ) ↔ ( 𝑤 ∈ ℝ ∧ ( ( 𝑥 − 𝑧 ) < 𝑤 ∧ 𝑤 < ( 𝑧 + 𝑥 ) ) ) )
185 183 184 bitrdi ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ↔ ( 𝑤 ∈ ℝ ∧ ( ( 𝑥 − 𝑧 ) < 𝑤 ∧ 𝑤 < ( 𝑧 + 𝑥 ) ) ) ) )
186 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ )
187 75 ad5antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → 𝑥 ∈ ℝ )
188 186 187 resubcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → ( 𝑤 − 𝑥 ) ∈ ℝ )
189 77 ad3antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → 𝑧 ∈ ℝ )
190 188 189 absltd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 ↔ ( - 𝑧 < ( 𝑤 − 𝑥 ) ∧ ( 𝑤 − 𝑥 ) < 𝑧 ) ) )
191 189 renegcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → - 𝑧 ∈ ℝ )
192 187 191 186 ltaddsub2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → ( ( 𝑥 + - 𝑧 ) < 𝑤 ↔ - 𝑧 < ( 𝑤 − 𝑥 ) ) )
193 187 recnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → 𝑥 ∈ ℂ )
194 189 recnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → 𝑧 ∈ ℂ )
195 193 194 negsubd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → ( 𝑥 + - 𝑧 ) = ( 𝑥 − 𝑧 ) )
196 195 breq1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → ( ( 𝑥 + - 𝑧 ) < 𝑤 ↔ ( 𝑥 − 𝑧 ) < 𝑤 ) )
197 192 196 bitr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → ( - 𝑧 < ( 𝑤 − 𝑥 ) ↔ ( 𝑥 − 𝑧 ) < 𝑤 ) )
198 186 187 189 ltsubaddd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → ( ( 𝑤 − 𝑥 ) < 𝑧 ↔ 𝑤 < ( 𝑧 + 𝑥 ) ) )
199 197 198 anbi12d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → ( ( - 𝑧 < ( 𝑤 − 𝑥 ) ∧ ( 𝑤 − 𝑥 ) < 𝑧 ) ↔ ( ( 𝑥 − 𝑧 ) < 𝑤 ∧ 𝑤 < ( 𝑧 + 𝑥 ) ) ) )
200 190 199 bitrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 ↔ ( ( 𝑥 − 𝑧 ) < 𝑤 ∧ 𝑤 < ( 𝑧 + 𝑥 ) ) ) )
201 200 pm5.32da ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( ( 𝑤 ∈ ℝ ∧ ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 ) ↔ ( 𝑤 ∈ ℝ ∧ ( ( 𝑥 − 𝑧 ) < 𝑤 ∧ 𝑤 < ( 𝑧 + 𝑥 ) ) ) ) )
202 185 201 bitr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ↔ ( 𝑤 ∈ ℝ ∧ ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 ) ) )
203 202 biimpa ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) → ( 𝑤 ∈ ℝ ∧ ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 ) )
204 pm3.35 ⊢ ( ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) )
205 204 ancoms ⊢ ( ( ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) )
206 70 ad6antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) → 𝑦 ∈ ℝ )
207 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
208 2 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
209 208 ffvelrnda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 0 [,) +∞ ) )
210 207 209 sselid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) → ( 𝐹 ‘ 𝑤 ) ∈ ℝ )
211 210 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ℝ )
212 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
213 212 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
214 207 213 sselid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
215 75 214 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
216 215 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
217 210 216 resubcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
218 70 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑦 ∈ ℝ )
219 215 218 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ∈ ℝ )
220 219 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ∈ ℝ )
221 217 220 absltd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ↔ ( - ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) < ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ∧ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) )
222 215 recnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
223 rpcn ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ )
224 223 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑦 ∈ ℂ )
225 222 224 negsubdi2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → - ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) = ( 𝑦 − ( 𝐹 ‘ 𝑥 ) ) )
226 225 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) → - ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) = ( 𝑦 − ( 𝐹 ‘ 𝑥 ) ) )
227 226 breq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) → ( - ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) < ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑦 − ( 𝐹 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) )
228 227 anbi1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) → ( ( - ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) < ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ∧ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ↔ ( ( 𝑦 − ( 𝐹 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ∧ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) )
229 221 228 bitrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ↔ ( ( 𝑦 − ( 𝐹 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ∧ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) )
230 229 simprbda ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) → ( 𝑦 − ( 𝐹 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) )
231 215 ad4antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
232 206 211 231 ltsub1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) → ( 𝑦 < ( 𝐹 ‘ 𝑤 ) ↔ ( 𝑦 − ( 𝐹 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) )
233 230 232 mpbird ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) → 𝑦 < ( 𝐹 ‘ 𝑤 ) )
234 206 211 233 ltled ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) → 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) )
235 205 234 sylan2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ ) ∧ ( ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 ) ) → 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) )
236 235 an4s ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ ( 𝑤 ∈ ℝ ∧ ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 ) ) → 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) )
237 203 236 syldan ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) → 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) )
238 237 iftrued ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) → if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) = 𝑦 )
239 175 238 breqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) → 𝑦 ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) )
240 0le0 ⊢ 0 ≤ 0
241 breq2 ⊢ ( 𝑦 = if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) → ( 0 ≤ 𝑦 ↔ 0 ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) ) )
242 breq2 ⊢ ( 0 = if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) ) )
243 241 242 ifboth ⊢ ( ( 0 ≤ 𝑦 ∧ 0 ≤ 0 ) → 0 ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) )
244 157 240 243 sylancl ⊢ ( 𝑦 ∈ ℝ+ → 0 ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) )
245 244 ad6antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ ¬ 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) → 0 ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) )
246 172 173 239 245 ifbothda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) )
247 171 246 sylan2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ∧ 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ) ) → if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) )
248 247 anassrs ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ) → if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) ≤ if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) )
249 iftrue ⊢ ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) → if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) , 0 ) = if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) )
250 249 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ) → if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) , 0 ) = if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) )
251 iftrue ⊢ ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) → if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) , 0 ) = if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) )
252 251 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ) → if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) , 0 ) = if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) )
253 248 250 252 3brtr4d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ) → if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) , 0 ) ≤ if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) , 0 ) )
254 253 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) → if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) , 0 ) ≤ if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) , 0 ) ) )
255 240 a1i ⊢ ( ¬ 𝑤 ∈ ( 𝑋 (,) 𝑌 ) → 0 ≤ 0 )
256 iffalse ⊢ ( ¬ 𝑤 ∈ ( 𝑋 (,) 𝑌 ) → if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) , 0 ) = 0 )
257 iffalse ⊢ ( ¬ 𝑤 ∈ ( 𝑋 (,) 𝑌 ) → if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) , 0 ) = 0 )
258 255 256 257 3brtr4d ⊢ ( ¬ 𝑤 ∈ ( 𝑋 (,) 𝑌 ) → if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) , 0 ) ≤ if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) , 0 ) )
259 254 258 pm2.61d1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) , 0 ) ≤ if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) , 0 ) )
260 elin ⊢ ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) ↔ ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ∧ 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) )
261 ifbi ⊢ ( ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) ↔ ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ∧ 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) ) → if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) = if ( ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ∧ 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) )
262 260 261 ax-mp ⊢ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) = if ( ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ∧ 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 )
263 ifan ⊢ if ( ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ∧ 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) = if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) , 0 )
264 262 263 eqtri ⊢ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) = if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑤 ∈ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) , 𝑦 , 0 ) , 0 )
265 fveq2 ⊢ ( 𝑣 = 𝑤 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑤 ) )
266 265 breq2d ⊢ ( 𝑣 = 𝑤 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) ↔ 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) ) )
267 266 elrab ⊢ ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } ↔ ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) ) )
268 ifbi ⊢ ( ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } ↔ ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) ) ) → if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) = if ( ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) ) , 𝑦 , 0 ) )
269 267 268 ax-mp ⊢ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) = if ( ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) ) , 𝑦 , 0 )
270 ifan ⊢ if ( ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) ) , 𝑦 , 0 ) = if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) , 0 )
271 269 270 eqtri ⊢ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) = if ( 𝑤 ∈ ( 𝑋 (,) 𝑌 ) , if ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) , 𝑦 , 0 ) , 0 )
272 259 264 271 3brtr4g ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ≤ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) )
273 272 ralrimivw ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ∀ 𝑤 ∈ ℝ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ≤ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) )
274 reex ⊢ ℝ ∈ V
275 274 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ℝ ∈ V )
276 57 ad6antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ∈ ( 0 [,] +∞ ) )
277 64 ad6antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) ∧ 𝑤 ∈ ℝ ) → if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ∈ ( 0 [,] +∞ ) )
278 eqidd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) = ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) )
279 eqidd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) = ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) )
280 275 276 277 278 279 ofrfval2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ∘r ≤ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ↔ ∀ 𝑤 ∈ ℝ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ≤ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) )
281 273 280 mpbird ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ∘r ≤ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) )
282 itg2le ⊢ ( ( ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ∘r ≤ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) )
283 166 167 281 282 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ ( ( 𝑋 (,) 𝑌 ) ∩ ( ( 𝑥 − 𝑧 ) (,) ( 𝑧 + 𝑥 ) ) ) , 𝑦 , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) )
284 50 62 69 165 283 xrltletrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) → 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) )
285 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
286 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) → 𝑥 ∈ ( 𝑋 (,) 𝑌 ) )
287 fssres ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 𝑋 (,) 𝑌 ) ⊆ ℝ ) → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) : ( 𝑋 (,) 𝑌 ) ⟶ ( 0 [,) +∞ ) )
288 27 287 mpan2 ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) : ( 𝑋 (,) 𝑌 ) ⟶ ( 0 [,) +∞ ) )
289 fss ⊢ ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) : ( 𝑋 (,) 𝑌 ) ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) : ( 𝑋 (,) 𝑌 ) ⟶ ℝ )
290 207 289 mpan2 ⊢ ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) : ( 𝑋 (,) 𝑌 ) ⟶ ( 0 [,) +∞ ) → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) : ( 𝑋 (,) 𝑌 ) ⟶ ℝ )
291 2 288 290 3syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) : ( 𝑋 (,) 𝑌 ) ⟶ ℝ )
292 291 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) : ( 𝑋 (,) 𝑌 ) ⟶ ℝ )
293 292 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ∈ ℝ )
294 293 218 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) ∈ ℝ )
295 294 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) → ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) ∈ ℝ )
296 218 293 posdifd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑦 < ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ↔ 0 < ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) ) )
297 296 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) → 0 < ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) )
298 295 297 elrpd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) → ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) ∈ ℝ+ )
299 cncfi ⊢ ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ∧ ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑢 ) − ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) ) < ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) ) )
300 285 286 298 299 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑢 ) − ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) ) < ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) ) )
301 300 ex ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑦 < ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑢 ) − ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) ) < ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) ) ) )
302 fvres ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
303 302 breq2d ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → ( 𝑦 < ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ↔ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) )
304 303 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑦 < ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ↔ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) )
305 fvres ⊢ ( 𝑢 ∈ ( 𝑋 (,) 𝑌 ) → ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑢 ) = ( 𝐹 ‘ 𝑢 ) )
306 305 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑢 ) = ( 𝐹 ‘ 𝑢 ) )
307 302 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
308 306 307 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑢 ) − ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) )
309 308 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑢 ) − ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) )
310 302 oveq1d ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) )
311 310 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) )
312 309 311 breq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( abs ‘ ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑢 ) − ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) ) < ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) )
313 312 imbi2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑢 ) − ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) ) < ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) ) ↔ ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) )
314 313 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑢 ) − ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) ) < ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) ) ↔ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) )
315 314 rexbidv ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑢 ) − ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) ) ) < ( ( ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑥 ) − 𝑦 ) ) ↔ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) )
316 301 304 315 3imtr3d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑦 < ( 𝐹 ‘ 𝑥 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) ) )
317 316 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ( 𝑋 (,) 𝑌 ) ( ( abs ‘ ( 𝑢 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑥 ) ) ) < ( ( 𝐹 ‘ 𝑥 ) − 𝑦 ) ) )
318 284 317 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) ∧ 𝑦 < ( 𝐹 ‘ 𝑥 ) ) → 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) )
319 318 rexlimdva2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) 𝑦 < ( 𝐹 ‘ 𝑥 ) → 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ) )
320 49 319 sylbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) → 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ) )
321 320 imp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) )
322 66 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
323 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
324 fss ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
325 2 323 324 sylancl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
326 325 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
327 breq1 ⊢ ( 𝑦 = if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) → ( 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) ↔ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ≤ ( 𝐹 ‘ 𝑤 ) ) )
328 breq1 ⊢ ( 0 = if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑤 ) ↔ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ≤ ( 𝐹 ‘ 𝑤 ) ) )
329 267 simprbi ⊢ ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } → 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) )
330 329 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } ) → 𝑦 ≤ ( 𝐹 ‘ 𝑤 ) )
331 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 0 [,) +∞ ) )
332 elrege0 ⊢ ( ( 𝐹 ‘ 𝑤 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑤 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑤 ) ) )
333 331 332 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑤 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑤 ) ) )
334 333 simprd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 0 ≤ ( 𝐹 ‘ 𝑤 ) )
335 334 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ¬ 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } ) → 0 ≤ ( 𝐹 ‘ 𝑤 ) )
336 327 328 330 335 ifbothda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ≤ ( 𝐹 ‘ 𝑤 ) )
337 336 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ ℝ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ≤ ( 𝐹 ‘ 𝑤 ) )
338 337 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → ∀ 𝑤 ∈ ℝ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ≤ ( 𝐹 ‘ 𝑤 ) )
339 274 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → ℝ ∈ V )
340 64 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) ∧ 𝑤 ∈ ℝ ) → if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ∈ ( 0 [,] +∞ ) )
341 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) ∧ 𝑤 ∈ ℝ ) → ( 𝐹 ‘ 𝑤 ) ∈ V )
342 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) = ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) )
343 2 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ ℝ ↦ ( 𝐹 ‘ 𝑤 ) ) )
344 343 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → 𝐹 = ( 𝑤 ∈ ℝ ↦ ( 𝐹 ‘ 𝑤 ) ) )
345 339 340 341 342 344 ofrfval2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → ( ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑤 ∈ ℝ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ≤ ( 𝐹 ‘ 𝑤 ) ) )
346 338 345 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ∘r ≤ 𝐹 )
347 itg2le ⊢ ( ( ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
348 322 326 346 347 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
349 41 321 348 jca32 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → ( 𝑦 ∈ ℝ+ ∧ ( 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ∧ ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) ) )
350 349 expl ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ+ ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → ( 𝑦 ∈ ℝ+ ∧ ( 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ∧ ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) ) ) )
351 40 350 syl5 ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℚ ∧ ( 0 < 𝑦 ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) ) → ( 𝑦 ∈ ℝ+ ∧ ( 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ∧ ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) ) ) )
352 351 reximdv2 ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℚ ( 0 < 𝑦 ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → ∃ 𝑦 ∈ ℝ+ ( 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ∧ ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) ) )
353 68 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ∈ ℝ* )
354 itg2cl ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
355 325 354 syl ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
356 355 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
357 xrltletr ⊢ ( ( 0 ∈ ℝ* ∧ ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ∈ ℝ* ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ* ) → ( ( 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ∧ ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → 0 < ( ∫2 ‘ 𝐹 ) ) )
358 5 353 356 357 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ∧ ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → 0 < ( ∫2 ‘ 𝐹 ) ) )
359 358 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ+ ( 0 < ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ∧ ( ∫2 ‘ ( 𝑤 ∈ ℝ ↦ if ( 𝑤 ∈ { 𝑣 ∈ ( 𝑋 (,) 𝑌 ) ∣ 𝑦 ≤ ( 𝐹 ‘ 𝑣 ) } , 𝑦 , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → 0 < ( ∫2 ‘ 𝐹 ) ) )
360 352 359 syld ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℚ ( 0 < 𝑦 ∧ 𝑦 < sup ( ( 𝐹 “ ( 𝑋 (,) 𝑌 ) ) , ℝ* , < ) ) → 0 < ( ∫2 ‘ 𝐹 ) ) )
361 34 360 mpd ⊢ ( 𝜑 → 0 < ( ∫2 ‘ 𝐹 ) )