resinf1o

Description: The sine function is a bijection when restricted to its principal domain. (Contributed by Mario Carneiro, 12-May-2014)

		Ref	Expression
	Assertion	resinf1o	$⊢ ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1]$

Proof

Step	Hyp	Ref	Expression
1		recosf1o	$⊢ ({\cos ↾}_{[0, π]}) : [0, π] \underset{1-1 onto}{⟶} [- 1, 1]$
2		eqid	$⊢ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) = (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)$
3		halfpire	$⊢ \frac{π}{2} \in ℝ$
4		neghalfpire	$⊢ - \frac{π}{2} \in ℝ$
5		iccssre	$⊢ (- \frac{π}{2} \in ℝ \land \frac{π}{2} \in ℝ) \to [- \frac{π}{2}, \frac{π}{2}] \subseteq ℝ$
6	4 3 5	mp2an	$⊢ [- \frac{π}{2}, \frac{π}{2}] \subseteq ℝ$
7	6	sseli	$⊢ x \in [- \frac{π}{2}, \frac{π}{2}] \to x \in ℝ$
8		resubcl	$⊢ (\frac{π}{2} \in ℝ \land x \in ℝ) \to (\frac{π}{2}) - x \in ℝ$
9	3 7 8	sylancr	$⊢ x \in [- \frac{π}{2}, \frac{π}{2}] \to (\frac{π}{2}) - x \in ℝ$
10	4 3	elicc2i	$⊢ x \in [- \frac{π}{2}, \frac{π}{2}] \leftrightarrow (x \in ℝ \land - \frac{π}{2} \leq x \land x \leq \frac{π}{2})$
11	10	simp3bi	$⊢ x \in [- \frac{π}{2}, \frac{π}{2}] \to x \leq \frac{π}{2}$
12		subge0	$⊢ (\frac{π}{2} \in ℝ \land x \in ℝ) \to (0 \leq (\frac{π}{2}) - x \leftrightarrow x \leq \frac{π}{2})$
13	3 7 12	sylancr	$⊢ x \in [- \frac{π}{2}, \frac{π}{2}] \to (0 \leq (\frac{π}{2}) - x \leftrightarrow x \leq \frac{π}{2})$
14	11 13	mpbird	$⊢ x \in [- \frac{π}{2}, \frac{π}{2}] \to 0 \leq (\frac{π}{2}) - x$
15	3	recni	$⊢ \frac{π}{2} \in ℂ$
16		picn	$⊢ π \in ℂ$
17	15	negcli	$⊢ - \frac{π}{2} \in ℂ$
18	16 15	negsubi	$⊢ π + (- \frac{π}{2}) = π - (\frac{π}{2})$
19		pidiv2halves	$⊢ (\frac{π}{2}) + (\frac{π}{2}) = π$
20	16 15 15 19	subaddrii	$⊢ π - (\frac{π}{2}) = \frac{π}{2}$
21	18 20	eqtri	$⊢ π + (- \frac{π}{2}) = \frac{π}{2}$
22	15 16 17 21	subaddrii	$⊢ (\frac{π}{2}) - π = - \frac{π}{2}$
23	10	simp2bi	$⊢ x \in [- \frac{π}{2}, \frac{π}{2}] \to - \frac{π}{2} \leq x$
24	22 23	eqbrtrid	$⊢ x \in [- \frac{π}{2}, \frac{π}{2}] \to (\frac{π}{2}) - π \leq x$
25		pire	$⊢ π \in ℝ$
26		suble	$⊢ (\frac{π}{2} \in ℝ \land π \in ℝ \land x \in ℝ) \to ((\frac{π}{2}) - π \leq x \leftrightarrow (\frac{π}{2}) - x \leq π)$
27	3 25 7 26	mp3an12i	$⊢ x \in [- \frac{π}{2}, \frac{π}{2}] \to ((\frac{π}{2}) - π \leq x \leftrightarrow (\frac{π}{2}) - x \leq π)$
28	24 27	mpbid	$⊢ x \in [- \frac{π}{2}, \frac{π}{2}] \to (\frac{π}{2}) - x \leq π$
29		0re	$⊢ 0 \in ℝ$
30	29 25	elicc2i	$⊢ (\frac{π}{2}) - x \in [0, π] \leftrightarrow ((\frac{π}{2}) - x \in ℝ \land 0 \leq (\frac{π}{2}) - x \land (\frac{π}{2}) - x \leq π)$
31	9 14 28 30	syl3anbrc	$⊢ x \in [- \frac{π}{2}, \frac{π}{2}] \to (\frac{π}{2}) - x \in [0, π]$
32	31	adantl	$⊢ (⊤ \land x \in [- \frac{π}{2}, \frac{π}{2}]) \to (\frac{π}{2}) - x \in [0, π]$
33	29 25	elicc2i	$⊢ y \in [0, π] \leftrightarrow (y \in ℝ \land 0 \leq y \land y \leq π)$
34	33	simp1bi	$⊢ y \in [0, π] \to y \in ℝ$
35		resubcl	$⊢ (\frac{π}{2} \in ℝ \land y \in ℝ) \to (\frac{π}{2}) - y \in ℝ$
36	3 34 35	sylancr	$⊢ y \in [0, π] \to (\frac{π}{2}) - y \in ℝ$
37	33	simp3bi	$⊢ y \in [0, π] \to y \leq π$
38	15 15	subnegi	$⊢ (\frac{π}{2}) - (- \frac{π}{2}) = (\frac{π}{2}) + (\frac{π}{2})$
39	38 19	eqtri	$⊢ (\frac{π}{2}) - (- \frac{π}{2}) = π$
40	37 39	breqtrrdi	$⊢ y \in [0, π] \to y \leq (\frac{π}{2}) - (- \frac{π}{2})$
41		lesub	$⊢ (y \in ℝ \land \frac{π}{2} \in ℝ \land - \frac{π}{2} \in ℝ) \to (y \leq (\frac{π}{2}) - (- \frac{π}{2}) \leftrightarrow - \frac{π}{2} \leq (\frac{π}{2}) - y)$
42	3 4 41	mp3an23	$⊢ y \in ℝ \to (y \leq (\frac{π}{2}) - (- \frac{π}{2}) \leftrightarrow - \frac{π}{2} \leq (\frac{π}{2}) - y)$
43	34 42	syl	$⊢ y \in [0, π] \to (y \leq (\frac{π}{2}) - (- \frac{π}{2}) \leftrightarrow - \frac{π}{2} \leq (\frac{π}{2}) - y)$
44	40 43	mpbid	$⊢ y \in [0, π] \to - \frac{π}{2} \leq (\frac{π}{2}) - y$
45	15	subidi	$⊢ (\frac{π}{2}) - (\frac{π}{2}) = 0$
46	33	simp2bi	$⊢ y \in [0, π] \to 0 \leq y$
47	45 46	eqbrtrid	$⊢ y \in [0, π] \to (\frac{π}{2}) - (\frac{π}{2}) \leq y$
48		suble	$⊢ (\frac{π}{2} \in ℝ \land \frac{π}{2} \in ℝ \land y \in ℝ) \to ((\frac{π}{2}) - (\frac{π}{2}) \leq y \leftrightarrow (\frac{π}{2}) - y \leq \frac{π}{2})$
49	3 3 34 48	mp3an12i	$⊢ y \in [0, π] \to ((\frac{π}{2}) - (\frac{π}{2}) \leq y \leftrightarrow (\frac{π}{2}) - y \leq \frac{π}{2})$
50	47 49	mpbid	$⊢ y \in [0, π] \to (\frac{π}{2}) - y \leq \frac{π}{2}$
51	4 3	elicc2i	$⊢ (\frac{π}{2}) - y \in [- \frac{π}{2}, \frac{π}{2}] \leftrightarrow ((\frac{π}{2}) - y \in ℝ \land - \frac{π}{2} \leq (\frac{π}{2}) - y \land (\frac{π}{2}) - y \leq \frac{π}{2})$
52	36 44 50 51	syl3anbrc	$⊢ y \in [0, π] \to (\frac{π}{2}) - y \in [- \frac{π}{2}, \frac{π}{2}]$
53	52	adantl	$⊢ (⊤ \land y \in [0, π]) \to (\frac{π}{2}) - y \in [- \frac{π}{2}, \frac{π}{2}]$
54		iccssre	$⊢ (0 \in ℝ \land π \in ℝ) \to [0, π] \subseteq ℝ$
55	29 25 54	mp2an	$⊢ [0, π] \subseteq ℝ$
56		ax-resscn	$⊢ ℝ \subseteq ℂ$
57	55 56	sstri	$⊢ [0, π] \subseteq ℂ$
58	57	sseli	$⊢ y \in [0, π] \to y \in ℂ$
59	6 56	sstri	$⊢ [- \frac{π}{2}, \frac{π}{2}] \subseteq ℂ$
60	59	sseli	$⊢ x \in [- \frac{π}{2}, \frac{π}{2}] \to x \in ℂ$
61		subsub23	$⊢ (\frac{π}{2} \in ℂ \land y \in ℂ \land x \in ℂ) \to ((\frac{π}{2}) - y = x \leftrightarrow (\frac{π}{2}) - x = y)$
62	15 61	mp3an1	$⊢ (y \in ℂ \land x \in ℂ) \to ((\frac{π}{2}) - y = x \leftrightarrow (\frac{π}{2}) - x = y)$
63	58 60 62	syl2anr	$⊢ (x \in [- \frac{π}{2}, \frac{π}{2}] \land y \in [0, π]) \to ((\frac{π}{2}) - y = x \leftrightarrow (\frac{π}{2}) - x = y)$
64	63	adantl	$⊢ (⊤ \land (x \in [- \frac{π}{2}, \frac{π}{2}] \land y \in [0, π])) \to ((\frac{π}{2}) - y = x \leftrightarrow (\frac{π}{2}) - x = y)$
65		eqcom	$⊢ x = (\frac{π}{2}) - y \leftrightarrow (\frac{π}{2}) - y = x$
66		eqcom	$⊢ y = (\frac{π}{2}) - x \leftrightarrow (\frac{π}{2}) - x = y$
67	64 65 66	3bitr4g	$⊢ (⊤ \land (x \in [- \frac{π}{2}, \frac{π}{2}] \land y \in [0, π])) \to (x = (\frac{π}{2}) - y \leftrightarrow y = (\frac{π}{2}) - x)$
68	2 32 53 67	f1o2d	$⊢ ⊤ \to (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [0, π]$
69	68	mptru	$⊢ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [0, π]$
70		f1oco	$⊢ (({\cos ↾}_{[0, π]}) : [0, π] \underset{1-1 onto}{⟶} [- 1, 1] \land (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [0, π]) \to (({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1]$
71	1 69 70	mp2an	$⊢ (({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1]$
72		cosf	$⊢ \cos : ℂ ⟶ ℂ$
73		ffn	$⊢ \cos : ℂ ⟶ ℂ \to \cos Fn ℂ$
74	72 73	ax-mp	$⊢ \cos Fn ℂ$
75		fnssres	$⊢ (\cos Fn ℂ \land [0, π] \subseteq ℂ) \to ({\cos ↾}_{[0, π]}) Fn [0, π]$
76	74 57 75	mp2an	$⊢ ({\cos ↾}_{[0, π]}) Fn [0, π]$
77	2 31	fmpti	$⊢ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) : [- \frac{π}{2}, \frac{π}{2}] ⟶ [0, π]$
78		fnfco	$⊢ (({\cos ↾}_{[0, π]}) Fn [0, π] \land (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) : [- \frac{π}{2}, \frac{π}{2}] ⟶ [0, π]) \to (({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)) Fn [- \frac{π}{2}, \frac{π}{2}]$
79	76 77 78	mp2an	$⊢ (({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)) Fn [- \frac{π}{2}, \frac{π}{2}]$
80		sinf	$⊢ \sin : ℂ ⟶ ℂ$
81		ffn	$⊢ \sin : ℂ ⟶ ℂ \to \sin Fn ℂ$
82	80 81	ax-mp	$⊢ \sin Fn ℂ$
83		fnssres	$⊢ (\sin Fn ℂ \land [- \frac{π}{2}, \frac{π}{2}] \subseteq ℂ) \to ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) Fn [- \frac{π}{2}, \frac{π}{2}]$
84	82 59 83	mp2an	$⊢ ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) Fn [- \frac{π}{2}, \frac{π}{2}]$
85		eqfnfv	$⊢ ((({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)) Fn [- \frac{π}{2}, \frac{π}{2}] \land ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) Fn [- \frac{π}{2}, \frac{π}{2}]) \to (({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) = {\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]} \leftrightarrow \forall y \in [- \frac{π}{2}, \frac{π}{2}] (({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)) (y) = ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) (y))$
86	79 84 85	mp2an	$⊢ ({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) = {\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]} \leftrightarrow \forall y \in [- \frac{π}{2}, \frac{π}{2}] (({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)) (y) = ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) (y)$
87	77	ffvelcdmi	$⊢ y \in [- \frac{π}{2}, \frac{π}{2}] \to (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) (y) \in [0, π]$
88	87	fvresd	$⊢ y \in [- \frac{π}{2}, \frac{π}{2}] \to ({\cos ↾}_{[0, π]}) ((x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) (y)) = \cos (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) (y)$
89		oveq2	$⊢ x = y \to (\frac{π}{2}) - x = (\frac{π}{2}) - y$
90		ovex	$⊢ (\frac{π}{2}) - y \in V$
91	89 2 90	fvmpt	$⊢ y \in [- \frac{π}{2}, \frac{π}{2}] \to (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) (y) = (\frac{π}{2}) - y$
92	91	fveq2d	$⊢ y \in [- \frac{π}{2}, \frac{π}{2}] \to \cos (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) (y) = \cos ((\frac{π}{2}) - y)$
93	59	sseli	$⊢ y \in [- \frac{π}{2}, \frac{π}{2}] \to y \in ℂ$
94		coshalfpim	$⊢ y \in ℂ \to \cos ((\frac{π}{2}) - y) = \sin y$
95	93 94	syl	$⊢ y \in [- \frac{π}{2}, \frac{π}{2}] \to \cos ((\frac{π}{2}) - y) = \sin y$
96	88 92 95	3eqtrd	$⊢ y \in [- \frac{π}{2}, \frac{π}{2}] \to ({\cos ↾}_{[0, π]}) ((x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) (y)) = \sin y$
97		fvco3	$⊢ ((x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) : [- \frac{π}{2}, \frac{π}{2}] ⟶ [0, π] \land y \in [- \frac{π}{2}, \frac{π}{2}]) \to (({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)) (y) = ({\cos ↾}_{[0, π]}) ((x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) (y))$
98	77 97	mpan	$⊢ y \in [- \frac{π}{2}, \frac{π}{2}] \to (({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)) (y) = ({\cos ↾}_{[0, π]}) ((x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) (y))$
99		fvres	$⊢ y \in [- \frac{π}{2}, \frac{π}{2}] \to ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) (y) = \sin y$
100	96 98 99	3eqtr4d	$⊢ y \in [- \frac{π}{2}, \frac{π}{2}] \to (({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)) (y) = ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) (y)$
101	86 100	mprgbir	$⊢ ({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) = {\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}$
102		f1oeq1	$⊢ ({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x) = {\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]} \to ((({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1] \leftrightarrow ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1])$
103	101 102	ax-mp	$⊢ (({\cos ↾}_{[0, π]}) \circ (x \in [- \frac{π}{2}, \frac{π}{2}] ⟼ (\frac{π}{2}) - x)) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1] \leftrightarrow ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1]$
104	71 103	mpbi	$⊢ ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1]$

Metamath Proof Explorer

Theorem resinf1o

Proof