Theorem tan2h 38072

Description: Half-angle rule for tangent. (Contributed by Brendan Leahy, 4-Aug-2018.)

Assertion

Ref	Expression
tan2h	⊢ (𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / (1 + (cos‘𝐴)))))

Proof of Theorem tan2h

Step	Hyp	Ref	Expression
1		0re 11177	. . . . . . . 8 ⊢ 0 ∈ ℝ
2		pire 26507	. . . . . . . . 9 ⊢ π ∈ ℝ
3	2	rexri 11234	. . . . . . . 8 ⊢ π ∈ ℝ*
4		icossre 13426	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ π ∈ ℝ*) → (0[,)π) ⊆ ℝ)
5	1, 3, 4	mp2an 702	. . . . . . 7 ⊢ (0[,)π) ⊆ ℝ
6	5	sseli 3930	. . . . . 6 ⊢ (𝐴 ∈ (0[,)π) → 𝐴 ∈ ℝ)
7	6	recnd 11204	. . . . 5 ⊢ (𝐴 ∈ (0[,)π) → 𝐴 ∈ ℂ)
8	7	halfcld 12460	. . . 4 ⊢ (𝐴 ∈ (0[,)π) → (𝐴 / 2) ∈ ℂ)
9	6	rehalfcld 12462	. . . . . . 7 ⊢ (𝐴 ∈ (0[,)π) → (𝐴 / 2) ∈ ℝ)
10	9	rered 15242	. . . . . 6 ⊢ (𝐴 ∈ (0[,)π) → (ℜ‘(𝐴 / 2)) = (𝐴 / 2))
11		elico2 13408	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ π ∈ ℝ*) → (𝐴 ∈ (0[,)π) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < π)))
12	1, 3, 11	mp2an 702	. . . . . . 7 ⊢ (𝐴 ∈ (0[,)π) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < π))
13		pipos 26511	. . . . . . . . . . . . 13 ⊢ 0 < π
14		lt0neg2 11688	. . . . . . . . . . . . . 14 ⊢ (π ∈ ℝ → (0 < π ↔ -π < 0))
15	2, 14	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (0 < π ↔ -π < 0)
16	13, 15	mpbi 232	. . . . . . . . . . . 12 ⊢ -π < 0
17	2	renegcli 11486	. . . . . . . . . . . . 13 ⊢ -π ∈ ℝ
18		ltletr 11269	. . . . . . . . . . . . 13 ⊢ ((-π ∈ ℝ ∧ 0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((-π < 0 ∧ 0 ≤ 𝐴) → -π < 𝐴))
19	17, 1, 18	mp3an12 1471	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → ((-π < 0 ∧ 0 ≤ 𝐴) → -π < 𝐴))
20	16, 19	mpani 706	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 → -π < 𝐴))
21		2re 12286	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ
22		2pos 12316	. . . . . . . . . . . . . 14 ⊢ 0 < 2
23	21, 22	pm3.2i 474	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℝ ∧ 0 < 2)
24		ltdiv1 12050	. . . . . . . . . . . . 13 ⊢ ((-π ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (-π < 𝐴 ↔ (-π / 2) < (𝐴 / 2)))
25	17, 23, 24	mp3an13 1472	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → (-π < 𝐴 ↔ (-π / 2) < (𝐴 / 2)))
26		picn 26509	. . . . . . . . . . . . . 14 ⊢ π ∈ ℂ
27		2cn 12287	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
28		2ne0 12318	. . . . . . . . . . . . . 14 ⊢ 2 ≠ 0
29		divneg 11876	. . . . . . . . . . . . . 14 ⊢ ((π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) = (-π / 2))
30	26, 27, 28, 29	mp3an 1481	. . . . . . . . . . . . 13 ⊢ -(π / 2) = (-π / 2)
31	30	breq1i 5104	. . . . . . . . . . . 12 ⊢ (-(π / 2) < (𝐴 / 2) ↔ (-π / 2) < (𝐴 / 2))
32	25, 31	bitr4di 291	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → (-π < 𝐴 ↔ -(π / 2) < (𝐴 / 2)))
33	20, 32	sylibd 241	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 → -(π / 2) < (𝐴 / 2)))
34		ltdiv1 12050	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ π ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐴 < π ↔ (𝐴 / 2) < (π / 2)))
35	2, 23, 34	mp3an23 1473	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → (𝐴 < π ↔ (𝐴 / 2) < (π / 2)))
36	35	biimpd 231	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (𝐴 < π → (𝐴 / 2) < (π / 2)))
37	33, 36	anim12d 618	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → ((0 ≤ 𝐴 ∧ 𝐴 < π) → (-(π / 2) < (𝐴 / 2) ∧ (𝐴 / 2) < (π / 2))))
38		rehalfcl 12442	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈ ℝ)
39	38	rexrd 11226	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈ ℝ*)
40		halfpire 26517	. . . . . . . . . . . . 13 ⊢ (π / 2) ∈ ℝ
41	40	renegcli 11486	. . . . . . . . . . . 12 ⊢ -(π / 2) ∈ ℝ
42	41	rexri 11234	. . . . . . . . . . 11 ⊢ -(π / 2) ∈ ℝ*
43	40	rexri 11234	. . . . . . . . . . 11 ⊢ (π / 2) ∈ ℝ*
44		elioo5 13401	. . . . . . . . . . 11 ⊢ ((-(π / 2) ∈ ℝ* ∧ (π / 2) ∈ ℝ* ∧ (𝐴 / 2) ∈ ℝ*) → ((𝐴 / 2) ∈ (-(π / 2)(,)(π / 2)) ↔ (-(π / 2) < (𝐴 / 2) ∧ (𝐴 / 2) < (π / 2))))
45	42, 43, 44	mp3an12 1471	. . . . . . . . . 10 ⊢ ((𝐴 / 2) ∈ ℝ* → ((𝐴 / 2) ∈ (-(π / 2)(,)(π / 2)) ↔ (-(π / 2) < (𝐴 / 2) ∧ (𝐴 / 2) < (π / 2))))
46	39, 45	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → ((𝐴 / 2) ∈ (-(π / 2)(,)(π / 2)) ↔ (-(π / 2) < (𝐴 / 2) ∧ (𝐴 / 2) < (π / 2))))
47	37, 46	sylibrd 261	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → ((0 ≤ 𝐴 ∧ 𝐴 < π) → (𝐴 / 2) ∈ (-(π / 2)(,)(π / 2))))
48	47	3impib 1128	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < π) → (𝐴 / 2) ∈ (-(π / 2)(,)(π / 2)))
49	12, 48	sylbi 219	. . . . . 6 ⊢ (𝐴 ∈ (0[,)π) → (𝐴 / 2) ∈ (-(π / 2)(,)(π / 2)))
50	10, 49	eqeltrd 2861	. . . . 5 ⊢ (𝐴 ∈ (0[,)π) → (ℜ‘(𝐴 / 2)) ∈ (-(π / 2)(,)(π / 2)))
51		cosne0 26582	. . . . 5 ⊢ (((𝐴 / 2) ∈ ℂ ∧ (ℜ‘(𝐴 / 2)) ∈ (-(π / 2)(,)(π / 2))) → (cos‘(𝐴 / 2)) ≠ 0)
52	8, 50, 51	syl2anc 593	. . . 4 ⊢ (𝐴 ∈ (0[,)π) → (cos‘(𝐴 / 2)) ≠ 0)
53		tanval 16151	. . . 4 ⊢ (((𝐴 / 2) ∈ ℂ ∧ (cos‘(𝐴 / 2)) ≠ 0) → (tan‘(𝐴 / 2)) = ((sin‘(𝐴 / 2)) / (cos‘(𝐴 / 2))))
54	8, 52, 53	syl2anc 593	. . 3 ⊢ (𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = ((sin‘(𝐴 / 2)) / (cos‘(𝐴 / 2))))
55		0xr 11223	. . . . . . 7 ⊢ 0 ∈ ℝ*
56		elico1 13386	. . . . . . 7 ⊢ ((0 ∈ ℝ* ∧ π ∈ ℝ*) → (𝐴 ∈ (0[,)π) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 < π)))
57	55, 3, 56	mp2an 702	. . . . . 6 ⊢ (𝐴 ∈ (0[,)π) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 < π))
58	21, 2	remulcli 11192	. . . . . . . . . . 11 ⊢ (2 · π) ∈ ℝ
59	58	rexri 11234	. . . . . . . . . 10 ⊢ (2 · π) ∈ ℝ*
60		1lt2 12384	. . . . . . . . . . . . 13 ⊢ 1 < 2
61		ltmulgt12 12046	. . . . . . . . . . . . . 14 ⊢ ((π ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < π) → (1 < 2 ↔ π < (2 · π)))
62	2, 21, 13, 61	mp3an 1481	. . . . . . . . . . . . 13 ⊢ (1 < 2 ↔ π < (2 · π))
63	60, 62	mpbi 232	. . . . . . . . . . . 12 ⊢ π < (2 · π)
64		xrlttr 13136	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ* ∧ π ∈ ℝ* ∧ (2 · π) ∈ ℝ*) → ((𝐴 < π ∧ π < (2 · π)) → 𝐴 < (2 · π)))
65	3, 64	mp3an2 1469	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ* ∧ (2 · π) ∈ ℝ*) → ((𝐴 < π ∧ π < (2 · π)) → 𝐴 < (2 · π)))
66	63, 65	mpan2i 707	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ* ∧ (2 · π) ∈ ℝ*) → (𝐴 < π → 𝐴 < (2 · π)))
67		xrltle 13145	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ* ∧ (2 · π) ∈ ℝ*) → (𝐴 < (2 · π) → 𝐴 ≤ (2 · π)))
68	66, 67	syld 47	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ* ∧ (2 · π) ∈ ℝ*) → (𝐴 < π → 𝐴 ≤ (2 · π)))
69	59, 68	mpan2 701	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ* → (𝐴 < π → 𝐴 ≤ (2 · π)))
70	69	anim2d 621	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ* → ((0 ≤ 𝐴 ∧ 𝐴 < π) → (0 ≤ 𝐴 ∧ 𝐴 ≤ (2 · π))))
71		elicc4 13411	. . . . . . . . 9 ⊢ ((0 ∈ ℝ* ∧ (2 · π) ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐴 ∈ (0[,](2 · π)) ↔ (0 ≤ 𝐴 ∧ 𝐴 ≤ (2 · π))))
72	55, 59, 71	mp3an12 1471	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ (0[,](2 · π)) ↔ (0 ≤ 𝐴 ∧ 𝐴 ≤ (2 · π))))
73	70, 72	sylibrd 261	. . . . . . 7 ⊢ (𝐴 ∈ ℝ* → ((0 ≤ 𝐴 ∧ 𝐴 < π) → 𝐴 ∈ (0[,](2 · π))))
74	73	3impib 1128	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 < π) → 𝐴 ∈ (0[,](2 · π)))
75	57, 74	sylbi 219	. . . . 5 ⊢ (𝐴 ∈ (0[,)π) → 𝐴 ∈ (0[,](2 · π)))
76		sin2h 38070	. . . . 5 ⊢ (𝐴 ∈ (0[,](2 · π)) → (sin‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / 2)))
77	75, 76	syl 17	. . . 4 ⊢ (𝐴 ∈ (0[,)π) → (sin‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / 2)))
78	1, 2, 13	ltleii 11300	. . . . . . . . . . 11 ⊢ 0 ≤ π
79		le0neg2 11690	. . . . . . . . . . . 12 ⊢ (π ∈ ℝ → (0 ≤ π ↔ -π ≤ 0))
80	2, 79	ax-mp 5	. . . . . . . . . . 11 ⊢ (0 ≤ π ↔ -π ≤ 0)
81	78, 80	mpbi 232	. . . . . . . . . 10 ⊢ -π ≤ 0
82	17	rexri 11234	. . . . . . . . . . 11 ⊢ -π ∈ ℝ*
83		xrletr 13154	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → ((-π ≤ 0 ∧ 0 ≤ 𝐴) → -π ≤ 𝐴))
84	82, 55, 83	mp3an12 1471	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ* → ((-π ≤ 0 ∧ 0 ≤ 𝐴) → -π ≤ 𝐴))
85	81, 84	mpani 706	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ* → (0 ≤ 𝐴 → -π ≤ 𝐴))
86		xrltle 13145	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ* ∧ π ∈ ℝ*) → (𝐴 < π → 𝐴 ≤ π))
87	3, 86	mpan2 701	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ* → (𝐴 < π → 𝐴 ≤ π))
88	85, 87	anim12d 618	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ* → ((0 ≤ 𝐴 ∧ 𝐴 < π) → (-π ≤ 𝐴 ∧ 𝐴 ≤ π)))
89		elicc4 13411	. . . . . . . . 9 ⊢ ((-π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐴 ∈ (-π[,]π) ↔ (-π ≤ 𝐴 ∧ 𝐴 ≤ π)))
90	82, 3, 89	mp3an12 1471	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ (-π[,]π) ↔ (-π ≤ 𝐴 ∧ 𝐴 ≤ π)))
91	88, 90	sylibrd 261	. . . . . . 7 ⊢ (𝐴 ∈ ℝ* → ((0 ≤ 𝐴 ∧ 𝐴 < π) → 𝐴 ∈ (-π[,]π)))
92	91	3impib 1128	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 < π) → 𝐴 ∈ (-π[,]π))
93	57, 92	sylbi 219	. . . . 5 ⊢ (𝐴 ∈ (0[,)π) → 𝐴 ∈ (-π[,]π))
94		cos2h 38071	. . . . 5 ⊢ (𝐴 ∈ (-π[,]π) → (cos‘(𝐴 / 2)) = (√‘((1 + (cos‘𝐴)) / 2)))
95	93, 94	syl 17	. . . 4 ⊢ (𝐴 ∈ (0[,)π) → (cos‘(𝐴 / 2)) = (√‘((1 + (cos‘𝐴)) / 2)))
96	77, 95	oveq12d 7409	. . 3 ⊢ (𝐴 ∈ (0[,)π) → ((sin‘(𝐴 / 2)) / (cos‘(𝐴 / 2))) = ((√‘((1 − (cos‘𝐴)) / 2)) / (√‘((1 + (cos‘𝐴)) / 2))))
97	54, 96	eqtrd 2796	. 2 ⊢ (𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = ((√‘((1 − (cos‘𝐴)) / 2)) / (√‘((1 + (cos‘𝐴)) / 2))))
98		1re 11175	. . . . 5 ⊢ 1 ∈ ℝ
99	6	recoscld 16167	. . . . 5 ⊢ (𝐴 ∈ (0[,)π) → (cos‘𝐴) ∈ ℝ)
100		resubcl 11489	. . . . 5 ⊢ ((1 ∈ ℝ ∧ (cos‘𝐴) ∈ ℝ) → (1 − (cos‘𝐴)) ∈ ℝ)
101	98, 99, 100	sylancr 596	. . . 4 ⊢ (𝐴 ∈ (0[,)π) → (1 − (cos‘𝐴)) ∈ ℝ)
102	101	rehalfcld 12462	. . 3 ⊢ (𝐴 ∈ (0[,)π) → ((1 − (cos‘𝐴)) / 2) ∈ ℝ)
103		cosbnd 16204	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (-1 ≤ (cos‘𝐴) ∧ (cos‘𝐴) ≤ 1))
104	103	simprd 499	. . . . 5 ⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ≤ 1)
105		recoscl 16164	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈ ℝ)
106		subge0 11694	. . . . . . 7 ⊢ ((1 ∈ ℝ ∧ (cos‘𝐴) ∈ ℝ) → (0 ≤ (1 − (cos‘𝐴)) ↔ (cos‘𝐴) ≤ 1))
107		halfnneg2 12446	. . . . . . . 8 ⊢ ((1 − (cos‘𝐴)) ∈ ℝ → (0 ≤ (1 − (cos‘𝐴)) ↔ 0 ≤ ((1 − (cos‘𝐴)) / 2)))
108	100, 107	syl 17	. . . . . . 7 ⊢ ((1 ∈ ℝ ∧ (cos‘𝐴) ∈ ℝ) → (0 ≤ (1 − (cos‘𝐴)) ↔ 0 ≤ ((1 − (cos‘𝐴)) / 2)))
109	106, 108	bitr3d 283	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ (cos‘𝐴) ∈ ℝ) → ((cos‘𝐴) ≤ 1 ↔ 0 ≤ ((1 − (cos‘𝐴)) / 2)))
110	98, 105, 109	sylancr 596	. . . . 5 ⊢ (𝐴 ∈ ℝ → ((cos‘𝐴) ≤ 1 ↔ 0 ≤ ((1 − (cos‘𝐴)) / 2)))
111	104, 110	mpbid 234	. . . 4 ⊢ (𝐴 ∈ ℝ → 0 ≤ ((1 − (cos‘𝐴)) / 2))
112	6, 111	syl 17	. . 3 ⊢ (𝐴 ∈ (0[,)π) → 0 ≤ ((1 − (cos‘𝐴)) / 2))
113		readdcl 11150	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ (cos‘𝐴) ∈ ℝ) → (1 + (cos‘𝐴)) ∈ ℝ)
114	98, 99, 113	sylancr 596	. . . . 5 ⊢ (𝐴 ∈ (0[,)π) → (1 + (cos‘𝐴)) ∈ ℝ)
115	103	simpld 498	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -1 ≤ (cos‘𝐴))
116	98	renegcli 11486	. . . . . . . . . 10 ⊢ -1 ∈ ℝ
117		subge0 11694	. . . . . . . . . 10 ⊢ (((cos‘𝐴) ∈ ℝ ∧ -1 ∈ ℝ) → (0 ≤ ((cos‘𝐴) − -1) ↔ -1 ≤ (cos‘𝐴)))
118	105, 116, 117	sylancl 595	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → (0 ≤ ((cos‘𝐴) − -1) ↔ -1 ≤ (cos‘𝐴)))
119		recn 11157	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
120	119	coscld 16154	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈ ℂ)
121		ax-1cn 11125	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
122		subneg 11474	. . . . . . . . . . . 12 ⊢ (((cos‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → ((cos‘𝐴) − -1) = ((cos‘𝐴) + 1))
123		addcom 11363	. . . . . . . . . . . 12 ⊢ (((cos‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → ((cos‘𝐴) + 1) = (1 + (cos‘𝐴)))
124	122, 123	eqtrd 2796	. . . . . . . . . . 11 ⊢ (((cos‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → ((cos‘𝐴) − -1) = (1 + (cos‘𝐴)))
125	120, 121, 124	sylancl 595	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → ((cos‘𝐴) − -1) = (1 + (cos‘𝐴)))
126	125	breq2d 5109	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → (0 ≤ ((cos‘𝐴) − -1) ↔ 0 ≤ (1 + (cos‘𝐴))))
127	118, 126	bitr3d 283	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → (-1 ≤ (cos‘𝐴) ↔ 0 ≤ (1 + (cos‘𝐴))))
128	115, 127	mpbid 234	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → 0 ≤ (1 + (cos‘𝐴)))
129	6, 128	syl 17	. . . . . 6 ⊢ (𝐴 ∈ (0[,)π) → 0 ≤ (1 + (cos‘𝐴)))
130		snunioo 13476	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ π ∈ ℝ* ∧ 0 < π) → ({0} ∪ (0(,)π)) = (0[,)π))
131	55, 3, 13, 130	mp3an 1481	. . . . . . . . 9 ⊢ ({0} ∪ (0(,)π)) = (0[,)π)
132	131	eleq2i 2853	. . . . . . . 8 ⊢ (𝐴 ∈ ({0} ∪ (0(,)π)) ↔ 𝐴 ∈ (0[,)π))
133		elun 4104	. . . . . . . 8 ⊢ (𝐴 ∈ ({0} ∪ (0(,)π)) ↔ (𝐴 ∈ {0} ∨ 𝐴 ∈ (0(,)π)))
134	132, 133	bitr3i 279	. . . . . . 7 ⊢ (𝐴 ∈ (0[,)π) ↔ (𝐴 ∈ {0} ∨ 𝐴 ∈ (0(,)π)))
135		elsni 4596	. . . . . . . . 9 ⊢ (𝐴 ∈ {0} → 𝐴 = 0)
136		fveq2 6862	. . . . . . . . . . . . 13 ⊢ (𝐴 = 0 → (cos‘𝐴) = (cos‘0))
137		cos0 16173	. . . . . . . . . . . . 13 ⊢ (cos‘0) = 1
138	136, 137	eqtrdi 2812	. . . . . . . . . . . 12 ⊢ (𝐴 = 0 → (cos‘𝐴) = 1)
139	138	oveq2d 7407	. . . . . . . . . . 11 ⊢ (𝐴 = 0 → (1 + (cos‘𝐴)) = (1 + 1))
140		df-2 12274	. . . . . . . . . . 11 ⊢ 2 = (1 + 1)
141	139, 140	eqtr4di 2814	. . . . . . . . . 10 ⊢ (𝐴 = 0 → (1 + (cos‘𝐴)) = 2)
142	28	a1i 11	. . . . . . . . . 10 ⊢ (𝐴 = 0 → 2 ≠ 0)
143	141, 142	eqnetrd 3023	. . . . . . . . 9 ⊢ (𝐴 = 0 → (1 + (cos‘𝐴)) ≠ 0)
144	135, 143	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ {0} → (1 + (cos‘𝐴)) ≠ 0)
145		sinq12gt0 26560	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)π) → 0 < (sin‘𝐴))
146		ltne 11274	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 0 < (sin‘𝐴)) → (sin‘𝐴) ≠ 0)
147	1, 146	mpan 700	. . . . . . . . . 10 ⊢ (0 < (sin‘𝐴) → (sin‘𝐴) ≠ 0)
148		elioore 13373	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (0(,)π) → 𝐴 ∈ ℝ)
149	148	recnd 11204	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (0(,)π) → 𝐴 ∈ ℂ)
150		oveq1 7398	. . . . . . . . . . . . . 14 ⊢ (-1 = (cos‘𝐴) → (-1↑2) = ((cos‘𝐴)↑2))
151	150	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (-1 = (cos‘𝐴) → (-1↑2) = ((cos‘𝐴)↑2)))
152		df-neg 11411	. . . . . . . . . . . . . . 15 ⊢ -1 = (0 − 1)
153	152	eqeq1i 2766	. . . . . . . . . . . . . 14 ⊢ (-1 = (cos‘𝐴) ↔ (0 − 1) = (cos‘𝐴))
154		coscl 16150	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
155		0cn 11165	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℂ
156		subadd 11427	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℂ ∧ 1 ∈ ℂ ∧ (cos‘𝐴) ∈ ℂ) → ((0 − 1) = (cos‘𝐴) ↔ (1 + (cos‘𝐴)) = 0))
157	155, 121, 156	mp3an12 1471	. . . . . . . . . . . . . . 15 ⊢ ((cos‘𝐴) ∈ ℂ → ((0 − 1) = (cos‘𝐴) ↔ (1 + (cos‘𝐴)) = 0))
158	154, 157	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((0 − 1) = (cos‘𝐴) ↔ (1 + (cos‘𝐴)) = 0))
159	153, 158	bitrid 285	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (-1 = (cos‘𝐴) ↔ (1 + (cos‘𝐴)) = 0))
160		sincl 16149	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
161	160	sqcld 14151	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → ((sin‘𝐴)↑2) ∈ ℂ)
162		0cnd 11166	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → 0 ∈ ℂ)
163	154	sqcld 14151	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴)↑2) ∈ ℂ)
164	161, 162, 163	addcan2d 11381	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = (0 + ((cos‘𝐴)↑2)) ↔ ((sin‘𝐴)↑2) = 0))
165		sincossq 16199	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = 1)
166		neg1sqe1 14203	. . . . . . . . . . . . . . . 16 ⊢ (-1↑2) = 1
167	165, 166	eqtr4di 2814	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = (-1↑2))
168	163	addlidd 11378	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (0 + ((cos‘𝐴)↑2)) = ((cos‘𝐴)↑2))
169	167, 168	eqeq12d 2777	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = (0 + ((cos‘𝐴)↑2)) ↔ (-1↑2) = ((cos‘𝐴)↑2)))
170		sqeq0 14127	. . . . . . . . . . . . . . 15 ⊢ ((sin‘𝐴) ∈ ℂ → (((sin‘𝐴)↑2) = 0 ↔ (sin‘𝐴) = 0))
171	160, 170	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (((sin‘𝐴)↑2) = 0 ↔ (sin‘𝐴) = 0))
172	164, 169, 171	3bitr3d 311	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((-1↑2) = ((cos‘𝐴)↑2) ↔ (sin‘𝐴) = 0))
173	151, 159, 172	3imtr3d 295	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((1 + (cos‘𝐴)) = 0 → (sin‘𝐴) = 0))
174	149, 173	syl 17	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)π) → ((1 + (cos‘𝐴)) = 0 → (sin‘𝐴) = 0))
175	174	necon3d 2977	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)π) → ((sin‘𝐴) ≠ 0 → (1 + (cos‘𝐴)) ≠ 0))
176	147, 175	syl5 34	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,)π) → (0 < (sin‘𝐴) → (1 + (cos‘𝐴)) ≠ 0))
177	145, 176	mpd 15	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)π) → (1 + (cos‘𝐴)) ≠ 0)
178	144, 177	jaoi 868	. . . . . . 7 ⊢ ((𝐴 ∈ {0} ∨ 𝐴 ∈ (0(,)π)) → (1 + (cos‘𝐴)) ≠ 0)
179	134, 178	sylbi 219	. . . . . 6 ⊢ (𝐴 ∈ (0[,)π) → (1 + (cos‘𝐴)) ≠ 0)
180	114, 129, 179	ne0gt0d 11314	. . . . 5 ⊢ (𝐴 ∈ (0[,)π) → 0 < (1 + (cos‘𝐴)))
181	114, 180	elrpd 13028	. . . 4 ⊢ (𝐴 ∈ (0[,)π) → (1 + (cos‘𝐴)) ∈ ℝ+)
182	181	rphalfcld 13043	. . 3 ⊢ (𝐴 ∈ (0[,)π) → ((1 + (cos‘𝐴)) / 2) ∈ ℝ+)
183	102, 112, 182	sqrtdivd 15442	. 2 ⊢ (𝐴 ∈ (0[,)π) → (√‘(((1 − (cos‘𝐴)) / 2) / ((1 + (cos‘𝐴)) / 2))) = ((√‘((1 − (cos‘𝐴)) / 2)) / (√‘((1 + (cos‘𝐴)) / 2))))
184	7	coscld 16154	. . . . 5 ⊢ (𝐴 ∈ (0[,)π) → (cos‘𝐴) ∈ ℂ)
185		subcl 11423	. . . . 5 ⊢ ((1 ∈ ℂ ∧ (cos‘𝐴) ∈ ℂ) → (1 − (cos‘𝐴)) ∈ ℂ)
186	121, 184, 185	sylancr 596	. . . 4 ⊢ (𝐴 ∈ (0[,)π) → (1 − (cos‘𝐴)) ∈ ℂ)
187		addcl 11149	. . . . 5 ⊢ ((1 ∈ ℂ ∧ (cos‘𝐴) ∈ ℂ) → (1 + (cos‘𝐴)) ∈ ℂ)
188	121, 184, 187	sylancr 596	. . . 4 ⊢ (𝐴 ∈ (0[,)π) → (1 + (cos‘𝐴)) ∈ ℂ)
189		2cnne0 12424	. . . . 5 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
190		divcan7 11894	. . . . 5 ⊢ (((1 − (cos‘𝐴)) ∈ ℂ ∧ ((1 + (cos‘𝐴)) ∈ ℂ ∧ (1 + (cos‘𝐴)) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((1 − (cos‘𝐴)) / 2) / ((1 + (cos‘𝐴)) / 2)) = ((1 − (cos‘𝐴)) / (1 + (cos‘𝐴))))
191	189, 190	mp3an3 1470	. . . 4 ⊢ (((1 − (cos‘𝐴)) ∈ ℂ ∧ ((1 + (cos‘𝐴)) ∈ ℂ ∧ (1 + (cos‘𝐴)) ≠ 0)) → (((1 − (cos‘𝐴)) / 2) / ((1 + (cos‘𝐴)) / 2)) = ((1 − (cos‘𝐴)) / (1 + (cos‘𝐴))))
192	186, 188, 179, 191	syl12anc 847	. . 3 ⊢ (𝐴 ∈ (0[,)π) → (((1 − (cos‘𝐴)) / 2) / ((1 + (cos‘𝐴)) / 2)) = ((1 − (cos‘𝐴)) / (1 + (cos‘𝐴))))
193	192	fveq2d 6866	. 2 ⊢ (𝐴 ∈ (0[,)π) → (√‘(((1 − (cos‘𝐴)) / 2) / ((1 + (cos‘𝐴)) / 2))) = (√‘((1 − (cos‘𝐴)) / (1 + (cos‘𝐴)))))
194	97, 183, 193	3eqtr2d 2802	1 ⊢ (𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / (1 + (cos‘𝐴)))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141   ≠ wne 2956   ∪ cun 3900   ⊆ wss 3902  {csn 4579   class class class wbr 5097  ‘cfv 6516  (class class class)co 7391  ℂcc 11065  ℝcr 11066  0cc0 11067  1c1 11068   + caddc 11070   · cmul 11072  ℝ^*cxr 11209   < clt 11210   ≤ cle 11211   − cmin 11408  -cneg 11409   / cdiv 11838  2c2 12266  (,)cioo 13343  [,)cico 13345  [,]cicc 13346  ↑cexp 14068  ℜcre 15115  √csqrt 15251  sincsin 16084  cosccos 16085  tanctan 16086  πcpi 16087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-inf2 9590  ax-cnex 11123  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143  ax-pre-mulgt0 11144  ax-pre-sup 11145  ax-addf 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4863  df-int 4903  df-iun 4948  df-iin 4949  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-se 5597  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-isom 6525  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-of 7655  df-om 7842  df-1st 7965  df-2nd 7966  df-supp 8135  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-1o 8431  df-2o 8432  df-er 8672  df-map 8804  df-pm 8805  df-ixp 8874  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-fsupp 9302  df-fi 9351  df-sup 9382  df-inf 9383  df-oi 9452  df-card 9891  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-sub 11410  df-neg 11411  df-div 11839  df-nn 12205  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281  df-n0 12476  df-z 12563  df-dec 12683  df-uz 12834  df-q 12944  df-rp 12988  df-xneg 13108  df-xadd 13109  df-xmul 13110  df-ioo 13347  df-ioc 13348  df-ico 13349  df-icc 13350  df-fz 13507  df-fzo 13654  df-fl 13796  df-mod 13874  df-seq 14009  df-exp 14069  df-fac 14281  df-bc 14310  df-hash 14338  df-shft 15074  df-cj 15117  df-re 15118  df-im 15119  df-sqrt 15253  df-abs 15254  df-limsup 15489  df-clim 15506  df-rlim 15507  df-sum 15705  df-ef 16088  df-sin 16090  df-cos 16091  df-tan 16092  df-pi 16093  df-struct 17174  df-sets 17191  df-slot 17209  df-ndx 17221  df-base 17237  df-ress 17258  df-plusg 17290  df-mulr 17291  df-starv 17292  df-sca 17293  df-vsca 17294  df-ip 17295  df-tset 17296  df-ple 17297  df-ds 17299  df-unif 17300  df-hom 17301  df-cco 17302  df-rest 17442  df-topn 17443  df-0g 17461  df-gsum 17462  df-topgen 17463  df-pt 17464  df-prds 17467  df-xrs 17523  df-qtop 17528  df-imas 17529  df-xps 17531  df-mre 17605  df-mrc 17606  df-acs 17608  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-mulg 19101  df-cntz 19348  df-cmn 19813  df-psmet 21404  df-xmet 21405  df-met 21406  df-bl 21407  df-mopn 21408  df-fbas 21409  df-fg 21410  df-cnfld 21413  df-top 22942  df-topon 22959  df-topsp 22981  df-bases 22994  df-cld 23067  df-ntr 23068  df-cls 23069  df-nei 23146  df-lp 23184  df-perf 23185  df-cn 23275  df-cnp 23276  df-haus 23363  df-tx 23610  df-hmeo 23803  df-fil 23894  df-fm 23986  df-flim 23987  df-flf 23988  df-xms 24368  df-ms 24369  df-tms 24370  df-cncf 24928  df-limc 25916  df-dv 25917

This theorem is referenced by: (None)