Theorem cosh111lem1 8714

Description: Lemma for cosh111t 8717.

Hypotheses

Ref	Expression
cosh111lem1.1	|- A e. RR
cosh111lem1.2	|- B e. RR
cosh111lem1.3	|- 0 <_ A
cosh111lem1.4	|- 0 <_ B
cosh111lem1.5	|- A < pi
cosh111lem1.6	|- B < pi

Assertion

Ref	Expression
cosh111lem1	|- (A < B -> (cos` B) < (cos` A))

Proof of Theorem cosh111lem1

Step	Hyp	Ref	Expression
1		cosh111lem1.2	. . . . . . . . 9 |- B e. RR
2		cosh111lem1.1	. . . . . . . . 9 |- A e. RR
3	1, 2	readdcl 5334	. . . . . . . 8 |- (B + A) e. RR
4		2re 5979	. . . . . . . 8 |- 2 e. RR
5		2ne0 5990	. . . . . . . 8 |- 2 =/= 0
6	3, 4, 5	redivcl 5798	. . . . . . 7 |- ((B + A) / 2) e. RR
7		resinclt 7438	. . . . . . 7 |- (((B + A) / 2) e. RR -> (sin` ((B + A) / 2)) e. RR)
8	6, 7	ax-mp 7	. . . . . 6 |- (sin` ((B + A) / 2)) e. RR
9	1, 2	resubcl 5439	. . . . . . . 8 |- (B - A) e. RR
10	9, 4, 5	redivcl 5798	. . . . . . 7 |- ((B - A) / 2) e. RR
11		resinclt 7438	. . . . . . 7 |- (((B - A) / 2) e. RR -> (sin` ((B - A) / 2)) e. RR)
12	10, 11	ax-mp 7	. . . . . 6 |- (sin` ((B - A) / 2)) e. RR
13	8, 12	mulgt0 5606	. . . . 5 |- ((0 < (sin` ((B + A) / 2)) /\ 0 < (sin` ((B - A) / 2))) -> 0 < ((sin` ((B + A) / 2)) x. (sin` ((B - A) / 2))))
14		cosh111lem1.3	. . . . . . 7 |- 0 <_ A
15		0re 5440	. . . . . . . 8 |- 0 e. RR
16	15, 2, 1	lelttr 5586	. . . . . . 7 |- ((0 <_ A /\ A < B) -> 0 < B)
17	14, 16	mpan 695	. . . . . 6 |- (A < B -> 0 < B)
18		addgtge0t 5649	. . . . . . . . 9 |- (((B e. RR /\ A e. RR) /\ (0 < B /\ 0 <_ A)) -> 0 < (B + A))
19	1, 2, 18	mpanl12 708	. . . . . . . 8 |- ((0 < B /\ 0 <_ A) -> 0 < (B + A))
20	14, 19	mpan2 696	. . . . . . 7 |- (0 < B -> 0 < (B + A))
21		2pos 5989	. . . . . . . 8 |- 0 < 2
22	3, 4, 21	divgt0i2 5859	. . . . . . 7 |- (0 < (B + A) -> 0 < ((B + A) / 2))
23	20, 22	syl 10	. . . . . 6 |- (0 < B -> 0 < ((B + A) / 2))
24		cosh111lem1.6	. . . . . . . . . . 11 |- B < pi
25		cosh111lem1.5	. . . . . . . . . . 11 |- A < pi
26		pire 8677	. . . . . . . . . . . 12 |- pi e. RR
27	1, 2, 26, 26	lt2add 5596	. . . . . . . . . . 11 |- ((B < pi /\ A < pi) -> (B + A) < (pi + pi))
28	24, 25, 27	mp2an 697	. . . . . . . . . 10 |- (B + A) < (pi + pi)
29	26	recn 5314	. . . . . . . . . . 11 |- pi e. CC
30	29	2times 6003	. . . . . . . . . 10 |- (2 x. pi) = (pi + pi)
31	28, 30	breqtrr 2640	. . . . . . . . 9 |- (B + A) < (2 x. pi)
32	4, 26	remulcl 5335	. . . . . . . . . 10 |- (2 x. pi) e. RR
33	3, 32, 4, 21	ltdiv1i 5823	. . . . . . . . 9 |- ((B + A) < (2 x. pi) <-> ((B + A) / 2) < ((2 x. pi) / 2))
34	31, 33	mpbi 189	. . . . . . . 8 |- ((B + A) / 2) < ((2 x. pi) / 2)
35		2cn 5980	. . . . . . . . 9 |- 2 e. CC
36	29, 35, 5	divcan3 5752	. . . . . . . 8 |- ((2 x. pi) / 2) = pi
37	34, 36	breqtr 2638	. . . . . . 7 |- ((B + A) / 2) < pi
38		elioo2t 6379	. . . . . . . . . 10 |- ((0 e. RR* /\ pi e. RR*) -> (((B + A) / 2) e. (0(,)pi) <-> (((B + A) / 2) e. RR /\ 0 < ((B + A) / 2) /\ ((B + A) / 2) < pi)))
39		rexrt 5499	. . . . . . . . . 10 |- (0 e. RR -> 0 e. RR*)
40		rexrt 5499	. . . . . . . . . 10 |- (pi e. RR -> pi e. RR*)
41	38, 39, 40	syl2an 454	. . . . . . . . 9 |- ((0 e. RR /\ pi e. RR) -> (((B + A) / 2) e. (0(,)pi) <-> (((B + A) / 2) e. RR /\ 0 < ((B + A) / 2) /\ ((B + A) / 2) < pi)))
42	15, 26, 41	mp2an 697	. . . . . . . 8 |- (((B + A) / 2) e. (0(,)pi) <-> (((B + A) / 2) e. RR /\ 0 < ((B + A) / 2) /\ ((B + A) / 2) < pi))
43		sinq12gt0t 8708	. . . . . . . 8 |- (((B + A) / 2) e. (0(,)pi) -> 0 < (sin` ((B + A) / 2)))
44	42, 43	sylbir 201	. . . . . . 7 |- ((((B + A) / 2) e. RR /\ 0 < ((B + A) / 2) /\ ((B + A) / 2) < pi) -> 0 < (sin` ((B + A) / 2)))
45	6, 37, 44	mp3an13 907	. . . . . 6 |- (0 < ((B + A) / 2) -> 0 < (sin` ((B + A) / 2)))
46	17, 23, 45	3syl 20	. . . . 5 |- (A < B -> 0 < (sin` ((B + A) / 2)))
47	2, 1	posdif 5665	. . . . . . 7 |- (A < B <-> 0 < (B - A))
48		gt0divt 5853	. . . . . . . 8 |- (((B - A) e. RR /\ 2 e. RR /\ 0 < 2) -> (0 < (B - A) <-> 0 < ((B - A) / 2)))
49	9, 4, 21, 48	mp3an 916	. . . . . . 7 |- (0 < (B - A) <-> 0 < ((B - A) / 2))
50	47, 49	bitr 173	. . . . . 6 |- (A < B <-> 0 < ((B - A) / 2))
51	29	addid2 5331	. . . . . . . . . . . . 13 |- (0 + pi) = pi
52	15, 2, 26	leadd1 5592	. . . . . . . . . . . . . 14 |- (0 <_ A <-> (0 + pi) <_ (A + pi))
53	14, 52	mpbi 189	. . . . . . . . . . . . 13 |- (0 + pi) <_ (A + pi)
54	51, 53	eqbrtrr 2636	. . . . . . . . . . . 12 |- pi <_ (A + pi)
55	2, 26	readdcl 5334	. . . . . . . . . . . . 13 |- (A + pi) e. RR
56	1, 26, 55	ltletr 5587	. . . . . . . . . . . 12 |- ((B < pi /\ pi <_ (A + pi)) -> B < (A + pi))
57	24, 54, 56	mp2an 697	. . . . . . . . . . 11 |- B < (A + pi)
58	1, 2, 26	ltsubadd2 5637	. . . . . . . . . . 11 |- ((B - A) < pi <-> B < (A + pi))
59	57, 58	mpbir 190	. . . . . . . . . 10 |- (B - A) < pi
60		1lt2 6028	. . . . . . . . . . 11 |- 1 < 2
61		pipos 8678	. . . . . . . . . . . 12 |- 0 < pi
62		ltmulgt12t 5847	. . . . . . . . . . . 12 |- ((pi e. RR /\ 2 e. RR /\ 0 < pi) -> (1 < 2 <-> pi < (2 x. pi)))
63	26, 4, 61, 62	mp3an 916	. . . . . . . . . . 11 |- (1 < 2 <-> pi < (2 x. pi))
64	60, 63	mpbi 189	. . . . . . . . . 10 |- pi < (2 x. pi)
65	9, 26, 32	lttr 5585	. . . . . . . . . 10 |- (((B - A) < pi /\ pi < (2 x. pi)) -> (B - A) < (2 x. pi))
66	59, 64, 65	mp2an 697	. . . . . . . . 9 |- (B - A) < (2 x. pi)
67	9, 32, 4, 21	ltdiv1i 5823	. . . . . . . . 9 |- ((B - A) < (2 x. pi) <-> ((B - A) / 2) < ((2 x. pi) / 2))
68	66, 67	mpbi 189	. . . . . . . 8 |- ((B - A) / 2) < ((2 x. pi) / 2)
69	68, 36	breqtr 2638	. . . . . . 7 |- ((B - A) / 2) < pi
70		elioo2t 6379	. . . . . . . . . 10 |- ((0 e. RR* /\ pi e. RR*) -> (((B - A) / 2) e. (0(,)pi) <-> (((B - A) / 2) e. RR /\ 0 < ((B - A) / 2) /\ ((B - A) / 2) < pi)))
71	70, 39, 40	syl2an 454	. . . . . . . . 9 |- ((0 e. RR /\ pi e. RR) -> (((B - A) / 2) e. (0(,)pi) <-> (((B - A) / 2) e. RR /\ 0 < ((B - A) / 2) /\ ((B - A) / 2) < pi)))
72	15, 26, 71	mp2an 697	. . . . . . . 8 |- (((B - A) / 2) e. (0(,)pi) <-> (((B - A) / 2) e. RR /\ 0 < ((B - A) / 2) /\ ((B - A) / 2) < pi))
73		sinq12gt0t 8708	. . . . . . . 8 |- (((B - A) / 2) e. (0(,)pi) -> 0 < (sin` ((B - A) / 2)))
74	72, 73	sylbir 201	. . . . . . 7 |- ((((B - A) / 2) e. RR /\ 0 < ((B - A) / 2) /\ ((B - A) / 2) < pi) -> 0 < (sin` ((B - A) / 2)))
75	10, 69, 74	mp3an13 907	. . . . . 6 |- (0 < ((B - A) / 2) -> 0 < (sin` ((B - A) / 2)))
76	50, 75	sylbi 199	. . . . 5 |- (A < B -> 0 < (sin` ((B - A) / 2)))
77	13, 46, 76	sylanc 471	. . . 4 |- (A < B -> 0 < ((sin` ((B + A) / 2)) x. (sin` ((B - A) / 2))))
78	8, 12	remulcl 5335	. . . . . 6 |- ((sin` ((B + A) / 2)) x. (sin` ((B - A) / 2))) e. RR
79	4, 78	mulgt0 5606	. . . . 5 |- ((0 < 2 /\ 0 < ((sin` ((B + A) / 2)) x. (sin` ((B - A) / 2)))) -> 0 < (2 x. ((sin` ((B + A) / 2)) x. (sin` ((B - A) / 2)))))
80	21, 79	mpan 695	. . . 4 |- (0 < ((sin` ((B + A) / 2)) x. (sin` ((B - A) / 2))) -> 0 < (2 x. ((sin` ((B + A) / 2)) x. (sin` ((B - A) / 2)))))
81	77, 80	syl 10	. . 3 |- (A < B -> 0 < (2 x. ((sin` ((B + A) / 2)) x. (sin` ((B - A) / 2)))))
82	1	recn 5314	. . . . . . 7 |- B e. CC
83	2	recn 5314	. . . . . . 7 |- A e. CC
84		subcost 7460	. . . . . . 7 |- ((B e. CC /\ A e. CC) -> ((cos` B) - (