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	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( abs ‘ ( ( 𝑥 − 𝑦 ) / ( 2 · π ) ) ) = ( ( abs ‘ ( 𝑥 − 𝑦 ) ) / ( 2 · π ) ) )
52	4	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( 2 · π ) )
53	35	mulridi	⊢ ( ( 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	ffvelcdmi	⊢ ( ( ℑ ‘ ( √ ‘ 𝑥 ) ) ∈ ( - 1 [,] 1 ) → ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
136	127 135	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
137	126 136	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ∈ ℝ )
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	eqtrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑆 ‘ ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) = ( 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	mullidd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( 1 · ( exp ‘ ( i · 𝑦 ) ) ) = ( exp ‘ ( i · 𝑦 ) ) )
227	224 226	eqeq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( ( exp ‘ ( i · ( ( 2 · ( ◡ 𝑆 ‘ ( ℑ ‘ ( √ ‘ 𝑥 ) ) ) ) − 𝑦 ) ) ) · ( exp ‘ ( i · 𝑦 ) ) ) = ( 1 · ( exp ‘ ( i · 𝑦 ) ) ) ↔ 𝑥 = ( exp ‘ ( i · 𝑦 ) ) ) )
228	141 227	imbitrid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 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→ 𝐶 )