Theorem efcnlem4 7422

Description: Lemma for efcn 7423.

Assertion

Ref	Expression
efcnlem4	|- ((X e. CC /\ W e. CC /\ (Y e. RR /\ 0 < Y)) -> ((abs` (X - W)) < (Y / ((abs` (exp` X)) + Y)) -> (abs` ((exp` X) - (exp` W))) < Y))

Proof of Theorem efcnlem4

Step	Hyp	Ref	Expression
1		opreq1 3968	. . . . 5 |- (X = if(X e. CC, X, 0) -> (X - W) = (if(X e. CC, X, 0) - W))
2	1	fveq2d 3728	. . . 4 |- (X = if(X e. CC, X, 0) -> (abs` (X - W)) = (abs` (if(X e. CC, X, 0) - W)))
3		fveq2 3724	. . . . . 6 |- (X = if(X e. CC, X, 0) -> (exp` X) = (exp` if(X e. CC, X, 0)))
4		fveq2 3724	. . . . . 6 |- ((exp` X) = (exp` if(X e. CC, X, 0)) -> (abs` (exp` X)) = (abs` (exp` if(X e. CC, X, 0))))
5		opreq1 3968	. . . . . 6 |- ((abs` (exp` X)) = (abs` (exp` if(X e. CC, X, 0))) -> ((abs` (exp` X)) + Y) = ((abs` (exp` if(X e. CC, X, 0))) + Y))
6	3, 4, 5	3syl 20	. . . . 5 |- (X = if(X e. CC, X, 0) -> ((abs` (exp` X)) + Y) = ((abs` (exp` if(X e. CC, X, 0))) + Y))
7	6	opreq2d 3976	. . . 4 |- (X = if(X e. CC, X, 0) -> (Y / ((abs` (exp` X)) + Y)) = (Y / ((abs` (exp` if(X e. CC, X, 0))) + Y)))
8	2, 7	breq12d 2631	. . 3 |- (X = if(X e. CC, X, 0) -> ((abs` (X - W)) < (Y / ((abs` (exp` X)) + Y)) <-> (abs` (if(X e. CC, X, 0) - W)) < (Y / ((abs` (exp` if(X e. CC, X, 0))) + Y))))
9		opreq1 3968	. . . . 5 |- ((exp` X) = (exp` if(X e. CC, X, 0)) -> ((exp` X) - (exp` W)) = ((exp` if(X e. CC, X, 0)) - (exp` W)))
10		fveq2 3724	. . . . 5 |- (((exp` X) - (exp` W)) = ((exp` if(X e. CC, X, 0)) - (exp` W)) -> (abs` ((exp` X) - (exp` W))) = (abs` ((exp` if(X e. CC, X, 0)) - (exp` W))))
11	3, 9, 10	3syl 20	. . . 4 |- (X = if(X e. CC, X, 0) -> (abs` ((exp` X) - (exp` W))) = (abs` ((exp` if(X e. CC, X, 0)) - (exp` W))))
12	11	breq1d 2629	. . 3 |- (X = if(X e. CC, X, 0) -> ((abs` ((exp` X) - (exp` W))) < Y <-> (abs` ((exp` if(X e. CC, X, 0)) - (exp` W))) < Y))
13	8, 12	imbi12d 626	. 2 |- (X = if(X e. CC, X, 0) -> (((abs` (X - W)) < (Y / ((abs` (exp` X)) + Y)) -> (abs` ((exp` X) - (exp` W))) < Y) <-> ((abs` (if(X e. CC, X, 0) - W)) < (Y / ((abs` (exp` if(X e. CC, X, 0))) + Y)) -> (abs` ((exp` if(X e. CC, X, 0)) - (exp` W))) < Y)))
14		opreq2 3969	. . . . 5 |- (W = if(W e. CC, W, 0) -> (if(X e. CC, X, 0) - W) = (if(X e. CC, X, 0) - if(W e. CC, W, 0)))
15	14	fveq2d 3728	. . . 4 |- (W = if(W e. CC, W, 0) -> (abs` (if(X e. CC, X, 0) - W)) = (abs` (if(X e. CC, X, 0) - if(W e. CC, W, 0))))
16	15	breq1d 2629	. . 3 |- (W = if(W e. CC, W, 0) -> ((abs` (if(X e. CC, X, 0) - W)) < (Y / ((abs` (exp` if(X e. CC, X, 0))) + Y)) <-> (abs` (if(X e. CC, X, 0) - if(W e. CC, W, 0))) < (Y / ((abs` (exp` if(X e. CC, X, 0))) + Y))))
17		fveq2 3724	. . . . 5 |- (W = if(W e. CC, W, 0) -> (exp` W) = (exp` if(W e. CC, W, 0)))
18		opreq2 3969	. . . . 5 |- ((exp` W) = (exp` if(W e. CC, W, 0)) -> ((exp` if(X e. CC, X, 0)) - (exp` W)) = ((exp` if(X e. CC, X, 0)) - (exp` if(W e. CC, W, 0))))
19		fveq2 3724	. . . . 5 |- (((exp` if(X e. CC, X, 0)) - (exp` W)) = ((exp` if(X e. CC, X, 0)) - (exp` if(W e. CC, W, 0))) -> (abs` ((exp` if(X e. CC, X, 0)) - (exp` W))) = (abs` ((exp` if(X e. CC, X, 0)) - (exp` if(W e. CC, W, 0)))))
20	17, 18, 19	3syl 20	. . . 4 |- (W = if(W e. CC, W, 0) -> (abs` ((exp` if(X e. CC, X, 0)) - (exp` W))) = (abs` ((exp` if(X e. CC, X, 0)) - (exp` if(W e. CC, W, 0)))))
21	20	breq1d 2629	. . 3 |- (W = if(W e. CC, W, 0) -> ((abs` ((exp` if(X e. CC, X, 0)) - (exp` W))) < Y <-> (abs` ((exp` if(X e. CC, X, 0)) - (exp` if(W e. CC, W, 0)))) < Y))
22	16, 21	imbi12d 626	. 2 |- (W = if(W e. CC, W, 0) -> (((abs` (if(X e. CC, X, 0) - W)) < (Y / ((abs` (exp` if(X e. CC, X, 0))) + Y)) -> (abs` ((exp` if(X e. CC, X, 0)) - (exp` W))) < Y) <-> ((abs` (if(X e. CC, X, 0) - if(W e. CC, W, 0))) < (Y / ((abs` (exp` if(X e. CC, X, 0))) + Y)) -> (abs` ((exp` if(X e. CC, X, 0)) - (exp` if(W e. CC, W, 0)))) < Y)))
23		id 59	. . . . 5 |- (Y = if((Y e. RR /\ 0 < Y), Y, 1) -> Y = if((Y e. RR /\ 0 < Y), Y, 1))
24		opreq2 3969	. . . . 5 |- (Y = if((Y e. RR /\ 0 < Y), Y, 1) -> ((abs` (exp` if(X e. CC, X, 0))) + Y) = ((abs` (exp` if(X e. CC, X, 0))) + if((Y e. RR /\ 0 < Y), Y, 1)))
25	23, 24	opreq12d 3978	. . . 4 |- (Y = if((Y e. RR /\ 0 < Y), Y, 1) -> (Y / ((abs` (exp` if(X e. CC, X, 0))) + Y)) = (if((Y e. RR /\ 0 < Y), Y, 1) / ((abs` (exp` if(X e. CC, X, 0))) + if((Y e. RR /\ 0 < Y), Y, 1))))
26	25	breq2d 2630	. . 3 |- (Y = if((Y e. RR /\ 0 < Y), Y, 1) -> ((abs` (if(X e. CC, X, 0) - if(W e. CC, W, 0))) < (Y / ((abs` (exp` if(X e. CC, X, 0))) + Y)) <-> (abs` (if(X e. CC, X, 0) - if(W e. CC, W, 0))) < (if((Y e. RR /\ 0 < Y), Y, 1) / ((abs` (exp` if(X e. CC, X, 0))) + if((Y e. RR /\ 0 < Y), Y, 1)))))
27		breq2 2623	. . 3 |- (Y = if((Y e. RR /\ 0 < Y), Y, 1) -> ((abs` ((exp` if(X