Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvasin Structured version   Visualization version   GIF version

Theorem dvasin 33626
 Description: Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018.)
Hypothesis
Ref Expression
dvasin.d 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
Assertion
Ref Expression
dvasin (ℂ D (arcsin ↾ 𝐷)) = (𝑥𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
Distinct variable group:   𝑥,𝐷

Proof of Theorem dvasin
Dummy variables 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-asin 24637 . . . . 5 arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
21reseq1i 5424 . . . 4 (arcsin ↾ 𝐷) = ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷)
3 dvasin.d . . . . . 6 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
4 difss 3770 . . . . . 6 (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆ ℂ
53, 4eqsstri 3668 . . . . 5 𝐷 ⊆ ℂ
6 resmpt 5484 . . . . 5 (𝐷 ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) = (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
75, 6ax-mp 5 . . . 4 ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) = (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
82, 7eqtri 2673 . . 3 (arcsin ↾ 𝐷) = (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
98oveq2i 6701 . 2 (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
10 cnelprrecn 10067 . . . . 5 ℂ ∈ {ℝ, ℂ}
1110a1i 11 . . . 4 (⊤ → ℂ ∈ {ℝ, ℂ})
125sseli 3632 . . . . . . 7 (𝑥𝐷𝑥 ∈ ℂ)
13 ax-icn 10033 . . . . . . . . 9 i ∈ ℂ
14 mulcl 10058 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
1513, 14mpan 706 . . . . . . . 8 (𝑥 ∈ ℂ → (i · 𝑥) ∈ ℂ)
16 ax-1cn 10032 . . . . . . . . . 10 1 ∈ ℂ
17 sqcl 12965 . . . . . . . . . 10 (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
18 subcl 10318 . . . . . . . . . 10 ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
1916, 17, 18sylancr 696 . . . . . . . . 9 (𝑥 ∈ ℂ → (1 − (𝑥↑2)) ∈ ℂ)
2019sqrtcld 14220 . . . . . . . 8 (𝑥 ∈ ℂ → (√‘(1 − (𝑥↑2))) ∈ ℂ)
2115, 20addcld 10097 . . . . . . 7 (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
2212, 21syl 17 . . . . . 6 (𝑥𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
23 asinlem 24640 . . . . . . 7 (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
2412, 23syl 17 . . . . . 6 (𝑥𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
2522, 24logcld 24362 . . . . 5 (𝑥𝐷 → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
2625adantl 481 . . . 4 ((⊤ ∧ 𝑥𝐷) → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
27 ovexd 6720 . . . 4 ((⊤ ∧ 𝑥𝐷) → (i / (√‘(1 − (𝑥↑2)))) ∈ V)
28 simpr 476 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
29 asinlem3 24643 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
30 rere 13906 . . . . . . . . . . . . . . . . . . 19 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
3130breq2d 4697 . . . . . . . . . . . . . . . . . 18 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
3231biimpac 502 . . . . . . . . . . . . . . . . 17 ((0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
3329, 32sylan 487 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
3423adantr 480 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
3528, 33, 34ne0gt0d 10212 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
36 0re 10078 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
37 ltnle 10155 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
3836, 37mpan 706 . . . . . . . . . . . . . . . 16 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
3938adantl 481 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4035, 39mpbid 222 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)
4140ex 449 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4212, 41syl 17 . . . . . . . . . . . 12 (𝑥𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
43 imor 427 . . . . . . . . . . . 12 ((((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4442, 43sylib 208 . . . . . . . . . . 11 (𝑥𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4544orcomd 402 . . . . . . . . . 10 (𝑥𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
4645olcd 407 . . . . . . . . 9 (𝑥𝐷 → (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
47 3ianor 1074 . . . . . . . . . . 11 (¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
48 3orrot 1061 . . . . . . . . . . 11 ((¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
49 3orass 1057 . . . . . . . . . . 11 ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
5047, 48, 493bitrri 287 . . . . . . . . . 10 ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
51 mnfxr 10134 . . . . . . . . . . 11 -∞ ∈ ℝ*
52 elioc2 12274 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)))
5351, 36, 52mp2an 708 . . . . . . . . . 10 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
5450, 53xchbinxr 324 . . . . . . . . 9 ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
5546, 54sylib 208 . . . . . . . 8 (𝑥𝐷 → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
5622, 55eldifd 3618 . . . . . . 7 (𝑥𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
5756adantl 481 . . . . . 6 ((⊤ ∧ 𝑥𝐷) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
58 ovexd 6720 . . . . . 6 ((⊤ ∧ 𝑥𝐷) → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))) ∈ V)
59 eldifi 3765 . . . . . . . 8 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ∈ ℂ)
60 eldifn 3766 . . . . . . . . 9 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0))
61 0xr 10124 . . . . . . . . . . . 12 0 ∈ ℝ*
62 mnflt0 11997 . . . . . . . . . . . 12 -∞ < 0
63 ubioc1 12265 . . . . . . . . . . . 12 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ -∞ < 0) → 0 ∈ (-∞(,]0))
6451, 61, 62, 63mp3an 1464 . . . . . . . . . . 11 0 ∈ (-∞(,]0)
65 eleq1 2718 . . . . . . . . . . 11 (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈ (-∞(,]0)))
6664, 65mpbiri 248 . . . . . . . . . 10 (𝑦 = 0 → 𝑦 ∈ (-∞(,]0))
6766necon3bi 2849 . . . . . . . . 9 𝑦 ∈ (-∞(,]0) → 𝑦 ≠ 0)
6860, 67syl 17 . . . . . . . 8 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ≠ 0)
6959, 68logcld 24362 . . . . . . 7 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (log‘𝑦) ∈ ℂ)
7069adantl 481 . . . . . 6 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ)
71 ovexd 6720 . . . . . 6 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V)
7213a1i 11 . . . . . . . . . 10 (𝑥𝐷 → i ∈ ℂ)
7372, 12mulcld 10098 . . . . . . . . 9 (𝑥𝐷 → (i · 𝑥) ∈ ℂ)
7473adantl 481 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → (i · 𝑥) ∈ ℂ)
7513a1i 11 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → i ∈ ℂ)
7612adantl 481 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → 𝑥 ∈ ℂ)
77 1cnd 10094 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → 1 ∈ ℂ)
78 simpr 476 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
79 1cnd 10094 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
8011dvmptid 23765 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
815a1i 11 . . . . . . . . . . 11 (⊤ → 𝐷 ⊆ ℂ)
82 eqid 2651 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
8382cnfldtopon 22633 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
8483toponunii 20769 . . . . . . . . . . . . . 14 ℂ = (TopOpen‘ℂfld)
8584restid 16141 . . . . . . . . . . . . 13 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
8683, 85ax-mp 5 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
8786eqcomi 2660 . . . . . . . . . . 11 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
8882recld2 22664 . . . . . . . . . . . . . . 15 ℝ ∈ (Clsd‘(TopOpen‘ℂfld))
89 neg1rr 11163 . . . . . . . . . . . . . . . . . 18 -1 ∈ ℝ
90 iocmnfcld 22619 . . . . . . . . . . . . . . . . . 18 (-1 ∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))))
9189, 90ax-mp 5 . . . . . . . . . . . . . . . . 17 (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,)))
92 1re 10077 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
93 icopnfcld 22618 . . . . . . . . . . . . . . . . . 18 (1 ∈ ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
9492, 93ax-mp 5 . . . . . . . . . . . . . . . . 17 (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))
95 uncld 20893 . . . . . . . . . . . . . . . . 17 (((-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))) ∧ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,))))
9691, 94, 95mp2an 708 . . . . . . . . . . . . . . . 16 ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,)))
9782tgioo2 22653 . . . . . . . . . . . . . . . . 17 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
9897fveq2i 6232 . . . . . . . . . . . . . . . 16 (Clsd‘(topGen‘ran (,))) = (Clsd‘((TopOpen‘ℂfld) ↾t ℝ))
9996, 98eleqtri 2728 . . . . . . . . . . . . . . 15 ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂfld) ↾t ℝ))
100 restcldr 21026 . . . . . . . . . . . . . . 15 ((ℝ ∈ (Clsd‘(TopOpen‘ℂfld)) ∧ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂfld) ↾t ℝ))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂfld)))
10188, 99, 100mp2an 708 . . . . . . . . . . . . . 14 ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂfld))
10284cldopn 20883 . . . . . . . . . . . . . 14 (((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂfld))
103101, 102ax-mp 5 . . . . . . . . . . . . 13 (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂfld)
1043, 103eqeltri 2726 . . . . . . . . . . . 12 𝐷 ∈ (TopOpen‘ℂfld)
105104a1i 11 . . . . . . . . . . 11 (⊤ → 𝐷 ∈ (TopOpen‘ℂfld))
10611, 78, 79, 80, 81, 87, 82, 105dvmptres 23771 . . . . . . . . . 10 (⊤ → (ℂ D (𝑥𝐷𝑥)) = (𝑥𝐷 ↦ 1))
10713a1i 11 . . . . . . . . . 10 (⊤ → i ∈ ℂ)
10811, 76, 77, 106, 107dvmptcmul 23772 . . . . . . . . 9 (⊤ → (ℂ D (𝑥𝐷 ↦ (i · 𝑥))) = (𝑥𝐷 ↦ (i · 1)))
10913mulid1i 10080 . . . . . . . . . 10 (i · 1) = i
110109mpteq2i 4774 . . . . . . . . 9 (𝑥𝐷 ↦ (i · 1)) = (𝑥𝐷 ↦ i)
111108, 110syl6eq 2701 . . . . . . . 8 (⊤ → (ℂ D (𝑥𝐷 ↦ (i · 𝑥))) = (𝑥𝐷 ↦ i))
11212sqcld 13046 . . . . . . . . . . 11 (𝑥𝐷 → (𝑥↑2) ∈ ℂ)
11316, 112, 18sylancr 696 . . . . . . . . . 10 (𝑥𝐷 → (1 − (𝑥↑2)) ∈ ℂ)
114113sqrtcld 14220 . . . . . . . . 9 (𝑥𝐷 → (√‘(1 − (𝑥↑2))) ∈ ℂ)
115114adantl 481 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → (√‘(1 − (𝑥↑2))) ∈ ℂ)
116 ovexd 6720 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → (-𝑥 / (√‘(1 − (𝑥↑2)))) ∈ V)
117 elin 3829 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥𝐷𝑥 ∈ ℝ))
1183asindmre 33625 . . . . . . . . . . . . . . . . 17 (𝐷 ∩ ℝ) = (-1(,)1)
119118eqimssi 3692 . . . . . . . . . . . . . . . 16 (𝐷 ∩ ℝ) ⊆ (-1(,)1)
120119sseli 3632 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ (-1(,)1))
121117, 120sylbir 225 . . . . . . . . . . . . . 14 ((𝑥𝐷𝑥 ∈ ℝ) → 𝑥 ∈ (-1(,)1))
122 incom 3838 . . . . . . . . . . . . . . . 16 ((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩ (0(,)+∞))
123 pnfxr 10130 . . . . . . . . . . . . . . . . 17 +∞ ∈ ℝ*
124 df-ioc 12218 . . . . . . . . . . . . . . . . . 18 (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
125 df-ioo 12217 . . . . . . . . . . . . . . . . . 18 (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
126 xrltnle 10143 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℝ*𝑤 ∈ ℝ*) → (0 < 𝑤 ↔ ¬ 𝑤 ≤ 0))
127124, 125, 126ixxdisj 12228 . . . . . . . . . . . . . . . . 17 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((-∞(,]0) ∩ (0(,)+∞)) = ∅)
12851, 61, 123, 127mp3an 1464 . . . . . . . . . . . . . . . 16 ((-∞(,]0) ∩ (0(,)+∞)) = ∅
129122, 128eqtri 2673 . . . . . . . . . . . . . . 15 ((0(,)+∞) ∩ (-∞(,]0)) = ∅
130 elioore 12243 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (-1(,)1) → 𝑥 ∈ ℝ)
131130resqcld 13075 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (-1(,)1) → (𝑥↑2) ∈ ℝ)
132 resubcl 10383 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 − (𝑥↑2)) ∈ ℝ)
13392, 131, 132sylancr 696 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ)
13489rexri 10135 . . . . . . . . . . . . . . . . . . 19 -1 ∈ ℝ*
13592rexri 10135 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ*
136 elioo2 12254 . . . . . . . . . . . . . . . . . . 19 ((-1 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥𝑥 < 1)))
137134, 135, 136mp2an 708 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥𝑥 < 1))
138 recn 10064 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
139138abscld 14219 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
140138absge0d 14227 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → 0 ≤ (abs‘𝑥))
141 0le1 10589 . . . . . . . . . . . . . . . . . . . . . . 23 0 ≤ 1
142 lt2sq 12977 . . . . . . . . . . . . . . . . . . . . . . 23 ((((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
14392, 141, 142mpanr12 721 . . . . . . . . . . . . . . . . . . . . . 22 (((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
144139, 140, 143syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
145 abslt 14098 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥𝑥 < 1)))
14692, 145mpan2 707 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥𝑥 < 1)))
147 absresq 14086 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → ((abs‘𝑥)↑2) = (𝑥↑2))
148 sq1 12998 . . . . . . . . . . . . . . . . . . . . . . . 24 (1↑2) = 1
149148a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → (1↑2) = 1)
150147, 149breq12d 4698 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ (𝑥↑2) < 1))
151 resqcl 12971 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → (𝑥↑2) ∈ ℝ)
152 posdif 10559 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥↑2) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
153151, 92, 152sylancl 695 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
154150, 153bitrd 268 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ 0 < (1 − (𝑥↑2))))
155144, 146, 1543bitr3d 298 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → ((-1 < 𝑥𝑥 < 1) ↔ 0 < (1 − (𝑥↑2))))
156155biimpd 219 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → ((-1 < 𝑥𝑥 < 1) → 0 < (1 − (𝑥↑2))))
1571563impib 1281 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ -1 < 𝑥𝑥 < 1) → 0 < (1 − (𝑥↑2)))
158137, 157sylbi 207 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (-1(,)1) → 0 < (1 − (𝑥↑2)))
159133, 158elrpd 11907 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ+)
160 ioorp 12289 . . . . . . . . . . . . . . . 16 (0(,)+∞) = ℝ+
161159, 160syl6eleqr 2741 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ (0(,)+∞))
162 disjel 4056 . . . . . . . . . . . . . . 15 ((((0(,)+∞) ∩ (-∞(,]0)) = ∅ ∧ (1 − (𝑥↑2)) ∈ (0(,)+∞)) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
163129, 161, 162sylancr 696 . . . . . . . . . . . . . 14 (𝑥 ∈ (-1(,)1) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
164121, 163syl 17 . . . . . . . . . . . . 13 ((𝑥𝐷𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
165 elioc2 12274 . . . . . . . . . . . . . . . . . . . . . . . 24 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0)))
16651, 36, 165mp2an 708 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
167166biimpi 206 . . . . . . . . . . . . . . . . . . . . . 22 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
168167simp1d 1093 . . . . . . . . . . . . . . . . . . . . 21 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ)
169 resubcl 10383 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
17092, 168, 169sylancr 696 . . . . . . . . . . . . . . . . . . . 20 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
171 nncan 10348 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
17216, 171mpan 706 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥↑2) ∈ ℂ → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
173172eleq1d 2715 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥↑2) ∈ ℂ → ((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈ ℝ))
174173biimpa 500 . . . . . . . . . . . . . . . . . . . 20 (((𝑥↑2) ∈ ℂ ∧ (1 − (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈ ℝ)
175170, 174sylan2 490 . . . . . . . . . . . . . . . . . . 19 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥↑2) ∈ ℝ)
176168adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ)
177167simp3d 1095 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ≤ 0)
178177adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0)
179 letr 10169 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1 − (𝑥↑2)) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
18036, 92, 179mp3an23 1456 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 − (𝑥↑2)) ∈ ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
181141, 180mpan2i 713 . . . . . . . . . . . . . . . . . . . . . 22 ((1 − (𝑥↑2)) ∈ ℝ → ((1 − (𝑥↑2)) ≤ 0 → (1 − (𝑥↑2)) ≤ 1))
182176, 178, 181sylc 65 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 1)
183 subge0 10579 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
18492, 176, 183sylancr 696 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
185182, 184mpbird 247 . . . . . . . . . . . . . . . . . . . 20 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2))))
186172adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
187185, 186breqtrd 4711 . . . . . . . . . . . . . . . . . . 19 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (𝑥↑2))
188175, 187resqrtcld 14200 . . . . . . . . . . . . . . . . . 18 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
18917, 188sylan 487 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
190 eleq1 2718 . . . . . . . . . . . . . . . . 17 (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ (√‘(𝑥↑2)) ∈ ℝ))
191189, 190syl5ibrcom 237 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
192189renegcld 10495 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ)
193 eleq1 2718 . . . . . . . . . . . . . . . . 17 (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ -(√‘(𝑥↑2)) ∈ ℝ))
194192, 193syl5ibrcom 237 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = -(√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
195 eqid 2651 . . . . . . . . . . . . . . . . . 18 (𝑥↑2) = (𝑥↑2)
196 eqsqrtor 14150 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
19717, 196mpdan 703 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
198195, 197mpbii 223 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
199198adantr 480 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
200191, 194, 199mpjaod 395 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 𝑥 ∈ ℝ)
201200stoic1a 1737 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
20212, 201sylan 487 . . . . . . . . . . . . 13 ((𝑥𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
203164, 202pm2.61dan 849 . . . . . . . . . . . 12 (𝑥𝐷 → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
204113, 203eldifd 3618 . . . . . . . . . . 11 (𝑥𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
205204adantl 481 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
206 2cnd 11131 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → 2 ∈ ℂ)
207 id 22 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
208206, 207mulcld 10098 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
209208negcld 10417 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → -(2 · 𝑥) ∈ ℂ)
210209adantl 481 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → -(2 · 𝑥) ∈ ℂ)
21112, 210sylan2 490 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → -(2 · 𝑥) ∈ ℂ)
21259sqrtcld 14220 . . . . . . . . . . 11 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (√‘𝑦) ∈ ℂ)
213212adantl 481 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈ ℂ)
214 ovexd 6720 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 · (√‘𝑦))) ∈ V)
21519adantl 481 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
21636a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → 0 ∈ ℝ)
217 1cnd 10094 . . . . . . . . . . . . . 14 (⊤ → 1 ∈ ℂ)
21811, 217dvmptc 23766 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 1)) = (𝑥 ∈ ℂ ↦ 0))
21917adantl 481 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥↑2) ∈ ℂ)
220 2cn 11129 . . . . . . . . . . . . . . 15 2 ∈ ℂ
221 mulcl 10058 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
222220, 221mpan 706 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
223222adantl 481 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
224 2nn 11223 . . . . . . . . . . . . . . . 16 2 ∈ ℕ
225 dvexp 23761 . . . . . . . . . . . . . . . 16 (2 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))))
226224, 225ax-mp 5 . . . . . . . . . . . . . . 15 (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1))))
227 2m1e1 11173 . . . . . . . . . . . . . . . . . . 19 (2 − 1) = 1
228227oveq2i 6701 . . . . . . . . . . . . . . . . . 18 (𝑥↑(2 − 1)) = (𝑥↑1)
229 exp1 12906 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥)
230228, 229syl5eq 2697 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥)
231230oveq2d 6706 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥))
232231mpteq2ia 4773 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
233226, 232eqtri 2673 . . . . . . . . . . . . . 14 (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
234233a1i 11 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥)))
23511, 79, 216, 218, 219, 223, 234dvmptsub 23775 . . . . . . . . . . . 12 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥))))
236 df-neg 10307 . . . . . . . . . . . . 13 -(2 · 𝑥) = (0 − (2 · 𝑥))
237236mpteq2i 4774 . . . . . . . . . . . 12 (𝑥 ∈ ℂ ↦ -(2 · 𝑥)) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥)))
238235, 237syl6eqr 2703 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥)))
23911, 215, 210, 238, 81, 87, 82, 105dvmptres 23771 . . . . . . . . . 10 (⊤ → (ℂ D (𝑥𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥𝐷 ↦ -(2 · 𝑥)))
240 eqid 2651 . . . . . . . . . . . 12 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
241240dvcnsqrt 24530 . . . . . . . . . . 11 (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦))))
242241a1i 11 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦)))))
243 fveq2 6229 . . . . . . . . . 10 (𝑦 = (1 − (𝑥↑2)) → (√‘𝑦) = (√‘(1 − (𝑥↑2))))
244243oveq2d 6706 . . . . . . . . . . 11 (𝑦 = (1 − (𝑥↑2)) → (2 · (√‘𝑦)) = (2 · (√‘(1 − (𝑥↑2)))))
245244oveq2d 6706 . . . . . . . . . 10 (𝑦 = (1 − (𝑥↑2)) → (1 / (2 · (√‘𝑦))) = (1 / (2 · (√‘(1 − (𝑥↑2))))))
24611, 11, 205, 211, 213, 214, 239, 242, 243, 245dvmptco 23780 . . . . . . . . 9 (⊤ → (ℂ D (𝑥𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))))
247 mulneg2 10505 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥))
248220, 12, 247sylancr 696 . . . . . . . . . . . 12 (𝑥𝐷 → (2 · -𝑥) = -(2 · 𝑥))
249248oveq1d 6705 . . . . . . . . . . 11 (𝑥𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))))
25012negcld 10417 . . . . . . . . . . . 12 (𝑥𝐷 → -𝑥 ∈ ℂ)
251 eldifn 3766 . . . . . . . . . . . . . . 15 (𝑥 ∈ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
252251, 3eleq2s 2748 . . . . . . . . . . . . . 14 (𝑥𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
253 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 = -1 → 𝑥 = -1)
254 mnflt 11995 . . . . . . . . . . . . . . . . . . . 20 (-1 ∈ ℝ → -∞ < -1)
25589, 254ax-mp 5 . . . . . . . . . . . . . . . . . . 19 -∞ < -1
256 ubioc1 12265 . . . . . . . . . . . . . . . . . . 19 ((-∞ ∈ ℝ* ∧ -1 ∈ ℝ* ∧ -∞ < -1) → -1 ∈ (-∞(,]-1))
25751, 134, 255, 256mp3an 1464 . . . . . . . . . . . . . . . . . 18 -1 ∈ (-∞(,]-1)
258253, 257syl6eqel 2738 . . . . . . . . . . . . . . . . 17 (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1))
259 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 = 1 → 𝑥 = 1)
260 ltpnf 11992 . . . . . . . . . . . . . . . . . . . 20 (1 ∈ ℝ → 1 < +∞)
26192, 260ax-mp 5 . . . . . . . . . . . . . . . . . . 19 1 < +∞
262 lbico1 12266 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1 < +∞) → 1 ∈ (1[,)+∞))
263135, 123, 261, 262mp3an 1464 . . . . . . . . . . . . . . . . . 18 1 ∈ (1[,)+∞)
264259, 263syl6eqel 2738 . . . . . . . . . . . . . . . . 17 (𝑥 = 1 → 𝑥 ∈ (1[,)+∞))
265258, 264orim12i 537 . . . . . . . . . . . . . . . 16 ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
266265orcoms 403 . . . . . . . . . . . . . . 15 ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
267 elun 3786 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)) ↔ (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
268266, 267sylibr 224 . . . . . . . . . . . . . 14 ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
269252, 268nsyl 135 . . . . . . . . . . . . 13 (𝑥𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1))
270 1cnd 10094 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 ∈ ℂ)
27117adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ)
27219adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈ ℂ)
273 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (√‘(1 − (𝑥↑2))) = 0)
274272, 273sqr00d 14224 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0)
275270, 271, 274subeq0d 10438 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2))
276148, 275syl5req 2698 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2))
277276ex 449 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2)))
278 sqeqor 13018 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
27916, 278mpan2 707 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
280277, 279sylibd 229 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1)))
281280necon3bd 2837 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (¬ (𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1 − (𝑥↑2))) ≠ 0))
28212, 269, 281sylc 65 . . . . . . . . . . . 12 (𝑥𝐷 → (√‘(1 − (𝑥↑2))) ≠ 0)
283 2cnne0 11280 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
284 divcan5 10765 . . . . . . . . . . . . 13 ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
285283, 284mp3an3 1453 . . . . . . . . . . . 12 ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
286250, 114, 282, 285syl12anc 1364 . . . . . . . . . . 11 (𝑥𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
287220, 12, 221sylancr 696 . . . . . . . . . . . . 13 (𝑥𝐷 → (2 · 𝑥) ∈ ℂ)
288287negcld 10417 . . . . . . . . . . . 12 (𝑥𝐷 → -(2 · 𝑥) ∈ ℂ)
289 mulcl 10058 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
290220, 114, 289sylancr 696 . . . . . . . . . . . 12 (𝑥𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
291 mulne0 10707 . . . . . . . . . . . . . 14 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
292283, 291mpan 706 . . . . . . . . . . . . 13 (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
293114, 282, 292syl2anc 694 . . . . . . . . . . . 12 (𝑥𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
294288, 290, 293divrec2d 10843 . . . . . . . . . . 11 (𝑥𝐷 → (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)))
295249, 286, 2943eqtr3rd 2694 . . . . . . . . . 10 (𝑥𝐷 → ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
296295mpteq2ia 4773 . . . . . . . . 9 (𝑥𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) = (𝑥𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2)))))
297246, 296syl6eq 2701 . . . . . . . 8 (⊤ → (ℂ D (𝑥𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2))))))
29811, 74, 75, 111, 115, 116, 297dvmptadd 23768 . . . . . . 7 (⊤ → (ℂ D (𝑥𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))))
299 mulcl 10058 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
30013, 20, 299sylancr 696 . . . . . . . . . . 11 (𝑥 ∈ ℂ → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
30112, 300syl 17 . . . . . . . . . 10 (𝑥𝐷 → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
302301, 250, 114, 282divdird 10877 . . . . . . . . 9 (𝑥𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))))
303 ixi 10694 . . . . . . . . . . . . . . . 16 (i · i) = -1
304303eqcomi 2660 . . . . . . . . . . . . . . 15 -1 = (i · i)
305304oveq1i 6700 . . . . . . . . . . . . . 14 (-1 · 𝑥) = ((i · i) · 𝑥)
306 mulm1 10509 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → (-1 · 𝑥) = -𝑥)
307 mulass 10062 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i) · 𝑥) = (i · (i · 𝑥)))
30813, 13, 307mp3an12 1454 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → ((i · i) · 𝑥) = (i · (i · 𝑥)))
309305, 306, 3083eqtr3a 2709 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥)))
310309oveq1d 6705 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → (-𝑥 + (i · (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
311 negcl 10319 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
312300, 311addcomd 10276 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (-𝑥 + (i · (√‘(1 − (𝑥↑2))))))
31313a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → i ∈ ℂ)
314313, 15, 20adddid 10102 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
315310, 312, 3143eqtr4d 2695 . . . . . . . . . . 11 (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
31612, 315syl 17 . . . . . . . . . 10 (𝑥𝐷 → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
317316oveq1d 6705 . . . . . . . . 9 (𝑥𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
31872, 114, 282divcan4d 10845 . . . . . . . . . 10 (𝑥𝐷 → ((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) = i)
319318oveq1d 6705 . . . . . . . . 9 (𝑥𝐷 → (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))) = (i + (-𝑥 / (√‘(1 − (𝑥↑2))))))
320302, 317, 3193eqtr3rd 2694 . . . . . . . 8 (𝑥𝐷 → (i + (-𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
321320mpteq2ia 4773 . . . . . . 7 (𝑥𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
322298, 321syl6eq 2701 . . . . . 6 (⊤ → (ℂ D (𝑥𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
323240dvlog 24442 . . . . . . 7 (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦))
324 logf1o 24356 . . . . . . . . . 10 log:(ℂ ∖ {0})–1-1-onto→ran log
325 f1of 6175 . . . . . . . . . 10 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
326324, 325mp1i 13 . . . . . . . . 9 (⊤ → log:(ℂ ∖ {0})⟶ran log)
327 snssi 4371 . . . . . . . . . . 11 (0 ∈ (-∞(,]0) → {0} ⊆ (-∞(,]0))
32864, 327ax-mp 5 . . . . . . . . . 10 {0} ⊆ (-∞(,]0)
329 sscon 3777 . . . . . . . . . 10 ({0} ⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
330328, 329mp1i 13 . . . . . . . . 9 (⊤ → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
331326, 330feqresmpt 6289 . . . . . . . 8 (⊤ → (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦)))
332331oveq2d 6706 . . . . . . 7 (⊤ → (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))))
333323, 332syl5reqr 2700 . . . . . 6 (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦)))
334 fveq2 6229 . . . . . 6 (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (log‘𝑦) = (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
335 oveq2 6698 . . . . . 6 (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (1 / 𝑦) = (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
33611, 11, 57, 58, 70, 71, 322, 333, 334, 335dvmptco 23780 . . . . 5 (⊤ → (ℂ D (𝑥𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))))
33722, 24reccld 10832 . . . . . . . 8 (𝑥𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
338 mulcl 10058 . . . . . . . . . 10 ((i ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ) → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
33913, 21, 338sylancr 696 . . . . . . . . 9 (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
34012, 339syl 17 . . . . . . . 8 (𝑥𝐷 → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
341337, 340, 114, 282divassd 10874 . . . . . . 7 (𝑥𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
342340, 22, 24divrec2d 10843 . . . . . . . . 9 (𝑥𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
34372, 22, 24divcan4d 10845 . . . . . . . . 9 (𝑥𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = i)
344342, 343eqtr3d 2687 . . . . . . . 8 (𝑥𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = i)
345344oveq1d 6705 . . . . . . 7 (𝑥𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = (i / (√‘(1 − (𝑥↑2)))))
346341, 345eqtr3d 2687 . . . . . 6 (𝑥𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))) = (i / (√‘(1 − (𝑥↑2)))))
347346mpteq2ia 4773 . . . . 5 (𝑥𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ (i / (√‘(1 − (𝑥↑2)))))
348336, 347syl6eq 2701 . . . 4 (⊤ → (ℂ D (𝑥𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥𝐷 ↦ (i / (√‘(1 − (𝑥↑2))))))
349 negicn 10320 . . . . 5 -i ∈ ℂ
350349a1i 11 . . . 4 (⊤ → -i ∈ ℂ)
35111, 26, 27, 348, 350dvmptcmul 23772 . . 3 (⊤ → (ℂ D (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))))
352351trud 1533 . 2 (ℂ D (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2))))))
35313, 13mulneg1i 10514 . . . . . 6 (-i · i) = -(i · i)
354303negeqi 10312 . . . . . 6 -(i · i) = --1
355 negneg1e1 11166 . . . . . 6 --1 = 1
356353, 354, 3553eqtri 2677 . . . . 5 (-i · i) = 1
357356oveq1i 6700 . . . 4 ((-i · i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 − (𝑥↑2))))
358 divass 10741 . . . . . 6 ((-i ∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
359349, 13, 358mp3an12 1454 . . . . 5 (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
360114, 282, 359syl2anc 694 . . . 4 (𝑥𝐷 → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
361357, 360syl5reqr 2700 . . 3 (𝑥𝐷 → (-i · (i / (√‘(1 − (𝑥↑2))))) = (1 / (√‘(1 − (𝑥↑2)))))
362361mpteq2ia 4773 . 2 (𝑥𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
3639, 352, 3623eqtri 2677 1 (ℂ D (arcsin ↾ 𝐷)) = (𝑥𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∨ w3o 1053   ∧ w3a 1054   = wceq 1523  ⊤wtru 1524   ∈ wcel 2030   ≠ wne 2823  Vcvv 3231   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  {csn 4210  {cpr 4212   class class class wbr 4685   ↦ cmpt 4762  ran crn 5144   ↾ cres 5145  ⟶wf 5922  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975  ici 9976   + caddc 9977   · cmul 9979  +∞cpnf 10109  -∞cmnf 10110  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304  -cneg 10305   / cdiv 10722  ℕcn 11058  2c2 11108  ℝ+crp 11870  (,)cioo 12213  (,]cioc 12214  [,)cico 12215  ↑cexp 12900  ℜcre 13881  √csqrt 14017  abscabs 14018   ↾t crest 16128  TopOpenctopn 16129  topGenctg 16145  ℂfldccnfld 19794  TopOnctopon 20763  Clsdccld 20868   D cdv 23672  logclog 24346  arcsincasin 24634 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-tan 14846  df-pi 14847  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676  df-log 24348  df-cxp 24349  df-asin 24637 This theorem is referenced by:  dvacos  33627  dvreasin  33628
 Copyright terms: Public domain W3C validator