Theorem smfmullem1

Description: The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfmullem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	smfmullem1.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
	smfmullem1.v	⊢ ( 𝜑 → 𝑉 ∈ ℝ )
	smfmullem1.l	⊢ ( 𝜑 → ( 𝑈 · 𝑉 ) < 𝐴 )
	smfmullem1.x	⊢ 𝑋 = ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
	smfmullem1.y	⊢ 𝑌 = if ( 1 ≤ 𝑋 , 1 , 𝑋 )
	smfmullem1.p	⊢ ( 𝜑 → 𝑃 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) )
	smfmullem1.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) )
	smfmullem1.s	⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) )
	smfmullem1.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) )
	smfmullem1.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑃 (,) 𝑅 ) )
	smfmullem1.i	⊢ ( 𝜑 → 𝐼 ∈ ( 𝑆 (,) 𝑍 ) )
Assertion	smfmullem1	⊢ ( 𝜑 → ( 𝐻 · 𝐼 ) < 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		smfmullem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		smfmullem1.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
3		smfmullem1.v	⊢ ( 𝜑 → 𝑉 ∈ ℝ )
4		smfmullem1.l	⊢ ( 𝜑 → ( 𝑈 · 𝑉 ) < 𝐴 )
5		smfmullem1.x	⊢ 𝑋 = ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
6		smfmullem1.y	⊢ 𝑌 = if ( 1 ≤ 𝑋 , 1 , 𝑋 )
7		smfmullem1.p	⊢ ( 𝜑 → 𝑃 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) )
8		smfmullem1.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) )
9		smfmullem1.s	⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) )
10		smfmullem1.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) )
11		smfmullem1.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑃 (,) 𝑅 ) )
12		smfmullem1.i	⊢ ( 𝜑 → 𝐼 ∈ ( 𝑆 (,) 𝑍 ) )
13	11	elioored	⊢ ( 𝜑 → 𝐻 ∈ ℝ )
14	13	recnd	⊢ ( 𝜑 → 𝐻 ∈ ℂ )
15	2	recnd	⊢ ( 𝜑 → 𝑈 ∈ ℂ )
16	12	elioored	⊢ ( 𝜑 → 𝐼 ∈ ℝ )
17	16	recnd	⊢ ( 𝜑 → 𝐼 ∈ ℂ )
18	3	recnd	⊢ ( 𝜑 → 𝑉 ∈ ℂ )
19	14 15 17 18	mulsubd	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) = ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) )
20	14 15 18	subdird	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · 𝑉 ) = ( ( 𝐻 · 𝑉 ) − ( 𝑈 · 𝑉 ) ) )
21	15 17 18	subdid	⊢ ( 𝜑 → ( 𝑈 · ( 𝐼 − 𝑉 ) ) = ( ( 𝑈 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) )
22	20 21	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) = ( ( ( 𝐻 · 𝑉 ) − ( 𝑈 · 𝑉 ) ) + ( ( 𝑈 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) ) )
23	14 18	mulcld	⊢ ( 𝜑 → ( 𝐻 · 𝑉 ) ∈ ℂ )
24	15 17	mulcld	⊢ ( 𝜑 → ( 𝑈 · 𝐼 ) ∈ ℂ )
25	15 18	mulcld	⊢ ( 𝜑 → ( 𝑈 · 𝑉 ) ∈ ℂ )
26	23 24 25 25	addsub4d	⊢ ( 𝜑 → ( ( ( 𝐻 · 𝑉 ) + ( 𝑈 · 𝐼 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) = ( ( ( 𝐻 · 𝑉 ) − ( 𝑈 · 𝑉 ) ) + ( ( 𝑈 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) ) )
27	26	eqcomd	⊢ ( 𝜑 → ( ( ( 𝐻 · 𝑉 ) − ( 𝑈 · 𝑉 ) ) + ( ( 𝑈 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) ) = ( ( ( 𝐻 · 𝑉 ) + ( 𝑈 · 𝐼 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) )
28	15 17	mulcomd	⊢ ( 𝜑 → ( 𝑈 · 𝐼 ) = ( 𝐼 · 𝑈 ) )
29	28	oveq2d	⊢ ( 𝜑 → ( ( 𝐻 · 𝑉 ) + ( 𝑈 · 𝐼 ) ) = ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) )
30	29	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐻 · 𝑉 ) + ( 𝑈 · 𝐼 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) = ( ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) )
31	22 27 30	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) = ( ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) )
32	19 31	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) + ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ) = ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) ) )
33	14 17	mulcld	⊢ ( 𝜑 → ( 𝐻 · 𝐼 ) ∈ ℂ )
34	18 15	mulcld	⊢ ( 𝜑 → ( 𝑉 · 𝑈 ) ∈ ℂ )
35	33 34	addcld	⊢ ( 𝜑 → ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) ∈ ℂ )
36	17 15	mulcld	⊢ ( 𝜑 → ( 𝐼 · 𝑈 ) ∈ ℂ )
37	23 36	addcld	⊢ ( 𝜑 → ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ∈ ℂ )
38	35 37	npcand	⊢ ( 𝜑 → ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) = ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) )
39	18 15	mulcomd	⊢ ( 𝜑 → ( 𝑉 · 𝑈 ) = ( 𝑈 · 𝑉 ) )
40	39	oveq2d	⊢ ( 𝜑 → ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) = ( ( 𝐻 · 𝐼 ) + ( 𝑈 · 𝑉 ) ) )
41	38 40	eqtrd	⊢ ( 𝜑 → ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) = ( ( 𝐻 · 𝐼 ) + ( 𝑈 · 𝑉 ) ) )
42	41	eqcomd	⊢ ( 𝜑 → ( ( 𝐻 · 𝐼 ) + ( 𝑈 · 𝑉 ) ) = ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) )
43	42	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐻 · 𝐼 ) + ( 𝑈 · 𝑉 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) = ( ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) )
44	35 37	subcld	⊢ ( 𝜑 → ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) ∈ ℂ )
45	25 25	addcld	⊢ ( 𝜑 → ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ∈ ℂ )
46	44 37 45	addsubassd	⊢ ( 𝜑 → ( ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) = ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) ) )
47	43 46	eqtr2d	⊢ ( 𝜑 → ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) ) = ( ( ( 𝐻 · 𝐼 ) + ( 𝑈 · 𝑉 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) )
48	33 25 25	pnpcan2d	⊢ ( 𝜑 → ( ( ( 𝐻 · 𝐼 ) + ( 𝑈 · 𝑉 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) = ( ( 𝐻 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) )
49	32 47 48	3eqtrrd	⊢ ( 𝜑 → ( ( 𝐻 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) = ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) + ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ) )
50	13 2	jca	⊢ ( 𝜑 → ( 𝐻 ∈ ℝ ∧ 𝑈 ∈ ℝ ) )
51		resubcl	⊢ ( ( 𝐻 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 𝐻 − 𝑈 ) ∈ ℝ )
52	50 51	syl	⊢ ( 𝜑 → ( 𝐻 − 𝑈 ) ∈ ℝ )
53	16 3	jca	⊢ ( 𝜑 → ( 𝐼 ∈ ℝ ∧ 𝑉 ∈ ℝ ) )
54		resubcl	⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑉 ∈ ℝ ) → ( 𝐼 − 𝑉 ) ∈ ℝ )
55	53 54	syl	⊢ ( 𝜑 → ( 𝐼 − 𝑉 ) ∈ ℝ )
56	52 55	jca	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) ∈ ℝ ∧ ( 𝐼 − 𝑉 ) ∈ ℝ ) )
57		remulcl	⊢ ( ( ( 𝐻 − 𝑈 ) ∈ ℝ ∧ ( 𝐼 − 𝑉 ) ∈ ℝ ) → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ∈ ℝ )
58	56 57	syl	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ∈ ℝ )
59	52 3	jca	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) ∈ ℝ ∧ 𝑉 ∈ ℝ ) )
60		remulcl	⊢ ( ( ( 𝐻 − 𝑈 ) ∈ ℝ ∧ 𝑉 ∈ ℝ ) → ( ( 𝐻 − 𝑈 ) · 𝑉 ) ∈ ℝ )
61	59 60	syl	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · 𝑉 ) ∈ ℝ )
62	2 55	jca	⊢ ( 𝜑 → ( 𝑈 ∈ ℝ ∧ ( 𝐼 − 𝑉 ) ∈ ℝ ) )
63		remulcl	⊢ ( ( 𝑈 ∈ ℝ ∧ ( 𝐼 − 𝑉 ) ∈ ℝ ) → ( 𝑈 · ( 𝐼 − 𝑉 ) ) ∈ ℝ )
64	62 63	syl	⊢ ( 𝜑 → ( 𝑈 · ( 𝐼 − 𝑉 ) ) ∈ ℝ )
65	61 64	jca	⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) ∈ ℝ ∧ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ∈ ℝ ) )
66		readdcl	⊢ ( ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) ∈ ℝ ∧ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ∈ ℝ ) → ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ∈ ℝ )
67	65 66	syl	⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ∈ ℝ )
68	58 67	jca	⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ∈ ℝ ∧ ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ∈ ℝ ) )
69		readdcl	⊢ ( ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ∈ ℝ ∧ ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ∈ ℝ ) → ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) + ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ) ∈ ℝ )
70	68 69	syl	⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) + ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ) ∈ ℝ )
71	6	a1i	⊢ ( 𝜑 → 𝑌 = if ( 1 ≤ 𝑋 , 1 , 𝑋 ) )
72		1rp	⊢ 1 ∈ ℝ+
73	72	a1i	⊢ ( 𝜑 → 1 ∈ ℝ+ )
74	5	a1i	⊢ ( 𝜑 → 𝑋 = ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) )
75	2 3	remulcld	⊢ ( 𝜑 → ( 𝑈 · 𝑉 ) ∈ ℝ )
76		difrp	⊢ ( ( ( 𝑈 · 𝑉 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑈 · 𝑉 ) < 𝐴 ↔ ( 𝐴 − ( 𝑈 · 𝑉 ) ) ∈ ℝ+ ) )
77	75 1 76	syl2anc	⊢ ( 𝜑 → ( ( 𝑈 · 𝑉 ) < 𝐴 ↔ ( 𝐴 − ( 𝑈 · 𝑉 ) ) ∈ ℝ+ ) )
78	4 77	mpbid	⊢ ( 𝜑 → ( 𝐴 − ( 𝑈 · 𝑉 ) ) ∈ ℝ+ )
79		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
80	15	abscld	⊢ ( 𝜑 → ( abs ‘ 𝑈 ) ∈ ℝ )
81	18	abscld	⊢ ( 𝜑 → ( abs ‘ 𝑉 ) ∈ ℝ )
82	80 81	readdcld	⊢ ( 𝜑 → ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ∈ ℝ )
83	79 82	readdcld	⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ∈ ℝ )
84		0re	⊢ 0 ∈ ℝ
85	84	a1i	⊢ ( 𝜑 → 0 ∈ ℝ )
86	73	rpgt0d	⊢ ( 𝜑 → 0 < 1 )
87	15	absge0d	⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝑈 ) )
88	18	absge0d	⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝑉 ) )
89	80 81	addge01d	⊢ ( 𝜑 → ( 0 ≤ ( abs ‘ 𝑉 ) ↔ ( abs ‘ 𝑈 ) ≤ ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
90	88 89	mpbid	⊢ ( 𝜑 → ( abs ‘ 𝑈 ) ≤ ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) )
91	85 80 82 87 90	letrd	⊢ ( 𝜑 → 0 ≤ ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) )
92	79 82	addge01d	⊢ ( 𝜑 → ( 0 ≤ ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ↔ 1 ≤ ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) )
93	91 92	mpbid	⊢ ( 𝜑 → 1 ≤ ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
94	85 79 83 86 93	ltletrd	⊢ ( 𝜑 → 0 < ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
95	83 94	elrpd	⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ∈ ℝ+ )
96	78 95	rpdivcld	⊢ ( 𝜑 → ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) ∈ ℝ+ )
97	74 96	eqeltrd	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
98	73 97	ifcld	⊢ ( 𝜑 → if ( 1 ≤ 𝑋 , 1 , 𝑋 ) ∈ ℝ+ )
99	71 98	eqeltrd	⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
100	99	rpred	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
101		resqcl	⊢ ( 𝑌 ∈ ℝ → ( 𝑌 ↑ 2 ) ∈ ℝ )
102	100 101	syl	⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ∈ ℝ )
103	100 81	remulcld	⊢ ( 𝜑 → ( 𝑌 · ( abs ‘ 𝑉 ) ) ∈ ℝ )
104	100 80	remulcld	⊢ ( 𝜑 → ( 𝑌 · ( abs ‘ 𝑈 ) ) ∈ ℝ )
105	103 104	jca	⊢ ( 𝜑 → ( ( 𝑌 · ( abs ‘ 𝑉 ) ) ∈ ℝ ∧ ( 𝑌 · ( abs ‘ 𝑈 ) ) ∈ ℝ ) )
106		readdcl	⊢ ( ( ( 𝑌 · ( abs ‘ 𝑉 ) ) ∈ ℝ ∧ ( 𝑌 · ( abs ‘ 𝑈 ) ) ∈ ℝ ) → ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ∈ ℝ )
107	105 106	syl	⊢ ( 𝜑 → ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ∈ ℝ )
108	102 107	jca	⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) ∈ ℝ ∧ ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ∈ ℝ ) )
109		readdcl	⊢ ( ( ( 𝑌 ↑ 2 ) ∈ ℝ ∧ ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ∈ ℝ ) → ( ( 𝑌 ↑ 2 ) + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) ∈ ℝ )
110	108 109	syl	⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) ∈ ℝ )
111	1 75	resubcld	⊢ ( 𝜑 → ( 𝐴 − ( 𝑈 · 𝑉 ) ) ∈ ℝ )
112	100	resqcld	⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ∈ ℝ )
113	103 104	readdcld	⊢ ( 𝜑 → ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ∈ ℝ )
114	19 44	eqeltrd	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ∈ ℂ )
115	114	abscld	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ) ∈ ℝ )
116	100 100	remulcld	⊢ ( 𝜑 → ( 𝑌 · 𝑌 ) ∈ ℝ )
117	58	leabsd	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ≤ ( abs ‘ ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ) )
118	52	recnd	⊢ ( 𝜑 → ( 𝐻 − 𝑈 ) ∈ ℂ )
119	55	recnd	⊢ ( 𝜑 → ( 𝐼 − 𝑉 ) ∈ ℂ )
120	118 119	absmuld	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ) = ( ( abs ‘ ( 𝐻 − 𝑈 ) ) · ( abs ‘ ( 𝐼 − 𝑉 ) ) ) )
121	118	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝐻 − 𝑈 ) ) ∈ ℝ )
122	119	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝐼 − 𝑉 ) ) ∈ ℝ )
123	118	absge0d	⊢ ( 𝜑 → 0 ≤ ( abs ‘ ( 𝐻 − 𝑈 ) ) )
124	2 100	resubcld	⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) ∈ ℝ )
125	7	elioored	⊢ ( 𝜑 → 𝑃 ∈ ℝ )
126	124	rexrd	⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) ∈ ℝ* )
127	2	rexrd	⊢ ( 𝜑 → 𝑈 ∈ ℝ* )
128		ioogtlb	⊢ ( ( ( 𝑈 − 𝑌 ) ∈ ℝ* ∧ 𝑈 ∈ ℝ* ∧ 𝑃 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) → ( 𝑈 − 𝑌 ) < 𝑃 )
129	126 127 7 128	syl3anc	⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) < 𝑃 )
130	125	rexrd	⊢ ( 𝜑 → 𝑃 ∈ ℝ* )
131	8	elioored	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
132	131	rexrd	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
133		ioogtlb	⊢ ( ( 𝑃 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ∧ 𝐻 ∈ ( 𝑃 (,) 𝑅 ) ) → 𝑃 < 𝐻 )
134	130 132 11 133	syl3anc	⊢ ( 𝜑 → 𝑃 < 𝐻 )
135	124 125 13 129 134	lttrd	⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) < 𝐻 )
136	2 100	readdcld	⊢ ( 𝜑 → ( 𝑈 + 𝑌 ) ∈ ℝ )
137		iooltub	⊢ ( ( 𝑃 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ∧ 𝐻 ∈ ( 𝑃 (,) 𝑅 ) ) → 𝐻 < 𝑅 )
138	130 132 11 137	syl3anc	⊢ ( 𝜑 → 𝐻 < 𝑅 )
139	136	rexrd	⊢ ( 𝜑 → ( 𝑈 + 𝑌 ) ∈ ℝ* )
140		iooltub	⊢ ( ( 𝑈 ∈ ℝ* ∧ ( 𝑈 + 𝑌 ) ∈ ℝ* ∧ 𝑅 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) → 𝑅 < ( 𝑈 + 𝑌 ) )
141	127 139 8 140	syl3anc	⊢ ( 𝜑 → 𝑅 < ( 𝑈 + 𝑌 ) )
142	13 131 136 138 141	lttrd	⊢ ( 𝜑 → 𝐻 < ( 𝑈 + 𝑌 ) )
143	135 142	jca	⊢ ( 𝜑 → ( ( 𝑈 − 𝑌 ) < 𝐻 ∧ 𝐻 < ( 𝑈 + 𝑌 ) ) )
144	13 2 100	absdifltd	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐻 − 𝑈 ) ) < 𝑌 ↔ ( ( 𝑈 − 𝑌 ) < 𝐻 ∧ 𝐻 < ( 𝑈 + 𝑌 ) ) ) )
145	143 144	mpbird	⊢ ( 𝜑 → ( abs ‘ ( 𝐻 − 𝑈 ) ) < 𝑌 )
146	119	absge0d	⊢ ( 𝜑 → 0 ≤ ( abs ‘ ( 𝐼 − 𝑉 ) ) )
147	3 100	resubcld	⊢ ( 𝜑 → ( 𝑉 − 𝑌 ) ∈ ℝ )
148	9	elioored	⊢ ( 𝜑 → 𝑆 ∈ ℝ )
149	147	rexrd	⊢ ( 𝜑 → ( 𝑉 − 𝑌 ) ∈ ℝ* )
150	3	rexrd	⊢ ( 𝜑 → 𝑉 ∈ ℝ* )
151	149 150 9	ioogtlbd	⊢ ( 𝜑 → ( 𝑉 − 𝑌 ) < 𝑆 )
152	148	rexrd	⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
153	10	elioored	⊢ ( 𝜑 → 𝑍 ∈ ℝ )
154	153	rexrd	⊢ ( 𝜑 → 𝑍 ∈ ℝ* )
155	152 154 12	ioogtlbd	⊢ ( 𝜑 → 𝑆 < 𝐼 )
156	147 148 16 151 155	lttrd	⊢ ( 𝜑 → ( 𝑉 − 𝑌 ) < 𝐼 )
157	3 100	readdcld	⊢ ( 𝜑 → ( 𝑉 + 𝑌 ) ∈ ℝ )
158	152 154 12	iooltubd	⊢ ( 𝜑 → 𝐼 < 𝑍 )
159	157	rexrd	⊢ ( 𝜑 → ( 𝑉 + 𝑌 ) ∈ ℝ* )
160	150 159 10	iooltubd	⊢ ( 𝜑 → 𝑍 < ( 𝑉 + 𝑌 ) )
161	16 153 157 158 160	lttrd	⊢ ( 𝜑 → 𝐼 < ( 𝑉 + 𝑌 ) )
162	156 161	jca	⊢ ( 𝜑 → ( ( 𝑉 − 𝑌 ) < 𝐼 ∧ 𝐼 < ( 𝑉 + 𝑌 ) ) )
163	16 3 100	absdifltd	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐼 − 𝑉 ) ) < 𝑌 ↔ ( ( 𝑉 − 𝑌 ) < 𝐼 ∧ 𝐼 < ( 𝑉 + 𝑌 ) ) ) )
164	162 163	mpbird	⊢ ( 𝜑 → ( abs ‘ ( 𝐼 − 𝑉 ) ) < 𝑌 )
165	121 100 122 100 123 145 146 164	ltmul12ad	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐻 − 𝑈 ) ) · ( abs ‘ ( 𝐼 − 𝑉 ) ) ) < ( 𝑌 · 𝑌 ) )
166	120 165	eqbrtrd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ) < ( 𝑌 · 𝑌 ) )
167	58 115 116 117 166	lelttrd	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) < ( 𝑌 · 𝑌 ) )
168	100	recnd	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
169	168	sqvald	⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) = ( 𝑌 · 𝑌 ) )
170	169	eqcomd	⊢ ( 𝜑 → ( 𝑌 · 𝑌 ) = ( 𝑌 ↑ 2 ) )
171	167 170	breqtrd	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) < ( 𝑌 ↑ 2 ) )
172	61	recnd	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · 𝑉 ) ∈ ℂ )
173	172	abscld	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐻 − 𝑈 ) · 𝑉 ) ) ∈ ℝ )
174	61	leabsd	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · 𝑉 ) ≤ ( abs ‘ ( ( 𝐻 − 𝑈 ) · 𝑉 ) ) )
175	118 18	absmuld	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐻 − 𝑈 ) · 𝑉 ) ) = ( ( abs ‘ ( 𝐻 − 𝑈 ) ) · ( abs ‘ 𝑉 ) ) )
176	121 100 145	ltled	⊢ ( 𝜑 → ( abs ‘ ( 𝐻 − 𝑈 ) ) ≤ 𝑌 )
177	121 100 81 88 176	lemul1ad	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐻 − 𝑈 ) ) · ( abs ‘ 𝑉 ) ) ≤ ( 𝑌 · ( abs ‘ 𝑉 ) ) )
178	175 177	eqbrtrd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐻 − 𝑈 ) · 𝑉 ) ) ≤ ( 𝑌 · ( abs ‘ 𝑉 ) ) )
179	61 173 103 174 178	letrd	⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · 𝑉 ) ≤ ( 𝑌 · ( abs ‘ 𝑉 ) ) )
180	64	recnd	⊢ ( 𝜑 → ( 𝑈 · ( 𝐼 − 𝑉 ) ) ∈ ℂ )
181	180	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ∈ ℝ )
182	64	leabsd	⊢ ( 𝜑 → ( 𝑈 · ( 𝐼 − 𝑉 ) ) ≤ ( abs ‘ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) )
183	15 119	absmuld	⊢ ( 𝜑 → ( abs ‘ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) = ( ( abs ‘ 𝑈 ) · ( abs ‘ ( 𝐼 − 𝑉 ) ) ) )
184	80	recnd	⊢ ( 𝜑 → ( abs ‘ 𝑈 ) ∈ ℂ )
185	122	recnd	⊢ ( 𝜑 → ( abs ‘ ( 𝐼 − 𝑉 ) ) ∈ ℂ )
186	184 185	mulcomd	⊢ ( 𝜑 → ( ( abs ‘ 𝑈 ) · ( abs ‘ ( 𝐼 − 𝑉 ) ) ) = ( ( abs ‘ ( 𝐼 − 𝑉 ) ) · ( abs ‘ 𝑈 ) ) )
187	183 186	eqtrd	⊢ ( 𝜑 → ( abs ‘ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) = ( ( abs ‘ ( 𝐼 − 𝑉 ) ) · ( abs ‘ 𝑈 ) ) )
188	122 100 164	ltled	⊢ ( 𝜑 → ( abs ‘ ( 𝐼 − 𝑉 ) ) ≤ 𝑌 )
189	122 100 80 87 188	lemul1ad	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐼 − 𝑉 ) ) · ( abs ‘ 𝑈 ) ) ≤ ( 𝑌 · ( abs ‘ 𝑈 ) ) )
190	187 189	eqbrtrd	⊢ ( 𝜑 → ( abs ‘ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ≤ ( 𝑌 · ( abs ‘ 𝑈 ) ) )
191	64 181 104 182 190	letrd	⊢ ( 𝜑 → ( 𝑈 · ( 𝐼 − 𝑉 ) ) ≤ ( 𝑌 · ( abs ‘ 𝑈 ) ) )
192	61 64 103 104 179 191	leadd12dd	⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ≤ ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) )
193	58 67 112 113 171 192	ltleaddd	⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) + ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ) < ( ( 𝑌 ↑ 2 ) + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) )
194	100 107	readdcld	⊢ ( 𝜑 → ( 𝑌 + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) ∈ ℝ )
195	85 121 100 123 176	letrd	⊢ ( 𝜑 → 0 ≤ 𝑌 )
196	97	rpred	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
197		min1	⊢ ( ( 1 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → if ( 1 ≤ 𝑋 , 1 , 𝑋 ) ≤ 1 )
198	79 196 197	syl2anc	⊢ ( 𝜑 → if ( 1 ≤ 𝑋 , 1 , 𝑋 ) ≤ 1 )
199	6 198	eqbrtrid	⊢ ( 𝜑 → 𝑌 ≤ 1 )
200	85 79 100 195 199	eliccd	⊢ ( 𝜑 → 𝑌 ∈ ( 0 [,] 1 ) )
201	100	sqrlearg	⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) ≤ 𝑌 ↔ 𝑌 ∈ ( 0 [,] 1 ) ) )
202	200 201	mpbird	⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ≤ 𝑌 )
203	102 100 107 202	leadd1dd	⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) ≤ ( 𝑌 + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) )
204		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
205	81	recnd	⊢ ( 𝜑 → ( abs ‘ 𝑉 ) ∈ ℂ )
206	205 184	addcld	⊢ ( 𝜑 → ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ∈ ℂ )
207	168 204 206	adddid	⊢ ( 𝜑 → ( 𝑌 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) = ( ( 𝑌 · 1 ) + ( 𝑌 · ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
208	168	mulridd	⊢ ( 𝜑 → ( 𝑌 · 1 ) = 𝑌 )
209	168 205 184	adddid	⊢ ( 𝜑 → ( 𝑌 · ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) = ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) )
210	208 209	oveq12d	⊢ ( 𝜑 → ( ( 𝑌 · 1 ) + ( 𝑌 · ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) = ( 𝑌 + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) )
211	207 210	eqtr2d	⊢ ( 𝜑 → ( 𝑌 + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) = ( 𝑌 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
212	81 80	readdcld	⊢ ( 𝜑 → ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ∈ ℝ )
213	79 212	readdcld	⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ∈ ℝ )
214	81 80	addge01d	⊢ ( 𝜑 → ( 0 ≤ ( abs ‘ 𝑈 ) ↔ ( abs ‘ 𝑉 ) ≤ ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) )
215	87 214	mpbid	⊢ ( 𝜑 → ( abs ‘ 𝑉 ) ≤ ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) )
216	85 81 212 88 215	letrd	⊢ ( 𝜑 → 0 ≤ ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) )
217	79 212	addge01d	⊢ ( 𝜑 → ( 0 ≤ ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ↔ 1 ≤ ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
218	216 217	mpbid	⊢ ( 𝜑 → 1 ≤ ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) )
219	85 79 213 86 218	ltletrd	⊢ ( 𝜑 → 0 < ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) )
220	85 213 219	ltled	⊢ ( 𝜑 → 0 ≤ ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) )
221		min2	⊢ ( ( 1 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → if ( 1 ≤ 𝑋 , 1 , 𝑋 ) ≤ 𝑋 )
222	79 196 221	syl2anc	⊢ ( 𝜑 → if ( 1 ≤ 𝑋 , 1 , 𝑋 ) ≤ 𝑋 )
223	71 222	eqbrtrd	⊢ ( 𝜑 → 𝑌 ≤ 𝑋 )
224	100 196 213 220 223	lemul1ad	⊢ ( 𝜑 → ( 𝑌 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) ≤ ( 𝑋 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
225	74	oveq1d	⊢ ( 𝜑 → ( 𝑋 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) = ( ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
226	184 205	addcomd	⊢ ( 𝜑 → ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) = ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) )
227	226	oveq2d	⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) = ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) )
228	227	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) = ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
229	228	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) = ( ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
230	111	recnd	⊢ ( 𝜑 → ( 𝐴 − ( 𝑈 · 𝑉 ) ) ∈ ℂ )
231	204 206	addcld	⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ∈ ℂ )
232	85 219	gtned	⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ≠ 0 )
233	230 231 232	divcan1d	⊢ ( 𝜑 → ( ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) = ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
234	225 229 233	3eqtrd	⊢ ( 𝜑 → ( 𝑋 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) = ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
235	224 234	breqtrd	⊢ ( 𝜑 → ( 𝑌 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) ≤ ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
236	211 235	eqbrtrd	⊢ ( 𝜑 → ( 𝑌 + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) ≤ ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
237	110 194 111 203 236	letrd	⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) ≤ ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
238	70 110 111 193 237	ltletrd	⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) + ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ) < ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
239	49 238	eqbrtrd	⊢ ( 𝜑 → ( ( 𝐻 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) < ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
240	13 16	remulcld	⊢ ( 𝜑 → ( 𝐻 · 𝐼 ) ∈ ℝ )
241	240 1 75	ltsub1d	⊢ ( 𝜑 → ( ( 𝐻 · 𝐼 ) < 𝐴 ↔ ( ( 𝐻 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) < ( 𝐴 − ( 𝑈 · 𝑉 ) ) ) )
242	239 241	mpbird	⊢ ( 𝜑 → ( 𝐻 · 𝐼 ) < 𝐴 )