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