Theorem pell1234qrmulcl 40191

Description: General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014.)

Assertion

Ref	Expression
pell1234qrmulcl	⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷) ∧ 𝐵 ∈ (Pell1234QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell1234QR‘𝐷))

Proof of Theorem pell1234qrmulcl

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		remulcl 10660	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
2	1	ad5antlr 734	. . . . . . . . . 10 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝐴 · 𝐵) ∈ ℝ)
3		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℤ)
4	3	ad3antrrr 729	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → 𝑎 ∈ ℤ)
5		simplrl 776	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → 𝑐 ∈ ℤ)
6	4, 5	zmulcld 12132	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑎 · 𝑐) ∈ ℤ)
7		eldifi 4032	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → 𝐷 ∈ ℕ)
8	7	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐷 ∈ ℕ)
9	8	nnzd 12125	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐷 ∈ ℤ)
10	9	ad3antrrr 729	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → 𝐷 ∈ ℤ)
11		simplrr 777	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → 𝑑 ∈ ℤ)
12		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℤ)
13	12	ad3antrrr 729	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → 𝑏 ∈ ℤ)
14	11, 13	zmulcld 12132	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑑 · 𝑏) ∈ ℤ)
15	10, 14	zmulcld 12132	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝐷 · (𝑑 · 𝑏)) ∈ ℤ)
16	6, 15	zaddcld 12130	. . . . . . . . . . 11 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) ∈ ℤ)
17	4, 11	zmulcld 12132	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑎 · 𝑑) ∈ ℤ)
18	5, 13	zmulcld 12132	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑐 · 𝑏) ∈ ℤ)
19	17, 18	zaddcld 12130	. . . . . . . . . . 11 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ ℤ)
20		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)))
21	20	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → 𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)))
22		simprl 770	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → 𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)))
23	21, 22	oveq12d 7168	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝐴 · 𝐵) = ((𝑎 + ((√‘𝐷) · 𝑏)) · (𝑐 + ((√‘𝐷) · 𝑑))))
24		zcn 12025	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℤ → 𝑎 ∈ ℂ)
25	24	ad2antrl 727	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℂ)
26	25	ad3antrrr 729	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → 𝑎 ∈ ℂ)
27	8	nncnd 11690	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐷 ∈ ℂ)
28	27	ad3antrrr 729	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → 𝐷 ∈ ℂ)
29	28	sqrtcld 14845	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (√‘𝐷) ∈ ℂ)
30		zcn 12025	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ ℤ → 𝑏 ∈ ℂ)
31	30	ad2antll 728	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℂ)
32	31	ad3antrrr 729	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → 𝑏 ∈ ℂ)
33	29, 32	mulcld 10699	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((√‘𝐷) · 𝑏) ∈ ℂ)
34		zcn 12025	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ ℤ → 𝑐 ∈ ℂ)
35	34	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ) → 𝑐 ∈ ℂ)
36	35	ad2antlr 726	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → 𝑐 ∈ ℂ)
37		zcn 12025	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ ℤ → 𝑑 ∈ ℂ)
38	37	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ) → 𝑑 ∈ ℂ)
39	38	ad2antlr 726	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → 𝑑 ∈ ℂ)
40	29, 39	mulcld 10699	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((√‘𝐷) · 𝑑) ∈ ℂ)
41	26, 33, 36, 40	muladdd 11136	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎 + ((√‘𝐷) · 𝑏)) · (𝑐 + ((√‘𝐷) · 𝑑))) = (((𝑎 · 𝑐) + (((√‘𝐷) · 𝑑) · ((√‘𝐷) · 𝑏))) + ((𝑎 · ((√‘𝐷) · 𝑑)) + (𝑐 · ((√‘𝐷) · 𝑏)))))
42	29, 39, 29, 32	mul4d 10890	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((√‘𝐷) · 𝑑) · ((√‘𝐷) · 𝑏)) = (((√‘𝐷) · (√‘𝐷)) · (𝑑 · 𝑏)))
43	28	msqsqrtd 14848	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((√‘𝐷) · (√‘𝐷)) = 𝐷)
44	43	oveq1d 7165	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((√‘𝐷) · (√‘𝐷)) · (𝑑 · 𝑏)) = (𝐷 · (𝑑 · 𝑏)))
45	42, 44	eqtrd 2793	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((√‘𝐷) · 𝑑) · ((√‘𝐷) · 𝑏)) = (𝐷 · (𝑑 · 𝑏)))
46	45	oveq2d 7166	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎 · 𝑐) + (((√‘𝐷) · 𝑑) · ((√‘𝐷) · 𝑏))) = ((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))))
47	26, 29, 39	mul12d 10887	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑎 · ((√‘𝐷) · 𝑑)) = ((√‘𝐷) · (𝑎 · 𝑑)))
48	36, 29, 32	mul12d 10887	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑐 · ((√‘𝐷) · 𝑏)) = ((√‘𝐷) · (𝑐 · 𝑏)))
49	47, 48	oveq12d 7168	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎 · ((√‘𝐷) · 𝑑)) + (𝑐 · ((√‘𝐷) · 𝑏))) = (((√‘𝐷) · (𝑎 · 𝑑)) + ((√‘𝐷) · (𝑐 · 𝑏))))
50	26, 39	mulcld 10699	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑎 · 𝑑) ∈ ℂ)
51	36, 32	mulcld 10699	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑐 · 𝑏) ∈ ℂ)
52	29, 50, 51	adddid 10703	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏))) = (((√‘𝐷) · (𝑎 · 𝑑)) + ((√‘𝐷) · (𝑐 · 𝑏))))
53	49, 52	eqtr4d 2796	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎 · ((√‘𝐷) · 𝑑)) + (𝑐 · ((√‘𝐷) · 𝑏))) = ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏))))
54	46, 53	oveq12d 7168	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((𝑎 · 𝑐) + (((√‘𝐷) · 𝑑) · ((√‘𝐷) · 𝑏))) + ((𝑎 · ((√‘𝐷) · 𝑑)) + (𝑐 · ((√‘𝐷) · 𝑏)))) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))))
55	23, 41, 54	3eqtrd 2797	. . . . . . . . . . 11 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝐴 · 𝐵) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))))
56	50, 51	addcld 10698	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ ℂ)
57	29, 56	sqmuld 13572	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))↑2) = (((√‘𝐷)↑2) · (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2)))
58	28	sqsqrtd 14847	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((√‘𝐷)↑2) = 𝐷)
59	58	oveq1d 7165	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((√‘𝐷)↑2) · (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2)) = (𝐷 · (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2)))
60	57, 59	eqtr2d 2794	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝐷 · (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2)) = (((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))↑2))
61	60	oveq2d 7166	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2))) = ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))↑2)))
62	26, 36	mulcld 10699	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑎 · 𝑐) ∈ ℂ)
63	39, 32	mulcld 10699	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑑 · 𝑏) ∈ ℂ)
64	28, 63	mulcld 10699	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝐷 · (𝑑 · 𝑏)) ∈ ℂ)
65	62, 64	addcld 10698	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) ∈ ℂ)
66	29, 56	mulcld 10699	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏))) ∈ ℂ)
67		subsq 13622	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) ∈ ℂ ∧ ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏))) ∈ ℂ) → ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))↑2)) = ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))) · (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) − ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏))))))
68	65, 66, 67	syl2anc 587	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))↑2)) = ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))) · (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) − ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏))))))
69	41, 54	eqtr2d 2794	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))) = ((𝑎 + ((√‘𝐷) · 𝑏)) · (𝑐 + ((√‘𝐷) · 𝑑))))
70	26, 33, 36, 40	mulsubd 11137	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎 − ((√‘𝐷) · 𝑏)) · (𝑐 − ((√‘𝐷) · 𝑑))) = (((𝑎 · 𝑐) + (((√‘𝐷) · 𝑑) · ((√‘𝐷) · 𝑏))) − ((𝑎 · ((√‘𝐷) · 𝑑)) + (𝑐 · ((√‘𝐷) · 𝑏)))))
71	46, 53	oveq12d 7168	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((𝑎 · 𝑐) + (((√‘𝐷) · 𝑑) · ((√‘𝐷) · 𝑏))) − ((𝑎 · ((√‘𝐷) · 𝑑)) + (𝑐 · ((√‘𝐷) · 𝑏)))) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) − ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))))
72	70, 71	eqtr2d 2794	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) − ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))) = ((𝑎 − ((√‘𝐷) · 𝑏)) · (𝑐 − ((√‘𝐷) · 𝑑))))
73	69, 72	oveq12d 7168	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))) · (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) − ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏))))) = (((𝑎 + ((√‘𝐷) · 𝑏)) · (𝑐 + ((√‘𝐷) · 𝑑))) · ((𝑎 − ((√‘𝐷) · 𝑏)) · (𝑐 − ((√‘𝐷) · 𝑑)))))
74	61, 68, 73	3eqtrd 2797	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2))) = (((𝑎 + ((√‘𝐷) · 𝑏)) · (𝑐 + ((√‘𝐷) · 𝑑))) · ((𝑎 − ((√‘𝐷) · 𝑏)) · (𝑐 − ((√‘𝐷) · 𝑑)))))
75	26, 33	addcld 10698	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑎 + ((√‘𝐷) · 𝑏)) ∈ ℂ)
76	36, 40	addcld 10698	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑐 + ((√‘𝐷) · 𝑑)) ∈ ℂ)
77	26, 33	subcld 11035	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑎 − ((√‘𝐷) · 𝑏)) ∈ ℂ)
78	36, 40	subcld 11035	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (𝑐 − ((√‘𝐷) · 𝑑)) ∈ ℂ)
79	75, 76, 77, 78	mul4d 10890	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((𝑎 + ((√‘𝐷) · 𝑏)) · (𝑐 + ((√‘𝐷) · 𝑑))) · ((𝑎 − ((√‘𝐷) · 𝑏)) · (𝑐 − ((√‘𝐷) · 𝑑)))) = (((𝑎 + ((√‘𝐷) · 𝑏)) · (𝑎 − ((√‘𝐷) · 𝑏))) · ((𝑐 + ((√‘𝐷) · 𝑑)) · (𝑐 − ((√‘𝐷) · 𝑑)))))
80		subsq 13622	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℂ ∧ ((√‘𝐷) · 𝑏) ∈ ℂ) → ((𝑎↑2) − (((√‘𝐷) · 𝑏)↑2)) = ((𝑎 + ((√‘𝐷) · 𝑏)) · (𝑎 − ((√‘𝐷) · 𝑏))))
81	26, 33, 80	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎↑2) − (((√‘𝐷) · 𝑏)↑2)) = ((𝑎 + ((√‘𝐷) · 𝑏)) · (𝑎 − ((√‘𝐷) · 𝑏))))
82		subsq 13622	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ ℂ ∧ ((√‘𝐷) · 𝑑) ∈ ℂ) → ((𝑐↑2) − (((√‘𝐷) · 𝑑)↑2)) = ((𝑐 + ((√‘𝐷) · 𝑑)) · (𝑐 − ((√‘𝐷) · 𝑑))))
83	36, 40, 82	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑐↑2) − (((√‘𝐷) · 𝑑)↑2)) = ((𝑐 + ((√‘𝐷) · 𝑑)) · (𝑐 − ((√‘𝐷) · 𝑑))))
84	81, 83	oveq12d 7168	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((𝑎↑2) − (((√‘𝐷) · 𝑏)↑2)) · ((𝑐↑2) − (((√‘𝐷) · 𝑑)↑2))) = (((𝑎 + ((√‘𝐷) · 𝑏)) · (𝑎 − ((√‘𝐷) · 𝑏))) · ((𝑐 + ((√‘𝐷) · 𝑑)) · (𝑐 − ((√‘𝐷) · 𝑑)))))
85	29, 32	sqmuld 13572	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((√‘𝐷) · 𝑏)↑2) = (((√‘𝐷)↑2) · (𝑏↑2)))
86	85	oveq2d 7166	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎↑2) − (((√‘𝐷) · 𝑏)↑2)) = ((𝑎↑2) − (((√‘𝐷)↑2) · (𝑏↑2))))
87	29, 39	sqmuld 13572	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((√‘𝐷) · 𝑑)↑2) = (((√‘𝐷)↑2) · (𝑑↑2)))
88	87	oveq2d 7166	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑐↑2) − (((√‘𝐷) · 𝑑)↑2)) = ((𝑐↑2) − (((√‘𝐷)↑2) · (𝑑↑2))))
89	86, 88	oveq12d 7168	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((𝑎↑2) − (((√‘𝐷) · 𝑏)↑2)) · ((𝑐↑2) − (((√‘𝐷) · 𝑑)↑2))) = (((𝑎↑2) − (((√‘𝐷)↑2) · (𝑏↑2))) · ((𝑐↑2) − (((√‘𝐷)↑2) · (𝑑↑2)))))
90	79, 84, 89	3eqtr2d 2799	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((𝑎 + ((√‘𝐷) · 𝑏)) · (𝑐 + ((√‘𝐷) · 𝑑))) · ((𝑎 − ((√‘𝐷) · 𝑏)) · (𝑐 − ((√‘𝐷) · 𝑑)))) = (((𝑎↑2) − (((√‘𝐷)↑2) · (𝑏↑2))) · ((𝑐↑2) − (((√‘𝐷)↑2) · (𝑑↑2)))))
91	58	oveq1d 7165	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((√‘𝐷)↑2) · (𝑏↑2)) = (𝐷 · (𝑏↑2)))
92	91	oveq2d 7166	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎↑2) − (((√‘𝐷)↑2) · (𝑏↑2))) = ((𝑎↑2) − (𝐷 · (𝑏↑2))))
93	58	oveq1d 7165	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((√‘𝐷)↑2) · (𝑑↑2)) = (𝐷 · (𝑑↑2)))
94	93	oveq2d 7166	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑐↑2) − (((√‘𝐷)↑2) · (𝑑↑2))) = ((𝑐↑2) − (𝐷 · (𝑑↑2))))
95	92, 94	oveq12d 7168	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((𝑎↑2) − (((√‘𝐷)↑2) · (𝑏↑2))) · ((𝑐↑2) − (((√‘𝐷)↑2) · (𝑑↑2)))) = (((𝑎↑2) − (𝐷 · (𝑏↑2))) · ((𝑐↑2) − (𝐷 · (𝑑↑2)))))
96		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
97	96	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
98		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)
99	97, 98	oveq12d 7168	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((𝑎↑2) − (𝐷 · (𝑏↑2))) · ((𝑐↑2) − (𝐷 · (𝑑↑2)))) = (1 · 1))
100		1t1e1 11836	. . . . . . . . . . . . . 14 ⊢ (1 · 1) = 1
101	100	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (1 · 1) = 1)
102	95, 99, 101	3eqtrd 2797	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → (((𝑎↑2) − (((√‘𝐷)↑2) · (𝑏↑2))) · ((𝑐↑2) − (((√‘𝐷)↑2) · (𝑑↑2)))) = 1)
103	74, 90, 102	3eqtrd 2797	. . . . . . . . . . 11 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2))) = 1)
104		oveq1 7157	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) → (𝑒 + ((√‘𝐷) · 𝑓)) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · 𝑓)))
105	104	eqeq2d 2769	. . . . . . . . . . . . 13 ⊢ (𝑒 = ((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) → ((𝐴 · 𝐵) = (𝑒 + ((√‘𝐷) · 𝑓)) ↔ (𝐴 · 𝐵) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · 𝑓))))
106		oveq1 7157	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) → (𝑒↑2) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2))
107	106	oveq1d 7165	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) → ((𝑒↑2) − (𝐷 · (𝑓↑2))) = ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (𝑓↑2))))
108	107	eqeq1d 2760	. . . . . . . . . . . . 13 ⊢ (𝑒 = ((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) → (((𝑒↑2) − (𝐷 · (𝑓↑2))) = 1 ↔ ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (𝑓↑2))) = 1))
109	105, 108	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑒 = ((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) → (((𝐴 · 𝐵) = (𝑒 + ((√‘𝐷) · 𝑓)) ∧ ((𝑒↑2) − (𝐷 · (𝑓↑2))) = 1) ↔ ((𝐴 · 𝐵) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · 𝑓)) ∧ ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (𝑓↑2))) = 1)))
110		oveq2 7158	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ((𝑎 · 𝑑) + (𝑐 · 𝑏)) → ((√‘𝐷) · 𝑓) = ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏))))
111	110	oveq2d 7166	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ((𝑎 · 𝑑) + (𝑐 · 𝑏)) → (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · 𝑓)) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))))
112	111	eqeq2d 2769	. . . . . . . . . . . . 13 ⊢ (𝑓 = ((𝑎 · 𝑑) + (𝑐 · 𝑏)) → ((𝐴 · 𝐵) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · 𝑓)) ↔ (𝐴 · 𝐵) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏))))))
113		oveq1 7157	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ((𝑎 · 𝑑) + (𝑐 · 𝑏)) → (𝑓↑2) = (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2))
114	113	oveq2d 7166	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ((𝑎 · 𝑑) + (𝑐 · 𝑏)) → (𝐷 · (𝑓↑2)) = (𝐷 · (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2)))
115	114	oveq2d 7166	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ((𝑎 · 𝑑) + (𝑐 · 𝑏)) → ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (𝑓↑2))) = ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2))))
116	115	eqeq1d 2760	. . . . . . . . . . . . 13 ⊢ (𝑓 = ((𝑎 · 𝑑) + (𝑐 · 𝑏)) → (((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (𝑓↑2))) = 1 ↔ ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2))) = 1))
117	112, 116	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑓 = ((𝑎 · 𝑑) + (𝑐 · 𝑏)) → (((𝐴 · 𝐵) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · 𝑓)) ∧ ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (𝑓↑2))) = 1) ↔ ((𝐴 · 𝐵) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))) ∧ ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2))) = 1)))
118	109, 117	rspc2ev 3553	. . . . . . . . . . 11 ⊢ ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) ∈ ℤ ∧ ((𝑎 · 𝑑) + (𝑐 · 𝑏)) ∈ ℤ ∧ ((𝐴 · 𝐵) = (((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏))) + ((√‘𝐷) · ((𝑎 · 𝑑) + (𝑐 · 𝑏)))) ∧ ((((𝑎 · 𝑐) + (𝐷 · (𝑑 · 𝑏)))↑2) − (𝐷 · (((𝑎 · 𝑑) + (𝑐 · 𝑏))↑2))) = 1)) → ∃𝑒 ∈ ℤ ∃𝑓 ∈ ℤ ((𝐴 · 𝐵) = (𝑒 + ((√‘𝐷) · 𝑓)) ∧ ((𝑒↑2) − (𝐷 · (𝑓↑2))) = 1))
119	16, 19, 55, 103, 118	syl112anc 1371	. . . . . . . . . 10 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ∃𝑒 ∈ ℤ ∃𝑓 ∈ ℤ ((𝐴 · 𝐵) = (𝑒 + ((√‘𝐷) · 𝑓)) ∧ ((𝑒↑2) − (𝐷 · (𝑓↑2))) = 1))
120	2, 119	jca 515	. . . . . . . . 9 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) ∧ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝐴 · 𝐵) ∈ ℝ ∧ ∃𝑒 ∈ ℤ ∃𝑓 ∈ ℤ ((𝐴 · 𝐵) = (𝑒 + ((√‘𝐷) · 𝑓)) ∧ ((𝑒↑2) − (𝐷 · (𝑓↑2))) = 1)))
121	120	ex 416	. . . . . . . 8 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ)) → ((𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1) → ((𝐴 · 𝐵) ∈ ℝ ∧ ∃𝑒 ∈ ℤ ∃𝑓 ∈ ℤ ((𝐴 · 𝐵) = (𝑒 + ((√‘𝐷) · 𝑓)) ∧ ((𝑒↑2) − (𝐷 · (𝑓↑2))) = 1))))
122	121	rexlimdvva 3218	. . . . . . 7 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1) → ((𝐴 · 𝐵) ∈ ℝ ∧ ∃𝑒 ∈ ℤ ∃𝑓 ∈ ℤ ((𝐴 · 𝐵) = (𝑒 + ((√‘𝐷) · 𝑓)) ∧ ((𝑒↑2) − (𝐷 · (𝑓↑2))) = 1))))
123	122	ex 416	. . . . . 6 ⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1) → ((𝐴 · 𝐵) ∈ ℝ ∧ ∃𝑒 ∈ ℤ ∃𝑓 ∈ ℤ ((𝐴 · 𝐵) = (𝑒 + ((√‘𝐷) · 𝑓)) ∧ ((𝑒↑2) − (𝐷 · (𝑓↑2))) = 1)))))
124	123	rexlimdvva 3218	. . . . 5 ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1) → ((𝐴 · 𝐵) ∈ ℝ ∧ ∃𝑒 ∈ ℤ ∃𝑓 ∈ ℤ ((𝐴 · 𝐵) = (𝑒 + ((√‘𝐷) · 𝑓)) ∧ ((𝑒↑2) − (𝐷 · (𝑓↑2))) = 1)))))
125	124	impd 414	. . . 4 ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → ((∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) ∧ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) → ((𝐴 · 𝐵) ∈ ℝ ∧ ∃𝑒 ∈ ℤ ∃𝑓 ∈ ℤ ((𝐴 · 𝐵) = (𝑒 + ((√‘𝐷) · 𝑓)) ∧ ((𝑒↑2) − (𝐷 · (𝑓↑2))) = 1))))
126	125	expimpd 457	. . 3 ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) ∧ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1))) → ((𝐴 · 𝐵) ∈ ℝ ∧ ∃𝑒 ∈ ℤ ∃𝑓 ∈ ℤ ((𝐴 · 𝐵) = (𝑒 + ((√‘𝐷) · 𝑓)) ∧ ((𝑒↑2) − (𝐷 · (𝑓↑2))) = 1))))
127		elpell1234qr 40187	. . . . 5 ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1234QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1))))
128		elpell1234qr 40187	. . . . 5 ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐵 ∈ (Pell1234QR‘𝐷) ↔ (𝐵 ∈ ℝ ∧ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1))))
129	127, 128	anbi12d 633	. . . 4 ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ((𝐴 ∈ (Pell1234QR‘𝐷) ∧ 𝐵 ∈ (Pell1234QR‘𝐷)) ↔ ((𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝐵 ∈ ℝ ∧ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)))))
130		an4 655	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) ∧ (𝐵 ∈ ℝ ∧ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1))) ↔ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) ∧ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1))))
131	129, 130	bitrdi 290	. . 3 ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ((𝐴 ∈ (Pell1234QR‘𝐷) ∧ 𝐵 ∈ (Pell1234QR‘𝐷)) ↔ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) ∧ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ (𝐵 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)))))
132		elpell1234qr 40187	. . 3 ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ((𝐴 · 𝐵) ∈ (Pell1234QR‘𝐷) ↔ ((𝐴 · 𝐵) ∈ ℝ ∧ ∃𝑒 ∈ ℤ ∃𝑓 ∈ ℤ ((𝐴 · 𝐵) = (𝑒 + ((√‘𝐷) · 𝑓)) ∧ ((𝑒↑2) − (𝐷 · (𝑓↑2))) = 1))))
133	126, 131, 132	3imtr4d 297	. 2 ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ((𝐴 ∈ (Pell1234QR‘𝐷) ∧ 𝐵 ∈ (Pell1234QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell1234QR‘𝐷)))
134	133	3impib 1113	1 ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷) ∧ 𝐵 ∈ (Pell1234QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell1234QR‘𝐷))

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∃wrex 3071   ∖ cdif 3855  ‘cfv 6335  (class class class)co 7150  ℂcc 10573  ℝcr 10574  1c1 10576   + caddc 10578   · cmul 10580   − cmin 10908  ℕcn 11674  2c2 11729  ℤcz 12020  ↑cexp 13479  √csqrt 14640  ◻_NNcsquarenn 40172  Pell1234QRcpell1234qr 40174

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-er 8299  df-en 8528  df-dom 8529  df-sdom 8530  df-sup 8939  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-n0 11935  df-z 12021  df-uz 12283  df-rp 12431  df-seq 13419  df-exp 13480  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-pell1234qr 40180

This theorem is referenced by:  pell14qrmulcl  40199