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 27277

Description: The arcsine function composed with sin is equal to the identity. This plus sinasin 27274 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 27281). (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 16338	. . . 4 ⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
2	1	adantr 486	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
3		asinval 27267	. . 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 11298	. . . . . . . 8 ⊢ i ∈ ℂ
6		mulcl 11323	. . . . . . . 8 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
7	5, 2, 6	sylancr 599	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
8		simpl 488	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ)
9		mulcl 11323	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · 𝐴) ∈ ℂ)
10	5, 8, 9	sylancr 599	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ℂ)
11		efcl 16292	. . . . . . . 8 ⊢ ((i · 𝐴) ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
12	10, 11	syl 18	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) ∈ ℂ)
13	7, 12	pncan3d 11711	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) + ((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))) = (exp‘(i · 𝐴)))
14	12, 7	subcld 11708	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (i · (sin‘𝐴))) ∈ ℂ)
15		ax-1cn 11297	. . . . . . . . 9 ⊢ 1 ∈ ℂ
16	2	sqcld 14327	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((sin‘𝐴)↑2) ∈ ℂ)
17		subcl 11595	. . . . . . . . 9 ⊢ ((1 ∈ ℂ ∧ ((sin‘𝐴)↑2) ∈ ℂ) → (1 − ((sin‘𝐴)↑2)) ∈ ℂ)
18	15, 16, 17	sylancr 599	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (1 − ((sin‘𝐴)↑2)) ∈ ℂ)
19		binom2sub 14405	. . . . . . . . . 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 14326	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴))↑2) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
22		2cn 12458	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
23	22	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 2 ∈ ℂ)
24	23, 12, 7	mul12d 11558	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (2 · ((exp‘(i · 𝐴)) · (i · (sin‘𝐴)))) = ((exp‘(i · 𝐴)) · (2 · (i · (sin‘𝐴)))))
25	21, 24	oveq12d 7469	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴))↑2) − (2 · ((exp‘(i · 𝐴)) · (i · (sin‘𝐴))))) = (((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) − ((exp‘(i · 𝐴)) · (2 · (i · (sin‘𝐴))))))
26		coscl 16339	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
27	26	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
28		subsq 14394	. . . . . . . . . . . . 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 14302	. . . . . . . . . . . . . . . 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 14386	. . . . . . . . . . . . . . . . 17 ⊢ (i↑2) = -1
33	32	oveq1i 7461	. . . . . . . . . . . . . . . 16 ⊢ ((i↑2) · ((sin‘𝐴)↑2)) = ( -1 · ((sin‘𝐴)↑2))
34	16	mulm1d 11807	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ( -1 · ((sin‘𝐴)↑2)) = -((sin‘𝐴)↑2))
35	33, 34	eqtrid 2810	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((i↑2) · ((sin‘𝐴)↑2)) = -((sin‘𝐴)↑2))
36	31, 35	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴))↑2) = -((sin‘𝐴)↑2))
37	36	oveq2d 7467	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − ((i · (sin‘𝐴))↑2)) = (((cos‘𝐴)↑2) − -((sin‘𝐴)↑2)))
38	27	sqcld 14327	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((cos‘𝐴)↑2) ∈ ℂ)
39	38, 16	subnegd 11715	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − -((sin‘𝐴)↑2)) = (((cos‘𝐴)↑2) + ((sin‘𝐴)↑2)))
40	38, 16	addcomd 11551	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) + ((sin‘𝐴)↑2)) = (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)))
41	37, 39, 40	3eqtrd 2802	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − ((i · (sin‘𝐴))↑2)) = (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)))
42		efival 16364	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
43	42	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
44	7	2timesd 12629	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (2 · (i · (sin‘𝐴))) = ((i · (sin‘𝐴)) + (i · (sin‘𝐴))))
45	43, 44	oveq12d 7469	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (2 · (i · (sin‘𝐴)))) = (((cos‘𝐴) + (i · (sin‘𝐴))) − ((i · (sin‘𝐴)) + (i · (sin‘𝐴)))))
46	27, 7, 7	pnpcan2d 11746	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) − ((i · (sin‘𝐴)) + (i · (sin‘𝐴)))) = ((cos‘𝐴) − (i · (sin‘𝐴))))
47	45, 46	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (2 · (i · (sin‘𝐴)))) = ((cos‘𝐴) − (i · (sin‘𝐴))))
48	43, 47	oveq12d 7469	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) · ((exp‘(i · 𝐴)) − (2 · (i · (sin‘𝐴))))) = (((cos‘𝐴) + (i · (sin‘𝐴))) · ((cos‘𝐴) − (i · (sin‘𝐴)))))
49		mulcl 11323	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ) → (2 · (i · (sin‘𝐴))) ∈ ℂ)
50	22, 7, 49	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (2 · (i · (sin‘𝐴))) ∈ ℂ)
51	12, 12, 50	subdid 11811	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) · ((exp‘(i · 𝐴)) − (2 · (i · (sin‘𝐴))))) = (((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) − ((exp‘(i · 𝐴)) · (2 · (i · (sin‘𝐴))))))
52	48, 51	eqtr3d 2800	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) · ((cos‘𝐴) − (i · (sin‘𝐴)))) = (((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) − ((exp‘(i · 𝐴)) · (2 · (i · (sin‘𝐴))))))
53	29, 41, 52	3eqtr3d 2806	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = (((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) − ((exp‘(i · 𝐴)) · (2 · (i · (sin‘𝐴))))))
54		sincossq 16388	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = 1)
55	54	adantr 486	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = 1)
56	25, 53, 55	3eqtr2d 2804	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴))↑2) − (2 · ((exp‘(i · 𝐴)) · (i · (sin‘𝐴))))) = 1)
57	56, 36	oveq12d 7469	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((((exp‘(i · 𝐴))↑2) − (2 · ((exp‘(i · 𝐴)) · (i · (sin‘𝐴))))) + ((i · (sin‘𝐴))↑2)) = (1 + -((sin‘𝐴)↑2)))
58		negsub 11645	. . . . . . . . . 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 2802	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))↑2) = (1 − ((sin‘𝐴)↑2)))
61		halfre 12599	. . . . . . . . . . . 12 ⊢ (1 / 2) ∈ ℝ
62	61	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (1 / 2) ∈ ℝ)
63		negicn 11597	. . . . . . . . . . . . . . 15 ⊢ -i ∈ ℂ
64		mulcl 11323	. . . . . . . . . . . . . . 15 ⊢ (( -i ∈ ℂ ∧ 𝐴 ∈ ℂ) → ( -i · 𝐴) ∈ ℂ)
65	63, 8, 64	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ( -i · 𝐴) ∈ ℂ)
66		efcl 16292	. . . . . . . . . . . . . 14 ⊢ (( -i · 𝐴) ∈ ℂ → (exp‘( -i · 𝐴)) ∈ ℂ)
67	65, 66	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (exp‘( -i · 𝐴)) ∈ ℂ)
68	12, 67	addcld 11367	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))) ∈ ℂ)
69	68	recld 15404	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴)))) ∈ ℝ)
70		halfgt0 12601	. . . . . . . . . . . 12 ⊢ 0 < (1 / 2)
71	70	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (1 / 2))
72	12	recld 15404	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(i · 𝐴))) ∈ ℝ)
73	67	recld 15404	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘(exp‘( -i · 𝐴))) ∈ ℝ)
74		asinsinlem 27276	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i · 𝐴))))
75		negcl 11596	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
76	75	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -𝐴 ∈ ℂ)
77		reneg 15335	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (ℜ‘ -𝐴) = -(ℜ‘𝐴))
78	77	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘ -𝐴) = -(ℜ‘𝐴))
79		halfpire 26850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (π / 2) ∈ ℝ
80	79	renegcli 11658	. . . . . . . . . . . . . . . . . . 19 ⊢ -(π / 2) ∈ ℝ
81		recl 15320	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
82		iooneg 13642	. . . . . . . . . . . . . . . . . . 19 ⊢ (( -(π / 2) ∈ ℝ ∧ (π / 2) ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → ((ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2)) ↔ -(ℜ‘𝐴) ∈ ( -(π / 2)(,) - -(π / 2))))
83	80, 79, 81, 82	mp3an12i 1495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2)) ↔ -(ℜ‘𝐴) ∈ ( -(π / 2)(,) - -(π / 2))))
84	83	biimpa 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -(ℜ‘𝐴) ∈ ( -(π / 2)(,) - -(π / 2)))
85	79	recni 11362	. . . . . . . . . . . . . . . . . . 19 ⊢ (π / 2) ∈ ℂ
86	85	negnegi 11667	. . . . . . . . . . . . . . . . . 18 ⊢ - -(π / 2) = (π / 2)
87	86	oveq2i 7462	. . . . . . . . . . . . . . . . 17 ⊢ ( -(π / 2)(,) - -(π / 2)) = ( -(π / 2)(,)(π / 2))
88	84, 87	eleqtrdi 2874	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -(ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2)))
89	78, 88	eqeltrd 2864	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘ -𝐴) ∈ ( -(π / 2)(,)(π / 2)))
90		asinsinlem 27276	. . . . . . . . . . . . . . 15 ⊢ (( -𝐴 ∈ ℂ ∧ (ℜ‘ -𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i · -𝐴))))
91	76, 89, 90	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i · -𝐴))))
92		mulneg12 11793	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → ( -i · 𝐴) = (i · -𝐴))
93	5, 8, 92	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ( -i · 𝐴) = (i · -𝐴))
94	93	fveq2d 6920	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (exp‘( -i · 𝐴)) = (exp‘(i · -𝐴)))
95	94	fveq2d 6920	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘(exp‘( -i · 𝐴))) = (ℜ‘(exp‘(i · -𝐴))))
96	91, 95	breqtrrd 5139	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘( -i · 𝐴))))
97	72, 73, 74, 96	addgt0d 11931	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < ((ℜ‘(exp‘(i · 𝐴))) + (ℜ‘(exp‘( -i · 𝐴)))))
98	12, 67	readdd 15424	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴)))) = ((ℜ‘(exp‘(i · 𝐴))) + (ℜ‘(exp‘( -i · 𝐴)))))
99	97, 98	breqtrrd 5139	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴)))))
100	62, 69, 71, 99	mulgt0d 11504	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < ((1 / 2) · (ℜ‘((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))))))
101		cosval 16335	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) = (((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))) / 2))
102	101	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (cos‘𝐴) = (((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))) / 2))
103		2ne0 12489	. . . . . . . . . . . . . . 15 ⊢ 2 ≠ 0
104	103	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 2 ≠ 0)
105	68, 23, 104	divrec2d 12137	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))) / 2) = ((1 / 2) · ((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴)))))
106	102, 105	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (cos‘𝐴) = ((1 / 2) · ((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴)))))
107	106	fveq2d 6920	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘(cos‘𝐴)) = (ℜ‘((1 / 2) · ((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))))))
108		remul2 15340	. . . . . . . . . . . 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 2798	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘(cos‘𝐴)) = ((1 / 2) · (ℜ‘((exp‘(i · 𝐴)) + (exp‘( -i · 𝐴))))))
111	100, 110	breqtrrd 5139	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘(cos‘𝐴)))
112	27, 7, 43	mvrraddd 11766	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (i · (sin‘𝐴))) = (cos‘𝐴))
113	112	fveq2d 6920	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))) = (ℜ‘(cos‘𝐴)))
114	111, 113	breqtrrd 5139	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → 0 < (ℜ‘((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))))
115	14, 18, 60, 114	eqsqrt2d 15580	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (i · (sin‘𝐴))) = (√‘(1 − ((sin‘𝐴)↑2))))
116	115	oveq2d 7467	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) + ((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))) = ((i · (sin‘𝐴)) + (√‘(1 − ((sin‘𝐴)↑2)))))
117	13, 116	eqtr3d 2800	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((i · (sin‘𝐴)) + (√‘(1 − ((sin‘𝐴)↑2)))))
118	117	fveq2d 6920	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (log‘(exp‘(i · 𝐴))) = (log‘((i · (sin‘𝐴)) + (√‘(1 − ((sin‘𝐴)↑2))))))
119		pire 26840	. . . . . . . . . 10 ⊢ π ∈ ℝ
120	119	renegcli 11658	. . . . . . . . 9 ⊢ -π ∈ ℝ
121	120	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -π ∈ ℝ)
122	80	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -(π / 2) ∈ ℝ)
123		elioore 13546	. . . . . . . . 9 ⊢ ((ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2)) → (ℜ‘𝐴) ∈ ℝ)
124	123	adantl 487	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ)
125		pirp 26847	. . . . . . . . . . 11 ⊢ π ∈ ℝ⁺
126		rphalflt 13191	. . . . . . . . . . 11 ⊢ (π ∈ ℝ⁺ → (π / 2) < π)
127	125, 126	ax-mp 5	. . . . . . . . . 10 ⊢ (π / 2) < π
128	79, 119	ltnegi 11900	. . . . . . . . . 10 ⊢ ((π / 2) < π ↔ -π < -(π / 2))
129	127, 128	mpbi 233	. . . . . . . . 9 ⊢ -π < -(π / 2)
130	129	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -π < -(π / 2))
131		eliooord 13576	. . . . . . . . . 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 11510	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → -π < (ℜ‘𝐴))
135		imre 15318	. . . . . . . . 9 ⊢ ((i · 𝐴) ∈ ℂ → (ℑ‘(i · 𝐴)) = (ℜ‘( -i · (i · 𝐴))))
136	10, 135	syl 18	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘( -i · (i · 𝐴))))
137	5, 5	mulneg1i 11801	. . . . . . . . . . . 12 ⊢ ( -i · i) = -(i · i)
138		ixi 11985	. . . . . . . . . . . . 13 ⊢ (i · i) = -1
139	138	negeqi 11589	. . . . . . . . . . . 12 ⊢ -(i · i) = - -1
140	15	negnegi 11667	. . . . . . . . . . . 12 ⊢ - -1 = 1
141	137, 139, 140	3eqtri 2790	. . . . . . . . . . 11 ⊢ ( -i · i) = 1
142	141	oveq1i 7461	. . . . . . . . . 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 11371	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (( -i · i) · 𝐴) = ( -i · (i · 𝐴)))
146		mullid 11346	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
147	146	adantr 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (1 · 𝐴) = 𝐴)
148	142, 145, 147	3eqtr3a 2822	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ( -i · (i · 𝐴)) = 𝐴)
149	148	fveq2d 6920	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘( -i · (i · 𝐴))) = (ℜ‘𝐴))
150	136, 149	eqtrd 2798	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘𝐴))
151	134, 150	breqtrrd 5139	. . . . . 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 11510	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘𝐴) < π)
157	124, 152, 156	ltled 11497	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ≤ π)
158	150, 157	eqbrtrd 5133	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) ≤ π)
159		ellogrn 26944	. . . . . 6 ⊢ ((i · 𝐴) ∈ ran log ↔ ((i · 𝐴) ∈ ℂ ∧ -π < (ℑ‘(i · 𝐴)) ∧ (ℑ‘(i · 𝐴)) ≤ π))
160	10, 151, 158, 159	syl3anbrc 1362	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ran log)
161		logef 26966	. . . . 5 ⊢ ((i · 𝐴) ∈ ran log → (log‘(exp‘(i · 𝐴))) = (i · 𝐴))
162	160, 161	syl 18	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (log‘(exp‘(i · 𝐴))) = (i · 𝐴))
163	118, 162	eqtr3d 2800	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (log‘((i · (sin‘𝐴)) + (√‘(1 − ((sin‘𝐴)↑2))))) = (i · 𝐴))
164	163	oveq2d 7467	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → ( -i · (log‘((i · (sin‘𝐴)) + (√‘(1 − ((sin‘𝐴)↑2)))))) = ( -i · (i · 𝐴)))
165	4, 164, 148	3eqtrd 2802	1 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ( -(π / 2)(,)(π / 2))) → (arcsin‘(sin‘𝐴)) = 𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 class class class wbr 5108 ran crn 5659 ‘cfv 6566 (class class class)co 7451 ℂcc 11237 ℝcr 11238 0cc0 11239 1c1 11240 ici 11241 + caddc 11242 · cmul 11244 < clt 11382 ≤ cle 11383 − cmin 11580 -cneg 11581 / cdiv 12013 2c2 12437 ℝ⁺crp 13160 (,)cioo 13516 ↑cexp 14244 ℜcre 15307 ℑcim 15308 √csqrt 15443 expce 16271 sincsin 16273 cosccos 16274 πcpi 16276 logclog 26939 arcsincasin 27247

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-inf2 9679 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317 ax-addf 11318

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-of 7725 df-om 7912 df-1st 8035 df-2nd 8036 df-supp 8215 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-2o 8515 df-er 8755 df-map 8887 df-pm 8888 df-ixp 8964 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-fsupp 9392 df-fi 9440 df-sup 9471 df-inf 9472 df-oi 9541 df-card 10057 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-7 12450 df-8 12451 df-9 12452 df-n0 12647 df-z 12734 df-dec 12855 df-uz 13006 df-q 13116 df-rp 13161 df-xneg 13281 df-xadd 13282 df-xmul 13283 df-ioo 13520 df-ioc 13521 df-ico 13522 df-icc 13523 df-fz 13680 df-fzo 13829 df-fl 13972 df-mod 14050 df-seq 14185 df-exp 14245 df-fac 14459 df-bc 14488 df-hash 14516 df-shft 15263 df-cj 15309 df-re 15310 df-im 15311 df-sqrt 15445 df-abs 15446 df-limsup 15682 df-clim 15699 df-rlim 15700 df-sum 15898 df-ef 16277 df-sin 16279 df-cos 16280 df-pi 16282 df-struct 17369 df-sets 17386 df-slot 17404 df-ndx 17416 df-base 17432 df-ress 17453 df-plusg 17486 df-mulr 17487 df-starv 17488 df-sca 17489 df-vsca 17490 df-ip 17491 df-tset 17492 df-ple 17493 df-ds 17495 df-unif 17496 df-hom 17497 df-cco 17498 df-euf 17499 df-rest 17643 df-topn 17644 df-0g 17662 df-gsum 17663 df-topgen 17664 df-pt 17665 df-prds 17668 df-xrs 17724 df-qtop 17729 df-imas 17730 df-xps 17732 df-mre 17806 df-mrc 17807 df-acs 17809 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-submnd 19029 df-mulg 19328 df-cntz 19582 df-cmn 20047 df-psmet 21721 df-xmet 21722 df-met 21723 df-bl 21724 df-mopn 21725 df-fbas 21726 df-fg 21727 df-cnfld 21730 df-top 23267 df-topon 23284 df-topsp 23306 df-bases 23319 df-cld 23392 df-ntr 23393 df-cls 23394 df-nei 23471 df-lp 23509 df-perf 23510 df-cn 23600 df-cnp 23601 df-haus 23688 df-tx 23936 df-hmeo 24129 df-fil 24220 df-fm 24312 df-flim 24313 df-flf 24314 df-xms 24694 df-ms 24695 df-tms 24696 df-cncf 25254 df-limc 26241 df-dv 26242 df-log 26941 df-asin 27250

This theorem is used by: acoscos 27278 reasinsin 27281 asinsinb 27282

W3C validator