Metamath Proof Explorer

Theorem 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 π ⟶ 1-1 onto − 1 1

Proof

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