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

Theorem dvasin 35861
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 26015 . . . . 5 arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
21reseq1i 5887 . . . 4 (arcsin ↾ 𝐷) = ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷)
3 dvasin.d . . . . . 6 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
4 difss 4066 . . . . . 6 (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆ ℂ
53, 4eqsstri 3955 . . . . 5 𝐷 ⊆ ℂ
6 resmpt 5945 . . . . 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 2766 . . 3 (arcsin ↾ 𝐷) = (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
98oveq2i 7286 . 2 (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
10 cnelprrecn 10964 . . . . 5 ℂ ∈ {ℝ, ℂ}
1110a1i 11 . . . 4 (⊤ → ℂ ∈ {ℝ, ℂ})
125sseli 3917 . . . . . . 7 (𝑥𝐷𝑥 ∈ ℂ)
13 ax-icn 10930 . . . . . . . . 9 i ∈ ℂ
14 mulcl 10955 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
1513, 14mpan 687 . . . . . . . 8 (𝑥 ∈ ℂ → (i · 𝑥) ∈ ℂ)
16 ax-1cn 10929 . . . . . . . . . 10 1 ∈ ℂ
17 sqcl 13838 . . . . . . . . . 10 (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
18 subcl 11220 . . . . . . . . . 10 ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
1916, 17, 18sylancr 587 . . . . . . . . 9 (𝑥 ∈ ℂ → (1 − (𝑥↑2)) ∈ ℂ)
2019sqrtcld 15149 . . . . . . . 8 (𝑥 ∈ ℂ → (√‘(1 − (𝑥↑2))) ∈ ℂ)
2115, 20addcld 10994 . . . . . . 7 (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
2212, 21syl 17 . . . . . 6 (𝑥𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
23 asinlem 26018 . . . . . . 7 (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
2412, 23syl 17 . . . . . 6 (𝑥𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
2522, 24logcld 25726 . . . . 5 (𝑥𝐷 → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
2625adantl 482 . . . 4 ((⊤ ∧ 𝑥𝐷) → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
27 ovexd 7310 . . . 4 ((⊤ ∧ 𝑥𝐷) → (i / (√‘(1 − (𝑥↑2)))) ∈ V)
28 simpr 485 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
29 asinlem3 26021 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
30 rere 14833 . . . . . . . . . . . . . . . . . . 19 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
3130breq2d 5086 . . . . . . . . . . . . . . . . . 18 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
3231biimpac 479 . . . . . . . . . . . . . . . . 17 ((0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
3329, 32sylan 580 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
3423adantr 481 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
3528, 33, 34ne0gt0d 11112 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
36 0re 10977 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
37 ltnle 11054 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
3836, 37mpan 687 . . . . . . . . . . . . . . . 16 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
3938adantl 482 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4035, 39mpbid 231 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)
4140ex 413 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4212, 41syl 17 . . . . . . . . . . . 12 (𝑥𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
43 imor 850 . . . . . . . . . . . 12 ((((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4442, 43sylib 217 . . . . . . . . . . 11 (𝑥𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4544orcomd 868 . . . . . . . . . 10 (𝑥𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
4645olcd 871 . . . . . . . . 9 (𝑥𝐷 → (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
47 3ianor 1106 . . . . . . . . . . 11 (¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
48 3orrot 1091 . . . . . . . . . . 11 ((¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
49 3orass 1089 . . . . . . . . . . 11 ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
5047, 48, 493bitrri 298 . . . . . . . . . 10 ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
51 mnfxr 11032 . . . . . . . . . . 11 -∞ ∈ ℝ*
52 elioc2 13142 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)))
5351, 36, 52mp2an 689 . . . . . . . . . 10 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
5450, 53xchbinxr 335 . . . . . . . . 9 ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
5546, 54sylib 217 . . . . . . . 8 (𝑥𝐷 → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
5622, 55eldifd 3898 . . . . . . 7 (𝑥𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
5756adantl 482 . . . . . 6 ((⊤ ∧ 𝑥𝐷) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
58 ovexd 7310 . . . . . 6 ((⊤ ∧ 𝑥𝐷) → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))) ∈ V)
59 eldifi 4061 . . . . . . . 8 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ∈ ℂ)
60 eldifn 4062 . . . . . . . . 9 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0))
61 0xr 11022 . . . . . . . . . . . 12 0 ∈ ℝ*
62 mnflt0 12861 . . . . . . . . . . . 12 -∞ < 0
63 ubioc1 13132 . . . . . . . . . . . 12 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ -∞ < 0) → 0 ∈ (-∞(,]0))
6451, 61, 62, 63mp3an 1460 . . . . . . . . . . 11 0 ∈ (-∞(,]0)
65 eleq1 2826 . . . . . . . . . . 11 (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈ (-∞(,]0)))
6664, 65mpbiri 257 . . . . . . . . . 10 (𝑦 = 0 → 𝑦 ∈ (-∞(,]0))
6766necon3bi 2970 . . . . . . . . 9 𝑦 ∈ (-∞(,]0) → 𝑦 ≠ 0)
6860, 67syl 17 . . . . . . . 8 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ≠ 0)
6959, 68logcld 25726 . . . . . . 7 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (log‘𝑦) ∈ ℂ)
7069adantl 482 . . . . . 6 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ)
71 ovexd 7310 . . . . . 6 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V)
7213a1i 11 . . . . . . . . . 10 (𝑥𝐷 → i ∈ ℂ)
7372, 12mulcld 10995 . . . . . . . . 9 (𝑥𝐷 → (i · 𝑥) ∈ ℂ)
7473adantl 482 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → (i · 𝑥) ∈ ℂ)
7513a1i 11 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → i ∈ ℂ)
7612adantl 482 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → 𝑥 ∈ ℂ)
77 1cnd 10970 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → 1 ∈ ℂ)
78 simpr 485 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
79 1cnd 10970 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
8011dvmptid 25121 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
815a1i 11 . . . . . . . . . . 11 (⊤ → 𝐷 ⊆ ℂ)
82 eqid 2738 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
8382cnfldtopon 23946 . . . . . . . . . . . 12 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
8483toponrestid 22070 . . . . . . . . . . 11 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
8582recld2 23977 . . . . . . . . . . . . . . 15 ℝ ∈ (Clsd‘(TopOpen‘ℂfld))
86 neg1rr 12088 . . . . . . . . . . . . . . . . . 18 -1 ∈ ℝ
87 iocmnfcld 23932 . . . . . . . . . . . . . . . . . 18 (-1 ∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))))
8886, 87ax-mp 5 . . . . . . . . . . . . . . . . 17 (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,)))
89 1re 10975 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
90 icopnfcld 23931 . . . . . . . . . . . . . . . . . 18 (1 ∈ ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
9189, 90ax-mp 5 . . . . . . . . . . . . . . . . 17 (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))
92 uncld 22192 . . . . . . . . . . . . . . . . 17 (((-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))) ∧ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,))))
9388, 91, 92mp2an 689 . . . . . . . . . . . . . . . 16 ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,)))
9482tgioo2 23966 . . . . . . . . . . . . . . . . 17 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
9594fveq2i 6777 . . . . . . . . . . . . . . . 16 (Clsd‘(topGen‘ran (,))) = (Clsd‘((TopOpen‘ℂfld) ↾t ℝ))
9693, 95eleqtri 2837 . . . . . . . . . . . . . . 15 ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂfld) ↾t ℝ))
97 restcldr 22325 . . . . . . . . . . . . . . 15 ((ℝ ∈ (Clsd‘(TopOpen‘ℂfld)) ∧ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂfld) ↾t ℝ))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂfld)))
9885, 96, 97mp2an 689 . . . . . . . . . . . . . 14 ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂfld))
9983toponunii 22065 . . . . . . . . . . . . . . 15 ℂ = (TopOpen‘ℂfld)
10099cldopn 22182 . . . . . . . . . . . . . 14 (((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂfld))
10198, 100ax-mp 5 . . . . . . . . . . . . 13 (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂfld)
1023, 101eqeltri 2835 . . . . . . . . . . . 12 𝐷 ∈ (TopOpen‘ℂfld)
103102a1i 11 . . . . . . . . . . 11 (⊤ → 𝐷 ∈ (TopOpen‘ℂfld))
10411, 78, 79, 80, 81, 84, 82, 103dvmptres 25127 . . . . . . . . . 10 (⊤ → (ℂ D (𝑥𝐷𝑥)) = (𝑥𝐷 ↦ 1))
10513a1i 11 . . . . . . . . . 10 (⊤ → i ∈ ℂ)
10611, 76, 77, 104, 105dvmptcmul 25128 . . . . . . . . 9 (⊤ → (ℂ D (𝑥𝐷 ↦ (i · 𝑥))) = (𝑥𝐷 ↦ (i · 1)))
10713mulid1i 10979 . . . . . . . . . 10 (i · 1) = i
108107mpteq2i 5179 . . . . . . . . 9 (𝑥𝐷 ↦ (i · 1)) = (𝑥𝐷 ↦ i)
109106, 108eqtrdi 2794 . . . . . . . 8 (⊤ → (ℂ D (𝑥𝐷 ↦ (i · 𝑥))) = (𝑥𝐷 ↦ i))
11012sqcld 13862 . . . . . . . . . . 11 (𝑥𝐷 → (𝑥↑2) ∈ ℂ)
11116, 110, 18sylancr 587 . . . . . . . . . 10 (𝑥𝐷 → (1 − (𝑥↑2)) ∈ ℂ)
112111sqrtcld 15149 . . . . . . . . 9 (𝑥𝐷 → (√‘(1 − (𝑥↑2))) ∈ ℂ)
113112adantl 482 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → (√‘(1 − (𝑥↑2))) ∈ ℂ)
114 ovexd 7310 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → (-𝑥 / (√‘(1 − (𝑥↑2)))) ∈ V)
115 elin 3903 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥𝐷𝑥 ∈ ℝ))
1163asindmre 35860 . . . . . . . . . . . . . . . . 17 (𝐷 ∩ ℝ) = (-1(,)1)
117116eqimssi 3979 . . . . . . . . . . . . . . . 16 (𝐷 ∩ ℝ) ⊆ (-1(,)1)
118117sseli 3917 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ (-1(,)1))
119115, 118sylbir 234 . . . . . . . . . . . . . 14 ((𝑥𝐷𝑥 ∈ ℝ) → 𝑥 ∈ (-1(,)1))
120 incom 4135 . . . . . . . . . . . . . . . 16 ((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩ (0(,)+∞))
121 pnfxr 11029 . . . . . . . . . . . . . . . . 17 +∞ ∈ ℝ*
122 df-ioc 13084 . . . . . . . . . . . . . . . . . 18 (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
123 df-ioo 13083 . . . . . . . . . . . . . . . . . 18 (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
124 xrltnle 11042 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℝ*𝑤 ∈ ℝ*) → (0 < 𝑤 ↔ ¬ 𝑤 ≤ 0))
125122, 123, 124ixxdisj 13094 . . . . . . . . . . . . . . . . 17 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((-∞(,]0) ∩ (0(,)+∞)) = ∅)
12651, 61, 121, 125mp3an 1460 . . . . . . . . . . . . . . . 16 ((-∞(,]0) ∩ (0(,)+∞)) = ∅
127120, 126eqtri 2766 . . . . . . . . . . . . . . 15 ((0(,)+∞) ∩ (-∞(,]0)) = ∅
128 elioore 13109 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (-1(,)1) → 𝑥 ∈ ℝ)
129128resqcld 13965 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (-1(,)1) → (𝑥↑2) ∈ ℝ)
130 resubcl 11285 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 − (𝑥↑2)) ∈ ℝ)
13189, 129, 130sylancr 587 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ)
13286rexri 11033 . . . . . . . . . . . . . . . . . . 19 -1 ∈ ℝ*
133 1xr 11034 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ*
134 elioo2 13120 . . . . . . . . . . . . . . . . . . 19 ((-1 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥𝑥 < 1)))
135132, 133, 134mp2an 689 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥𝑥 < 1))
136 recn 10961 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
137136abscld 15148 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
138136absge0d 15156 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → 0 ≤ (abs‘𝑥))
139 0le1 11498 . . . . . . . . . . . . . . . . . . . . . . 23 0 ≤ 1
140 lt2sq 13852 . . . . . . . . . . . . . . . . . . . . . . 23 ((((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
14189, 139, 140mpanr12 702 . . . . . . . . . . . . . . . . . . . . . 22 (((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
142137, 138, 141syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
143 abslt 15026 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥𝑥 < 1)))
14489, 143mpan2 688 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥𝑥 < 1)))
145 absresq 15014 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → ((abs‘𝑥)↑2) = (𝑥↑2))
146 sq1 13912 . . . . . . . . . . . . . . . . . . . . . . . 24 (1↑2) = 1
147146a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → (1↑2) = 1)
148145, 147breq12d 5087 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ (𝑥↑2) < 1))
149 resqcl 13844 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → (𝑥↑2) ∈ ℝ)
150 posdif 11468 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥↑2) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
151149, 89, 150sylancl 586 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
152148, 151bitrd 278 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ 0 < (1 − (𝑥↑2))))
153142, 144, 1523bitr3d 309 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → ((-1 < 𝑥𝑥 < 1) ↔ 0 < (1 − (𝑥↑2))))
154153biimpd 228 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → ((-1 < 𝑥𝑥 < 1) → 0 < (1 − (𝑥↑2))))
1551543impib 1115 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ -1 < 𝑥𝑥 < 1) → 0 < (1 − (𝑥↑2)))
156135, 155sylbi 216 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (-1(,)1) → 0 < (1 − (𝑥↑2)))
157131, 156elrpd 12769 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ+)
158 ioorp 13157 . . . . . . . . . . . . . . . 16 (0(,)+∞) = ℝ+
159157, 158eleqtrrdi 2850 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ (0(,)+∞))
160 disjel 4390 . . . . . . . . . . . . . . 15 ((((0(,)+∞) ∩ (-∞(,]0)) = ∅ ∧ (1 − (𝑥↑2)) ∈ (0(,)+∞)) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
161127, 159, 160sylancr 587 . . . . . . . . . . . . . 14 (𝑥 ∈ (-1(,)1) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
162119, 161syl 17 . . . . . . . . . . . . 13 ((𝑥𝐷𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
163 elioc2 13142 . . . . . . . . . . . . . . . . . . . . . . . 24 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0)))
16451, 36, 163mp2an 689 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
165164biimpi 215 . . . . . . . . . . . . . . . . . . . . . 22 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
166165simp1d 1141 . . . . . . . . . . . . . . . . . . . . 21 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ)
167 resubcl 11285 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
16889, 166, 167sylancr 587 . . . . . . . . . . . . . . . . . . . 20 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
169 nncan 11250 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
17016, 169mpan 687 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥↑2) ∈ ℂ → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
171170eleq1d 2823 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥↑2) ∈ ℂ → ((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈ ℝ))
172171biimpa 477 . . . . . . . . . . . . . . . . . . . 20 (((𝑥↑2) ∈ ℂ ∧ (1 − (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈ ℝ)
173168, 172sylan2 593 . . . . . . . . . . . . . . . . . . 19 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥↑2) ∈ ℝ)
174166adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ)
175165simp3d 1143 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ≤ 0)
176175adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0)
177 letr 11069 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1 − (𝑥↑2)) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
17836, 89, 177mp3an23 1452 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 − (𝑥↑2)) ∈ ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
179139, 178mpan2i 694 . . . . . . . . . . . . . . . . . . . . . 22 ((1 − (𝑥↑2)) ∈ ℝ → ((1 − (𝑥↑2)) ≤ 0 → (1 − (𝑥↑2)) ≤ 1))
180174, 176, 179sylc 65 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 1)
181 subge0 11488 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
18289, 174, 181sylancr 587 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
183180, 182mpbird 256 . . . . . . . . . . . . . . . . . . . 20 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2))))
184170adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
185183, 184breqtrd 5100 . . . . . . . . . . . . . . . . . . 19 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (𝑥↑2))
186173, 185resqrtcld 15129 . . . . . . . . . . . . . . . . . 18 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
18717, 186sylan 580 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
188 eleq1 2826 . . . . . . . . . . . . . . . . 17 (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ (√‘(𝑥↑2)) ∈ ℝ))
189187, 188syl5ibrcom 246 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
190187renegcld 11402 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ)
191 eleq1 2826 . . . . . . . . . . . . . . . . 17 (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ -(√‘(𝑥↑2)) ∈ ℝ))
192190, 191syl5ibrcom 246 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = -(√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
193 eqid 2738 . . . . . . . . . . . . . . . . . 18 (𝑥↑2) = (𝑥↑2)
194 eqsqrtor 15078 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
19517, 194mpdan 684 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
196193, 195mpbii 232 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
197196adantr 481 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
198189, 192, 197mpjaod 857 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 𝑥 ∈ ℝ)
199198stoic1a 1775 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
20012, 199sylan 580 . . . . . . . . . . . . 13 ((𝑥𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
201162, 200pm2.61dan 810 . . . . . . . . . . . 12 (𝑥𝐷 → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
202111, 201eldifd 3898 . . . . . . . . . . 11 (𝑥𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
203202adantl 482 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
204 2cnd 12051 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → 2 ∈ ℂ)
205 id 22 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
206204, 205mulcld 10995 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
207206negcld 11319 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → -(2 · 𝑥) ∈ ℂ)
208207adantl 482 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → -(2 · 𝑥) ∈ ℂ)
20912, 208sylan2 593 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → -(2 · 𝑥) ∈ ℂ)
21059sqrtcld 15149 . . . . . . . . . . 11 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (√‘𝑦) ∈ ℂ)
211210adantl 482 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈ ℂ)
212 ovexd 7310 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 · (√‘𝑦))) ∈ V)
21319adantl 482 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
21436a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → 0 ∈ ℝ)
215 1cnd 10970 . . . . . . . . . . . . . 14 (⊤ → 1 ∈ ℂ)
21611, 215dvmptc 25122 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 1)) = (𝑥 ∈ ℂ ↦ 0))
21717adantl 482 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥↑2) ∈ ℂ)
218 2cn 12048 . . . . . . . . . . . . . . 15 2 ∈ ℂ
219 mulcl 10955 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
220218, 219mpan 687 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
221220adantl 482 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
222 2nn 12046 . . . . . . . . . . . . . . . 16 2 ∈ ℕ
223 dvexp 25117 . . . . . . . . . . . . . . . 16 (2 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))))
224222, 223ax-mp 5 . . . . . . . . . . . . . . 15 (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1))))
225 2m1e1 12099 . . . . . . . . . . . . . . . . . . 19 (2 − 1) = 1
226225oveq2i 7286 . . . . . . . . . . . . . . . . . 18 (𝑥↑(2 − 1)) = (𝑥↑1)
227 exp1 13788 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥)
228226, 227eqtrid 2790 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥)
229228oveq2d 7291 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥))
230229mpteq2ia 5177 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
231224, 230eqtri 2766 . . . . . . . . . . . . . 14 (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
232231a1i 11 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥)))
23311, 79, 214, 216, 217, 221, 232dvmptsub 25131 . . . . . . . . . . . 12 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥))))
234 df-neg 11208 . . . . . . . . . . . . 13 -(2 · 𝑥) = (0 − (2 · 𝑥))
235234mpteq2i 5179 . . . . . . . . . . . 12 (𝑥 ∈ ℂ ↦ -(2 · 𝑥)) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥)))
236233, 235eqtr4di 2796 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥)))
23711, 213, 208, 236, 81, 84, 82, 103dvmptres 25127 . . . . . . . . . 10 (⊤ → (ℂ D (𝑥𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥𝐷 ↦ -(2 · 𝑥)))
238 eqid 2738 . . . . . . . . . . . 12 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
239238dvcnsqrt 25897 . . . . . . . . . . 11 (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦))))
240239a1i 11 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦)))))
241 fveq2 6774 . . . . . . . . . 10 (𝑦 = (1 − (𝑥↑2)) → (√‘𝑦) = (√‘(1 − (𝑥↑2))))
242241oveq2d 7291 . . . . . . . . . . 11 (𝑦 = (1 − (𝑥↑2)) → (2 · (√‘𝑦)) = (2 · (√‘(1 − (𝑥↑2)))))
243242oveq2d 7291 . . . . . . . . . 10 (𝑦 = (1 − (𝑥↑2)) → (1 / (2 · (√‘𝑦))) = (1 / (2 · (√‘(1 − (𝑥↑2))))))
24411, 11, 203, 209, 211, 212, 237, 240, 241, 243dvmptco 25136 . . . . . . . . 9 (⊤ → (ℂ D (𝑥𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))))
245 mulneg2 11412 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥))
246218, 12, 245sylancr 587 . . . . . . . . . . . 12 (𝑥𝐷 → (2 · -𝑥) = -(2 · 𝑥))
247246oveq1d 7290 . . . . . . . . . . 11 (𝑥𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))))
24812negcld 11319 . . . . . . . . . . . 12 (𝑥𝐷 → -𝑥 ∈ ℂ)
249 eldifn 4062 . . . . . . . . . . . . . . 15 (𝑥 ∈ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
250249, 3eleq2s 2857 . . . . . . . . . . . . . 14 (𝑥𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
251 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 = -1 → 𝑥 = -1)
252 mnflt 12859 . . . . . . . . . . . . . . . . . . . 20 (-1 ∈ ℝ → -∞ < -1)
25386, 252ax-mp 5 . . . . . . . . . . . . . . . . . . 19 -∞ < -1
254 ubioc1 13132 . . . . . . . . . . . . . . . . . . 19 ((-∞ ∈ ℝ* ∧ -1 ∈ ℝ* ∧ -∞ < -1) → -1 ∈ (-∞(,]-1))
25551, 132, 253, 254mp3an 1460 . . . . . . . . . . . . . . . . . 18 -1 ∈ (-∞(,]-1)
256251, 255eqeltrdi 2847 . . . . . . . . . . . . . . . . 17 (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1))
257 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 = 1 → 𝑥 = 1)
258 ltpnf 12856 . . . . . . . . . . . . . . . . . . . 20 (1 ∈ ℝ → 1 < +∞)
25989, 258ax-mp 5 . . . . . . . . . . . . . . . . . . 19 1 < +∞
260 lbico1 13133 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1 < +∞) → 1 ∈ (1[,)+∞))
261133, 121, 259, 260mp3an 1460 . . . . . . . . . . . . . . . . . 18 1 ∈ (1[,)+∞)
262257, 261eqeltrdi 2847 . . . . . . . . . . . . . . . . 17 (𝑥 = 1 → 𝑥 ∈ (1[,)+∞))
263256, 262orim12i 906 . . . . . . . . . . . . . . . 16 ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
264263orcoms 869 . . . . . . . . . . . . . . 15 ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
265 elun 4083 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)) ↔ (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
266264, 265sylibr 233 . . . . . . . . . . . . . 14 ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
267250, 266nsyl 140 . . . . . . . . . . . . 13 (𝑥𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1))
268 1cnd 10970 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 ∈ ℂ)
26917adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ)
27019adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈ ℂ)
271 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (√‘(1 − (𝑥↑2))) = 0)
272270, 271sqr00d 15153 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0)
273268, 269, 272subeq0d 11340 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2))
274146, 273eqtr2id 2791 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2))
275274ex 413 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2)))
276 sqeqor 13932 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
27716, 276mpan2 688 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
278275, 277sylibd 238 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1)))
279278necon3bd 2957 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (¬ (𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1 − (𝑥↑2))) ≠ 0))
28012, 267, 279sylc 65 . . . . . . . . . . . 12 (𝑥𝐷 → (√‘(1 − (𝑥↑2))) ≠ 0)
281 2cnne0 12183 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
282 divcan5 11677 . . . . . . . . . . . . 13 ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
283281, 282mp3an3 1449 . . . . . . . . . . . 12 ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
284248, 112, 280, 283syl12anc 834 . . . . . . . . . . 11 (𝑥𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
285218, 12, 219sylancr 587 . . . . . . . . . . . . 13 (𝑥𝐷 → (2 · 𝑥) ∈ ℂ)
286285negcld 11319 . . . . . . . . . . . 12 (𝑥𝐷 → -(2 · 𝑥) ∈ ℂ)
287 mulcl 10955 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
288218, 112, 287sylancr 587 . . . . . . . . . . . 12 (𝑥𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
289 mulne0 11617 . . . . . . . . . . . . . 14 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
290281, 289mpan 687 . . . . . . . . . . . . 13 (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
291112, 280, 290syl2anc 584 . . . . . . . . . . . 12 (𝑥𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
292286, 288, 291divrec2d 11755 . . . . . . . . . . 11 (𝑥𝐷 → (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)))
293247, 284, 2923eqtr3rd 2787 . . . . . . . . . 10 (𝑥𝐷 → ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
294293mpteq2ia 5177 . . . . . . . . 9 (𝑥𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) = (𝑥𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2)))))
295244, 294eqtrdi 2794 . . . . . . . 8 (⊤ → (ℂ D (𝑥𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2))))))
29611, 74, 75, 109, 113, 114, 295dvmptadd 25124 . . . . . . 7 (⊤ → (ℂ D (𝑥𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))))
297 mulcl 10955 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
29813, 20, 297sylancr 587 . . . . . . . . . . 11 (𝑥 ∈ ℂ → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
29912, 298syl 17 . . . . . . . . . 10 (𝑥𝐷 → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
300299, 248, 112, 280divdird 11789 . . . . . . . . 9 (𝑥𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))))
301 ixi 11604 . . . . . . . . . . . . . . . 16 (i · i) = -1
302301eqcomi 2747 . . . . . . . . . . . . . . 15 -1 = (i · i)
303302oveq1i 7285 . . . . . . . . . . . . . 14 (-1 · 𝑥) = ((i · i) · 𝑥)
304 mulm1 11416 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → (-1 · 𝑥) = -𝑥)
305 mulass 10959 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i) · 𝑥) = (i · (i · 𝑥)))
30613, 13, 305mp3an12 1450 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → ((i · i) · 𝑥) = (i · (i · 𝑥)))
307303, 304, 3063eqtr3a 2802 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥)))
308307oveq1d 7290 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → (-𝑥 + (i · (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
309 negcl 11221 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
310298, 309addcomd 11177 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (-𝑥 + (i · (√‘(1 − (𝑥↑2))))))
31113a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → i ∈ ℂ)
312311, 15, 20adddid 10999 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
313308, 310, 3123eqtr4d 2788 . . . . . . . . . . 11 (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
31412, 313syl 17 . . . . . . . . . 10 (𝑥𝐷 → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
315314oveq1d 7290 . . . . . . . . 9 (𝑥𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
31672, 112, 280divcan4d 11757 . . . . . . . . . 10 (𝑥𝐷 → ((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) = i)
317316oveq1d 7290 . . . . . . . . 9 (𝑥𝐷 → (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))) = (i + (-𝑥 / (√‘(1 − (𝑥↑2))))))
318300, 315, 3173eqtr3rd 2787 . . . . . . . 8 (𝑥𝐷 → (i + (-𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
319318mpteq2ia 5177 . . . . . . 7 (𝑥𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
320296, 319eqtrdi 2794 . . . . . 6 (⊤ → (ℂ D (𝑥𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
321 logf1o 25720 . . . . . . . . . 10 log:(ℂ ∖ {0})–1-1-onto→ran log
322 f1of 6716 . . . . . . . . . 10 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
323321, 322mp1i 13 . . . . . . . . 9 (⊤ → log:(ℂ ∖ {0})⟶ran log)
324 snssi 4741 . . . . . . . . . . 11 (0 ∈ (-∞(,]0) → {0} ⊆ (-∞(,]0))
32564, 324ax-mp 5 . . . . . . . . . 10 {0} ⊆ (-∞(,]0)
326 sscon 4073 . . . . . . . . . 10 ({0} ⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
327325, 326mp1i 13 . . . . . . . . 9 (⊤ → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
328323, 327feqresmpt 6838 . . . . . . . 8 (⊤ → (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦)))
329328oveq2d 7291 . . . . . . 7 (⊤ → (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))))
330238dvlog 25806 . . . . . . 7 (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦))
331329, 330eqtr3di 2793 . . . . . 6 (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦)))
332 fveq2 6774 . . . . . 6 (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (log‘𝑦) = (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
333 oveq2 7283 . . . . . 6 (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (1 / 𝑦) = (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
33411, 11, 57, 58, 70, 71, 320, 331, 332, 333dvmptco 25136 . . . . 5 (⊤ → (ℂ D (𝑥𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))))
33522, 24reccld 11744 . . . . . . . 8 (𝑥𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
336 mulcl 10955 . . . . . . . . . 10 ((i ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ) → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
33713, 21, 336sylancr 587 . . . . . . . . 9 (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
33812, 337syl 17 . . . . . . . 8 (𝑥𝐷 → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
339335, 338, 112, 280divassd 11786 . . . . . . 7 (𝑥𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
340338, 22, 24divrec2d 11755 . . . . . . . . 9 (𝑥𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
34172, 22, 24divcan4d 11757 . . . . . . . . 9 (𝑥𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = i)
342340, 341eqtr3d 2780 . . . . . . . 8 (𝑥𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = i)
343342oveq1d 7290 . . . . . . 7 (𝑥𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = (i / (√‘(1 − (𝑥↑2)))))
344339, 343eqtr3d 2780 . . . . . 6 (𝑥𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))) = (i / (√‘(1 − (𝑥↑2)))))
345344mpteq2ia 5177 . . . . 5 (𝑥𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ (i / (√‘(1 − (𝑥↑2)))))
346334, 345eqtrdi 2794 . . . 4 (⊤ → (ℂ D (𝑥𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥𝐷 ↦ (i / (√‘(1 − (𝑥↑2))))))
347 negicn 11222 . . . . 5 -i ∈ ℂ
348347a1i 11 . . . 4 (⊤ → -i ∈ ℂ)
34911, 26, 27, 346, 348dvmptcmul 25128 . . 3 (⊤ → (ℂ D (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))))
350349mptru 1546 . 2 (ℂ D (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2))))))
351 divass 11651 . . . . . 6 ((-i ∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
352347, 13, 351mp3an12 1450 . . . . 5 (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
353112, 280, 352syl2anc 584 . . . 4 (𝑥𝐷 → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
35413, 13mulneg1i 11421 . . . . . 6 (-i · i) = -(i · i)
355301negeqi 11214 . . . . . 6 -(i · i) = --1
356 negneg1e1 12091 . . . . . 6 --1 = 1
357354, 355, 3563eqtri 2770 . . . . 5 (-i · i) = 1
358357oveq1i 7285 . . . 4 ((-i · i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 − (𝑥↑2))))
359353, 358eqtr3di 2793 . . 3 (𝑥𝐷 → (-i · (i / (√‘(1 − (𝑥↑2))))) = (1 / (√‘(1 − (𝑥↑2)))))
360359mpteq2ia 5177 . 2 (𝑥𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
3619, 350, 3603eqtri 2770 1 (ℂ D (arcsin ↾ 𝐷)) = (𝑥𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3o 1085  w3a 1086   = wceq 1539  wtru 1540  wcel 2106  wne 2943  Vcvv 3432  cdif 3884  cun 3885  cin 3886  wss 3887  c0 4256  {csn 4561  {cpr 4563   class class class wbr 5074  cmpt 5157  ran crn 5590  cres 5591  wf 6429  1-1-ontowf1o 6432  cfv 6433  (class class class)co 7275  cc 10869  cr 10870  0cc0 10871  1c1 10872  ici 10873   + caddc 10874   · cmul 10876  +∞cpnf 11006  -∞cmnf 11007  *cxr 11008   < clt 11009  cle 11010  cmin 11205  -cneg 11206   / cdiv 11632  cn 11973  2c2 12028  +crp 12730  (,)cioo 13079  (,]cioc 13080  [,)cico 13081  cexp 13782  cre 14808  csqrt 14944  abscabs 14945  t crest 17131  TopOpenctopn 17132  topGenctg 17148  fldccnfld 20597  Clsdccld 22167   D cdv 25027  logclog 25710  arcsincasin 26012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949  ax-addf 10950  ax-mulf 10951
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-er 8498  df-map 8617  df-pm 8618  df-ixp 8686  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-fi 9170  df-sup 9201  df-inf 9202  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-z 12320  df-dec 12438  df-uz 12583  df-q 12689  df-rp 12731  df-xneg 12848  df-xadd 12849  df-xmul 12850  df-ioo 13083  df-ioc 13084  df-ico 13085  df-icc 13086  df-fz 13240  df-fzo 13383  df-fl 13512  df-mod 13590  df-seq 13722  df-exp 13783  df-fac 13988  df-bc 14017  df-hash 14045  df-shft 14778  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-limsup 15180  df-clim 15197  df-rlim 15198  df-sum 15398  df-ef 15777  df-sin 15779  df-cos 15780  df-tan 15781  df-pi 15782  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-starv 16977  df-sca 16978  df-vsca 16979  df-ip 16980  df-tset 16981  df-ple 16982  df-ds 16984  df-unif 16985  df-hom 16986  df-cco 16987  df-rest 17133  df-topn 17134  df-0g 17152  df-gsum 17153  df-topgen 17154  df-pt 17155  df-prds 17158  df-xrs 17213  df-qtop 17218  df-imas 17219  df-xps 17221  df-mre 17295  df-mrc 17296  df-acs 17298  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-submnd 18431  df-mulg 18701  df-cntz 18923  df-cmn 19388  df-psmet 20589  df-xmet 20590  df-met 20591  df-bl 20592  df-mopn 20593  df-fbas 20594  df-fg 20595  df-cnfld 20598  df-top 22043  df-topon 22060  df-topsp 22082  df-bases 22096  df-cld 22170  df-ntr 22171  df-cls 22172  df-nei 22249  df-lp 22287  df-perf 22288  df-cn 22378  df-cnp 22379  df-haus 22466  df-cmp 22538  df-tx 22713  df-hmeo 22906  df-fil 22997  df-fm 23089  df-flim 23090  df-flf 23091  df-xms 23473  df-ms 23474  df-tms 23475  df-cncf 24041  df-limc 25030  df-dv 25031  df-log 25712  df-cxp 25713  df-asin 26015
This theorem is referenced by:  dvacos  35862  dvreasin  35863
  Copyright terms: Public domain W3C validator