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 ⊢ ( 𝑥 ∈ ( 0 [,] π ) → ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑥 ) = ( cos ‘ 𝑥 ) )
13 7 sseli ⊢ ( 𝑥 ∈ ( 0 [,] π ) → 𝑥 ∈ ℝ )
14 cosbnd2 ⊢ ( 𝑥 ∈ ℝ → ( cos ‘ 𝑥 ) ∈ ( - 1 [,] 1 ) )
15 13 14 syl ⊢ ( 𝑥 ∈ ( 0 [,] π ) → ( cos ‘ 𝑥 ) ∈ ( - 1 [,] 1 ) )
16 12 15 eqeltrd ⊢ ( 𝑥 ∈ ( 0 [,] π ) → ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑥 ) ∈ ( - 1 [,] 1 ) )
17 16 rgen ⊢ ∀ 𝑥 ∈ ( 0 [,] π ) ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑥 ) ∈ ( - 1 [,] 1 )
18 ffnfv ⊢ ( ( cos ↾ ( 0 [,] π ) ) : ( 0 [,] π ) ⟶ ( - 1 [,] 1 ) ↔ ( ( cos ↾ ( 0 [,] π ) ) Fn ( 0 [,] π ) ∧ ∀ 𝑥 ∈ ( 0 [,] π ) ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑥 ) ∈ ( - 1 [,] 1 ) ) )
19 11 17 18 mpbir2an ⊢ ( cos ↾ ( 0 [,] π ) ) : ( 0 [,] π ) ⟶ ( - 1 [,] 1 )
20 fvres ⊢ ( 𝑦 ∈ ( 0 [,] π ) → ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 ) = ( cos ‘ 𝑦 ) )
21 12 20 eqeqan12d ⊢ ( ( 𝑥 ∈ ( 0 [,] π ) ∧ 𝑦 ∈ ( 0 [,] π ) ) → ( ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑥 ) = ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 ) ↔ ( cos ‘ 𝑥 ) = ( cos ‘ 𝑦 ) ) )
22 cos11 ⊢ ( ( 𝑥 ∈ ( 0 [,] π ) ∧ 𝑦 ∈ ( 0 [,] π ) ) → ( 𝑥 = 𝑦 ↔ ( cos ‘ 𝑥 ) = ( cos ‘ 𝑦 ) ) )
23 22 biimprd ⊢ ( ( 𝑥 ∈ ( 0 [,] π ) ∧ 𝑦 ∈ ( 0 [,] π ) ) → ( ( cos ‘ 𝑥 ) = ( cos ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
24 21 23 sylbid ⊢ ( ( 𝑥 ∈ ( 0 [,] π ) ∧ 𝑦 ∈ ( 0 [,] π ) ) → ( ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑥 ) = ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
25 24 rgen2 ⊢ ∀ 𝑥 ∈ ( 0 [,] π ) ∀ 𝑦 ∈ ( 0 [,] π ) ( ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑥 ) = ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 )
26 dff13 ⊢ ( ( cos ↾ ( 0 [,] π ) ) : ( 0 [,] π ) –1-1→ ( - 1 [,] 1 ) ↔ ( ( cos ↾ ( 0 [,] π ) ) : ( 0 [,] π ) ⟶ ( - 1 [,] 1 ) ∧ ∀ 𝑥 ∈ ( 0 [,] π ) ∀ 𝑦 ∈ ( 0 [,] π ) ( ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑥 ) = ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
27 19 25 26 mpbir2an ⊢ ( cos ↾ ( 0 [,] π ) ) : ( 0 [,] π ) –1-1→ ( - 1 [,] 1 )
28 4 a1i ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → 0 ∈ ℝ )
29 5 a1i ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → π ∈ ℝ )
30 neg1rr ⊢ - 1 ∈ ℝ
31 1re ⊢ 1 ∈ ℝ
32 30 31 elicc2i ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) ↔ ( 𝑥 ∈ ℝ ∧ - 1 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) )
33 32 simp1bi ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → 𝑥 ∈ ℝ )
34 pipos ⊢ 0 < π
35 34 a1i ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → 0 < π )
36 9 a1i ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → ( 0 [,] π ) ⊆ ℂ )
37 coscn ⊢ cos ∈ ( ℂ –cn→ ℂ )
38 37 a1i ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → cos ∈ ( ℂ –cn→ ℂ ) )
39 7 sseli ⊢ ( 𝑧 ∈ ( 0 [,] π ) → 𝑧 ∈ ℝ )
40 39 recoscld ⊢ ( 𝑧 ∈ ( 0 [,] π ) → ( cos ‘ 𝑧 ) ∈ ℝ )
41 40 adantl ⊢ ( ( 𝑥 ∈ ( - 1 [,] 1 ) ∧ 𝑧 ∈ ( 0 [,] π ) ) → ( cos ‘ 𝑧 ) ∈ ℝ )
42 cospi ⊢ ( cos ‘ π ) = - 1
43 32 simp2bi ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → - 1 ≤ 𝑥 )
44 42 43 eqbrtrid ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → ( cos ‘ π ) ≤ 𝑥 )
45 32 simp3bi ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → 𝑥 ≤ 1 )
46 cos0 ⊢ ( cos ‘ 0 ) = 1
47 45 46 breqtrrdi ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → 𝑥 ≤ ( cos ‘ 0 ) )
48 44 47 jca ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → ( ( cos ‘ π ) ≤ 𝑥 ∧ 𝑥 ≤ ( cos ‘ 0 ) ) )
49 28 29 33 35 36 38 41 48 ivthle2 ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → ∃ 𝑦 ∈ ( 0 [,] π ) ( cos ‘ 𝑦 ) = 𝑥 )
50 eqcom ⊢ ( 𝑥 = ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 ) ↔ ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 ) = 𝑥 )
51 20 eqeq1d ⊢ ( 𝑦 ∈ ( 0 [,] π ) → ( ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 ) = 𝑥 ↔ ( cos ‘ 𝑦 ) = 𝑥 ) )
52 50 51 syl5bb ⊢ ( 𝑦 ∈ ( 0 [,] π ) → ( 𝑥 = ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 ) ↔ ( cos ‘ 𝑦 ) = 𝑥 ) )
53 52 rexbiia ⊢ ( ∃ 𝑦 ∈ ( 0 [,] π ) 𝑥 = ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ ( 0 [,] π ) ( cos ‘ 𝑦 ) = 𝑥 )
54 49 53 sylibr ⊢ ( 𝑥 ∈ ( - 1 [,] 1 ) → ∃ 𝑦 ∈ ( 0 [,] π ) 𝑥 = ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 ) )
55 54 rgen ⊢ ∀ 𝑥 ∈ ( - 1 [,] 1 ) ∃ 𝑦 ∈ ( 0 [,] π ) 𝑥 = ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 )
56 dffo3 ⊢ ( ( cos ↾ ( 0 [,] π ) ) : ( 0 [,] π ) –onto→ ( - 1 [,] 1 ) ↔ ( ( cos ↾ ( 0 [,] π ) ) : ( 0 [,] π ) ⟶ ( - 1 [,] 1 ) ∧ ∀ 𝑥 ∈ ( - 1 [,] 1 ) ∃ 𝑦 ∈ ( 0 [,] π ) 𝑥 = ( ( cos ↾ ( 0 [,] π ) ) ‘ 𝑦 ) ) )
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 )