Theorem efcnlem2 7377

Description: Lemma for efcn 7380.

Hypotheses

Ref	Expression
efcnlem2.1	|- X e. CC
efcnlem2.2	|- W e. CC
efcnlem2.3	|- Y e. RR
efcnlem2.4	|- 0 < Y
efcnlem2.5	|- S = (abs` (exp` X))
efcnlem2.6	|- H = (abs` (X - W))
efcnlem2.7	|- G = (H / (1 - H))
efcnlem2.8	|- D = (Y / (S + Y))

Assertion

Ref	Expression
efcnlem2	|- (H < D -> (abs` ((exp` X) - (exp` W))) < Y)

Proof of Theorem efcnlem2

Step	Hyp	Ref	Expression
1		efcnlem2.5	. . . . . . 7 |- S = (abs` (exp` X))
2		efcnlem2.1	. . . . . . . . 9 |- X e. CC
3		efclt 7271	. . . . . . . . 9 |- (X e. CC -> (exp` X) e. CC)
4	2, 3	ax-mp 7	. . . . . . . 8 |- (exp` X) e. CC
5	4	abscl 6789	. . . . . . 7 |- (abs` (exp` X)) e. RR
6	1, 5	eqeltr 1542	. . . . . 6 |- S e. RR
7		efcnlem2.2	. . . . . . . . . 10 |- W e. CC
8	7, 2	subcl 5349	. . . . . . . . 9 |- (W - X) e. CC
9		efclt 7271	. . . . . . . . 9 |- ((W - X) e. CC -> (exp` (W - X)) e. CC)
10	8, 9	ax-mp 7	. . . . . . . 8 |- (exp` (W - X)) e. CC
11		ax1cn 5252	. . . . . . . 8 |- 1 e. CC
12	10, 11	subcl 5349	. . . . . . 7 |- ((exp` (W - X)) - 1) e. CC
13	12	abscl 6789	. . . . . 6 |- (abs` ((exp` (W - X)) - 1)) e. RR
14	6, 13	remulcl 5318	. . . . 5 |- (S x. (abs` ((exp` (W - X)) - 1))) e. RR
15	14	a1i 8	. . . 4 |- (H < D -> (S x. (abs` ((exp` (W - X)) - 1))) e. RR)
16		axmulrcl 5257	. . . . 5 |- ((S e. RR /\ G e. RR) -> (S x. G) e. RR)
17	6	a1i 8	. . . . 5 |- (H < D -> S e. RR)
18		efcnlem2.8	. . . . . . . . 9 |- D = (Y / (S + Y))
19	18	breq2i 2623	. . . . . . . 8 |- (H < D <-> H < (Y / (S + Y)))
20		efcnlem2.6	. . . . . . . . . . 11 |- H = (abs` (X - W))
21	7, 2	negsubdi2 5433	. . . . . . . . . . . 12 |- -u(W - X) = (X - W)
22	21	fveq2i 3722	. . . . . . . . . . 11 |- (abs` -u(W - X)) = (abs` (X - W))
23	8	absneg 6794	. . . . . . . . . . 11 |- (abs` -u(W - X)) = (abs` (W - X))
24	20, 22, 23	3eqtr2 1499	. . . . . . . . . 10 |- H = (abs` (W - X))
25	8	abscl 6789	. . . . . . . . . 10 |- (abs` (W - X)) e. RR
26	24, 25	eqeltr 1542	. . . . . . . . 9 |- H e. RR
27		efcnlem2.3	. . . . . . . . 9 |- Y e. RR
28		efne0t 7328	. . . . . . . . . . . 12 |- (X e. CC -> (exp` X) =/= 0)
29	2, 28	ax-mp 7	. . . . . . . . . . 11 |- (exp` X) =/= 0
30	4	absgt0 6793	. . . . . . . . . . 11 |- ((exp` X) =/= 0 <-> 0 < (abs` (exp` X)))
31	29, 30	mpbi 189	. . . . . . . . . 10 |- 0 < (abs` (exp` X))
32	31, 1	breqtrr 2636	. . . . . . . . 9 |- 0 < S
33		efcnlem2.4	. . . . . . . . 9 |- 0 < Y
34	26, 6, 27, 32, 33	efcnlem1 7376	. . . . . . . 8 |- (H < (Y / (S + Y)) -> (H < 1 /\ (1 - H) =/= 0 /\ (S x. (H / (1 - H))) < Y))
35	19, 34	sylbi 199	. . . . . . 7 |- (H < D -> (H < 1 /\ (1 - H) =/= 0 /\ (S x. (H / (1 - H))) < Y))
36	35	3simp2d 794	. . . . . 6 |- (H < D -> (1 - H) =/= 0)
37		1re 5418	. . . . . . . . 9 |- 1 e. RR
38	37, 26	resubcl 5422	. . . . . . . 8 |- (1 - H) e. RR
39	26, 38	redivclz 5765	. . . . . . 7 |- ((1 - H) =/= 0 -> (H / (1 - H)) e. RR)
40		efcnlem2.7	. . . . . . 7 |- G = (H / (1 - H))
41	39, 40	syl5eqel 1550	. . . . . 6 |- ((1 - H) =/= 0 -> G e. RR)
42	36, 41	syl 10	. . . . 5 |- (H < D -> G e. RR)
43	16, 17, 42	sylanc 471	. . . 4 |- (H < D -> (S x. G) e. RR)
44	27	a1i 8	. . . 4 |- (H < D -> Y e. RR)
45	13	a1i 8	. . . . . 6 |- (H < D -> (abs` ((exp` (W - X)) - 1)) e. RR)
46	26	reefcl 7276	. . . . . . . 8 |- (exp` H) e. RR
47	46, 37	resubcl 5422	. . . . . . 7 |- ((exp` H) - 1) e. RR
48	47	a1i 8	. . . . . 6 |- (H < D -> ((exp` H) - 1) e. RR)
49	8	absefm1le 7369	. . . . . . . 8 |- (abs` ((exp` (W - X)) - 1)) <_ ((exp` (abs` (W - X))) - 1)
50	24	fveq2i 3722	. . . . . . . . 9 |- (exp` H) = (exp` (abs` (W - X)))
51	50	opreq1i 3966	. . . . . . . 8 |- ((exp` H) - 1) = ((exp` (abs` (W - X))) - 1)
52	49, 51	breqtrr 2636	. . . . . . 7 |- (abs` ((exp` (W - X)) - 1)) <_ ((exp` H) - 1)
53	52	a1i 8	. . . . . 6 |- (H < D -> (abs` ((exp` (W - X)) - 1)) <_ ((exp` H) - 1))
54	35	3simp1d 793	. . . . . . . 8 |- (H < D -> H < 1)
55	8	absge0 6790	. . . . . . . . . 10 |- 0 <_ (abs` (W - X))
56	55, 24	breqtrr 2636	. . . . . . . . 9 |- 0 <_ H
57		efm1legeot 7375	. . . . . . . . 9 |- ((H e. RR /\ 0 <_ H /\ H < 1) -> ((exp` H) - 1) <_ (H / (1 - H)))
58	26, 56, 57	mp3an12 905	. . . . . . . 8 |- (H < 1 -> ((exp` H) - 1) <_ (H / (1 - H)))
59	54, 58	syl 10	. . . . . . 7 |- (H < D -> ((exp` H) - 1) <_ (H / (1 - H)))
60	59, 40	syl6breqr 2651	. . . . . 6 |- (H < D -> ((exp` H) - 1) <_ G)
61	45, 48, 42, 53, 60	letrd 5509	. . . . 5 |- (H < D -> (abs` ((exp` (W - X)) - 1)) <_ G)
62		lemul2t 5799	. . . . . . 7 |- ((((abs` ((exp` (W - X)) - 1)) e. RR /\ G e. RR /\ S e. RR) /\ 0 < S) -> ((abs` ((exp` (W - X)) - 1)) <_ G <-> (S x. (abs` ((exp` (W - X)) - 1))) <_ (S x. G)))
63	32, 62	mpan2 695	. . . . . 6 |- (((abs` ((exp` (W - X)) - 1)) e. RR /\ G e. RR /\ S e. RR) -> ((abs` ((exp` (W - X)) - 1)) <_ G <-> (S x. (abs` ((exp` (W - X)) - 1))) <_ (S x. G)))
64	63, 45, 42, 17	syl3anc 857	. . . . 5 |- (H < D -> ((abs` ((exp` (W - X)) - 1)) <_ G <-> (S x. (abs` ((exp` (W - X)) - 1))) <_ (S x. G)))
65	61, 64	mpbid 195	. . . 4 |- (H < D -> (S x. (abs` ((exp` (W - X)) - 1))) <_ (S x. G))
66	35	3simp3d 795	. . . . 5 |- (H < D -> (S x. (H / (1 - H))) < Y)
67	40	opreq2i 3967	. . . . 5 |- (S x. G) = (S x. (H / (1 - H)))
68	66, 67	syl5eqbr 2644	. . . 4 |- (H < D -> (S x. G) < Y)
69	15, 43, 44, 65, 68	lelttrd 5510	. . 3 |- (H < D -> (S x. (abs` ((exp` (W - X)) - 1))) < Y)
70	4, 12	absmul 6797	. . . 4 |- (abs` ((exp` X) x. ((exp` (W - X)) - 1))) = ((abs` (exp` X)) x. (abs` ((exp` (W - X)) - 1)))
71	4, 10, 11	subdi 5412	. . . . . 6 |- ((exp` X) x. ((exp` (W - X)) - 1)) = (((exp` X) x. (exp` (W - X))) - ((exp` X) x. 1))
72	2, 8	efadd 7325	. . . . . . . 8 |- (exp` (X + (W - X))) = ((exp` X) x. (exp` (W - X)))
73	2, 7	pncan3 5361	. . . . . . . . 9 |- (X + (W - X)) = W
74	73	fveq2i 3722	. . . . . . . 8 |- (exp` (X + (W - X))) = (exp` W)
75	72, 74	eqtr3 1495	. . . . . . 7 |- ((exp` X) x. (exp` (W - X))) = (exp` W)
76	4	mulid1 5315	. . . . . . 7 |- ((exp` X) x. 1) = (exp` X)
77	75, 76	opreq12i 3968	. . . . . 6 |- (((exp` X) x. (exp` (W - X))) - ((exp` X) x. 1)) = ((exp` W) - (exp` X))
78	71, 77	eqtr2 1494	. . . . 5 |- ((exp` W) - (exp` X)) = ((exp` X) x. ((exp` (W - X)) - 1))
79	78	fveq2i 3722	. . . 4 |- (abs` ((exp` W) - (exp` X))) = (abs` ((exp` X) x. ((exp` (W - X)) - 1)))
80	1	opreq1i 3966	. . . 4 |- (S x. (abs` ((exp` (W - X)) - 1))) = ((abs` (exp` X)) x. (abs` ((exp` (W - X)) - 1)))
81	70, 79, 80	3eqtr4 1503	. . 3 |- (abs` ((exp` W) - (exp` X))) = (S x. (abs` ((exp` (W - X)) - 1)))
82	69, 81	syl5eqbr 2644	. 2 |- (H < D -> (abs` ((exp` W) - (exp` X))) < Y)
83		efclt 7271	. . . 4 |- (W e. CC -> (exp` W) e. CC)
84	7, 83	ax-mp 7	. . 3 |- (exp` W) e. CC
85	4, 84	abssub 6796	. 2 |- (abs` ((exp` X) - (exp` W))) = (