Metamath Proof Explorer

Theorem efif1olem4

Description: The exponential function of an imaginary number maps any interval of length 2 _pi one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008) (Proof shortened by Mario Carneiro, 13-May-2014)

Ref Expression
Hypotheses efif1o.1 ⊢ 𝐹 = ( 𝑤 ∈ 𝐷 ↦ ( exp ‘ ( i · 𝑤 ) ) )
efif1o.2 ⊢ 𝐶 = ( ◡ abs “ { 1 } )
efif1olem4.3 ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
efif1olem4.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( 2 · π ) )
efif1olem4.5 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐷 ( ( 𝑧 − 𝑦 ) / ( 2 · π ) ) ∈ ℤ )
efif1olem4.6 ⊢ 𝑆 = ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) )
Assertion efif1olem4 ( 𝜑 → 𝐹 : 𝐷 –1-1-onto→ 𝐶 )

Proof

Step Hyp Ref Expression
1 efif1o.1 ⊢ 𝐹 = ( 𝑤 ∈ 𝐷 ↦ ( exp ‘ ( i · 𝑤 ) ) )
2 efif1o.2 ⊢ 𝐶 = ( ◡ abs “ { 1 } )
3 efif1olem4.3 ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
4 efif1olem4.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( 2 · π ) )
5 efif1olem4.5 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐷 ( ( 𝑧 − 𝑦 ) / ( 2 · π ) ) ∈ ℤ )
6 efif1olem4.6 ⊢ 𝑆 = ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) )
7 3 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐷 ) → 𝑤 ∈ ℝ )
8 ax-icn ⊢ i ∈ ℂ
9 recn ⊢ ( 𝑤 ∈ ℝ → 𝑤 ∈ ℂ )
10 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( i · 𝑤 ) ∈ ℂ )
11 8 9 10 sylancr ⊢ ( 𝑤 ∈ ℝ → ( i · 𝑤 ) ∈ ℂ )
12 efcl ⊢ ( ( i · 𝑤 ) ∈ ℂ → ( exp ‘ ( i · 𝑤 ) ) ∈ ℂ )
13 11 12 syl ⊢ ( 𝑤 ∈ ℝ → ( exp ‘ ( i · 𝑤 ) ) ∈ ℂ )
14 absefi ⊢ ( 𝑤 ∈ ℝ → ( abs ‘ ( exp ‘ ( i · 𝑤 ) ) ) = 1 )
15 absf ⊢ abs : ℂ ⟶ ℝ
16 ffn ⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
17 15 16 ax-mp ⊢ abs Fn ℂ
18 fniniseg ⊢ ( abs Fn ℂ → ( ( exp ‘ ( i · 𝑤 ) ) ∈ ( ◡ abs “ { 1 } ) ↔ ( ( exp ‘ ( i · 𝑤 ) ) ∈ ℂ ∧ ( abs ‘ ( exp ‘ ( i · 𝑤 ) ) ) = 1 ) ) )
19 17 18 ax-mp ⊢ ( ( exp ‘ ( i · 𝑤 ) ) ∈ ( ◡ abs “ { 1 } ) ↔ ( ( exp ‘ ( i · 𝑤 ) ) ∈ ℂ ∧ ( abs ‘ ( exp ‘ ( i · 𝑤 ) ) ) = 1 ) )
20 13 14 19 sylanbrc ⊢ ( 𝑤 ∈ ℝ → ( exp ‘ ( i · 𝑤 ) ) ∈ ( ◡ abs “ { 1 } ) )
21 20 2 eleqtrrdi ⊢ ( 𝑤 ∈ ℝ → ( exp ‘ ( i · 𝑤 ) ) ∈ 𝐶 )
22 7 21 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐷 ) → ( exp ‘ ( i · 𝑤 ) ) ∈ 𝐶 )
23 22 1 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝐶 )
24 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐷 ⊆ ℝ )
25 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ 𝐷 )
26 24 25 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ ℝ )
27 26 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ ℂ )
28 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ 𝐷 )
29 24 28 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ ℝ )
30 29 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ ℂ )
31 27 30 subcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 − 𝑦 ) ∈ ℂ )
32 2re ⊢ 2 ∈ ℝ
33 pire ⊢ π ∈ ℝ
34 32 33 remulcli ⊢ ( 2 · π ) ∈ ℝ
35 34 recni ⊢ ( 2 · π ) ∈ ℂ
36 2pos ⊢ 0 < 2
37 pipos ⊢ 0 < π
38 32 33 36 37 mulgt0ii ⊢ 0 < ( 2 · π )
39 34 38 gt0ne0ii ⊢ ( 2 · π ) ≠ 0
40 divcl ⊢ ( ( ( 𝑥 − 𝑦 ) ∈ ℂ ∧ ( 2 · π ) ∈ ℂ ∧ ( 2 · π ) ≠ 0 ) → ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ∈ ℂ )
41 35 39 40 mp3an23 ⊢ ( ( 𝑥 − 𝑦 ) ∈ ℂ → ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ∈ ℂ )
42 31 41 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ∈ ℂ )
43 absdiv ⊢ ( ( ( 𝑥 − 𝑦 ) ∈ ℂ ∧ ( 2 · π ) ∈ ℂ ∧ ( 2 · π ) ≠ 0 ) → ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) = ( ( abs ‘ ( 𝑥 − 𝑦 ) ) / ( abs ‘ ( 2 · π ) ) ) )
44 35 39 43 mp3an23 ⊢ ( ( 𝑥 − 𝑦 ) ∈ ℂ → ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) = ( ( abs ‘ ( 𝑥 − 𝑦 ) ) / ( abs ‘ ( 2 · π ) ) ) )
45 31 44 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) = ( ( abs ‘ ( 𝑥 − 𝑦 ) ) / ( abs ‘ ( 2 · π ) ) ) )
46 0re ⊢ 0 ∈ ℝ
47 46 34 38 ltleii ⊢ 0 ≤ ( 2 · π )
48 absid ⊢ ( ( ( 2 · π ) ∈ ℝ ∧ 0 ≤ ( 2 · π ) ) → ( abs ‘ ( 2 · π ) ) = ( 2 · π ) )
49 34 47 48 mp2an ⊢ ( abs ‘ ( 2 · π ) ) = ( 2 · π )
50 49 oveq2i ⊢ ( ( abs ‘ ( 𝑥 − 𝑦 ) ) / ( abs ‘ ( 2 · π ) ) ) = ( ( abs ‘ ( 𝑥 − 𝑦 ) ) / ( 2 · π ) )
51 45 50 syl6eq ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) = ( ( abs ‘ ( 𝑥 − 𝑦 ) ) / ( 2 · π ) ) )
52 4 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( 2 · π ) )
53 35 mulid1i ⊢ ( ( 2 · π ) · 1 ) = ( 2 · π )
54 52 53 breqtrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( ( 2 · π ) · 1 ) )
55 31 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) ∈ ℝ )
56 1re ⊢ 1 ∈ ℝ
57 34 38 pm3.2i ⊢ ( ( 2 · π ) ∈ ℝ ∧ 0 < ( 2 · π ) )
58 ltdivmul ⊢ ( ( ( abs ‘ ( 𝑥 − 𝑦 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 2 · π ) ∈ ℝ ∧ 0 < ( 2 · π ) ) ) → ( ( ( abs ‘ ( 𝑥 − 𝑦 ) ) / ( 2 · π ) ) < 1 ↔ ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( ( 2 · π ) · 1 ) ) )
59 56 57 58 mp3an23 ⊢ ( ( abs ‘ ( 𝑥 − 𝑦 ) ) ∈ ℝ → ( ( ( abs ‘ ( 𝑥 − 𝑦 ) ) / ( 2 · π ) ) < 1 ↔ ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( ( 2 · π ) · 1 ) ) )
60 55 59 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( ( abs ‘ ( 𝑥 − 𝑦 ) ) / ( 2 · π ) ) < 1 ↔ ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( ( 2 · π ) · 1 ) ) )
61 54 60 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( abs ‘ ( 𝑥 − 𝑦 ) ) / ( 2 · π ) ) < 1 )
62 51 61 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) < 1 )
63 35 39 pm3.2i ⊢ ( ( 2 · π ) ∈ ℂ ∧ ( 2 · π ) ≠ 0 )
64 ine0 ⊢ i ≠ 0
65 8 64 pm3.2i ⊢ ( i ∈ ℂ ∧ i ≠ 0 )
66 divcan5 ⊢ ( ( ( 𝑥 − 𝑦 ) ∈ ℂ ∧ ( ( 2 · π ) ∈ ℂ ∧ ( 2 · π ) ≠ 0 ) ∧ ( i ∈ ℂ ∧ i ≠ 0 ) ) → ( ( i · ( 𝑥 − 𝑦 ) ) / ( i · ( 2 · π ) ) ) = ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) )
67 63 65 66 mp3an23 ⊢ ( ( 𝑥 − 𝑦 ) ∈ ℂ → ( ( i · ( 𝑥 − 𝑦 ) ) / ( i · ( 2 · π ) ) ) = ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) )
68 31 67 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( i · ( 𝑥 − 𝑦 ) ) / ( i · ( 2 · π ) ) ) = ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) )
69 8 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → i ∈ ℂ )
70 69 27 30 subdid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( i · ( 𝑥 − 𝑦 ) ) = ( ( i · 𝑥 ) − ( i · 𝑦 ) ) )
71 70 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( exp ‘ ( i · ( 𝑥 − 𝑦 ) ) ) = ( exp ‘ ( ( i · 𝑥 ) − ( i · 𝑦 ) ) ) )
72 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( i · 𝑥 ) ∈ ℂ )
73 8 27 72 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( i · 𝑥 ) ∈ ℂ )
74 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( i · 𝑦 ) ∈ ℂ )
75 8 30 74 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( i · 𝑦 ) ∈ ℂ )
76 efsub ⊢ ( ( ( i · 𝑥 ) ∈ ℂ ∧ ( i · 𝑦 ) ∈ ℂ ) → ( exp ‘ ( ( i · 𝑥 ) − ( i · 𝑦 ) ) ) = ( ( exp ‘ ( i · 𝑥 ) ) / ( exp ‘ ( i · 𝑦 ) ) ) )
77 73 75 76 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( exp ‘ ( ( i · 𝑥 ) − ( i · 𝑦 ) ) ) = ( ( exp ‘ ( i · 𝑥 ) ) / ( exp ‘ ( i · 𝑦 ) ) ) )
78 efcl ⊢ ( ( i · 𝑦 ) ∈ ℂ → ( exp ‘ ( i · 𝑦 ) ) ∈ ℂ )
79 75 78 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( exp ‘ ( i · 𝑦 ) ) ∈ ℂ )
80 efne0 ⊢ ( ( i · 𝑦 ) ∈ ℂ → ( exp ‘ ( i · 𝑦 ) ) ≠ 0 )
81 75 80 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( exp ‘ ( i · 𝑦 ) ) ≠ 0 )
82 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
83 oveq2 ⊢ ( 𝑤 = 𝑥 → ( i · 𝑤 ) = ( i · 𝑥 ) )
84 83 fveq2d ⊢ ( 𝑤 = 𝑥 → ( exp ‘ ( i · 𝑤 ) ) = ( exp ‘ ( i · 𝑥 ) ) )
85 fvex ⊢ ( exp ‘ ( i · 𝑥 ) ) ∈ V
86 84 1 85 fvmpt ⊢ ( 𝑥 ∈ 𝐷 → ( 𝐹 ‘ 𝑥 ) = ( exp ‘ ( i · 𝑥 ) ) )
87 25 86 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) = ( exp ‘ ( i · 𝑥 ) ) )
88 oveq2 ⊢ ( 𝑤 = 𝑦 → ( i · 𝑤 ) = ( i · 𝑦 ) )
89 88 fveq2d ⊢ ( 𝑤 = 𝑦 → ( exp ‘ ( i · 𝑤 ) ) = ( exp ‘ ( i · 𝑦 ) ) )
90 fvex ⊢ ( exp ‘ ( i · 𝑦 ) ) ∈ V
91 89 1 90 fvmpt ⊢ ( 𝑦 ∈ 𝐷 → ( 𝐹 ‘ 𝑦 ) = ( exp ‘ ( i · 𝑦 ) ) )
92 28 91 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑦 ) = ( exp ‘ ( i · 𝑦 ) ) )
93 82 87 92 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( exp ‘ ( i · 𝑥 ) ) = ( exp ‘ ( i · 𝑦 ) ) )
94 79 81 93 diveq1bd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( exp ‘ ( i · 𝑥 ) ) / ( exp ‘ ( i · 𝑦 ) ) ) = 1 )
95 71 77 94 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( exp ‘ ( i · ( 𝑥 − 𝑦 ) ) ) = 1 )
96 mulcl ⊢ ( ( i ∈ ℂ ∧ ( 𝑥 − 𝑦 ) ∈ ℂ ) → ( i · ( 𝑥 − 𝑦 ) ) ∈ ℂ )
97 8 31 96 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( i · ( 𝑥 − 𝑦 ) ) ∈ ℂ )
98 efeq1 ⊢ ( ( i · ( 𝑥 − 𝑦 ) ) ∈ ℂ → ( ( exp ‘ ( i · ( 𝑥 − 𝑦 ) ) ) = 1 ↔ ( ( i · ( 𝑥 − 𝑦 ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
99 97 98 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( exp ‘ ( i · ( 𝑥 − 𝑦 ) ) ) = 1 ↔ ( ( i · ( 𝑥 − 𝑦 ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
100 95 99 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( i · ( 𝑥 − 𝑦 ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ )
101 68 100 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ∈ ℤ )
102 nn0abscl ⊢ ( ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ∈ ℤ → ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) ∈ ℕ0 )
103 101 102 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) ∈ ℕ0 )
104 nn0lt10b ⊢ ( ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) ∈ ℕ0 → ( ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) < 1 ↔ ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) = 0 ) )
105 103 104 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) < 1 ↔ ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) = 0 ) )
106 62 105 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) = 0 )
107 42 106 abs00d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) = 0 )
108 diveq0 ⊢ ( ( ( 𝑥 − 𝑦 ) ∈ ℂ ∧ ( 2 · π ) ∈ ℂ ∧ ( 2 · π ) ≠ 0 ) → ( ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) = 0 ↔ ( 𝑥 − 𝑦 ) = 0 ) )
109 35 39 108 mp3an23 ⊢ ( ( 𝑥 − 𝑦 ) ∈ ℂ → ( ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) = 0 ↔ ( 𝑥 − 𝑦 ) = 0 ) )
110 31 109 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) = 0 ↔ ( 𝑥 − 𝑦 ) = 0 ) )
111 107 110 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 − 𝑦 ) = 0 )
112 27 30 111 subeq0d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
113 112 ex ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
114 113 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
115 dff13 ⊢ ( 𝐹 : 𝐷 –1-1→ 𝐶 ↔ ( 𝐹 : 𝐷 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
116 23 114 115 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐷 –1-1→ 𝐶 )
117 oveq1 ⊢ ( 𝑧 = ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( 𝑧 − 𝑦 ) = ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) )
118 117 oveq1d ⊢ ( 𝑧 = ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( ( 𝑧 − 𝑦 ) / ( 2 · π ) ) = ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) / ( 2 · π ) ) )
119 118 eleq1d ⊢ ( 𝑧 = ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( ( ( 𝑧 − 𝑦 ) / ( 2 · π ) ) ∈ ℤ ↔ ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) / ( 2 · π ) ) ∈ ℤ ) )
120 119 rexbidv ⊢ ( 𝑧 = ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( ∃ 𝑦 ∈ 𝐷 ( ( 𝑧 − 𝑦 ) / ( 2 · π ) ) ∈ ℤ ↔ ∃ 𝑦 ∈ 𝐷 ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) / ( 2 · π ) ) ∈ ℤ ) )
121 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ℝ ∃ 𝑦 ∈ 𝐷 ( ( 𝑧 − 𝑦 ) / ( 2 · π ) ) ∈ ℤ )
122 121 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∀ 𝑧 ∈ ℝ ∃ 𝑦 ∈ 𝐷 ( ( 𝑧 − 𝑦 ) / ( 2 · π ) ) ∈ ℤ )
123 neghalfpire ⊢ - ( π / 2 ) ∈ ℝ
124 halfpire ⊢ ( π / 2 ) ∈ ℝ
125 iccssre ⊢ ( ( - ( π / 2 ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( - ( π / 2 ) [,] ( π / 2 ) ) ⊆ ℝ )
126 123 124 125 mp2an ⊢ ( - ( π / 2 ) [,] ( π / 2 ) ) ⊆ ℝ
127 1 2 efif1olem3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∈ ( - 1 [,] 1 ) )
128 resinf1o ⊢ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) : ( - ( π / 2 ) [,] ( π / 2 ) ) –1-1-onto→ ( - 1 [,] 1 )
129 f1oeq1 ⊢ ( 𝑆 = ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) → ( 𝑆 : ( - ( π / 2 ) [,] ( π / 2 ) ) –1-1-onto→ ( - 1 [,] 1 ) ↔ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) : ( - ( π / 2 ) [,] ( π / 2 ) ) –1-1-onto→ ( - 1 [,] 1 ) ) )
130 6 129 ax-mp ⊢ ( 𝑆 : ( - ( π / 2 ) [,] ( π / 2 ) ) –1-1-onto→ ( - 1 [,] 1 ) ↔ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) : ( - ( π / 2 ) [,] ( π / 2 ) ) –1-1-onto→ ( - 1 [,] 1 ) )
131 128 130 mpbir ⊢ 𝑆 : ( - ( π / 2 ) [,] ( π / 2 ) ) –1-1-onto→ ( - 1 [,] 1 )
132 f1ocnv ⊢ ( 𝑆 : ( - ( π / 2 ) [,] ( π / 2 ) ) –1-1-onto→ ( - 1 [,] 1 ) → ◡ 𝑆 : ( - 1 [,] 1 ) –1-1-onto→ ( - ( π / 2 ) [,] ( π / 2 ) ) )
133 f1of ⊢ ( ◡ 𝑆 : ( - 1 [,] 1 ) –1-1-onto→ ( - ( π / 2 ) [,] ( π / 2 ) ) → ◡ 𝑆 : ( - 1 [,] 1 ) ⟶ ( - ( π / 2 ) [,] ( π / 2 ) ) )
134 131 132 133 mp2b ⊢ ◡ 𝑆 : ( - 1 [,] 1 ) ⟶ ( - ( π / 2 ) [,] ( π / 2 ) )
135 134 ffvelrni ⊢ ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∈ ( - 1 [,] 1 ) → ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
136 127 135 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
137 126 136 sseldi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ℝ )
138 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ℝ ) → ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ∈ ℝ )
139 32 137 138 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ∈ ℝ )
140 120 122 139 rspcdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑦 ∈ 𝐷 ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) / ( 2 · π ) ) ∈ ℤ )
141 oveq1 ⊢ ( ( exp ‘ ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ) = 1 → ( ( exp ‘ ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ) · ( exp ‘ ( i · 𝑦 ) ) ) = ( 1 · ( exp ‘ ( i · 𝑦 ) ) ) )
142 8 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → i ∈ ℂ )
143 139 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ∈ ℝ )
144 143 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ∈ ℂ )
145 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → 𝐷 ⊆ ℝ )
146 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 )
147 145 146 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ ℝ )
148 147 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ ℂ )
149 142 144 148 subdid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) = ( ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) − ( i · 𝑦 ) ) )
150 149 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) + ( i · 𝑦 ) ) = ( ( ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) − ( i · 𝑦 ) ) + ( i · 𝑦 ) ) )
151 mulcl ⊢ ( ( i ∈ ℂ ∧ ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ∈ ℂ ) → ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ∈ ℂ )
152 8 144 151 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ∈ ℂ )
153 8 148 74 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( i · 𝑦 ) ∈ ℂ )
154 152 153 npcand ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) − ( i · 𝑦 ) ) + ( i · 𝑦 ) ) = ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) )
155 150 154 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) + ( i · 𝑦 ) ) = ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) )
156 155 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( exp ‘ ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) + ( i · 𝑦 ) ) ) = ( exp ‘ ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ) )
157 144 148 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ∈ ℂ )
158 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ∈ ℂ ) → ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ∈ ℂ )
159 8 157 158 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ∈ ℂ )
160 efadd ⊢ ( ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ∈ ℂ ∧ ( i · 𝑦 ) ∈ ℂ ) → ( exp ‘ ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) + ( i · 𝑦 ) ) ) = ( ( exp ‘ ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ) · ( exp ‘ ( i · 𝑦 ) ) ) )
161 159 153 160 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( exp ‘ ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) + ( i · 𝑦 ) ) ) = ( ( exp ‘ ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ) · ( exp ‘ ( i · 𝑦 ) ) ) )
162 2cn ⊢ 2 ∈ ℂ
163 137 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ℂ )
164 mul12 ⊢ ( ( i ∈ ℂ ∧ 2 ∈ ℂ ∧ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ℂ ) → ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) = ( 2 · ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) )
165 8 162 163 164 mp3an12i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) = ( 2 · ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) )
166 165 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( exp ‘ ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ) = ( exp ‘ ( 2 · ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ) )
167 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ℂ ) → ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ∈ ℂ )
168 8 163 167 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ∈ ℂ )
169 2z ⊢ 2 ∈ ℤ
170 efexp ⊢ ( ( ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ∈ ℂ ∧ 2 ∈ ℤ ) → ( exp ‘ ( 2 · ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ) = ( ( exp ‘ ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ↑ 2 ) )
171 168 169 170 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( exp ‘ ( 2 · ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ) = ( ( exp ‘ ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ↑ 2 ) )
172 166 171 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( exp ‘ ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ) = ( ( exp ‘ ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ↑ 2 ) )
173 137 recoscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ∈ ℝ )
174 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐶 )
175 174 2 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ( ◡ abs “ { 1 } ) )
176 fniniseg ⊢ ( abs Fn ℂ → ( 𝑥 ∈ ( ◡ abs “ { 1 } ) ↔ ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) = 1 ) ) )
177 17 176 ax-mp ⊢ ( 𝑥 ∈ ( ◡ abs “ { 1 } ) ↔ ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) = 1 ) )
178 175 177 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) = 1 ) )
179 178 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ℂ )
180 179 sqrtcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( √ ‘ 𝑥 ) ∈ ℂ )
181 180 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ℜ ‘ ( √ ‘ 𝑥 ) ) ∈ ℝ )
182 cosq14ge0 ⊢ ( ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 0 ≤ ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) )
183 136 182 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 0 ≤ ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) )
184 179 sqrtrege0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 0 ≤ ( ℜ ‘ ( √ ‘ 𝑥 ) ) )
185 sincossq ⊢ ( ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ℂ → ( ( ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) + ( ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) ) = 1 )
186 163 185 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) + ( ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) ) = 1 )
187 179 sqsqrtd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( √ ‘ 𝑥 ) ↑ 2 ) = 𝑥 )
188 187 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( abs ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) = ( abs ‘ 𝑥 ) )
189 2nn0 ⊢ 2 ∈ ℕ0
190 absexp ⊢ ( ( ( √ ‘ 𝑥 ) ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( abs ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) = ( ( abs ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) )
191 180 189 190 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( abs ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) = ( ( abs ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) )
192 178 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( abs ‘ 𝑥 ) = 1 )
193 188 191 192 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( abs ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) = 1 )
194 180 absvalsq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( abs ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) + ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) ) )
195 186 193 194 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) + ( ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) ) = ( ( ( ℜ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) + ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) ) )
196 6 fveq1i ⊢ ( 𝑆 ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) = ( ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) )
197 136 fvresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) = ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) )
198 196 197 syl5eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑆 ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) = ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) )
199 f1ocnvfv2 ⊢ ( ( 𝑆 : ( - ( π / 2 ) [,] ( π / 2 ) ) –1-1-onto→ ( - 1 [,] 1 ) ∧ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∈ ( - 1 [,] 1 ) ) → ( 𝑆 ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) = ( ℑ ‘ ( √ ‘ 𝑥 ) ) )
200 131 127 199 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑆 ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) = ( ℑ ‘ ( √ ‘ 𝑥 ) ) )
201 198 200 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) = ( ℑ ‘ ( √ ‘ 𝑥 ) ) )
202 201 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) = ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) )
203 195 202 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) + ( ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) ) − ( ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) ) = ( ( ( ( ℜ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) + ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) ) − ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) ) )
204 163 sincld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ∈ ℂ )
205 204 sqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) ∈ ℂ )
206 163 coscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ∈ ℂ )
207 206 sqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) ∈ ℂ )
208 205 207 pncan2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) + ( ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) ) − ( ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) ) = ( ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) )
209 181 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ℜ ‘ ( √ ‘ 𝑥 ) ) ∈ ℂ )
210 209 sqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ℜ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) ∈ ℂ )
211 202 205 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) ∈ ℂ )
212 210 211 pncand ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( ( ℜ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) + ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) ) − ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) ) = ( ( ℜ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) )
213 203 208 212 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ↑ 2 ) = ( ( ℜ ‘ ( √ ‘ 𝑥 ) ) ↑ 2 ) )
214 173 181 183 184 213 sq11d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) = ( ℜ ‘ ( √ ‘ 𝑥 ) ) )
215 201 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( i · ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) = ( i · ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) )
216 214 215 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) + ( i · ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ) = ( ( ℜ ‘ ( √ ‘ 𝑥 ) ) + ( i · ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) )
217 efival ⊢ ( ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ℂ → ( exp ‘ ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) = ( ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) + ( i · ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ) )
218 163 217 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( exp ‘ ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) = ( ( cos ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) + ( i · ( sin ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ) )
219 180 replimd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( √ ‘ 𝑥 ) = ( ( ℜ ‘ ( √ ‘ 𝑥 ) ) + ( i · ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) )
220 216 218 219 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( exp ‘ ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) = ( √ ‘ 𝑥 ) )
221 220 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( exp ‘ ( i · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ↑ 2 ) = ( ( √ ‘ 𝑥 ) ↑ 2 ) )
222 172 221 187 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( exp ‘ ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ) = 𝑥 )
223 222 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( exp ‘ ( i · ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) ) ) = 𝑥 )
224 156 161 223 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( exp ‘ ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ) · ( exp ‘ ( i · 𝑦 ) ) ) = 𝑥 )
225 153 78 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( exp ‘ ( i · 𝑦 ) ) ∈ ℂ )
226 225 mulid2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( 1 · ( exp ‘ ( i · 𝑦 ) ) ) = ( exp ‘ ( i · 𝑦 ) ) )
227 224 226 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( ( exp ‘ ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ) · ( exp ‘ ( i · 𝑦 ) ) ) = ( 1 · ( exp ‘ ( i · 𝑦 ) ) ) ↔ 𝑥 = ( exp ‘ ( i · 𝑦 ) ) ) )
228 141 227 syl5ib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( exp ‘ ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ) = 1 → 𝑥 = ( exp ‘ ( i · 𝑦 ) ) ) )
229 efeq1 ⊢ ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ∈ ℂ → ( ( exp ‘ ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ) = 1 ↔ ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
230 159 229 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( exp ‘ ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ) = 1 ↔ ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
231 divcan5 ⊢ ( ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ∈ ℂ ∧ ( ( 2 · π ) ∈ ℂ ∧ ( 2 · π ) ≠ 0 ) ∧ ( i ∈ ℂ ∧ i ≠ 0 ) ) → ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) / ( i · ( 2 · π ) ) ) = ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) / ( 2 · π ) ) )
232 63 65 231 mp3an23 ⊢ ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ∈ ℂ → ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) / ( i · ( 2 · π ) ) ) = ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) / ( 2 · π ) ) )
233 157 232 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) / ( i · ( 2 · π ) ) ) = ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) / ( 2 · π ) ) )
234 233 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ↔ ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) / ( 2 · π ) ) ∈ ℤ ) )
235 230 234 bitr2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) / ( 2 · π ) ) ∈ ℤ ↔ ( exp ‘ ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ) = 1 ) )
236 91 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑦 ) = ( exp ‘ ( i · 𝑦 ) ) )
237 236 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = ( exp ‘ ( i · 𝑦 ) ) ) )
238 228 235 237 3imtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) / ( 2 · π ) ) ∈ ℤ → 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
239 238 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ∃ 𝑦 ∈ 𝐷 ( ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) / ( 2 · π ) ) ∈ ℤ → ∃ 𝑦 ∈ 𝐷 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
240 140 239 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑦 ∈ 𝐷 𝑥 = ( 𝐹 ‘ 𝑦 ) )
241 240 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 𝑥 = ( 𝐹 ‘ 𝑦 ) )
242 dffo3 ⊢ ( 𝐹 : 𝐷 –onto→ 𝐶 ↔ ( 𝐹 : 𝐷 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
243 23 241 242 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐷 –onto→ 𝐶 )
244 df-f1o ⊢ ( 𝐹 : 𝐷 –1-1-onto→ 𝐶 ↔ ( 𝐹 : 𝐷 –1-1→ 𝐶 ∧ 𝐹 : 𝐷 –onto→ 𝐶 ) )
245 116 243 244 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐷 –1-1-onto→ 𝐶 )