tangtx - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tangtx		Structured version Visualization version GIF version

Theorem tangtx 24061

Description: The tangent function is greater than its argument on positive reals in its principal domain. (Contributed by Mario Carneiro, 29-Jul-2014.)

**Assertion**
Ref	Expression
tangtx	⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 < (tan‘𝐴))

**Proof of Theorem tangtx**
Step	Hyp	Ref	Expression
1		elioore 12076	. . . . 5 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 ∈ ℝ)
2	1	recoscld 14713	. . . . 5 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (cos‘𝐴) ∈ ℝ)
3	1, 2	remulcld 9949	. . . 4 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 · (cos‘𝐴)) ∈ ℝ)
4		1re 9918	. . . . . . 7 ⊢ 1 ∈ ℝ
5		rehalfcl 11135	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈ ℝ)
6	1, 5	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 / 2) ∈ ℝ)
7	6	resqcld 12897	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2)↑2) ∈ ℝ)
8		3nn 11063	. . . . . . . 8 ⊢ 3 ∈ ℕ
9		nndivre 10933	. . . . . . . 8 ⊢ ((((𝐴 / 2)↑2) ∈ ℝ ∧ 3 ∈ ℕ) → (((𝐴 / 2)↑2) / 3) ∈ ℝ)
10	7, 8, 9	sylancl 693	. . . . . . 7 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (((𝐴 / 2)↑2) / 3) ∈ ℝ)
11		resubcl 10224	. . . . . . 7 ⊢ ((1 ∈ ℝ ∧ (((𝐴 / 2)↑2) / 3) ∈ ℝ) → (1 − (((𝐴 / 2)↑2) / 3)) ∈ ℝ)
12	4, 10, 11	sylancr 694	. . . . . 6 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (1 − (((𝐴 / 2)↑2) / 3)) ∈ ℝ)
13	1, 12	remulcld 9949	. . . . 5 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) ∈ ℝ)
14		2re 10967	. . . . . . 7 ⊢ 2 ∈ ℝ
15		remulcl 9900	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ (((𝐴 / 2)↑2) / 3) ∈ ℝ) → (2 · (((𝐴 / 2)↑2) / 3)) ∈ ℝ)
16	14, 10, 15	sylancr 694	. . . . . 6 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · (((𝐴 / 2)↑2) / 3)) ∈ ℝ)
17		resubcl 10224	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ (2 · (((𝐴 / 2)↑2) / 3)) ∈ ℝ) → (1 − (2 · (((𝐴 / 2)↑2) / 3))) ∈ ℝ)
18	4, 16, 17	sylancr 694	. . . . 5 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (1 − (2 · (((𝐴 / 2)↑2) / 3))) ∈ ℝ)
19	13, 18	remulcld 9949	. . . 4 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) ∈ ℝ)
20	1	resincld 14712	. . . 4 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (sin‘𝐴) ∈ ℝ)
21	12	resqcld 12897	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (((𝐴 / 2)↑2) / 3))↑2) ∈ ℝ)
22		remulcl 9900	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ ((1 − (((𝐴 / 2)↑2) / 3))↑2) ∈ ℝ) → (2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) ∈ ℝ)
23	14, 21, 22	sylancr 694	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) ∈ ℝ)
24		resubcl 10224	. . . . . . . 8 ⊢ (((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) ∈ ℝ ∧ 1 ∈ ℝ) → ((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) − 1) ∈ ℝ)
25	23, 4, 24	sylancl 693	. . . . . . 7 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) − 1) ∈ ℝ)
26	12, 18	remulcld 9949	. . . . . . 7 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) ∈ ℝ)
27	1	recnd 9947	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 ∈ ℂ)
28		2cn 10968	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
29	28	a1i 11	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 2 ∈ ℂ)
30		2ne0 10990	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
31	30	a1i 11	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 2 ≠ 0)
32	27, 29, 31	divcan2d 10682	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · (𝐴 / 2)) = 𝐴)
33	32	fveq2d 6107	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (cos‘(2 · (𝐴 / 2))) = (cos‘𝐴))
34	6	recnd 9947	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 / 2) ∈ ℂ)
35		cos2t 14747	. . . . . . . . . 10 ⊢ ((𝐴 / 2) ∈ ℂ → (cos‘(2 · (𝐴 / 2))) = ((2 · ((cos‘(𝐴 / 2))↑2)) − 1))
36	34, 35	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (cos‘(2 · (𝐴 / 2))) = ((2 · ((cos‘(𝐴 / 2))↑2)) − 1))
37	33, 36	eqtr3d 2646	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (cos‘𝐴) = ((2 · ((cos‘(𝐴 / 2))↑2)) − 1))
38	6	recoscld 14713	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (cos‘(𝐴 / 2)) ∈ ℝ)
39	38	resqcld 12897	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((cos‘(𝐴 / 2))↑2) ∈ ℝ)
40		remulcl 9900	. . . . . . . . . 10 ⊢ ((2 ∈ ℝ ∧ ((cos‘(𝐴 / 2))↑2) ∈ ℝ) → (2 · ((cos‘(𝐴 / 2))↑2)) ∈ ℝ)
41	14, 39, 40	sylancr 694	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · ((cos‘(𝐴 / 2))↑2)) ∈ ℝ)
42	4	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 1 ∈ ℝ)
43	14	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 2 ∈ ℝ)
44		eliooord 12104	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (0 < 𝐴 ∧ 𝐴 < (π / 2)))
45	44	simpld 474	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 < 𝐴)
46		2pos 10989	. . . . . . . . . . . . . . . 16 ⊢ 0 < 2
47	46	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 < 2)
48	1, 43, 45, 47	divgt0d 10838	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 < (𝐴 / 2))
49		pire 24014	. . . . . . . . . . . . . . . . . . 19 ⊢ π ∈ ℝ
50		rehalfcl 11135	. . . . . . . . . . . . . . . . . . 19 ⊢ (π ∈ ℝ → (π / 2) ∈ ℝ)
51	49, 50	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (π / 2) ∈ ℝ)
52	44	simprd 478	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 < (π / 2))
53		pigt2lt4 24012	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 < π ∧ π < 4)
54	53	simpri 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ π < 4
55		2t2e4 11054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 · 2) = 4
56	54, 55	breqtrri 4610	. . . . . . . . . . . . . . . . . . . 20 ⊢ π < (2 · 2)
57	14, 46	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 ∈ ℝ ∧ 0 < 2)
58		ltdivmul 10777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((π ∈ ℝ ∧ 2 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((π / 2) < 2 ↔ π < (2 · 2)))
59	49, 14, 57, 58	mp3an 1416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((π / 2) < 2 ↔ π < (2 · 2))
60	56, 59	mpbir 220	. . . . . . . . . . . . . . . . . . 19 ⊢ (π / 2) < 2
61	60	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (π / 2) < 2)
62	1, 51, 43, 52, 61	lttrd 10077	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 < 2)
63	28	mulid2i 9922	. . . . . . . . . . . . . . . . 17 ⊢ (1 · 2) = 2
64	62, 63	syl6breqr 4625	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 < (1 · 2))
65		ltdivmul2 10779	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝐴 / 2) < 1 ↔ 𝐴 < (1 · 2)))
66	1, 42, 43, 47, 65	syl112anc 1322	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2) < 1 ↔ 𝐴 < (1 · 2)))
67	64, 66	mpbird 246	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 / 2) < 1)
68	6, 42, 67	ltled 10064	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 / 2) ≤ 1)
69		0xr 9965	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ^*
70		elioc2 12107	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ) → ((𝐴 / 2) ∈ (0(,]1) ↔ ((𝐴 / 2) ∈ ℝ ∧ 0 < (𝐴 / 2) ∧ (𝐴 / 2) ≤ 1)))
71	69, 4, 70	mp2an 704	. . . . . . . . . . . . . 14 ⊢ ((𝐴 / 2) ∈ (0(,]1) ↔ ((𝐴 / 2) ∈ ℝ ∧ 0 < (𝐴 / 2) ∧ (𝐴 / 2) ≤ 1))
72	6, 48, 68, 71	syl3anbrc 1239	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 / 2) ∈ (0(,]1))
73		cos01bnd 14755	. . . . . . . . . . . . 13 ⊢ ((𝐴 / 2) ∈ (0(,]1) → ((1 − (2 · (((𝐴 / 2)↑2) / 3))) < (cos‘(𝐴 / 2)) ∧ (cos‘(𝐴 / 2)) < (1 − (((𝐴 / 2)↑2) / 3))))
74	72, 73	syl 17	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (2 · (((𝐴 / 2)↑2) / 3))) < (cos‘(𝐴 / 2)) ∧ (cos‘(𝐴 / 2)) < (1 − (((𝐴 / 2)↑2) / 3))))
75	74	simprd 478	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (cos‘(𝐴 / 2)) < (1 − (((𝐴 / 2)↑2) / 3)))
76		cos01gt0 14760	. . . . . . . . . . . . . 14 ⊢ ((𝐴 / 2) ∈ (0(,]1) → 0 < (cos‘(𝐴 / 2)))
77	72, 76	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 < (cos‘(𝐴 / 2)))
78		0re 9919	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
79		ltle 10005	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (cos‘(𝐴 / 2)) ∈ ℝ) → (0 < (cos‘(𝐴 / 2)) → 0 ≤ (cos‘(𝐴 / 2))))
80	78, 38, 79	sylancr 694	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (0 < (cos‘(𝐴 / 2)) → 0 ≤ (cos‘(𝐴 / 2))))
81	77, 80	mpd 15	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 ≤ (cos‘(𝐴 / 2)))
82	78	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 ∈ ℝ)
83	82, 38, 12, 77, 75	lttrd 10077	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 < (1 − (((𝐴 / 2)↑2) / 3)))
84	82, 12, 83	ltled 10064	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 ≤ (1 − (((𝐴 / 2)↑2) / 3)))
85	38, 12, 81, 84	lt2sqd 12905	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((cos‘(𝐴 / 2)) < (1 − (((𝐴 / 2)↑2) / 3)) ↔ ((cos‘(𝐴 / 2))↑2) < ((1 − (((𝐴 / 2)↑2) / 3))↑2)))
86	75, 85	mpbid 221	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((cos‘(𝐴 / 2))↑2) < ((1 − (((𝐴 / 2)↑2) / 3))↑2))
87		ltmul2 10753	. . . . . . . . . . 11 ⊢ ((((cos‘(𝐴 / 2))↑2) ∈ ℝ ∧ ((1 − (((𝐴 / 2)↑2) / 3))↑2) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((cos‘(𝐴 / 2))↑2) < ((1 − (((𝐴 / 2)↑2) / 3))↑2) ↔ (2 · ((cos‘(𝐴 / 2))↑2)) < (2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2))))
88	39, 21, 43, 47, 87	syl112anc 1322	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (((cos‘(𝐴 / 2))↑2) < ((1 − (((𝐴 / 2)↑2) / 3))↑2) ↔ (2 · ((cos‘(𝐴 / 2))↑2)) < (2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2))))
89	86, 88	mpbid 221	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · ((cos‘(𝐴 / 2))↑2)) < (2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)))
90	41, 23, 42, 89	ltsub1dd 10518	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((2 · ((cos‘(𝐴 / 2))↑2)) − 1) < ((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) − 1))
91	37, 90	eqbrtrd 4605	. . . . . . 7 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (cos‘𝐴) < ((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) − 1))
92		3re 10971	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
93		remulcl 9900	. . . . . . . . . 10 ⊢ ((3 ∈ ℝ ∧ (((𝐴 / 2)↑2) / 3) ∈ ℝ) → (3 · (((𝐴 / 2)↑2) / 3)) ∈ ℝ)
94	92, 10, 93	sylancr 694	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (3 · (((𝐴 / 2)↑2) / 3)) ∈ ℝ)
95		4re 10974	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
96		remulcl 9900	. . . . . . . . . 10 ⊢ ((4 ∈ ℝ ∧ (((𝐴 / 2)↑2) / 3) ∈ ℝ) → (4 · (((𝐴 / 2)↑2) / 3)) ∈ ℝ)
97	95, 10, 96	sylancr 694	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (4 · (((𝐴 / 2)↑2) / 3)) ∈ ℝ)
98	10	resqcld 12897	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((((𝐴 / 2)↑2) / 3)↑2) ∈ ℝ)
99		remulcl 9900	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ ((((𝐴 / 2)↑2) / 3)↑2) ∈ ℝ) → (2 · ((((𝐴 / 2)↑2) / 3)↑2)) ∈ ℝ)
100	14, 98, 99	sylancr 694	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · ((((𝐴 / 2)↑2) / 3)↑2)) ∈ ℝ)
101		readdcl 9898	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ (2 · ((((𝐴 / 2)↑2) / 3)↑2)) ∈ ℝ) → (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) ∈ ℝ)
102	4, 100, 101	sylancr 694	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) ∈ ℝ)
103		3lt4 11074	. . . . . . . . . 10 ⊢ 3 < 4
104	92	a1i 11	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 3 ∈ ℝ)
105	95	a1i 11	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 4 ∈ ℝ)
106	48	gt0ne0d 10471	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 / 2) ≠ 0)
107	6, 106	sqgt0d 12899	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 < ((𝐴 / 2)↑2))
108		3pos 10991	. . . . . . . . . . . . 13 ⊢ 0 < 3
109	108	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 < 3)
110	7, 104, 107, 109	divgt0d 10838	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 < (((𝐴 / 2)↑2) / 3))
111		ltmul1 10752	. . . . . . . . . . 11 ⊢ ((3 ∈ ℝ ∧ 4 ∈ ℝ ∧ ((((𝐴 / 2)↑2) / 3) ∈ ℝ ∧ 0 < (((𝐴 / 2)↑2) / 3))) → (3 < 4 ↔ (3 · (((𝐴 / 2)↑2) / 3)) < (4 · (((𝐴 / 2)↑2) / 3))))
112	104, 105, 10, 110, 111	syl112anc 1322	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (3 < 4 ↔ (3 · (((𝐴 / 2)↑2) / 3)) < (4 · (((𝐴 / 2)↑2) / 3))))
113	103, 112	mpbii 222	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (3 · (((𝐴 / 2)↑2) / 3)) < (4 · (((𝐴 / 2)↑2) / 3)))
114	94, 97, 102, 113	ltsub2dd 10519	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3))) < ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (3 · (((𝐴 / 2)↑2) / 3))))
115		sq1 12820	. . . . . . . . . . . . . . . 16 ⊢ (1↑2) = 1
116	115	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (1↑2) = 1)
117	10	recnd 9947	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (((𝐴 / 2)↑2) / 3) ∈ ℂ)
118	117	mulid2d 9937	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (1 · (((𝐴 / 2)↑2) / 3)) = (((𝐴 / 2)↑2) / 3))
119	118	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · (1 · (((𝐴 / 2)↑2) / 3))) = (2 · (((𝐴 / 2)↑2) / 3)))
120	116, 119	oveq12d 6567	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1↑2) − (2 · (1 · (((𝐴 / 2)↑2) / 3)))) = (1 − (2 · (((𝐴 / 2)↑2) / 3))))
121	120	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (((1↑2) − (2 · (1 · (((𝐴 / 2)↑2) / 3)))) + ((((𝐴 / 2)↑2) / 3)↑2)) = ((1 − (2 · (((𝐴 / 2)↑2) / 3))) + ((((𝐴 / 2)↑2) / 3)↑2)))
122		ax-1cn 9873	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
123		binom2sub 12843	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℂ ∧ (((𝐴 / 2)↑2) / 3) ∈ ℂ) → ((1 − (((𝐴 / 2)↑2) / 3))↑2) = (((1↑2) − (2 · (1 · (((𝐴 / 2)↑2) / 3)))) + ((((𝐴 / 2)↑2) / 3)↑2)))
124	122, 117, 123	sylancr 694	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (((𝐴 / 2)↑2) / 3))↑2) = (((1↑2) − (2 · (1 · (((𝐴 / 2)↑2) / 3)))) + ((((𝐴 / 2)↑2) / 3)↑2)))
125	42	recnd 9947	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 1 ∈ ℂ)
126	98	recnd 9947	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((((𝐴 / 2)↑2) / 3)↑2) ∈ ℂ)
127	16	recnd 9947	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · (((𝐴 / 2)↑2) / 3)) ∈ ℂ)
128	125, 126, 127	addsubd 10292	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 + ((((𝐴 / 2)↑2) / 3)↑2)) − (2 · (((𝐴 / 2)↑2) / 3))) = ((1 − (2 · (((𝐴 / 2)↑2) / 3))) + ((((𝐴 / 2)↑2) / 3)↑2)))
129	121, 124, 128	3eqtr4d 2654	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (((𝐴 / 2)↑2) / 3))↑2) = ((1 + ((((𝐴 / 2)↑2) / 3)↑2)) − (2 · (((𝐴 / 2)↑2) / 3))))
130	129	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) = (2 · ((1 + ((((𝐴 / 2)↑2) / 3)↑2)) − (2 · (((𝐴 / 2)↑2) / 3)))))
131		addcl 9897	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ ((((𝐴 / 2)↑2) / 3)↑2) ∈ ℂ) → (1 + ((((𝐴 / 2)↑2) / 3)↑2)) ∈ ℂ)
132	122, 126, 131	sylancr 694	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (1 + ((((𝐴 / 2)↑2) / 3)↑2)) ∈ ℂ)
133	29, 132, 127	subdid 10365	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · ((1 + ((((𝐴 / 2)↑2) / 3)↑2)) − (2 · (((𝐴 / 2)↑2) / 3)))) = ((2 · (1 + ((((𝐴 / 2)↑2) / 3)↑2))) − (2 · (2 · (((𝐴 / 2)↑2) / 3)))))
134	29, 125, 126	adddid 9943	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · (1 + ((((𝐴 / 2)↑2) / 3)↑2))) = ((2 · 1) + (2 · ((((𝐴 / 2)↑2) / 3)↑2))))
135	122	2timesi 11024	. . . . . . . . . . . . . . . 16 ⊢ (2 · 1) = (1 + 1)
136	135	oveq1i 6559	. . . . . . . . . . . . . . 15 ⊢ ((2 · 1) + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) = ((1 + 1) + (2 · ((((𝐴 / 2)↑2) / 3)↑2)))
137	100	recnd 9947	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · ((((𝐴 / 2)↑2) / 3)↑2)) ∈ ℂ)
138	125, 125, 137	addassd 9941	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 + 1) + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) = (1 + (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2)))))
139	136, 138	syl5eq 2656	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((2 · 1) + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) = (1 + (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2)))))
140	134, 139	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · (1 + ((((𝐴 / 2)↑2) / 3)↑2))) = (1 + (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2)))))
141	55	oveq1i 6559	. . . . . . . . . . . . . 14 ⊢ ((2 · 2) · (((𝐴 / 2)↑2) / 3)) = (4 · (((𝐴 / 2)↑2) / 3))
142	29, 29, 117	mulassd 9942	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((2 · 2) · (((𝐴 / 2)↑2) / 3)) = (2 · (2 · (((𝐴 / 2)↑2) / 3))))
143	141, 142	syl5reqr 2659	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · (2 · (((𝐴 / 2)↑2) / 3))) = (4 · (((𝐴 / 2)↑2) / 3)))
144	140, 143	oveq12d 6567	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((2 · (1 + ((((𝐴 / 2)↑2) / 3)↑2))) − (2 · (2 · (((𝐴 / 2)↑2) / 3)))) = ((1 + (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2)))) − (4 · (((𝐴 / 2)↑2) / 3))))
145		addcl 9897	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℂ ∧ (2 · ((((𝐴 / 2)↑2) / 3)↑2)) ∈ ℂ) → (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) ∈ ℂ)
146	122, 137, 145	sylancr 694	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) ∈ ℂ)
147	97	recnd 9947	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (4 · (((𝐴 / 2)↑2) / 3)) ∈ ℂ)
148	125, 146, 147	addsubassd 10291	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 + (1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2)))) − (4 · (((𝐴 / 2)↑2) / 3))) = (1 + ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3)))))
149	144, 148	eqtrd 2644	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((2 · (1 + ((((𝐴 / 2)↑2) / 3)↑2))) − (2 · (2 · (((𝐴 / 2)↑2) / 3)))) = (1 + ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3)))))
150	130, 133, 149	3eqtrd 2648	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) = (1 + ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3)))))
151	150	oveq1d 6564	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) − 1) = ((1 + ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3)))) − 1))
152	146, 147	subcld 10271	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3))) ∈ ℂ)
153		pncan2 10167	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3))) ∈ ℂ) → ((1 + ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3)))) − 1) = ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3))))
154	122, 152, 153	sylancr 694	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 + ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3)))) − 1) = ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3))))
155	151, 154	eqtrd 2644	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) − 1) = ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (4 · (((𝐴 / 2)↑2) / 3))))
156		subcl 10159	. . . . . . . . . . 11 ⊢ ((1 ∈ ℂ ∧ (((𝐴 / 2)↑2) / 3) ∈ ℂ) → (1 − (((𝐴 / 2)↑2) / 3)) ∈ ℂ)
157	122, 117, 156	sylancr 694	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (1 − (((𝐴 / 2)↑2) / 3)) ∈ ℂ)
158	157, 125, 127	subdid 10365	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) = (((1 − (((𝐴 / 2)↑2) / 3)) · 1) − ((1 − (((𝐴 / 2)↑2) / 3)) · (2 · (((𝐴 / 2)↑2) / 3)))))
159	157	mulid1d 9936	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (((𝐴 / 2)↑2) / 3)) · 1) = (1 − (((𝐴 / 2)↑2) / 3)))
160	125, 117, 127	subdird 10366	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (((𝐴 / 2)↑2) / 3)) · (2 · (((𝐴 / 2)↑2) / 3))) = ((1 · (2 · (((𝐴 / 2)↑2) / 3))) − ((((𝐴 / 2)↑2) / 3) · (2 · (((𝐴 / 2)↑2) / 3)))))
161	127	mulid2d 9937	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (1 · (2 · (((𝐴 / 2)↑2) / 3))) = (2 · (((𝐴 / 2)↑2) / 3)))
162	117, 29, 117	mul12d 10124	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((((𝐴 / 2)↑2) / 3) · (2 · (((𝐴 / 2)↑2) / 3))) = (2 · ((((𝐴 / 2)↑2) / 3) · (((𝐴 / 2)↑2) / 3))))
163	117	sqvald 12867	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((((𝐴 / 2)↑2) / 3)↑2) = ((((𝐴 / 2)↑2) / 3) · (((𝐴 / 2)↑2) / 3)))
164	163	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · ((((𝐴 / 2)↑2) / 3)↑2)) = (2 · ((((𝐴 / 2)↑2) / 3) · (((𝐴 / 2)↑2) / 3))))
165	162, 164	eqtr4d 2647	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((((𝐴 / 2)↑2) / 3) · (2 · (((𝐴 / 2)↑2) / 3))) = (2 · ((((𝐴 / 2)↑2) / 3)↑2)))
166	161, 165	oveq12d 6567	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 · (2 · (((𝐴 / 2)↑2) / 3))) − ((((𝐴 / 2)↑2) / 3) · (2 · (((𝐴 / 2)↑2) / 3)))) = ((2 · (((𝐴 / 2)↑2) / 3)) − (2 · ((((𝐴 / 2)↑2) / 3)↑2))))
167	160, 166	eqtrd 2644	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (((𝐴 / 2)↑2) / 3)) · (2 · (((𝐴 / 2)↑2) / 3))) = ((2 · (((𝐴 / 2)↑2) / 3)) − (2 · ((((𝐴 / 2)↑2) / 3)↑2))))
168	159, 167	oveq12d 6567	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (((1 − (((𝐴 / 2)↑2) / 3)) · 1) − ((1 − (((𝐴 / 2)↑2) / 3)) · (2 · (((𝐴 / 2)↑2) / 3)))) = ((1 − (((𝐴 / 2)↑2) / 3)) − ((2 · (((𝐴 / 2)↑2) / 3)) − (2 · ((((𝐴 / 2)↑2) / 3)↑2)))))
169	125, 117, 127, 137	subadd4d 10319	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (((𝐴 / 2)↑2) / 3)) − ((2 · (((𝐴 / 2)↑2) / 3)) − (2 · ((((𝐴 / 2)↑2) / 3)↑2)))) = ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − ((((𝐴 / 2)↑2) / 3) + (2 · (((𝐴 / 2)↑2) / 3)))))
170		df-3 10957	. . . . . . . . . . . . . 14 ⊢ 3 = (2 + 1)
171	28, 122	addcomi 10106	. . . . . . . . . . . . . 14 ⊢ (2 + 1) = (1 + 2)
172	170, 171	eqtri 2632	. . . . . . . . . . . . 13 ⊢ 3 = (1 + 2)
173	172	oveq1i 6559	. . . . . . . . . . . 12 ⊢ (3 · (((𝐴 / 2)↑2) / 3)) = ((1 + 2) · (((𝐴 / 2)↑2) / 3))
174	125, 29, 117	adddird 9944	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 + 2) · (((𝐴 / 2)↑2) / 3)) = ((1 · (((𝐴 / 2)↑2) / 3)) + (2 · (((𝐴 / 2)↑2) / 3))))
175	118	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 · (((𝐴 / 2)↑2) / 3)) + (2 · (((𝐴 / 2)↑2) / 3))) = ((((𝐴 / 2)↑2) / 3) + (2 · (((𝐴 / 2)↑2) / 3))))
176	174, 175	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 + 2) · (((𝐴 / 2)↑2) / 3)) = ((((𝐴 / 2)↑2) / 3) + (2 · (((𝐴 / 2)↑2) / 3))))
177	173, 176	syl5eq 2656	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (3 · (((𝐴 / 2)↑2) / 3)) = ((((𝐴 / 2)↑2) / 3) + (2 · (((𝐴 / 2)↑2) / 3))))
178	177	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (3 · (((𝐴 / 2)↑2) / 3))) = ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − ((((𝐴 / 2)↑2) / 3) + (2 · (((𝐴 / 2)↑2) / 3)))))
179	169, 178	eqtr4d 2647	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (((𝐴 / 2)↑2) / 3)) − ((2 · (((𝐴 / 2)↑2) / 3)) − (2 · ((((𝐴 / 2)↑2) / 3)↑2)))) = ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (3 · (((𝐴 / 2)↑2) / 3))))
180	158, 168, 179	3eqtrd 2648	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) = ((1 + (2 · ((((𝐴 / 2)↑2) / 3)↑2))) − (3 · (((𝐴 / 2)↑2) / 3))))
181	114, 155, 180	3brtr4d 4615	. . . . . . 7 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((2 · ((1 − (((𝐴 / 2)↑2) / 3))↑2)) − 1) < ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))))
182	2, 25, 26, 91, 181	lttrd 10077	. . . . . 6 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (cos‘𝐴) < ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))))
183		ltmul2 10753	. . . . . . 7 ⊢ (((cos‘𝐴) ∈ ℝ ∧ ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → ((cos‘𝐴) < ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) ↔ (𝐴 · (cos‘𝐴)) < (𝐴 · ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))))))
184	2, 26, 1, 45, 183	syl112anc 1322	. . . . . 6 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((cos‘𝐴) < ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) ↔ (𝐴 · (cos‘𝐴)) < (𝐴 · ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))))))
185	182, 184	mpbid 221	. . . . 5 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 · (cos‘𝐴)) < (𝐴 · ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3))))))
186	18	recnd 9947	. . . . . 6 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (1 − (2 · (((𝐴 / 2)↑2) / 3))) ∈ ℂ)
187	27, 157, 186	mulassd 9942	. . . . 5 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) = (𝐴 · ((1 − (((𝐴 / 2)↑2) / 3)) · (1 − (2 · (((𝐴 / 2)↑2) / 3))))))
188	185, 187	breqtrrd 4611	. . . 4 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 · (cos‘𝐴)) < ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))))
189	13, 38	remulcld 9949	. . . . 5 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (cos‘(𝐴 / 2))) ∈ ℝ)
190	74	simpld 474	. . . . . 6 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (1 − (2 · (((𝐴 / 2)↑2) / 3))) < (cos‘(𝐴 / 2)))
191	1, 12, 45, 83	mulgt0d 10071	. . . . . . 7 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 < (𝐴 · (1 − (((𝐴 / 2)↑2) / 3))))
192		ltmul2 10753	. . . . . . 7 ⊢ (((1 − (2 · (((𝐴 / 2)↑2) / 3))) ∈ ℝ ∧ (cos‘(𝐴 / 2)) ∈ ℝ ∧ ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) ∈ ℝ ∧ 0 < (𝐴 · (1 − (((𝐴 / 2)↑2) / 3))))) → ((1 − (2 · (((𝐴 / 2)↑2) / 3))) < (cos‘(𝐴 / 2)) ↔ ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) < ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (cos‘(𝐴 / 2)))))
193	18, 38, 13, 191, 192	syl112anc 1322	. . . . . 6 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((1 − (2 · (((𝐴 / 2)↑2) / 3))) < (cos‘(𝐴 / 2)) ↔ ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) < ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (cos‘(𝐴 / 2)))))
194	190, 193	mpbid 221	. . . . 5 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) < ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (cos‘(𝐴 / 2))))
195	29, 34, 157	mulassd 9942	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((2 · (𝐴 / 2)) · (1 − (((𝐴 / 2)↑2) / 3))) = (2 · ((𝐴 / 2) · (1 − (((𝐴 / 2)↑2) / 3)))))
196	32	oveq1d 6564	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((2 · (𝐴 / 2)) · (1 − (((𝐴 / 2)↑2) / 3))) = (𝐴 · (1 − (((𝐴 / 2)↑2) / 3))))
197	34, 125, 117	subdid 10365	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2) · (1 − (((𝐴 / 2)↑2) / 3))) = (((𝐴 / 2) · 1) − ((𝐴 / 2) · (((𝐴 / 2)↑2) / 3))))
198	34	mulid1d 9936	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2) · 1) = (𝐴 / 2))
199	170	oveq2i 6560	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 / 2)↑3) = ((𝐴 / 2)↑(2 + 1))
200		2nn0 11186	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ₀
201		expp1 12729	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 / 2) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((𝐴 / 2)↑(2 + 1)) = (((𝐴 / 2)↑2) · (𝐴 / 2)))
202	34, 200, 201	sylancl 693	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2)↑(2 + 1)) = (((𝐴 / 2)↑2) · (𝐴 / 2)))
203	199, 202	syl5eq 2656	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2)↑3) = (((𝐴 / 2)↑2) · (𝐴 / 2)))
204	7	recnd 9947	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2)↑2) ∈ ℂ)
205	204, 34	mulcomd 9940	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (((𝐴 / 2)↑2) · (𝐴 / 2)) = ((𝐴 / 2) · ((𝐴 / 2)↑2)))
206	203, 205	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2)↑3) = ((𝐴 / 2) · ((𝐴 / 2)↑2)))
207	206	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (((𝐴 / 2)↑3) / 3) = (((𝐴 / 2) · ((𝐴 / 2)↑2)) / 3))
208		3cn 10972	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℂ
209	208	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 3 ∈ ℂ)
210		3ne0 10992	. . . . . . . . . . . . . . 15 ⊢ 3 ≠ 0
211	210	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 3 ≠ 0)
212	34, 204, 209, 211	divassd 10715	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (((𝐴 / 2) · ((𝐴 / 2)↑2)) / 3) = ((𝐴 / 2) · (((𝐴 / 2)↑2) / 3)))
213	207, 212	eqtr2d 2645	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2) · (((𝐴 / 2)↑2) / 3)) = (((𝐴 / 2)↑3) / 3))
214	198, 213	oveq12d 6567	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (((𝐴 / 2) · 1) − ((𝐴 / 2) · (((𝐴 / 2)↑2) / 3))) = ((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)))
215	197, 214	eqtrd 2644	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2) · (1 − (((𝐴 / 2)↑2) / 3))) = ((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)))
216	215	oveq2d 6565	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · ((𝐴 / 2) · (1 − (((𝐴 / 2)↑2) / 3)))) = (2 · ((𝐴 / 2) − (((𝐴 / 2)↑3) / 3))))
217	195, 196, 216	3eqtr3d 2652	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) = (2 · ((𝐴 / 2) − (((𝐴 / 2)↑3) / 3))))
218		sin01bnd 14754	. . . . . . . . . . 11 ⊢ ((𝐴 / 2) ∈ (0(,]1) → (((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) < (sin‘(𝐴 / 2)) ∧ (sin‘(𝐴 / 2)) < (𝐴 / 2)))
219	72, 218	syl 17	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) < (sin‘(𝐴 / 2)) ∧ (sin‘(𝐴 / 2)) < (𝐴 / 2)))
220	219	simpld 474	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) < (sin‘(𝐴 / 2)))
221		3nn0 11187	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℕ₀
222		reexpcl 12739	. . . . . . . . . . . . 13 ⊢ (((𝐴 / 2) ∈ ℝ ∧ 3 ∈ ℕ₀) → ((𝐴 / 2)↑3) ∈ ℝ)
223	6, 221, 222	sylancl 693	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2)↑3) ∈ ℝ)
224		nndivre 10933	. . . . . . . . . . . 12 ⊢ ((((𝐴 / 2)↑3) ∈ ℝ ∧ 3 ∈ ℕ) → (((𝐴 / 2)↑3) / 3) ∈ ℝ)
225	223, 8, 224	sylancl 693	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (((𝐴 / 2)↑3) / 3) ∈ ℝ)
226	6, 225	resubcld 10337	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) ∈ ℝ)
227	6	resincld 14712	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (sin‘(𝐴 / 2)) ∈ ℝ)
228		ltmul2 10753	. . . . . . . . . 10 ⊢ ((((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) ∈ ℝ ∧ (sin‘(𝐴 / 2)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) < (sin‘(𝐴 / 2)) ↔ (2 · ((𝐴 / 2) − (((𝐴 / 2)↑3) / 3))) < (2 · (sin‘(𝐴 / 2)))))
229	226, 227, 43, 47, 228	syl112anc 1322	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (((𝐴 / 2) − (((𝐴 / 2)↑3) / 3)) < (sin‘(𝐴 / 2)) ↔ (2 · ((𝐴 / 2) − (((𝐴 / 2)↑3) / 3))) < (2 · (sin‘(𝐴 / 2)))))
230	220, 229	mpbid 221	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · ((𝐴 / 2) − (((𝐴 / 2)↑3) / 3))) < (2 · (sin‘(𝐴 / 2))))
231	217, 230	eqbrtrd 4605	. . . . . . 7 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) < (2 · (sin‘(𝐴 / 2))))
232		remulcl 9900	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ (sin‘(𝐴 / 2)) ∈ ℝ) → (2 · (sin‘(𝐴 / 2))) ∈ ℝ)
233	14, 227, 232	sylancr 694	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (2 · (sin‘(𝐴 / 2))) ∈ ℝ)
234		ltmul1 10752	. . . . . . . 8 ⊢ (((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) ∈ ℝ ∧ (2 · (sin‘(𝐴 / 2))) ∈ ℝ ∧ ((cos‘(𝐴 / 2)) ∈ ℝ ∧ 0 < (cos‘(𝐴 / 2)))) → ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) < (2 · (sin‘(𝐴 / 2))) ↔ ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (cos‘(𝐴 / 2))) < ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2)))))
235	13, 233, 38, 77, 234	syl112anc 1322	. . . . . . 7 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) < (2 · (sin‘(𝐴 / 2))) ↔ ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (cos‘(𝐴 / 2))) < ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2)))))
236	231, 235	mpbid 221	. . . . . 6 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (cos‘(𝐴 / 2))) < ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2))))
237	227	recnd 9947	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (sin‘(𝐴 / 2)) ∈ ℂ)
238	38	recnd 9947	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (cos‘(𝐴 / 2)) ∈ ℂ)
239	29, 237, 238	mulassd 9942	. . . . . . 7 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
240		sin2t 14746	. . . . . . . 8 ⊢ ((𝐴 / 2) ∈ ℂ → (sin‘(2 · (𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
241	34, 240	syl 17	. . . . . . 7 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (sin‘(2 · (𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
242	32	fveq2d 6107	. . . . . . 7 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (sin‘(2 · (𝐴 / 2))) = (sin‘𝐴))
243	239, 241, 242	3eqtr2rd 2651	. . . . . 6 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (sin‘𝐴) = ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2))))
244	236, 243	breqtrrd 4611	. . . . 5 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (cos‘(𝐴 / 2))) < (sin‘𝐴))
245	19, 189, 20, 194, 244	lttrd 10077	. . . 4 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 · (1 − (((𝐴 / 2)↑2) / 3))) · (1 − (2 · (((𝐴 / 2)↑2) / 3)))) < (sin‘𝐴))
246	3, 19, 20, 188, 245	lttrd 10077	. . 3 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (𝐴 · (cos‘𝐴)) < (sin‘𝐴))
247		sincosq1sgn 24054	. . . . 5 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
248	247	simprd 478	. . . 4 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 0 < (cos‘𝐴))
249		ltmuldiv 10775	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ (sin‘𝐴) ∈ ℝ ∧ ((cos‘𝐴) ∈ ℝ ∧ 0 < (cos‘𝐴))) → ((𝐴 · (cos‘𝐴)) < (sin‘𝐴) ↔ 𝐴 < ((sin‘𝐴) / (cos‘𝐴))))
250	1, 20, 2, 248, 249	syl112anc 1322	. . 3 ⊢ (𝐴 ∈ (0(,)(π / 2)) → ((𝐴 · (cos‘𝐴)) < (sin‘𝐴) ↔ 𝐴 < ((sin‘𝐴) / (cos‘𝐴))))
251	246, 250	mpbid 221	. 2 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 < ((sin‘𝐴) / (cos‘𝐴)))
252	248	gt0ne0d 10471	. . 3 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (cos‘𝐴) ≠ 0)
253		tanval 14697	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
254	27, 252, 253	syl2anc 691	. 2 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
255	251, 254	breqtrrd 4611	1 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 < (tan‘𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 class class class wbr 4583 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 ℝ^*cxr 9952 < clt 9953 ≤ cle 9954 − cmin 10145 / cdiv 10563 ℕcn 10897 2c2 10947 3c3 10948 4c4 10949 ℕ₀cn0 11169 (,)cioo 12046 (,]cioc 12047 ↑cexp 12722 sincsin 14633 cosccos 14634 tanctan 14635 πcpi 14636

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894 ax-mulf 9895

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-iin 4458 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-supp 7183 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-ixp 7795 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fsupp 8159 df-fi 8200 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-z 11255 df-dec 11370 df-uz 11564 df-q 11665 df-rp 11709 df-xneg 11822 df-xadd 11823 df-xmul 11824 df-ioo 12050 df-ioc 12051 df-ico 12052 df-icc 12053 df-fz 12198 df-fzo 12335 df-fl 12455 df-seq 12664 df-exp 12723 df-fac 12923 df-bc 12952 df-hash 12980 df-shft 13655 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-limsup 14050 df-clim 14067 df-rlim 14068 df-sum 14265 df-ef 14637 df-sin 14639 df-cos 14640 df-tan 14641 df-pi 14642 df-struct 15697 df-ndx 15698 df-slot 15699 df-base 15700 df-sets 15701 df-ress 15702 df-plusg 15781 df-mulr 15782 df-starv 15783 df-sca 15784 df-vsca 15785 df-ip 15786 df-tset 15787 df-ple 15788 df-ds 15791 df-unif 15792 df-hom 15793 df-cco 15794 df-rest 15906 df-topn 15907 df-0g 15925 df-gsum 15926 df-topgen 15927 df-pt 15928 df-prds 15931 df-xrs 15985 df-qtop 15990 df-imas 15991 df-xps 15993 df-mre 16069 df-mrc 16070 df-acs 16072 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-submnd 17159 df-mulg 17364 df-cntz 17573 df-cmn 18018 df-psmet 19559 df-xmet 19560 df-met 19561 df-bl 19562 df-mopn 19563 df-fbas 19564 df-fg 19565 df-cnfld 19568 df-top 20521 df-bases 20522 df-topon 20523 df-topsp 20524 df-cld 20633 df-ntr 20634 df-cls 20635 df-nei 20712 df-lp 20750 df-perf 20751 df-cn 20841 df-cnp 20842 df-haus 20929 df-tx 21175 df-hmeo 21368 df-fil 21460 df-fm 21552 df-flim 21553 df-flf 21554 df-xms 21935 df-ms 21936 df-tms 21937 df-cncf 22489 df-limc 23436 df-dv 23437

This theorem is referenced by: tanabsge 24062 basellem8 24614

W3C validator