Theorem smfmullem1 40998

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.)

Hypotheses

Ref	Expression
smfmullem1.a	|- ( ph -> A e. RR )
smfmullem1.u	|- ( ph -> U e. RR )
smfmullem1.v	|- ( ph -> V e. RR )
smfmullem1.l	|- ( ph -> ( U x. V ) < A )
smfmullem1.x	|- X = ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
smfmullem1.y	|- Y = if ( 1 <_ X , 1 , X )
smfmullem1.p	|- ( ph -> P e. ( ( U - Y ) (,) U ) )
smfmullem1.r	|- ( ph -> R e. ( U (,) ( U + Y ) ) )
smfmullem1.s	|- ( ph -> S e. ( ( V - Y ) (,) V ) )
smfmullem1.z	|- ( ph -> Z e. ( V (,) ( V + Y ) ) )
smfmullem1.h	|- ( ph -> H e. ( P (,) R ) )
smfmullem1.i	|- ( ph -> I e. ( S (,) Z ) )

Assertion

Ref	Expression
smfmullem1	|- ( ph -> ( H x. I ) < A )

Proof of Theorem smfmullem1

Step	Hyp	Ref	Expression
1		smfmullem1.h	. . . . . . . 8 |- ( ph -> H e. ( P (,) R ) )
2	1	elioored 39776	. . . . . . 7 |- ( ph -> H e. RR )
3	2	recnd 10068	. . . . . 6 |- ( ph -> H e. CC )
4		smfmullem1.u	. . . . . . 7 |- ( ph -> U e. RR )
5	4	recnd 10068	. . . . . 6 |- ( ph -> U e. CC )
6		smfmullem1.i	. . . . . . . 8 |- ( ph -> I e. ( S (,) Z ) )
7	6	elioored 39776	. . . . . . 7 |- ( ph -> I e. RR )
8	7	recnd 10068	. . . . . 6 |- ( ph -> I e. CC )
9		smfmullem1.v	. . . . . . 7 |- ( ph -> V e. RR )
10	9	recnd 10068	. . . . . 6 |- ( ph -> V e. CC )
11	3, 5, 8, 10	mulsubd 10490	. . . . 5 |- ( ph -> ( ( H - U ) x. ( I - V ) ) = ( ( ( H x. I ) + ( V x. U ) ) - ( ( H x. V ) + ( I x. U ) ) ) )
12	3, 5, 10	subdird 10487	. . . . . . 7 |- ( ph -> ( ( H - U ) x. V ) = ( ( H x. V ) - ( U x. V ) ) )
13	5, 8, 10	subdid 10486	. . . . . . 7 |- ( ph -> ( U x. ( I - V ) ) = ( ( U x. I ) - ( U x. V ) ) )
14	12, 13	oveq12d 6668	. . . . . 6 |- ( ph -> ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) = ( ( ( H x. V ) - ( U x. V ) ) + ( ( U x. I ) - ( U x. V ) ) ) )
15	3, 10	mulcld 10060	. . . . . . . 8 |- ( ph -> ( H x. V ) e. CC )
16	5, 8	mulcld 10060	. . . . . . . 8 |- ( ph -> ( U x. I ) e. CC )
17	5, 10	mulcld 10060	. . . . . . . 8 |- ( ph -> ( U x. V ) e. CC )
18	15, 16, 17, 17	addsub4d 10439	. . . . . . 7 |- ( ph -> ( ( ( H x. V ) + ( U x. I ) ) - ( ( U x. V ) + ( U x. V ) ) ) = ( ( ( H x. V ) - ( U x. V ) ) + ( ( U x. I ) - ( U x. V ) ) ) )
19	18	eqcomd 2628	. . . . . 6 |- ( ph -> ( ( ( H x. V ) - ( U x. V ) ) + ( ( U x. I ) - ( U x. V ) ) ) = ( ( ( H x. V ) + ( U x. I ) ) - ( ( U x. V ) + ( U x. V ) ) ) )
20	5, 8	mulcomd 10061	. . . . . . . 8 |- ( ph -> ( U x. I ) = ( I x. U ) )
21	20	oveq2d 6666	. . . . . . 7 |- ( ph -> ( ( H x. V ) + ( U x. I ) ) = ( ( H x. V ) + ( I x. U ) ) )
22	21	oveq1d 6665	. . . . . 6 |- ( ph -> ( ( ( H x. V ) + ( U x. I ) ) - ( ( U x. V ) + ( U x. V ) ) ) = ( ( ( H x. V ) + ( I x. U ) ) - ( ( U x. V ) + ( U x. V ) ) ) )
23	14, 19, 22	3eqtrd 2660	. . . . 5 |- ( ph -> ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) = ( ( ( H x. V ) + ( I x. U ) ) - ( ( U x. V ) + ( U x. V ) ) ) )
24	11, 23	oveq12d 6668	. . . 4 |- ( ph -> ( ( ( H - U ) x. ( I - V ) ) + ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) ) = ( ( ( ( H x. I ) + ( V x. U ) ) - ( ( H x. V ) + ( I x. U ) ) ) + ( ( ( H x. V ) + ( I x. U ) ) - ( ( U x. V ) + ( U x. V ) ) ) ) )
25	3, 8	mulcld 10060	. . . . . . . . . 10 |- ( ph -> ( H x. I ) e. CC )
26	10, 5	mulcld 10060	. . . . . . . . . 10 |- ( ph -> ( V x. U ) e. CC )
27	25, 26	addcld 10059	. . . . . . . . 9 |- ( ph -> ( ( H x. I ) + ( V x. U ) ) e. CC )
28	8, 5	mulcld 10060	. . . . . . . . . 10 |- ( ph -> ( I x. U ) e. CC )
29	15, 28	addcld 10059	. . . . . . . . 9 |- ( ph -> ( ( H x. V ) + ( I x. U ) ) e. CC )
30	27, 29	npcand 10396	. . . . . . . 8 |- ( ph -> ( ( ( ( H x. I ) + ( V x. U ) ) - ( ( H x. V ) + ( I x. U ) ) ) + ( ( H x. V ) + ( I x. U ) ) ) = ( ( H x. I ) + ( V x. U ) ) )
31	10, 5	mulcomd 10061	. . . . . . . . 9 |- ( ph -> ( V x. U ) = ( U x. V ) )
32	31	oveq2d 6666	. . . . . . . 8 |- ( ph -> ( ( H x. I ) + ( V x. U ) ) = ( ( H x. I ) + ( U x. V ) ) )
33	30, 32	eqtrd 2656	. . . . . . 7 |- ( ph -> ( ( ( ( H x. I ) + ( V x. U ) ) - ( ( H x. V ) + ( I x. U ) ) ) + ( ( H x. V ) + ( I x. U ) ) ) = ( ( H x. I ) + ( U x. V ) ) )
34	33	eqcomd 2628	. . . . . 6 |- ( ph -> ( ( H x. I ) + ( U x. V ) ) = ( ( ( ( H x. I ) + ( V x. U ) ) - ( ( H x. V ) + ( I x. U ) ) ) + ( ( H x. V ) + ( I x. U ) ) ) )
35	34	oveq1d 6665	. . . . 5 |- ( ph -> ( ( ( H x. I ) + ( U x. V ) ) - ( ( U x. V ) + ( U x. V ) ) ) = ( ( ( ( ( H x. I ) + ( V x. U ) ) - ( ( H x. V ) + ( I x. U ) ) ) + ( ( H x. V ) + ( I x. U ) ) ) - ( ( U x. V ) + ( U x. V ) ) ) )
36	27, 29	subcld 10392	. . . . . 6 |- ( ph -> ( ( ( H x. I ) + ( V x. U ) ) - ( ( H x. V ) + ( I x. U ) ) ) e. CC )
37	17, 17	addcld 10059	. . . . . 6 |- ( ph -> ( ( U x. V ) + ( U x. V ) ) e. CC )
38	36, 29, 37	addsubassd 10412	. . . . 5 |- ( ph -> ( ( ( ( ( H x. I ) + ( V x. U ) ) - ( ( H x. V ) + ( I x. U ) ) ) + ( ( H x. V ) + ( I x. U ) ) ) - ( ( U x. V ) + ( U x. V ) ) ) = ( ( ( ( H x. I ) + ( V x. U ) ) - ( ( H x. V ) + ( I x. U ) ) ) + ( ( ( H x. V ) + ( I x. U ) ) - ( ( U x. V ) + ( U x. V ) ) ) ) )
39	35, 38	eqtr2d 2657	. . . 4 |- ( ph -> ( ( ( ( H x. I ) + ( V x. U ) ) - ( ( H x. V ) + ( I x. U ) ) ) + ( ( ( H x. V ) + ( I x. U ) ) - ( ( U x. V ) + ( U x. V ) ) ) ) = ( ( ( H x. I ) + ( U x. V ) ) - ( ( U x. V ) + ( U x. V ) ) ) )
40	25, 17, 17	pnpcan2d 10430	. . . 4 |- ( ph -> ( ( ( H x. I ) + ( U x. V ) ) - ( ( U x. V ) + ( U x. V ) ) ) = ( ( H x. I ) - ( U x. V ) ) )
41	24, 39, 40	3eqtrrd 2661	. . 3 |- ( ph -> ( ( H x. I ) - ( U x. V ) ) = ( ( ( H - U ) x. ( I - V ) ) + ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) ) )
42	2, 4	jca 554	. . . . . . . . 9 |- ( ph -> ( H e. RR /\ U e. RR ) )
43		resubcl 10345	. . . . . . . . 9 |- ( ( H e. RR /\ U e. RR ) -> ( H - U ) e. RR )
44	42, 43	syl 17	. . . . . . . 8 |- ( ph -> ( H - U ) e. RR )
45	7, 9	jca 554	. . . . . . . . 9 |- ( ph -> ( I e. RR /\ V e. RR ) )
46		resubcl 10345	. . . . . . . . 9 |- ( ( I e. RR /\ V e. RR ) -> ( I - V ) e. RR )
47	45, 46	syl 17	. . . . . . . 8 |- ( ph -> ( I - V ) e. RR )
48	44, 47	jca 554	. . . . . . 7 |- ( ph -> ( ( H - U ) e. RR /\ ( I - V ) e. RR ) )
49		remulcl 10021	. . . . . . 7 |- ( ( ( H - U ) e. RR /\ ( I - V ) e. RR ) -> ( ( H - U ) x. ( I - V ) ) e. RR )
50	48, 49	syl 17	. . . . . 6 |- ( ph -> ( ( H - U ) x. ( I - V ) ) e. RR )
51	44, 9	jca 554	. . . . . . . . 9 |- ( ph -> ( ( H - U ) e. RR /\ V e. RR ) )
52		remulcl 10021	. . . . . . . . 9 |- ( ( ( H - U ) e. RR /\ V e. RR ) -> ( ( H - U ) x. V ) e. RR )
53	51, 52	syl 17	. . . . . . . 8 |- ( ph -> ( ( H - U ) x. V ) e. RR )
54	4, 47	jca 554	. . . . . . . . 9 |- ( ph -> ( U e. RR /\ ( I - V ) e. RR ) )
55		remulcl 10021	. . . . . . . . 9 |- ( ( U e. RR /\ ( I - V ) e. RR ) -> ( U x. ( I - V ) ) e. RR )
56	54, 55	syl 17	. . . . . . . 8 |- ( ph -> ( U x. ( I - V ) ) e. RR )
57	53, 56	jca 554	. . . . . . 7 |- ( ph -> ( ( ( H - U ) x. V ) e. RR /\ ( U x. ( I - V ) ) e. RR ) )
58		readdcl 10019	. . . . . . 7 |- ( ( ( ( H - U ) x. V ) e. RR /\ ( U x. ( I - V ) ) e. RR ) -> ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) e. RR )
59	57, 58	syl 17	. . . . . 6 |- ( ph -> ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) e. RR )
60	50, 59	jca 554	. . . . 5 |- ( ph -> ( ( ( H - U ) x. ( I - V ) ) e. RR /\ ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) e. RR ) )
61		readdcl 10019	. . . . 5 |- ( ( ( ( H - U ) x. ( I - V ) ) e. RR /\ ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) e. RR ) -> ( ( ( H - U ) x. ( I - V ) ) + ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) ) e. RR )
62	60, 61	syl 17	. . . 4 |- ( ph -> ( ( ( H - U ) x. ( I - V ) ) + ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) ) e. RR )
63		smfmullem1.y	. . . . . . . . . 10 |- Y = if ( 1 <_ X , 1 , X )
64	63	a1i 11	. . . . . . . . 9 |- ( ph -> Y = if ( 1 <_ X , 1 , X ) )
65		1rp 11836	. . . . . . . . . . 11 |- 1 e. RR+
66	65	a1i 11	. . . . . . . . . 10 |- ( ph -> 1 e. RR+ )
67		smfmullem1.x	. . . . . . . . . . . 12 |- X = ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
68	67	a1i 11	. . . . . . . . . . 11 |- ( ph -> X = ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) ) )
69		smfmullem1.l	. . . . . . . . . . . . 13 |- ( ph -> ( U x. V ) < A )
70	4, 9	remulcld 10070	. . . . . . . . . . . . . 14 |- ( ph -> ( U x. V ) e. RR )
71		smfmullem1.a	. . . . . . . . . . . . . 14 |- ( ph -> A e. RR )
72		difrp 11868	. . . . . . . . . . . . . 14 |- ( ( ( U x. V ) e. RR /\ A e. RR ) -> ( ( U x. V ) < A <-> ( A - ( U x. V ) ) e. RR+ ) )
73	70, 71, 72	syl2anc 693	. . . . . . . . . . . . 13 |- ( ph -> ( ( U x. V ) < A <-> ( A - ( U x. V ) ) e. RR+ ) )
74	69, 73	mpbid 222	. . . . . . . . . . . 12 |- ( ph -> ( A - ( U x. V ) ) e. RR+ )
75		1red 10055	. . . . . . . . . . . . . 14 |- ( ph -> 1 e. RR )
76	5	abscld 14175	. . . . . . . . . . . . . . 15 |- ( ph -> ( abs ` U ) e. RR )
77	10	abscld 14175	. . . . . . . . . . . . . . 15 |- ( ph -> ( abs ` V ) e. RR )
78	76, 77	readdcld 10069	. . . . . . . . . . . . . 14 |- ( ph -> ( ( abs ` U ) + ( abs ` V ) ) e. RR )
79	75, 78	readdcld 10069	. . . . . . . . . . . . 13 |- ( ph -> ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) e. RR )
80		0re 10040	. . . . . . . . . . . . . . 15 |- 0 e. RR
81	80	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> 0 e. RR )
82	66	rpgt0d 11875	. . . . . . . . . . . . . 14 |- ( ph -> 0 < 1 )
83	5	absge0d 14183	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 <_ ( abs ` U ) )
84	10	absge0d 14183	. . . . . . . . . . . . . . . . 17 |- ( ph -> 0 <_ ( abs ` V ) )
85	76, 77	addge01d 10615	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( 0 <_ ( abs ` V ) <-> ( abs ` U ) <_ ( ( abs ` U ) + ( abs ` V ) ) ) )
86	84, 85	mpbid 222	. . . . . . . . . . . . . . . 16 |- ( ph -> ( abs ` U ) <_ ( ( abs ` U ) + ( abs ` V ) ) )
87	81, 76, 78, 83, 86	letrd 10194	. . . . . . . . . . . . . . 15 |- ( ph -> 0 <_ ( ( abs ` U ) + ( abs ` V ) ) )
88	75, 78	addge01d 10615	. . . . . . . . . . . . . . 15 |- ( ph -> ( 0 <_ ( ( abs ` U ) + ( abs ` V ) ) <-> 1 <_ ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) ) )
89	87, 88	mpbid 222	. . . . . . . . . . . . . 14 |- ( ph -> 1 <_ ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
90	81, 75, 79, 82, 89	ltletrd 10197	. . . . . . . . . . . . 13 |- ( ph -> 0 < ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
91	79, 90	elrpd 11869	. . . . . . . . . . . 12 |- ( ph -> ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) e. RR+ )
92	74, 91	rpdivcld 11889	. . . . . . . . . . 11 |- ( ph -> ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) ) e. RR+ )
93	68, 92	eqeltrd 2701	. . . . . . . . . 10 |- ( ph -> X e. RR+ )
94	66, 93	ifcld 4131	. . . . . . . . 9 |- ( ph -> if ( 1 <_ X , 1 , X ) e. RR+ )
95	64, 94	eqeltrd 2701	. . . . . . . 8 |- ( ph -> Y e. RR+ )
96	95	rpred 11872	. . . . . . 7 |- ( ph -> Y e. RR )
97		resqcl 12931	. . . . . . 7 |- ( Y e. RR -> ( Y ^ 2 ) e. RR )
98	96, 97	syl 17	. . . . . 6 |- ( ph -> ( Y ^ 2 ) e. RR )
99	96, 77	remulcld 10070	. . . . . . . 8 |- ( ph -> ( Y x. ( abs ` V ) ) e. RR )
100	96, 76	remulcld 10070	. . . . . . . 8 |- ( ph -> ( Y x. ( abs ` U ) ) e. RR )
101	99, 100	jca 554	. . . . . . 7 |- ( ph -> ( ( Y x. ( abs ` V ) ) e. RR /\ ( Y x. ( abs ` U ) ) e. RR ) )
102		readdcl 10019	. . . . . . 7 |- ( ( ( Y x. ( abs ` V ) ) e. RR /\ ( Y x. ( abs ` U ) ) e. RR ) -> ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) e. RR )
103	101, 102	syl 17	. . . . . 6 |- ( ph -> ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) e. RR )
104	98, 103	jca 554	. . . . 5 |- ( ph -> ( ( Y ^ 2 ) e. RR /\ ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) e. RR ) )
105		readdcl 10019	. . . . 5 |- ( ( ( Y ^ 2 ) e. RR /\ ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) e. RR ) -> ( ( Y ^ 2 ) + ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) ) e. RR )
106	104, 105	syl 17	. . . 4 |- ( ph -> ( ( Y ^ 2 ) + ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) ) e. RR )
107	71, 70	resubcld 10458	. . . 4 |- ( ph -> ( A - ( U x. V ) ) e. RR )
108	96	resqcld 13035	. . . . 5 |- ( ph -> ( Y ^ 2 ) e. RR )
109	99, 100	readdcld 10069	. . . . 5 |- ( ph -> ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) e. RR )
110	11, 36	eqeltrd 2701	. . . . . . . 8 |- ( ph -> ( ( H - U ) x. ( I - V ) ) e. CC )
111	110	abscld 14175	. . . . . . 7 |- ( ph -> ( abs ` ( ( H - U ) x. ( I - V ) ) ) e. RR )
112	96, 96	remulcld 10070	. . . . . . 7 |- ( ph -> ( Y x. Y ) e. RR )
113	50	leabsd 14153	. . . . . . 7 |- ( ph -> ( ( H - U ) x. ( I - V ) ) <_ ( abs ` ( ( H - U ) x. ( I - V ) ) ) )
114	44	recnd 10068	. . . . . . . . 9 |- ( ph -> ( H - U ) e. CC )
115	47	recnd 10068	. . . . . . . . 9 |- ( ph -> ( I - V ) e. CC )
116	114, 115	absmuld 14193	. . . . . . . 8 |- ( ph -> ( abs ` ( ( H - U ) x. ( I - V ) ) ) = ( ( abs ` ( H - U ) ) x. ( abs ` ( I - V ) ) ) )
117	114	abscld 14175	. . . . . . . . 9 |- ( ph -> ( abs ` ( H - U ) ) e. RR )
118	115	abscld 14175	. . . . . . . . 9 |- ( ph -> ( abs ` ( I - V ) ) e. RR )
119	114	absge0d 14183	. . . . . . . . 9 |- ( ph -> 0 <_ ( abs ` ( H - U ) ) )
120	4, 96	resubcld 10458	. . . . . . . . . . . 12 |- ( ph -> ( U - Y ) e. RR )
121		smfmullem1.p	. . . . . . . . . . . . 13 |- ( ph -> P e. ( ( U - Y ) (,) U ) )
122	121	elioored 39776	. . . . . . . . . . . 12 |- ( ph -> P e. RR )
123	120	rexrd 10089	. . . . . . . . . . . . 13 |- ( ph -> ( U - Y ) e. RR* )
124	4	rexrd 10089	. . . . . . . . . . . . 13 |- ( ph -> U e. RR* )
125		ioogtlb 39717	. . . . . . . . . . . . 13 |- ( ( ( U - Y ) e. RR* /\ U e. RR* /\ P e. ( ( U - Y ) (,) U ) ) -> ( U - Y ) < P )
126	123, 124, 121, 125	syl3anc 1326	. . . . . . . . . . . 12 |- ( ph -> ( U - Y ) < P )
127	122	rexrd 10089	. . . . . . . . . . . . 13 |- ( ph -> P e. RR* )
128		smfmullem1.r	. . . . . . . . . . . . . . 15 |- ( ph -> R e. ( U (,) ( U + Y ) ) )
129	128	elioored 39776	. . . . . . . . . . . . . 14 |- ( ph -> R e. RR )
130	129	rexrd 10089	. . . . . . . . . . . . 13 |- ( ph -> R e. RR* )
131		ioogtlb 39717	. . . . . . . . . . . . 13 |- ( ( P e. RR* /\ R e. RR* /\ H e. ( P (,) R ) ) -> P < H )
132	127, 130, 1, 131	syl3anc 1326	. . . . . . . . . . . 12 |- ( ph -> P < H )
133	120, 122, 2, 126, 132	lttrd 10198	. . . . . . . . . . 11 |- ( ph -> ( U - Y ) < H )
134	4, 96	readdcld 10069	. . . . . . . . . . . 12 |- ( ph -> ( U + Y ) e. RR )
135		iooltub 39735	. . . . . . . . . . . . 13 |- ( ( P e. RR* /\ R e. RR* /\ H e. ( P (,) R ) ) -> H < R )
136	127, 130, 1, 135	syl3anc 1326	. . . . . . . . . . . 12 |- ( ph -> H < R )
137	134	rexrd 10089	. . . . . . . . . . . . 13 |- ( ph -> ( U + Y ) e. RR* )
138		iooltub 39735	. . . . . . . . . . . . 13 |- ( ( U e. RR* /\ ( U + Y ) e. RR* /\ R e. ( U (,) ( U + Y ) ) ) -> R < ( U + Y ) )
139	124, 137, 128, 138	syl3anc 1326	. . . . . . . . . . . 12 |- ( ph -> R < ( U + Y ) )
140	2, 129, 134, 136, 139	lttrd 10198	. . . . . . . . . . 11 |- ( ph -> H < ( U + Y ) )
141	133, 140	jca 554	. . . . . . . . . 10 |- ( ph -> ( ( U - Y ) < H /\ H < ( U + Y ) ) )
142	2, 4, 96	absdifltd 14172	. . . . . . . . . 10 |- ( ph -> ( ( abs ` ( H - U ) ) < Y <-> ( ( U - Y ) < H /\ H < ( U + Y ) ) ) )
143	141, 142	mpbird 247	. . . . . . . . 9 |- ( ph -> ( abs ` ( H - U ) ) < Y )
144	115	absge0d 14183	. . . . . . . . 9 |- ( ph -> 0 <_ ( abs ` ( I - V ) ) )
145	9, 96	resubcld 10458	. . . . . . . . . . . 12 |- ( ph -> ( V - Y ) e. RR )
146		smfmullem1.s	. . . . . . . . . . . . 13 |- ( ph -> S e. ( ( V - Y ) (,) V ) )
147	146	elioored 39776	. . . . . . . . . . . 12 |- ( ph -> S e. RR )
148	145	rexrd 10089	. . . . . . . . . . . . 13 |- ( ph -> ( V - Y ) e. RR* )
149	9	rexrd 10089	. . . . . . . . . . . . 13 |- ( ph -> V e. RR* )
150	148, 149, 146	ioogtlbd 39777	. . . . . . . . . . . 12 |- ( ph -> ( V - Y ) < S )
151	147	rexrd 10089	. . . . . . . . . . . . 13 |- ( ph -> S e. RR* )
152		smfmullem1.z	. . . . . . . . . . . . . . 15 |- ( ph -> Z e. ( V (,) ( V + Y ) ) )
153	152	elioored 39776	. . . . . . . . . . . . . 14 |- ( ph -> Z e. RR )
154	153	rexrd 10089	. . . . . . . . . . . . 13 |- ( ph -> Z e. RR* )
155	151, 154, 6	ioogtlbd 39777	. . . . . . . . . . . 12 |- ( ph -> S < I )
156	145, 147, 7, 150, 155	lttrd 10198	. . . . . . . . . . 11 |- ( ph -> ( V - Y ) < I )
157	9, 96	readdcld 10069	. . . . . . . . . . . 12 |- ( ph -> ( V + Y ) e. RR )
158	151, 154, 6	iooltubd 39771	. . . . . . . . . . . 12 |- ( ph -> I < Z )
159	157	rexrd 10089	. . . . . . . . . . . . 13 |- ( ph -> ( V + Y ) e. RR* )
160	149, 159, 152	iooltubd 39771	. . . . . . . . . . . 12 |- ( ph -> Z < ( V + Y ) )
161	7, 153, 157, 158, 160	lttrd 10198	. . . . . . . . . . 11 |- ( ph -> I < ( V + Y ) )
162	156, 161	jca 554	. . . . . . . . . 10 |- ( ph -> ( ( V - Y ) < I /\ I < ( V + Y ) ) )
163	7, 9, 96	absdifltd 14172	. . . . . . . . . 10 |- ( ph -> ( ( abs ` ( I - V ) ) < Y <-> ( ( V - Y ) < I /\ I < ( V + Y ) ) ) )
164	162, 163	mpbird 247	. . . . . . . . 9 |- ( ph -> ( abs ` ( I - V ) ) < Y )
165	117, 96, 118, 96, 119, 143, 144, 164	ltmul12ad 10965	. . . . . . . 8 |- ( ph -> ( ( abs ` ( H - U ) ) x. ( abs ` ( I - V ) ) ) < ( Y x. Y ) )
166	116, 165	eqbrtrd 4675	. . . . . . 7 |- ( ph -> ( abs ` ( ( H - U ) x. ( I - V ) ) ) < ( Y x. Y ) )
167	50, 111, 112, 113, 166	lelttrd 10195	. . . . . 6 |- ( ph -> ( ( H - U ) x. ( I - V ) ) < ( Y x. Y ) )
168	96	recnd 10068	. . . . . . . 8 |- ( ph -> Y e. CC )
169	168	sqvald 13005	. . . . . . 7 |- ( ph -> ( Y ^ 2 ) = ( Y x. Y ) )
170	169	eqcomd 2628	. . . . . 6 |- ( ph -> ( Y x. Y ) = ( Y ^ 2 ) )
171	167, 170	breqtrd 4679	. . . . 5 |- ( ph -> ( ( H - U ) x. ( I - V ) ) < ( Y ^ 2 ) )
172	53	recnd 10068	. . . . . . . 8 |- ( ph -> ( ( H - U ) x. V ) e. CC )
173	172	abscld 14175	. . . . . . 7 |- ( ph -> ( abs ` ( ( H - U ) x. V ) ) e. RR )
174	53	leabsd 14153	. . . . . . 7 |- ( ph -> ( ( H - U ) x. V ) <_ ( abs ` ( ( H - U ) x. V ) ) )
175	114, 10	absmuld 14193	. . . . . . . 8 |- ( ph -> ( abs ` ( ( H - U ) x. V ) ) = ( ( abs ` ( H - U ) ) x. ( abs ` V ) ) )
176	117, 96, 143	ltled 10185	. . . . . . . . 9 |- ( ph -> ( abs ` ( H - U ) ) <_ Y )
177	117, 96, 77, 84, 176	lemul1ad 10963	. . . . . . . 8 |- ( ph -> ( ( abs ` ( H - U ) ) x. ( abs ` V ) ) <_ ( Y x. ( abs ` V ) ) )
178	175, 177	eqbrtrd 4675	. . . . . . 7 |- ( ph -> ( abs ` ( ( H - U ) x. V ) ) <_ ( Y x. ( abs ` V ) ) )
179	53, 173, 99, 174, 178	letrd 10194	. . . . . 6 |- ( ph -> ( ( H - U ) x. V ) <_ ( Y x. ( abs ` V ) ) )
180	56	recnd 10068	. . . . . . . 8 |- ( ph -> ( U x. ( I - V ) ) e. CC )
181	180	abscld 14175	. . . . . . 7 |- ( ph -> ( abs ` ( U x. ( I - V ) ) ) e. RR )
182	56	leabsd 14153	. . . . . . 7 |- ( ph -> ( U x. ( I - V ) ) <_ ( abs ` ( U x. ( I - V ) ) ) )
183	5, 115	absmuld 14193	. . . . . . . . 9 |- ( ph -> ( abs ` ( U x. ( I - V ) ) ) = ( ( abs ` U ) x. ( abs ` ( I - V ) ) ) )
184	76	recnd 10068	. . . . . . . . . 10 |- ( ph -> ( abs ` U ) e. CC )
185	118	recnd 10068	. . . . . . . . . 10 |- ( ph -> ( abs ` ( I - V ) ) e. CC )
186	184, 185	mulcomd 10061	. . . . . . . . 9 |- ( ph -> ( ( abs ` U ) x. ( abs ` ( I - V ) ) ) = ( ( abs ` ( I - V ) ) x. ( abs ` U ) ) )
187	183, 186	eqtrd 2656	. . . . . . . 8 |- ( ph -> ( abs ` ( U x. ( I - V ) ) ) = ( ( abs ` ( I - V ) ) x. ( abs ` U ) ) )
188	118, 96, 164	ltled 10185	. . . . . . . . 9 |- ( ph -> ( abs ` ( I - V ) ) <_ Y )
189	118, 96, 76, 83, 188	lemul1ad 10963	. . . . . . . 8 |- ( ph -> ( ( abs ` ( I - V ) ) x. ( abs ` U ) ) <_ ( Y x. ( abs ` U ) ) )
190	187, 189	eqbrtrd 4675	. . . . . . 7 |- ( ph -> ( abs ` ( U x. ( I - V ) ) ) <_ ( Y x. ( abs ` U ) ) )
191	56, 181, 100, 182, 190	letrd 10194	. . . . . 6 |- ( ph -> ( U x. ( I - V ) ) <_ ( Y x. ( abs ` U ) ) )
192	53, 56, 99, 100, 179, 191	leadd12dd 39532	. . . . 5 |- ( ph -> ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) <_ ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) )
193	50, 59, 108, 109, 171, 192	ltleaddd 10648	. . . 4 |- ( ph -> ( ( ( H - U ) x. ( I - V ) ) + ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) ) < ( ( Y ^ 2 ) + ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) ) )
194	96, 103	readdcld 10069	. . . . 5 |- ( ph -> ( Y + ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) ) e. RR )
195	81, 117, 96, 119, 176	letrd 10194	. . . . . . . 8 |- ( ph -> 0 <_ Y )
196	93	rpred 11872	. . . . . . . . . 10 |- ( ph -> X e. RR )
197		min1 12020	. . . . . . . . . 10 |- ( ( 1 e. RR /\ X e. RR ) -> if ( 1 <_ X , 1 , X ) <_ 1 )
198	75, 196, 197	syl2anc 693	. . . . . . . . 9 |- ( ph -> if ( 1 <_ X , 1 , X ) <_ 1 )
199	63, 198	syl5eqbr 4688	. . . . . . . 8 |- ( ph -> Y <_ 1 )
200	81, 75, 96, 195, 199	eliccd 39726	. . . . . . 7 |- ( ph -> Y e. ( 0 [,] 1 ) )
201	96	sqrlearg 39780	. . . . . . 7 |- ( ph -> ( ( Y ^ 2 ) <_ Y <-> Y e. ( 0 [,] 1 ) ) )
202	200, 201	mpbird 247	. . . . . 6 |- ( ph -> ( Y ^ 2 ) <_ Y )
203	98, 96, 103, 202	leadd1dd 10641	. . . . 5 |- ( ph -> ( ( Y ^ 2 ) + ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) ) <_ ( Y + ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) ) )
204		1cnd 10056	. . . . . . . 8 |- ( ph -> 1 e. CC )
205	77	recnd 10068	. . . . . . . . 9 |- ( ph -> ( abs ` V ) e. CC )
206	205, 184	addcld 10059	. . . . . . . 8 |- ( ph -> ( ( abs ` V ) + ( abs ` U ) ) e. CC )
207	168, 204, 206	adddid 10064	. . . . . . 7 |- ( ph -> ( Y x. ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) = ( ( Y x. 1 ) + ( Y x. ( ( abs ` V ) + ( abs ` U ) ) ) ) )
208	168	mulid1d 10057	. . . . . . . 8 |- ( ph -> ( Y x. 1 ) = Y )
209	168, 205, 184	adddid 10064	. . . . . . . 8 |- ( ph -> ( Y x. ( ( abs ` V ) + ( abs ` U ) ) ) = ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) )
210	208, 209	oveq12d 6668	. . . . . . 7 |- ( ph -> ( ( Y x. 1 ) + ( Y x. ( ( abs ` V ) + ( abs ` U ) ) ) ) = ( Y + ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) ) )
211	207, 210	eqtr2d 2657	. . . . . 6 |- ( ph -> ( Y + ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) ) = ( Y x. ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) )
212	77, 76	readdcld 10069	. . . . . . . . 9 |- ( ph -> ( ( abs ` V ) + ( abs ` U ) ) e. RR )
213	75, 212	readdcld 10069	. . . . . . . 8 |- ( ph -> ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) e. RR )
214	77, 76	addge01d 10615	. . . . . . . . . . . . 13 |- ( ph -> ( 0 <_ ( abs ` U ) <-> ( abs ` V ) <_ ( ( abs ` V ) + ( abs ` U ) ) ) )
215	83, 214	mpbid 222	. . . . . . . . . . . 12 |- ( ph -> ( abs ` V ) <_ ( ( abs ` V ) + ( abs ` U ) ) )
216	81, 77, 212, 84, 215	letrd 10194	. . . . . . . . . . 11 |- ( ph -> 0 <_ ( ( abs ` V ) + ( abs ` U ) ) )
217	75, 212	addge01d 10615	. . . . . . . . . . 11 |- ( ph -> ( 0 <_ ( ( abs ` V ) + ( abs ` U ) ) <-> 1 <_ ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) )
218	216, 217	mpbid 222	. . . . . . . . . 10 |- ( ph -> 1 <_ ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) )
219	81, 75, 213, 82, 218	ltletrd 10197	. . . . . . . . 9 |- ( ph -> 0 < ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) )
220	81, 213, 219	ltled 10185	. . . . . . . 8 |- ( ph -> 0 <_ ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) )
221		min2 12021	. . . . . . . . . 10 |- ( ( 1 e. RR /\ X e. RR ) -> if ( 1 <_ X , 1 , X ) <_ X )
222	75, 196, 221	syl2anc 693	. . . . . . . . 9 |- ( ph -> if ( 1 <_ X , 1 , X ) <_ X )
223	64, 222	eqbrtrd 4675	. . . . . . . 8 |- ( ph -> Y <_ X )
224	96, 196, 213, 220, 223	lemul1ad 10963	. . . . . . 7 |- ( ph -> ( Y x. ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) <_ ( X x. ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) )
225	68	oveq1d 6665	. . . . . . . 8 |- ( ph -> ( X x. ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) = ( ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) ) x. ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) )
226	184, 205	addcomd 10238	. . . . . . . . . . 11 |- ( ph -> ( ( abs ` U ) + ( abs ` V ) ) = ( ( abs ` V ) + ( abs ` U ) ) )
227	226	oveq2d 6666	. . . . . . . . . 10 |- ( ph -> ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) = ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) )
228	227	oveq2d 6666	. . . . . . . . 9 |- ( ph -> ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) ) = ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) )
229	228	oveq1d 6665	. . . . . . . 8 |- ( ph -> ( ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) ) x. ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) = ( ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) x. ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) )
230	107	recnd 10068	. . . . . . . . 9 |- ( ph -> ( A - ( U x. V ) ) e. CC )
231	204, 206	addcld 10059	. . . . . . . . 9 |- ( ph -> ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) e. CC )
232	81, 219	gtned 10172	. . . . . . . . 9 |- ( ph -> ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) =/= 0 )
233	230, 231, 232	divcan1d 10802	. . . . . . . 8 |- ( ph -> ( ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) x. ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) = ( A - ( U x. V ) ) )
234	225, 229, 233	3eqtrd 2660	. . . . . . 7 |- ( ph -> ( X x. ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) = ( A - ( U x. V ) ) )
235	224, 234	breqtrd 4679	. . . . . 6 |- ( ph -> ( Y x. ( 1 + ( ( abs ` V ) + ( abs ` U ) ) ) ) <_ ( A - ( U x. V ) ) )
236	211, 235	eqbrtrd 4675	. . . . 5 |- ( ph -> ( Y + ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) ) <_ ( A - ( U x. V ) ) )
237	106, 194, 107, 203, 236	letrd 10194	. . . 4 |- ( ph -> ( ( Y ^ 2 ) + ( ( Y x. ( abs ` V ) ) + ( Y x. ( abs ` U ) ) ) ) <_ ( A - ( U x. V ) ) )
238	62, 106, 107, 193, 237	ltletrd 10197	. . 3 |- ( ph -> ( ( ( H - U ) x. ( I - V ) ) + ( ( ( H - U ) x. V ) + ( U x. ( I - V ) ) ) ) < ( A - ( U x. V ) ) )
239	41, 238	eqbrtrd 4675	. 2 |- ( ph -> ( ( H x. I ) - ( U x. V ) ) < ( A - ( U x. V ) ) )
240	2, 7	remulcld 10070	. . 3 |- ( ph -> ( H x. I ) e. RR )
241	240, 71, 70	ltsub1d 10636	. 2 |- ( ph -> ( ( H x. I ) < A <-> ( ( H x. I ) - ( U x. V ) ) < ( A - ( U x. V ) ) ) )
242	239, 241	mpbird 247	1 |- ( ph -> ( H x. I ) < A )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   ifcif 4086   class class class wbr 4653   ` cfv 5888  (class class class)co 6650   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   2c2 11070   RR+crp 11832   (,)cioo 12175   [,]cicc 12178   ^cexp 12860   abscabs 13974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-sup 8348  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-ioo 12179  df-icc 12182  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976

This theorem is referenced by:  smfmullem2  40999