Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rmxyneg Structured version   Visualization version   GIF version

Theorem rmxyneg 41056
Description: Negation law for X and Y sequences. JonesMatijasevic is inconsistent on whether the X and Y sequences have domain 0 or ; we use consistently to avoid the need for a separate subtraction law. (Contributed by Stefan O'Rear, 22-Sep-2014.)
Assertion
Ref Expression
rmxyneg ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm -𝑁) = (𝐴 Xrm 𝑁) ∧ (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁)))

Proof of Theorem rmxyneg
StepHypRef Expression
1 znegcl 12465 . . . 4 (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
2 rmxyval 41051 . . . 4 ((𝐴 ∈ (ℤ‘2) ∧ -𝑁 ∈ ℤ) → ((𝐴 Xrm -𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm -𝑁))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑-𝑁))
31, 2sylan2 594 . . 3 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm -𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm -𝑁))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑-𝑁))
4 rmxyval 41051 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁))
54oveq2d 7362 . . . 4 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (1 / ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)))) = (1 / ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)))
6 rmbaserp 41055 . . . . . . . . 9 (𝐴 ∈ (ℤ‘2) → (𝐴 + (√‘((𝐴↑2) − 1))) ∈ ℝ+)
76rpcnd 12884 . . . . . . . 8 (𝐴 ∈ (ℤ‘2) → (𝐴 + (√‘((𝐴↑2) − 1))) ∈ ℂ)
87adantr 482 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 + (√‘((𝐴↑2) − 1))) ∈ ℂ)
96rpne0d 12887 . . . . . . . 8 (𝐴 ∈ (ℤ‘2) → (𝐴 + (√‘((𝐴↑2) − 1))) ≠ 0)
109adantr 482 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 + (√‘((𝐴↑2) − 1))) ≠ 0)
11 simpr 486 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
128, 10, 11expclzd 13979 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁) ∈ ℂ)
134, 12eqeltrd 2838 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) ∈ ℂ)
14 frmx 41049 . . . . . . . 8 Xrm :((ℤ‘2) × ℤ)⟶ℕ0
1514fovcl 7473 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℕ0)
1615nn0cnd 12405 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℂ)
17 rmspecnonsq 41042 . . . . . . . . . . 11 (𝐴 ∈ (ℤ‘2) → ((𝐴↑2) − 1) ∈ (ℕ ∖ ◻NN))
1817eldifad 3917 . . . . . . . . . 10 (𝐴 ∈ (ℤ‘2) → ((𝐴↑2) − 1) ∈ ℕ)
1918nncnd 12099 . . . . . . . . 9 (𝐴 ∈ (ℤ‘2) → ((𝐴↑2) − 1) ∈ ℂ)
2019adantr 482 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴↑2) − 1) ∈ ℂ)
2120sqrtcld 15253 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (√‘((𝐴↑2) − 1)) ∈ ℂ)
22 frmy 41050 . . . . . . . . . 10 Yrm :((ℤ‘2) × ℤ)⟶ℤ
2322fovcl 7473 . . . . . . . . 9 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ)
2423zcnd 12537 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℂ)
2524negcld 11429 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → -(𝐴 Yrm 𝑁) ∈ ℂ)
2621, 25mulcld 11105 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((√‘((𝐴↑2) − 1)) · -(𝐴 Yrm 𝑁)) ∈ ℂ)
2716, 26addcld 11104 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · -(𝐴 Yrm 𝑁))) ∈ ℂ)
288, 10, 11expne0d 13980 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁) ≠ 0)
294, 28eqnetrd 3009 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) ≠ 0)
3021, 24mulneg2d 11539 . . . . . . . . 9 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((√‘((𝐴↑2) − 1)) · -(𝐴 Yrm 𝑁)) = -((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)))
3130oveq2d 7362 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · -(𝐴 Yrm 𝑁))) = ((𝐴 Xrm 𝑁) + -((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))))
3221, 24mulcld 11105 . . . . . . . . 9 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)) ∈ ℂ)
3316, 32negsubd 11448 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) + -((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) = ((𝐴 Xrm 𝑁) − ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))))
3431, 33eqtrd 2777 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · -(𝐴 Yrm 𝑁))) = ((𝐴 Xrm 𝑁) − ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))))
3534oveq2d 7362 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) · ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · -(𝐴 Yrm 𝑁)))) = (((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) · ((𝐴 Xrm 𝑁) − ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)))))
36 subsq 14036 . . . . . . 7 (((𝐴 Xrm 𝑁) ∈ ℂ ∧ ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)) ∈ ℂ) → (((𝐴 Xrm 𝑁)↑2) − (((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))↑2)) = (((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) · ((𝐴 Xrm 𝑁) − ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)))))
3716, 32, 36syl2anc 585 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑁)↑2) − (((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))↑2)) = (((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) · ((𝐴 Xrm 𝑁) − ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)))))
3821, 24sqmuld 13986 . . . . . . . . 9 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))↑2) = (((√‘((𝐴↑2) − 1))↑2) · ((𝐴 Yrm 𝑁)↑2)))
3920sqsqrtd 15255 . . . . . . . . . 10 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((√‘((𝐴↑2) − 1))↑2) = ((𝐴↑2) − 1))
4039oveq1d 7361 . . . . . . . . 9 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (((√‘((𝐴↑2) − 1))↑2) · ((𝐴 Yrm 𝑁)↑2)) = (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑁)↑2)))
4138, 40eqtrd 2777 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))↑2) = (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑁)↑2)))
4241oveq2d 7362 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑁)↑2) − (((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))↑2)) = (((𝐴 Xrm 𝑁)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑁)↑2))))
43 rmxynorm 41054 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑁)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑁)↑2))) = 1)
4442, 43eqtrd 2777 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑁)↑2) − (((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))↑2)) = 1)
4535, 37, 443eqtr2d 2783 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) · ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · -(𝐴 Yrm 𝑁)))) = 1)
4613, 27, 29, 45mvllmuld 11917 . . . 4 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · -(𝐴 Yrm 𝑁))) = (1 / ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)))))
478, 10, 11expnegd 13981 . . . 4 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 + (√‘((𝐴↑2) − 1)))↑-𝑁) = (1 / ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)))
485, 46, 473eqtr4rd 2788 . . 3 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 + (√‘((𝐴↑2) − 1)))↑-𝑁) = ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · -(𝐴 Yrm 𝑁))))
493, 48eqtrd 2777 . 2 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm -𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm -𝑁))) = ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · -(𝐴 Yrm 𝑁))))
50 rmspecsqrtnq 41041 . . . 4 (𝐴 ∈ (ℤ‘2) → (√‘((𝐴↑2) − 1)) ∈ (ℂ ∖ ℚ))
5150adantr 482 . . 3 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (√‘((𝐴↑2) − 1)) ∈ (ℂ ∖ ℚ))
52 nn0ssq 12807 . . . 4 0 ⊆ ℚ
5314fovcl 7473 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ -𝑁 ∈ ℤ) → (𝐴 Xrm -𝑁) ∈ ℕ0)
541, 53sylan2 594 . . . 4 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm -𝑁) ∈ ℕ0)
5552, 54sselid 3937 . . 3 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm -𝑁) ∈ ℚ)
56 zssq 12806 . . . 4 ℤ ⊆ ℚ
5722fovcl 7473 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ -𝑁 ∈ ℤ) → (𝐴 Yrm -𝑁) ∈ ℤ)
581, 57sylan2 594 . . . 4 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm -𝑁) ∈ ℤ)
5956, 58sselid 3937 . . 3 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm -𝑁) ∈ ℚ)
6052, 15sselid 3937 . . 3 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℚ)
6156, 23sselid 3937 . . . 4 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℚ)
62 qnegcl 12816 . . . 4 ((𝐴 Yrm 𝑁) ∈ ℚ → -(𝐴 Yrm 𝑁) ∈ ℚ)
6361, 62syl 17 . . 3 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → -(𝐴 Yrm 𝑁) ∈ ℚ)
64 qirropth 41043 . . 3 (((√‘((𝐴↑2) − 1)) ∈ (ℂ ∖ ℚ) ∧ ((𝐴 Xrm -𝑁) ∈ ℚ ∧ (𝐴 Yrm -𝑁) ∈ ℚ) ∧ ((𝐴 Xrm 𝑁) ∈ ℚ ∧ -(𝐴 Yrm 𝑁) ∈ ℚ)) → (((𝐴 Xrm -𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm -𝑁))) = ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · -(𝐴 Yrm 𝑁))) ↔ ((𝐴 Xrm -𝑁) = (𝐴 Xrm 𝑁) ∧ (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁))))
6551, 55, 59, 60, 63, 64syl122anc 1379 . 2 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm -𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm -𝑁))) = ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · -(𝐴 Yrm 𝑁))) ↔ ((𝐴 Xrm -𝑁) = (𝐴 Xrm 𝑁) ∧ (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁))))
6649, 65mpbid 231 1 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm -𝑁) = (𝐴 Xrm 𝑁) ∧ (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1541  wcel 2106  wne 2941  cdif 3902  cfv 6488  (class class class)co 7346  cc 10979  0cc0 10981  1c1 10982   + caddc 10984   · cmul 10986  cmin 11315  -cneg 11316   / cdiv 11742  cn 12083  2c2 12138  0cn0 12343  cz 12429  cuz 12692  cq 12798  cexp 13892  csqrt 15048  NNcsquarenn 40971   Xrm crmx 41035   Yrm crmy 41036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2708  ax-rep 5237  ax-sep 5251  ax-nul 5258  ax-pow 5315  ax-pr 5379  ax-un 7659  ax-inf2 9507  ax-cnex 11037  ax-resscn 11038  ax-1cn 11039  ax-icn 11040  ax-addcl 11041  ax-addrcl 11042  ax-mulcl 11043  ax-mulrcl 11044  ax-mulcom 11045  ax-addass 11046  ax-mulass 11047  ax-distr 11048  ax-i2m1 11049  ax-1ne0 11050  ax-1rid 11051  ax-rnegex 11052  ax-rrecex 11053  ax-cnre 11054  ax-pre-lttri 11055  ax-pre-lttrn 11056  ax-pre-ltadd 11057  ax-pre-mulgt0 11058  ax-pre-sup 11059  ax-addf 11060  ax-mulf 11061
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3735  df-csb 3851  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3924  df-nul 4278  df-if 4482  df-pw 4557  df-sn 4582  df-pr 4584  df-tp 4586  df-op 4588  df-uni 4861  df-int 4903  df-iun 4951  df-iin 4952  df-br 5101  df-opab 5163  df-mpt 5184  df-tr 5218  df-id 5525  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5582  df-se 5583  df-we 5584  df-xp 5633  df-rel 5634  df-cnv 5635  df-co 5636  df-dm 5637  df-rn 5638  df-res 5639  df-ima 5640  df-pred 6246  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6440  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-isom 6497  df-riota 7302  df-ov 7349  df-oprab 7350  df-mpo 7351  df-of 7604  df-om 7790  df-1st 7908  df-2nd 7909  df-supp 8057  df-frecs 8176  df-wrecs 8207  df-recs 8281  df-rdg 8320  df-1o 8376  df-2o 8377  df-oadd 8380  df-omul 8381  df-er 8578  df-map 8697  df-pm 8698  df-ixp 8766  df-en 8814  df-dom 8815  df-sdom 8816  df-fin 8817  df-fsupp 9236  df-fi 9277  df-sup 9308  df-inf 9309  df-oi 9376  df-card 9805  df-acn 9808  df-pnf 11121  df-mnf 11122  df-xr 11123  df-ltxr 11124  df-le 11125  df-sub 11317  df-neg 11318  df-div 11743  df-nn 12084  df-2 12146  df-3 12147  df-4 12148  df-5 12149  df-6 12150  df-7 12151  df-8 12152  df-9 12153  df-n0 12344  df-xnn0 12416  df-z 12430  df-dec 12548  df-uz 12693  df-q 12799  df-rp 12841  df-xneg 12958  df-xadd 12959  df-xmul 12960  df-ioo 13193  df-ioc 13194  df-ico 13195  df-icc 13196  df-fz 13350  df-fzo 13493  df-fl 13622  df-mod 13700  df-seq 13832  df-exp 13893  df-fac 14098  df-bc 14127  df-hash 14155  df-shft 14882  df-cj 14914  df-re 14915  df-im 14916  df-sqrt 15050  df-abs 15051  df-limsup 15284  df-clim 15301  df-rlim 15302  df-sum 15502  df-ef 15881  df-sin 15883  df-cos 15884  df-pi 15886  df-dvds 16068  df-gcd 16306  df-numer 16541  df-denom 16542  df-struct 16950  df-sets 16967  df-slot 16985  df-ndx 16997  df-base 17015  df-ress 17044  df-plusg 17077  df-mulr 17078  df-starv 17079  df-sca 17080  df-vsca 17081  df-ip 17082  df-tset 17083  df-ple 17084  df-ds 17086  df-unif 17087  df-hom 17088  df-cco 17089  df-rest 17235  df-topn 17236  df-0g 17254  df-gsum 17255  df-topgen 17256  df-pt 17257  df-prds 17260  df-xrs 17315  df-qtop 17320  df-imas 17321  df-xps 17323  df-mre 17397  df-mrc 17398  df-acs 17400  df-mgm 18428  df-sgrp 18477  df-mnd 18488  df-submnd 18533  df-mulg 18802  df-cntz 19024  df-cmn 19488  df-psmet 20699  df-xmet 20700  df-met 20701  df-bl 20702  df-mopn 20703  df-fbas 20704  df-fg 20705  df-cnfld 20708  df-top 22153  df-topon 22170  df-topsp 22192  df-bases 22206  df-cld 22280  df-ntr 22281  df-cls 22282  df-nei 22359  df-lp 22397  df-perf 22398  df-cn 22488  df-cnp 22489  df-haus 22576  df-tx 22823  df-hmeo 23016  df-fil 23107  df-fm 23199  df-flim 23200  df-flf 23201  df-xms 23583  df-ms 23584  df-tms 23585  df-cncf 24151  df-limc 25140  df-dv 25141  df-log 25822  df-squarenn 40976  df-pell1qr 40977  df-pell14qr 40978  df-pell1234qr 40979  df-pellfund 40980  df-rmx 41037  df-rmy 41038
This theorem is referenced by:  rmxneg  41060  rmyneg  41064
  Copyright terms: Public domain W3C validator