Theorem sqrtneglem 15328

Description: The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.)

Assertion

Ref	Expression
sqrtneglem	⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((i · (√‘𝐴))↑2) = -𝐴 ∧ 0 ≤ (ℜ‘(i · (√‘𝐴))) ∧ (i · (i · (√‘𝐴))) ∉ ℝ+))

Proof of Theorem sqrtneglem

Step	Hyp	Ref	Expression
1		ax-icn 11169	. . . 4 ⊢ i ∈ ℂ
2		resqrtcl 15315	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈ ℝ)
3		recn 11200	. . . . 5 ⊢ ((√‘𝐴) ∈ ℝ → (√‘𝐴) ∈ ℂ)
4	2, 3	syl 18	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈ ℂ)
5		sqmul 14166	. . . 4 ⊢ ((i ∈ ℂ ∧ (√‘𝐴) ∈ ℂ) → ((i · (√‘𝐴))↑2) = ((i↑2) · ((√‘𝐴)↑2)))
6	1, 4, 5	sylancr 599	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((i · (√‘𝐴))↑2) = ((i↑2) · ((√‘𝐴)↑2)))
7		i2 14249	. . . . 5 ⊢ (i↑2) = -1
8	7	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (i↑2) = -1)
9		resqrtth 15317	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴)
10	8, 9	oveq12d 7434	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((i↑2) · ((√‘𝐴)↑2)) = (-1 · 𝐴))
11		recn 11200	. . . . 5 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
12	11	adantr 486	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 𝐴 ∈ ℂ)
13	12	mulm1d 11676	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (-1 · 𝐴) = -𝐴)
14	6, 10, 13	3eqtrd 2805	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((i · (√‘𝐴))↑2) = -𝐴)
15		renegcl 11531	. . . 4 ⊢ ((√‘𝐴) ∈ ℝ → -(√‘𝐴) ∈ ℝ)
16		0re 11220	. . . . 5 ⊢ 0 ∈ ℝ
17		reim0 15180	. . . . . 6 ⊢ (-(√‘𝐴) ∈ ℝ → (ℑ‘-(√‘𝐴)) = 0)
18		recn 11200	. . . . . . 7 ⊢ (-(√‘𝐴) ∈ ℝ → -(√‘𝐴) ∈ ℂ)
19		imre 15170	. . . . . . 7 ⊢ (-(√‘𝐴) ∈ ℂ → (ℑ‘-(√‘𝐴)) = (ℜ‘(-i · -(√‘𝐴))))
20	18, 19	syl 18	. . . . . 6 ⊢ (-(√‘𝐴) ∈ ℝ → (ℑ‘-(√‘𝐴)) = (ℜ‘(-i · -(√‘𝐴))))
21	17, 20	eqtr3d 2803	. . . . 5 ⊢ (-(√‘𝐴) ∈ ℝ → 0 = (ℜ‘(-i · -(√‘𝐴))))
22		eqle 11322	. . . . 5 ⊢ ((0 ∈ ℝ ∧ 0 = (ℜ‘(-i · -(√‘𝐴)))) → 0 ≤ (ℜ‘(-i · -(√‘𝐴))))
23	16, 21, 22	sylancr 599	. . . 4 ⊢ (-(√‘𝐴) ∈ ℝ → 0 ≤ (ℜ‘(-i · -(√‘𝐴))))
24	2, 15, 23	3syl 19	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 0 ≤ (ℜ‘(-i · -(√‘𝐴))))
25		mul2neg 11663	. . . . 5 ⊢ ((i ∈ ℂ ∧ (√‘𝐴) ∈ ℂ) → (-i · -(√‘𝐴)) = (i · (√‘𝐴)))
26	1, 4, 25	sylancr 599	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (-i · -(√‘𝐴)) = (i · (√‘𝐴)))
27	26	fveq2d 6889	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (ℜ‘(-i · -(√‘𝐴))) = (ℜ‘(i · (√‘𝐴))))
28	24, 27	breqtrd 5140	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 0 ≤ (ℜ‘(i · (√‘𝐴))))
29		ixi 11853	. . . . . . 7 ⊢ (i · i) = -1
30	29	oveq1i 7426	. . . . . 6 ⊢ ((i · i) · (√‘𝐴)) = (-1 · (√‘𝐴))
31		mulass 11198	. . . . . . 7 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ ∧ (√‘𝐴) ∈ ℂ) → ((i · i) · (√‘𝐴)) = (i · (i · (√‘𝐴))))
32	1, 1, 31	mp3an12 1480	. . . . . 6 ⊢ ((√‘𝐴) ∈ ℂ → ((i · i) · (√‘𝐴)) = (i · (i · (√‘𝐴))))
33		mulm1 11665	. . . . . 6 ⊢ ((√‘𝐴) ∈ ℂ → (-1 · (√‘𝐴)) = -(√‘𝐴))
34	30, 32, 33	3eqtr3a 2825	. . . . 5 ⊢ ((√‘𝐴) ∈ ℂ → (i · (i · (√‘𝐴))) = -(√‘𝐴))
35	4, 34	syl 18	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (i · (i · (√‘𝐴))) = -(√‘𝐴))
36		sqrtge0 15319	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 0 ≤ (√‘𝐴))
37		le0neg2 11733	. . . . . . . 8 ⊢ ((√‘𝐴) ∈ ℝ → (0 ≤ (√‘𝐴) ↔ -(√‘𝐴) ≤ 0))
38		lenlt 11298	. . . . . . . . 9 ⊢ ((-(√‘𝐴) ∈ ℝ ∧ 0 ∈ ℝ) → (-(√‘𝐴) ≤ 0 ↔ ¬ 0 < -(√‘𝐴)))
39	15, 16, 38	sylancl 598	. . . . . . . 8 ⊢ ((√‘𝐴) ∈ ℝ → (-(√‘𝐴) ≤ 0 ↔ ¬ 0 < -(√‘𝐴)))
40	37, 39	bitrd 282	. . . . . . 7 ⊢ ((√‘𝐴) ∈ ℝ → (0 ≤ (√‘𝐴) ↔ ¬ 0 < -(√‘𝐴)))
41	2, 40	syl 18	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (0 ≤ (√‘𝐴) ↔ ¬ 0 < -(√‘𝐴)))
42	36, 41	mpbid 235	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ¬ 0 < -(√‘𝐴))
43		elrp 13028	. . . . . 6 ⊢ (-(√‘𝐴) ∈ ℝ+ ↔ (-(√‘𝐴) ∈ ℝ ∧ 0 < -(√‘𝐴)))
44	2, 15	syl 18	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → -(√‘𝐴) ∈ ℝ)
45	44	biantrurd 542	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (0 < -(√‘𝐴) ↔ (-(√‘𝐴) ∈ ℝ ∧ 0 < -(√‘𝐴))))
46	43, 45	bitr4id 293	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (-(√‘𝐴) ∈ ℝ+ ↔ 0 < -(√‘𝐴)))
47	42, 46	mtbird 328	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ¬ -(√‘𝐴) ∈ ℝ+)
48	35, 47	eqneltrd 2886	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ¬ (i · (i · (√‘𝐴))) ∈ ℝ+)
49		df-nel 3068	. . 3 ⊢ ((i · (i · (√‘𝐴))) ∉ ℝ+ ↔ ¬ (i · (i · (√‘𝐴))) ∈ ℝ+)
50	48, 49	sylibr 237	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (i · (i · (√‘𝐴))) ∉ ℝ+)
51	14, 28, 50	3jca 1146	1 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((i · (√‘𝐴))↑2) = -𝐴 ∧ 0 ≤ (ℜ‘(i · (√‘𝐴))) ∧ (i · (i · (√‘𝐴))) ∉ ℝ+))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ∉ wnel 3067   class class class wbr 5112  ‘cfv 6540  (class class class)co 7416  ℂcc 11108  ℝcr 11109  0cc0 11110  1c1 11111  ici 11112   · cmul 11115   < clt 11253   ≤ cle 11254  -cneg 11452  2c2 12305  ℝ⁺crp 13026  ↑cexp 14108  ℜcre 15159  ℑcim 15160  √csqrt 15295

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5260  ax-nul 5272  ax-pow 5339  ax-pr 5407  ax-un 7738  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-iun 4961  df-br 5113  df-opab 5177  df-mpt 5196  df-tr 5222  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-sup 9404  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11453  df-neg 11454  df-div 11882  df-nn 12244  df-2 12313  df-3 12314  df-n0 12515  df-z 12602  df-uz 12873  df-rp 13027  df-seq 14049  df-exp 14109  df-cj 15161  df-re 15162  df-im 15163  df-sqrt 15297

This theorem is used by:  sqrtneg  15329  sqreu  15423