Theorem bhmafibid1 30206

Description: The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. First result. (Contributed by Thierry Arnoux, 1-Feb-2020.)

Assertion

Ref	Expression
bhmafibid1	⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))

Proof of Theorem bhmafibid1

Step	Hyp	Ref	Expression
1		simpll 757	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐴 ∈ ℝ)
2	1	recnd 10405	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐴 ∈ ℂ)
3		ax-icn 10331	. . . . . . . . . 10 ⊢ i ∈ ℂ
4	3	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → i ∈ ℂ)
5		simplr 759	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐵 ∈ ℝ)
6	5	recnd 10405	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐵 ∈ ℂ)
7	4, 6	mulcld 10397	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (i · 𝐵) ∈ ℂ)
8	2, 7	addcld 10396	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐴 + (i · 𝐵)) ∈ ℂ)
9		simprl 761	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐶 ∈ ℝ)
10	9	recnd 10405	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐶 ∈ ℂ)
11		simprr 763	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐷 ∈ ℝ)
12	11	recnd 10405	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐷 ∈ ℂ)
13	4, 12	mulcld 10397	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (i · 𝐷) ∈ ℂ)
14	10, 13	addcld 10396	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐶 + (i · 𝐷)) ∈ ℂ)
15	8, 14	mulcld 10397	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℂ)
16	15	replimd 14344	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) = ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) + (i · (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))))))
17	8, 14	remuld 14365	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = (((ℜ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷)))) − ((ℑ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷))))))
18	1, 5	crred 14378	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
19	9, 11	crred 14378	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶)
20	18, 19	oveq12d 6940	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((ℜ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷)))) = (𝐴 · 𝐶))
21	1, 5	crimd 14379	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
22	9, 11	crimd 14379	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷)
23	21, 22	oveq12d 6940	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((ℑ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) = (𝐵 · 𝐷))
24	20, 23	oveq12d 6940	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((ℜ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷)))) − ((ℑ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷))))) = ((𝐴 · 𝐶) − (𝐵 · 𝐷)))
25	17, 24	eqtrd 2813	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = ((𝐴 · 𝐶) − (𝐵 · 𝐷)))
26	8, 14	immuld 14366	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = (((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) + ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷))))))
27	18, 22	oveq12d 6940	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) = (𝐴 · 𝐷))
28	21, 19	oveq12d 6940	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷)))) = (𝐵 · 𝐶))
29	27, 28	oveq12d 6940	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) + ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷))))) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
30	26, 29	eqtrd 2813	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = ((𝐴 · 𝐷) + (𝐵 · 𝐶)))
31	30	oveq2d 6938	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (i · (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))) = (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶))))
32	25, 31	oveq12d 6940	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) + (i · (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))))) = (((𝐴 · 𝐶) − (𝐵 · 𝐷)) + (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶)))))
33	16, 32	eqtrd 2813	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) = (((𝐴 · 𝐶) − (𝐵 · 𝐷)) + (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶)))))
34	33	fveq2d 6450	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = (abs‘(((𝐴 · 𝐶) − (𝐵 · 𝐷)) + (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶))))))
35	34	oveq1d 6937	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = ((abs‘(((𝐴 · 𝐶) − (𝐵 · 𝐷)) + (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶)))))↑2))
36	8, 14	absmuld 14601	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) = ((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷)))))
37	36	oveq1d 6937	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))↑2))
38	8	abscld 14583	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (abs‘(𝐴 + (i · 𝐵))) ∈ ℝ)
39	38	recnd 10405	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (abs‘(𝐴 + (i · 𝐵))) ∈ ℂ)
40	14	abscld 14583	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (abs‘(𝐶 + (i · 𝐷))) ∈ ℝ)
41	40	recnd 10405	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (abs‘(𝐶 + (i · 𝐷))) ∈ ℂ)
42	39, 41	sqmuld 13339	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))↑2) = (((abs‘(𝐴 + (i · 𝐵)))↑2) · ((abs‘(𝐶 + (i · 𝐷)))↑2)))
43		absreimsq 14439	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2)))
44		absreimsq 14439	. . . 4 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((abs‘(𝐶 + (i · 𝐷)))↑2) = ((𝐶↑2) + (𝐷↑2)))
45	43, 44	oveqan12d 6941	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((abs‘(𝐴 + (i · 𝐵)))↑2) · ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))))
46	37, 42, 45	3eqtrd 2817	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((abs‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))↑2) = (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))))
47	1, 9	remulcld 10407	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐴 · 𝐶) ∈ ℝ)
48	5, 11	remulcld 10407	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐵 · 𝐷) ∈ ℝ)
49	47, 48	resubcld 10803	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℝ)
50	1, 11	remulcld 10407	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐴 · 𝐷) ∈ ℝ)
51	5, 9	remulcld 10407	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℝ)
52	50, 51	readdcld 10406	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 · 𝐷) + (𝐵 · 𝐶)) ∈ ℝ)
53		absreimsq 14439	. . 3 ⊢ ((((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℝ ∧ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) ∈ ℝ) → ((abs‘(((𝐴 · 𝐶) − (𝐵 · 𝐷)) + (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶)))))↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
54	49, 52, 53	syl2anc 579	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((abs‘(((𝐴 · 𝐶) − (𝐵 · 𝐷)) + (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶)))))↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))
55	35, 46, 54	3eqtr3d 2821	1 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)))

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2106  ‘cfv 6135  (class class class)co 6922  ℂcc 10270  ℝcr 10271  ici 10274   + caddc 10275   · cmul 10277   − cmin 10606  2c2 11430  ↑cexp 13178  ℜcre 14244  ℑcim 14245  abscabs 14381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-sup 8636  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-n0 11643  df-z 11729  df-uz 11993  df-rp 12138  df-seq 13120  df-exp 13179  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383

This theorem is referenced by:  bhmafibid2  30207  2sqmod  30210