asinsin - Metamath Proof Explorer

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

Theorem asinsin 27227

Description: The arcsine function composed with sin is equal to the identity. This plus sinasin 27224 allow to view sin and arcsin as inverse operations to each other. For ease of use, we have not defined precisely the correct domain of correctness of this identity; in addition to the main region described here it is also true for some points on the branch cuts, namely when 𝐴 = (π / 2) − i𝑦 for nonnegative real 𝑦 and also symmetrically at 𝐴 = i𝑦 − (π / 2). In particular, when restricted to reals this identity extends to the closed interval [ -(π / 2), (π / 2)], not just the open interval (see reasinsin 27231). (Contributed by Mario Carneiro, 2-Apr-2015.)

**Assertion**
Ref	Expression
asinsin	⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (arcsin‘(sin‘𝐴)) = 𝐴)

**Proof of Theorem asinsin**
Step	Hyp	Ref	Expression
1		sincl 16301	. . . 4 ⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
2	1	adantr 486	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
3		asinval 27217	. . 3 ⊢ ((sin‘𝐴) ∈ ℂ → (arcsin‘(sin‘𝐴)) = ( -i · (log‘((i · (sin‘𝐴)) + (√‘(1 − ((sin‘𝐴)↑2)))))))
4	2, 3	syl 18	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (arcsin‘(sin‘𝐴)) = ( -i · (log‘((i · (sin‘𝐴)) + (√‘(1 − ((sin‘𝐴)↑2)))))))
5		ax-icn 11264	. . . . . . . 8 ⊢ i ∈ ℂ
6		mulcl 11289	. . . . . . . 8 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
7	5, 2, 6	sylancr 599	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
8		simpl 488	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ)
9		mulcl 11289	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · 𝐴) ∈ ℂ)
10	5, 8, 9	sylancr 599	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ℂ)
11		efcl 16255	. . . . . . . 8 ⊢ ((i · 𝐴) ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
12	10, 11	syl 18	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) ∈ ℂ)
13	7, 12	pncan3d 11677	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) + ((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))) = (exp‘(i · 𝐴)))
14	12, 7	subcld 11674	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (i · (sin‘𝐴))) ∈ ℂ)
15		ax-1cn 11263	. . . . . . . . 9 ⊢ 1 ∈ ℂ
16	2	sqcld 14292	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((sin‘𝐴)↑2) ∈ ℂ)
17		subcl 11561	. . . . . . . . 9 ⊢ ((1 ∈ ℂ ∧ ((sin‘𝐴)↑2) ∈ ℂ) → (1 − ((sin‘𝐴)↑2)) ∈ ℂ)
18	15, 16, 17	sylancr 599	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (1 − ((sin‘𝐴)↑2)) ∈ ℂ)
19		binom2sub 14369	. . . . . . . . . 10 ⊢ (((exp‘(i · 𝐴)) ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ) → (((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))↑2) = ((((exp‘(i · 𝐴))↑2) − (2 · ((exp‘(i · 𝐴)) · (i · (sin‘𝐴))))) + ((i · (sin‘𝐴))↑2)))
20	12, 7, 19	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))↑2) = ((((exp‘(i · 𝐴))↑2) − (2 · ((exp‘(i · 𝐴)) · (i · (sin‘𝐴))))) + ((i · (sin‘𝐴))↑2)))
21	12	sqvald 14291	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴))↑2) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
22		2cn 12423	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
23	22	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 2 ∈ ℂ)
24	23, 12, 7	mul12d 11524	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (2 · ((exp‘(i · 𝐴)) · (i · (sin‘𝐴)))) = ((exp‘(i · 𝐴)) · (2 · (i · (sin‘𝐴)))))
25	21, 24	oveq12d 7440	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴))↑2) − (2 · ((exp‘(i · 𝐴)) · (i · (sin‘𝐴))))) = (((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) − ((exp‘(i · 𝐴)) · (2 · (i · (sin‘𝐴))))))
26		coscl 16302	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
27	26	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
28		subsq 14359	. . . . . . . . . . . . 13 ⊢ (((cos‘𝐴) ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ) → (((cos‘𝐴)↑2) − ((i · (sin‘𝐴))↑2)) = (((cos‘𝐴) + (i · (sin‘𝐴))) · ((cos‘𝐴) − (i · (sin‘𝐴)))))
29	27, 7, 28	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − ((i · (sin‘𝐴))↑2)) = (((cos‘𝐴) + (i · (sin‘𝐴))) · ((cos‘𝐴) − (i · (sin‘𝐴)))))
30		sqmul 14267	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((i · (sin‘𝐴))↑2) = ((i↑2) · ((sin‘𝐴)↑2)))
31	5, 2, 30	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴))↑2) = ((i↑2) · ((sin‘𝐴)↑2)))
32		i2 14351	. . . . . . . . . . . . . . . . 17 ⊢ (i↑2) = -1
33	32	oveq1i 7432	. . . . . . . . . . . . . . . 16 ⊢ ((i↑2) · ((sin‘𝐴)↑2)) = ( -1 · ((sin‘𝐴)↑2))
34	16	mulm1d 11773	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ( -1 · ((sin‘𝐴)↑2)) = -((sin‘𝐴)↑2))
35	33, 34	eqtrid 2807	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((i↑2) · ((sin‘𝐴)↑2)) = -((sin‘𝐴)↑2))
36	31, 35	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴))↑2) = -((sin‘𝐴)↑2))
37	36	oveq2d 7438	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − ((i · (sin‘𝐴))↑2)) = (((cos‘𝐴)↑2) − -((sin‘𝐴)↑2)))
38	27	sqcld 14292	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((cos‘𝐴)↑2) ∈ ℂ)
39	38, 16	subnegd 11681	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − -((sin‘𝐴)↑2)) = (((cos‘𝐴)↑2) + ((sin‘𝐴)↑2)))
40	38, 16	addcomd 11517	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) + ((sin‘𝐴)↑2)) = (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)))
41	37, 39, 40	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − ((i · (sin‘𝐴))↑2)) = (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)))
42		efival 16327	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
43	42	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
44	7	2timesd 12594	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (2 · (i · (sin‘𝐴))) = ((i · (sin‘𝐴)) + (i · (sin‘𝐴))))
45	43, 44	oveq12d 7440	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (2 · (i · (sin‘𝐴)))) = (((cos‘𝐴) + (i · (sin‘𝐴))) − ((i · (sin‘𝐴)) + (i · (sin‘𝐴)))))
46	27, 7, 7	pnpcan2d 11712	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) − ((i · (sin‘𝐴)) + (i · (sin‘𝐴)))) = ((cos‘𝐴) − (i · (sin‘𝐴))))
47	45, 46	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (2 · (i · (sin‘𝐴)))) = ((cos‘𝐴) − (i · (sin‘𝐴))))
48	43, 47	oveq12d 7440	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) · ((exp‘(i · 𝐴)) − (2 · (i · (sin‘𝐴))))) = (((cos‘𝐴) + (i · (sin‘𝐴))) · ((cos‘𝐴) − (i · (sin‘𝐴)))))
49		mulcl 11289	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ) → (2 · (i · (sin‘𝐴))) ∈ ℂ)
50	22, 7, 49	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (2 · (i · (sin‘𝐴))) ∈ ℂ)
51	12, 12, 50	subdid 11777	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) · ((exp‘(i · 𝐴)) − (2 · (i · (sin‘𝐴))))) = (((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) − ((exp‘(i · 𝐴)) · (2 · (i · (sin‘𝐴))))))
52	48, 51	eqtr3d 2797	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) · ((cos‘𝐴) − (i · (sin‘𝐴)))) = (((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) − ((exp‘(i · 𝐴)) · (2 · (i · (sin‘𝐴))))))
53	29, 41, 52	3eqtr3d 2803	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = (((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) − ((exp‘(i · 𝐴)) · (2 · (i · (sin‘𝐴))))))
54		sincossq 16351	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = 1)
55	54	adantr 486	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = 1)
56	25, 53, 55	3eqtr2d 2801	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴))↑2) − (2 · ((exp‘(i · 𝐴)) · (i · (sin‘𝐴))))) = 1)
57	56, 36	oveq12d 7440	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((((exp‘(i · 𝐴))↑2) − (2 · ((exp‘(i · 𝐴)) · (i · (sin‘𝐴))))) + ((i · (sin‘𝐴))↑2)) = (1 + -((sin‘𝐴)↑2)))
58		negsub 11611	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ ((sin‘𝐴)↑2) ∈ ℂ) → (1 + -((sin‘𝐴)↑2)) = (1 − ((sin‘𝐴)↑2)))
59	15, 16, 58	sylancr 599	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (1 + -((sin‘𝐴)↑2)) = (1 − ((sin‘𝐴)↑2)))
60	20, 57, 59	3eqtrd 2799	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))↑2) = (1 − ((sin‘𝐴)↑2)))
61		halfre 12564	. . . . . . . . . . . 12 ⊢ (1 / 2) ∈ ℝ
62	61	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (1 / 2) ∈ ℝ)
63		negicn 11563	. . . . . . . . . . . . . . 15 ⊢ -i ∈ ℂ
64		mulcl 11289	. . . . . . . . . . . . . . 15 ⊢ (( -i ∈ ℂ ∧ 𝐴 ∈ ℂ) → ( -i · 𝐴) ∈ ℂ)
65	63, 8, 64	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ( -i · 𝐴) ∈ ℂ)
66		efcl 16255	. . . . . . . . . . . . . 14 ⊢ (( -i · 𝐴) ∈ ℂ → (exp‘( -i · 𝐴)) ∈ ℂ)
67	65, 66	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (exp‘( -i · 𝐴)) ∈ ℂ)
68	12, 67	addcld 11333	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))) ∈ ℂ)
69	68	recld 15368	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴)))) ∈ ℝ)
70		halfgt0 12566	. . . . . . . . . . . 12 ⊢ 0 < (1 / 2)
71	70	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (1 / 2))
72	12	recld 15368	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(i · 𝐴))) ∈ ℝ)
73	67	recld 15368	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘(exp‘( -i · 𝐴))) ∈ ℝ)
74		asinsinlem 27226	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i · 𝐴))))
75		negcl 11562	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
76	75	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -𝐴 ∈ ℂ)
77		reneg 15299	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (ℜ‘ -𝐴) = -(ℜ‘𝐴))
78	77	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘ -𝐴) = -(ℜ‘𝐴))
79		halfpire 26800	. . . . . . . . . . . . . . . . . . . 20 ⊢ (π / 2) ∈ ℝ
80	79	renegcli 11624	. . . . . . . . . . . . . . . . . . 19 ⊢ -(π / 2) ∈ ℝ
81		recl 15284	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
82		iooneg 13607	. . . . . . . . . . . . . . . . . . 19 ⊢ (( -(π / 2) ∈ ℝ ∧ (π / 2) ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → ((ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2)) ↔ -(ℜ‘𝐴) ∈ ( -(π / 2)(,) - -(π / 2))))
83	80, 79, 81, 82	mp3an12i 1494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2)) ↔ -(ℜ‘𝐴) ∈ ( -(π / 2)(,) - -(π / 2))))
84	83	biimpa 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -(ℜ‘𝐴) ∈ ( -(π / 2)(,) - -(π / 2)))
85	79	recni 11328	. . . . . . . . . . . . . . . . . . 19 ⊢ (π / 2) ∈ ℂ
86	85	negnegi 11633	. . . . . . . . . . . . . . . . . 18 ⊢ - -(π / 2) = (π / 2)
87	86	oveq2i 7433	. . . . . . . . . . . . . . . . 17 ⊢ ( -(π / 2)(,) - -(π / 2)) = ( -(π / 2)(,)(π / 2))
88	84, 87	eleqtrdi 2870	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -(ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2)))
89	78, 88	eqeltrd 2860	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘ -𝐴) ∈ ( -(π / 2)(,)(π / 2)))
90		asinsinlem 27226	. . . . . . . . . . . . . . 15 ⊢ (( -𝐴 ∈ ℂ ∧ (ℜ‘ -𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i · -𝐴))))
91	76, 89, 90	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i · -𝐴))))
92		mulneg12 11759	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → ( -i · 𝐴) = (i · -𝐴))
93	5, 8, 92	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ( -i · 𝐴) = (i · -𝐴))
94	93	fveq2d 6892	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (exp‘( -i · 𝐴)) = (exp‘(i · -𝐴)))
95	94	fveq2d 6892	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘(exp‘( -i · 𝐴))) = (ℜ‘(exp‘(i · -𝐴))))
96	91, 95	breqtrrd 5132	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘( -i · 𝐴))))
97	72, 73, 74, 96	addgt0d 11896	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < ((ℜ‘(exp‘(i · 𝐴))) + (ℜ‘(exp‘( -i · 𝐴)))))
98	12, 67	readdd 15388	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴)))) = ((ℜ‘(exp‘(i · 𝐴))) + (ℜ‘(exp‘( -i · 𝐴)))))
99	97, 98	breqtrrd 5132	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴)))))
100	62, 69, 71, 99	mulgt0d 11470	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < ((1 / 2) · (ℜ‘((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))))))
101		cosval 16298	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) = (((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))) / 2))
102	101	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (cos‘𝐴) = (((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))) / 2))
103		2ne0 12454	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 0
104	103	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 2 ≠ 0)
105	68, 23, 104	divrec2d 12102	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))) / 2) = ((1 / 2) · ((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴)))))
106	102, 105	eqtrd 2795	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (cos‘𝐴) = ((1 / 2) · ((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴)))))
107	106	fveq2d 6892	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘(cos‘𝐴)) = (ℜ‘((1 / 2) · ((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))))))
108		remul2 15304	. . . . . . . . . . . 12 ⊢ (((1 / 2) ∈ ℝ ∧ ((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))) ∈ ℂ) → (ℜ‘((1 / 2) · ((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))))) = ((1 / 2) · (ℜ‘((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))))))
109	61, 68, 108	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘((1 / 2) · ((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))))) = ((1 / 2) · (ℜ‘((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))))))
110	107, 109	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘(cos‘𝐴)) = ((1 / 2) · (ℜ‘((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))))))
111	100, 110	breqtrrd 5132	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘(cos‘𝐴)))
112	27, 7, 43	mvrraddd 11732	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (i · (sin‘𝐴))) = (cos‘𝐴))
113	112	fveq2d 6892	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))) = (ℜ‘(cos‘𝐴)))
114	111, 113	breqtrrd 5132	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))))
115	14, 18, 60, 114	eqsqrt2d 15543	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (i · (sin‘𝐴))) = (√‘(1 − ((sin‘𝐴)↑2))))
116	115	oveq2d 7438	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) + ((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))) = ((i · (sin‘𝐴)) + (√‘(1 − ((sin‘𝐴)↑2)))))
117	13, 116	eqtr3d 2797	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((i · (sin‘𝐴)) + (√‘(1 − ((sin‘𝐴)↑2)))))
118	117	fveq2d 6892	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (log‘(exp‘(i · 𝐴))) = (log‘((i · (sin‘𝐴)) + (√‘(1 − ((sin‘𝐴)↑2))))))
119		pire 26790	. . . . . . . . . 10 ⊢ π ∈ ℝ
120	119	renegcli 11624	. . . . . . . . 9 ⊢ -π ∈ ℝ
121	120	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -π ∈ ℝ)
122	80	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -(π / 2) ∈ ℝ)
123		elioore 13511	. . . . . . . . 9 ⊢ ((ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2)) → (ℜ‘𝐴) ∈ ℝ)
124	123	adantl 487	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ)
125		pirp 26797	. . . . . . . . . . 11 ⊢ π ∈ ℝ⁺
126		rphalflt 13156	. . . . . . . . . . 11 ⊢ (π ∈ ℝ⁺ → (π / 2) < π)
127	125, 126	ax-mp 5	. . . . . . . . . 10 ⊢ (π / 2) < π
128	79, 119	ltnegi 11865	. . . . . . . . . 10 ⊢ ((π / 2) < π ↔ -π < -(π / 2))
129	127, 128	mpbi 233	. . . . . . . . 9 ⊢ -π < -(π / 2)
130	129	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -π < -(π / 2))
131		eliooord 13541	. . . . . . . . . 10 ⊢ ((ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2)) → ( -(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2)))
132	131	adantl 487	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ( -(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π / 2)))
133	132	simpld 500	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -(π / 2) < (ℜ‘𝐴))
134	121, 122, 124, 130, 133	lttrd 11476	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -π < (ℜ‘𝐴))
135		imre 15282	. . . . . . . . 9 ⊢ ((i · 𝐴) ∈ ℂ → (ℑ‘(i · 𝐴)) = (ℜ‘( -i · (i · 𝐴))))
136	10, 135	syl 18	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘( -i · (i · 𝐴))))
137	5, 5	mulneg1i 11767	. . . . . . . . . . . 12 ⊢ ( -i · i) = -(i · i)
138		ixi 11950	. . . . . . . . . . . . 13 ⊢ (i · i) = -1
139	138	negeqi 11555	. . . . . . . . . . . 12 ⊢ -(i · i) = - -1
140	15	negnegi 11633	. . . . . . . . . . . 12 ⊢ - -1 = 1
141	137, 139, 140	3eqtri 2787	. . . . . . . . . . 11 ⊢ ( -i · i) = 1
142	141	oveq1i 7432	. . . . . . . . . 10 ⊢ (( -i · i) · 𝐴) = (1 · 𝐴)
143	63	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -i ∈ ℂ)
144	5	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → i ∈ ℂ)
145	143, 144, 8	mulassd 11337	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (( -i · i) · 𝐴) = ( -i · (i · 𝐴)))
146		mullid 11312	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
147	146	adantr 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (1 · 𝐴) = 𝐴)
148	142, 145, 147	3eqtr3a 2819	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ( -i · (i · 𝐴)) = 𝐴)
149	148	fveq2d 6892	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘( -i · (i · 𝐴))) = (ℜ‘𝐴))
150	136, 149	eqtrd 2795	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘𝐴))
151	134, 150	breqtrrd 5132	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -π < (ℑ‘(i · 𝐴)))
152	119	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → π ∈ ℝ)
153	79	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (π / 2) ∈ ℝ)
154	132	simprd 501	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘𝐴) < (π / 2))
155	127	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (π / 2) < π)
156	124, 153, 152, 154, 155	lttrd 11476	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘𝐴) < π)
157	124, 152, 156	ltled 11463	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ≤ π)
158	150, 157	eqbrtrd 5126	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) ≤ π)
159		ellogrn 26894	. . . . . 6 ⊢ ((i · 𝐴) ∈ ran log ↔ ((i · 𝐴) ∈ ℂ ∧ -π < (ℑ‘(i · 𝐴)) ∧ (ℑ‘(i · 𝐴)) ≤ π))
160	10, 151, 158, 159	syl3anbrc 1362	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ran log)
161		logef 26916	. . . . 5 ⊢ ((i · 𝐴) ∈ ran log → (log‘(exp‘(i · 𝐴))) = (i · 𝐴))
162	160, 161	syl 18	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (log‘(exp‘(i · 𝐴))) = (i · 𝐴))
163	118, 162	eqtr3d 2797	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (log‘((i · (sin‘𝐴)) + (√‘(1 − ((sin‘𝐴)↑2))))) = (i · 𝐴))
164	163	oveq2d 7438	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ( -i · (log‘((i · (sin‘𝐴)) + (√‘(1 − ((sin‘𝐴)↑2)))))) = ( -i · (i · 𝐴)))
165	4, 164, 148	3eqtrd 2799	1 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (arcsin‘(sin‘𝐴)) = 𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 class class class wbr 5102 ran crn 5651 ‘cfv 6541 (class class class)co 7422 ℂcc 11203 ℝcr 11204 0cc0 11205 1c1 11206 ici 11207 + caddc 11208 · cmul 11210 < clt 11348 ≤ cle 11349 − cmin 11546 -cneg 11547 / cdiv 11978 2c2 12402 ℝ⁺crp 13125 (,)cioo 13481 ↑cexp 14209 ℜcre 15271 ℑcim 15272 √csqrt 15407 expce 16234 sincsin 16236 cosccos 16237 πcpi 16239 logclog 26889 arcsincasin 27197

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7753 ax-inf2 9647 ax-cnex 11261 ax-resscn 11262 ax-1cn 11263 ax-icn 11264 ax-addcl 11265 ax-addrcl 11266 ax-mulcl 11267 ax-mulrcl 11268 ax-mulcom 11269 ax-addass 11270 ax-mulass 11271 ax-distr 11272 ax-i2m1 11273 ax-1ne0 11274 ax-1rid 11275 ax-rnegex 11276 ax-rrecex 11277 ax-cnre 11278 ax-pre-lttri 11279 ax-pre-lttrn 11280 ax-pre-ltadd 11281 ax-pre-mulgt0 11282 ax-pre-sup 11283 ax-addf 11284

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7379 df-ov 7425 df-oprab 7426 df-mpo 7427 df-of 7695 df-om 7880 df-1st 8003 df-2nd 8004 df-supp 8182 df-frecs 8304 df-wrecs 8335 df-recs 8384 df-rdg 8423 df-1o 8481 df-2o 8482 df-er 8722 df-map 8854 df-pm 8855 df-ixp 8931 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-fsupp 9359 df-fi 9408 df-sup 9439 df-inf 9440 df-oi 9509 df-card 10025 df-pnf 11350 df-mnf 11351 df-xr 11352 df-ltxr 11353 df-le 11354 df-sub 11548 df-neg 11549 df-div 11979 df-nn 12341 df-2 12410 df-3 12411 df-4 12412 df-5 12413 df-6 12414 df-7 12415 df-8 12416 df-9 12417 df-n0 12612 df-z 12699 df-dec 12820 df-uz 12971 df-q 13081 df-rp 13126 df-xneg 13246 df-xadd 13247 df-xmul 13248 df-ioo 13485 df-ioc 13486 df-ico 13487 df-icc 13488 df-fz 13645 df-fzo 13794 df-fl 13937 df-mod 14015 df-seq 14150 df-exp 14210 df-fac 14423 df-bc 14452 df-hash 14480 df-shft 15227 df-cj 15273 df-re 15274 df-im 15275 df-sqrt 15409 df-abs 15410 df-limsup 15645 df-clim 15662 df-rlim 15663 df-sum 15861 df-ef 16240 df-sin 16242 df-cos 16243 df-pi 16245 df-struct 17332 df-sets 17349 df-slot 17367 df-ndx 17379 df-base 17395 df-ress 17416 df-plusg 17448 df-mulr 17449 df-starv 17450 df-sca 17451 df-vsca 17452 df-ip 17453 df-tset 17454 df-ple 17455 df-ds 17457 df-unif 17458 df-hom 17459 df-cco 17460 df-rest 17600 df-topn 17601 df-0g 17619 df-gsum 17620 df-topgen 17621 df-pt 17622 df-prds 17625 df-xrs 17681 df-qtop 17686 df-imas 17687 df-xps 17689 df-mre 17763 df-mrc 17764 df-acs 17766 df-mgm 18823 df-sgrp 18915 df-mnd 18931 df-submnd 18986 df-mulg 19285 df-cntz 19538 df-cmn 20003 df-psmet 21677 df-xmet 21678 df-met 21679 df-bl 21680 df-mopn 21681 df-fbas 21682 df-fg 21683 df-cnfld 21686 df-top 23219 df-topon 23236 df-topsp 23258 df-bases 23271 df-cld 23344 df-ntr 23345 df-cls 23346 df-nei 23423 df-lp 23461 df-perf 23462 df-cn 23552 df-cnp 23553 df-haus 23640 df-tx 23888 df-hmeo 24081 df-fil 24172 df-fm 24264 df-flim 24265 df-flf 24266 df-xms 24646 df-ms 24647 df-tms 24648 df-cncf 25206 df-limc 26193 df-dv 26194 df-log 26891 df-asin 27200

This theorem is used by: acoscos 27228 reasinsin 27231 asinsinb 27232

W3C validator