recosf1o

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

		Ref	Expression
	Assertion	recosf1o	$⊢ ({\cos ↾}_{[0, π]}) : [0, π] \underset{1-1 onto}{⟶} [- 1, 1]$

Proof

Step	Hyp	Ref	Expression
1		cosf	$⊢ \cos : ℂ ⟶ ℂ$
2		ffn	$⊢ \cos : ℂ ⟶ ℂ \to \cos Fn ℂ$
3	1 2	ax-mp	$⊢ \cos Fn ℂ$
4		0re	$⊢ 0 \in ℝ$
5		pire	$⊢ π \in ℝ$
6		iccssre	$⊢ (0 \in ℝ \land π \in ℝ) \to [0, π] \subseteq ℝ$
7	4 5 6	mp2an	$⊢ [0, π] \subseteq ℝ$
8		ax-resscn	$⊢ ℝ \subseteq ℂ$
9	7 8	sstri	$⊢ [0, π] \subseteq ℂ$
10		fnssres	$⊢ (\cos Fn ℂ \land [0, π] \subseteq ℂ) \to ({\cos ↾}_{[0, π]}) Fn [0, π]$
11	3 9 10	mp2an	$⊢ ({\cos ↾}_{[0, π]}) Fn [0, π]$
12		fvres	$⊢ x \in [0, π] \to ({\cos ↾}_{[0, π]}) (x) = \cos x$
13	7	sseli	$⊢ x \in [0, π] \to x \in ℝ$
14		cosbnd2	$⊢ x \in ℝ \to \cos x \in [- 1, 1]$
15	13 14	syl	$⊢ x \in [0, π] \to \cos x \in [- 1, 1]$
16	12 15	eqeltrd	$⊢ x \in [0, π] \to ({\cos ↾}_{[0, π]}) (x) \in [- 1, 1]$
17	16	rgen	$⊢ \forall x \in [0, π] ({\cos ↾}_{[0, π]}) (x) \in [- 1, 1]$
18		ffnfv	$⊢ ({\cos ↾}_{[0, π]}) : [0, π] ⟶ [- 1, 1] \leftrightarrow (({\cos ↾}_{[0, π]}) Fn [0, π] \land \forall x \in [0, π] ({\cos ↾}_{[0, π]}) (x) \in [- 1, 1])$
19	11 17 18	mpbir2an	$⊢ ({\cos ↾}_{[0, π]}) : [0, π] ⟶ [- 1, 1]$
20		fvres	$⊢ y \in [0, π] \to ({\cos ↾}_{[0, π]}) (y) = \cos y$
21	12 20	eqeqan12d	$⊢ (x \in [0, π] \land y \in [0, π]) \to (({\cos ↾}_{[0, π]}) (x) = ({\cos ↾}_{[0, π]}) (y) \leftrightarrow \cos x = \cos y)$
22		cos11	$⊢ (x \in [0, π] \land y \in [0, π]) \to (x = y \leftrightarrow \cos x = \cos y)$
23	22	biimprd	$⊢ (x \in [0, π] \land y \in [0, π]) \to (\cos x = \cos y \to x = y)$
24	21 23	sylbid	$⊢ (x \in [0, π] \land y \in [0, π]) \to (({\cos ↾}_{[0, π]}) (x) = ({\cos ↾}_{[0, π]}) (y) \to x = y)$
25	24	rgen2	$⊢ \forall x \in [0, π] \forall y \in [0, π] (({\cos ↾}_{[0, π]}) (x) = ({\cos ↾}_{[0, π]}) (y) \to x = y)$
26		dff13	$⊢ ({\cos ↾}_{[0, π]}) : [0, π] \underset{1-1}{⟶} [- 1, 1] \leftrightarrow (({\cos ↾}_{[0, π]}) : [0, π] ⟶ [- 1, 1] \land \forall x \in [0, π] \forall y \in [0, π] (({\cos ↾}_{[0, π]}) (x) = ({\cos ↾}_{[0, π]}) (y) \to x = y))$
27	19 25 26	mpbir2an	$⊢ ({\cos ↾}_{[0, π]}) : [0, π] \underset{1-1}{⟶} [- 1, 1]$
28	4	a1i	$⊢ x \in [- 1, 1] \to 0 \in ℝ$
29	5	a1i	$⊢ x \in [- 1, 1] \to π \in ℝ$
30		neg1rr	$⊢ - 1 \in ℝ$
31		1re	$⊢ 1 \in ℝ$
32	30 31	elicc2i	$⊢ x \in [- 1, 1] \leftrightarrow (x \in ℝ \land - 1 \leq x \land x \leq 1)$
33	32	simp1bi	$⊢ x \in [- 1, 1] \to x \in ℝ$
34		pipos	$⊢ 0 < π$
35	34	a1i	$⊢ x \in [- 1, 1] \to 0 < π$
36	9	a1i	$⊢ x \in [- 1, 1] \to [0, π] \subseteq ℂ$
37		coscn	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ$
38	37	a1i	$⊢ x \in [- 1, 1] \to \cos : ℂ \underset{cn}{⟶} ℂ$
39	7	sseli	$⊢ z \in [0, π] \to z \in ℝ$
40	39	recoscld	$⊢ z \in [0, π] \to \cos z \in ℝ$
41	40	adantl	$⊢ (x \in [- 1, 1] \land z \in [0, π]) \to \cos z \in ℝ$
42		cospi	$⊢ \cos π = - 1$
43	32	simp2bi	$⊢ x \in [- 1, 1] \to - 1 \leq x$
44	42 43	eqbrtrid	$⊢ x \in [- 1, 1] \to \cos π \leq x$
45	32	simp3bi	$⊢ x \in [- 1, 1] \to x \leq 1$
46		cos0	$⊢ \cos 0 = 1$
47	45 46	breqtrrdi	$⊢ x \in [- 1, 1] \to x \leq \cos 0$
48	44 47	jca	$⊢ x \in [- 1, 1] \to (\cos π \leq x \land x \leq \cos 0)$
49	28 29 33 35 36 38 41 48	ivthle2	$⊢ x \in [- 1, 1] \to \exists y \in [0, π] \cos y = x$
50		eqcom	$⊢ x = ({\cos ↾}_{[0, π]}) (y) \leftrightarrow ({\cos ↾}_{[0, π]}) (y) = x$
51	20	eqeq1d	$⊢ y \in [0, π] \to (({\cos ↾}_{[0, π]}) (y) = x \leftrightarrow \cos y = x)$
52	50 51	bitrid	$⊢ y \in [0, π] \to (x = ({\cos ↾}_{[0, π]}) (y) \leftrightarrow \cos y = x)$
53	52	rexbiia	$⊢ \exists y \in [0, π] x = ({\cos ↾}_{[0, π]}) (y) \leftrightarrow \exists y \in [0, π] \cos y = x$
54	49 53	sylibr	$⊢ x \in [- 1, 1] \to \exists y \in [0, π] x = ({\cos ↾}_{[0, π]}) (y)$
55	54	rgen	$⊢ \forall x \in [- 1, 1] \exists y \in [0, π] x = ({\cos ↾}_{[0, π]}) (y)$
56		dffo3	$⊢ ({\cos ↾}_{[0, π]}) : [0, π] \underset{onto}{⟶} [- 1, 1] \leftrightarrow (({\cos ↾}_{[0, π]}) : [0, π] ⟶ [- 1, 1] \land \forall x \in [- 1, 1] \exists y \in [0, π] x = ({\cos ↾}_{[0, π]}) (y))$
57	19 55 56	mpbir2an	$⊢ ({\cos ↾}_{[0, π]}) : [0, π] \underset{onto}{⟶} [- 1, 1]$
58		df-f1o	$⊢ ({\cos ↾}_{[0, π]}) : [0, π] \underset{1-1 onto}{⟶} [- 1, 1] \leftrightarrow (({\cos ↾}_{[0, π]}) : [0, π] \underset{1-1}{⟶} [- 1, 1] \land ({\cos ↾}_{[0, π]}) : [0, π] \underset{onto}{⟶} [- 1, 1])$
59	27 57 58	mpbir2an	$⊢ ({\cos ↾}_{[0, π]}) : [0, π] \underset{1-1 onto}{⟶} [- 1, 1]$

Metamath Proof Explorer

Theorem recosf1o

Proof