Metamath Proof Explorer

Theorem pell1234qrmulcl

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

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

Proof

Step Hyp Ref Expression
1 remulcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
2 1 ad5antlr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
3 simprl ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℤ )
4 3 ad3antrrr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → 𝑎 ∈ ℤ )
5 simplrl ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → 𝑐 ∈ ℤ )
6 4 5 zmulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑎 · 𝑐 ) ∈ ℤ )
7 eldifi ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℕ )
8 7 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐷 ∈ ℕ )
9 8 nnzd ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐷 ∈ ℤ )
10 9 ad3antrrr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → 𝐷 ∈ ℤ )
11 simplrr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → 𝑑 ∈ ℤ )
12 simprr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℤ )
13 12 ad3antrrr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → 𝑏 ∈ ℤ )
14 11 13 zmulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑑 · 𝑏 ) ∈ ℤ )
15 10 14 zmulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 · ( 𝑑 · 𝑏 ) ) ∈ ℤ )
16 6 15 zaddcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ∈ ℤ )
17 4 11 zmulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑎 · 𝑑 ) ∈ ℤ )
18 5 13 zmulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑐 · 𝑏 ) ∈ ℤ )
19 17 18 zaddcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ∈ ℤ )
20 simprl ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
21 20 ad2antrr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
22 simprl ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) )
23 21 22 oveq12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝐴 · 𝐵 ) = ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) )
24 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
25 24 ad2antrl ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
26 25 ad3antrrr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → 𝑎 ∈ ℂ )
27 8 nncnd ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐷 ∈ ℂ )
28 27 ad3antrrr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → 𝐷 ∈ ℂ )
29 28 sqrtcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( √ ‘ 𝐷 ) ∈ ℂ )
30 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
31 30 ad2antll ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
32 31 ad3antrrr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → 𝑏 ∈ ℂ )
33 29 32 mulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ 𝐷 ) · 𝑏 ) ∈ ℂ )
34 zcn ⊢ ( 𝑐 ∈ ℤ → 𝑐 ∈ ℂ )
35 34 adantr ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → 𝑐 ∈ ℂ )
36 35 ad2antlr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → 𝑐 ∈ ℂ )
37 zcn ⊢ ( 𝑑 ∈ ℤ → 𝑑 ∈ ℂ )
38 37 adantl ⊢ ( ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → 𝑑 ∈ ℂ )
39 38 ad2antlr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → 𝑑 ∈ ℂ )
40 29 39 mulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ 𝐷 ) · 𝑑 ) ∈ ℂ )
41 26 33 36 40 muladdd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) = ( ( ( 𝑎 · 𝑐 ) + ( ( ( √ ‘ 𝐷 ) · 𝑑 ) · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) + ( ( 𝑎 · ( ( √ ‘ 𝐷 ) · 𝑑 ) ) + ( 𝑐 · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) ) )
42 29 39 29 32 mul4d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( √ ‘ 𝐷 ) · 𝑑 ) · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = ( ( ( √ ‘ 𝐷 ) · ( √ ‘ 𝐷 ) ) · ( 𝑑 · 𝑏 ) ) )
43 28 msqsqrtd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ 𝐷 ) · ( √ ‘ 𝐷 ) ) = 𝐷 )
44 43 oveq1d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( √ ‘ 𝐷 ) · ( √ ‘ 𝐷 ) ) · ( 𝑑 · 𝑏 ) ) = ( 𝐷 · ( 𝑑 · 𝑏 ) ) )
45 42 44 eqtrd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( √ ‘ 𝐷 ) · 𝑑 ) · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = ( 𝐷 · ( 𝑑 · 𝑏 ) ) )
46 45 oveq2d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 · 𝑐 ) + ( ( ( √ ‘ 𝐷 ) · 𝑑 ) · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) = ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) )
47 26 29 39 mul12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑎 · ( ( √ ‘ 𝐷 ) · 𝑑 ) ) = ( ( √ ‘ 𝐷 ) · ( 𝑎 · 𝑑 ) ) )
48 36 29 32 mul12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑐 · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = ( ( √ ‘ 𝐷 ) · ( 𝑐 · 𝑏 ) ) )
49 47 48 oveq12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 · ( ( √ ‘ 𝐷 ) · 𝑑 ) ) + ( 𝑐 · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) = ( ( ( √ ‘ 𝐷 ) · ( 𝑎 · 𝑑 ) ) + ( ( √ ‘ 𝐷 ) · ( 𝑐 · 𝑏 ) ) ) )
50 26 39 mulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑎 · 𝑑 ) ∈ ℂ )
51 36 32 mulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑐 · 𝑏 ) ∈ ℂ )
52 29 50 51 adddid ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) = ( ( ( √ ‘ 𝐷 ) · ( 𝑎 · 𝑑 ) ) + ( ( √ ‘ 𝐷 ) · ( 𝑐 · 𝑏 ) ) ) )
53 49 52 eqtr4d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 · ( ( √ ‘ 𝐷 ) · 𝑑 ) ) + ( 𝑐 · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) = ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) )
54 46 53 oveq12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( 𝑎 · 𝑐 ) + ( ( ( √ ‘ 𝐷 ) · 𝑑 ) · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) + ( ( 𝑎 · ( ( √ ‘ 𝐷 ) · 𝑑 ) ) + ( 𝑐 · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) )
55 23 41 54 3eqtrd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝐴 · 𝐵 ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) )
56 50 51 addcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ∈ ℂ )
57 29 56 sqmuld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ↑ 2 ) = ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) ) )
58 28 sqsqrtd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ 𝐷 ) ↑ 2 ) = 𝐷 )
59 58 oveq1d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) ) = ( 𝐷 · ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) ) )
60 57 59 eqtr2d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 · ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) ) = ( ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ↑ 2 ) )
61 60 oveq2d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) ) ) = ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ↑ 2 ) ) )
62 26 36 mulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑎 · 𝑐 ) ∈ ℂ )
63 39 32 mulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑑 · 𝑏 ) ∈ ℂ )
64 28 63 mulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 · ( 𝑑 · 𝑏 ) ) ∈ ℂ )
65 62 64 addcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ∈ ℂ )
66 29 56 mulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ∈ ℂ )
67 subsq ⊢ ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ∈ ℂ ∧ ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ∈ ℂ ) → ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ↑ 2 ) ) = ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) · ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) − ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) ) )
68 65 66 67 syl2anc ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ↑ 2 ) ) = ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) · ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) − ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) ) )
69 41 54 eqtr2d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) = ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) )
70 26 33 36 40 mulsubd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 − ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) = ( ( ( 𝑎 · 𝑐 ) + ( ( ( √ ‘ 𝐷 ) · 𝑑 ) · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) − ( ( 𝑎 · ( ( √ ‘ 𝐷 ) · 𝑑 ) ) + ( 𝑐 · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) ) )
71 46 53 oveq12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( 𝑎 · 𝑐 ) + ( ( ( √ ‘ 𝐷 ) · 𝑑 ) · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) − ( ( 𝑎 · ( ( √ ‘ 𝐷 ) · 𝑑 ) ) + ( 𝑐 · ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) − ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) )
72 70 71 eqtr2d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) − ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) = ( ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 − ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) )
73 69 72 oveq12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) · ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) − ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) ) = ( ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) · ( ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 − ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) ) )
74 61 68 73 3eqtrd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) ) ) = ( ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) · ( ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 − ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) ) )
75 26 33 addcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∈ ℂ )
76 36 40 addcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∈ ℂ )
77 26 33 subcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∈ ℂ )
78 36 40 subcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 𝑐 − ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∈ ℂ )
79 75 76 77 78 mul4d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) · ( ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 − ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) ) = ( ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) · ( ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) · ( 𝑐 − ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) ) )
80 subsq ⊢ ( ( 𝑎 ∈ ℂ ∧ ( ( √ ‘ 𝐷 ) · 𝑏 ) ∈ ℂ ) → ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) ) = ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) )
81 26 33 80 syl2anc ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) ) = ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) )
82 subsq ⊢ ( ( 𝑐 ∈ ℂ ∧ ( ( √ ‘ 𝐷 ) · 𝑑 ) ∈ ℂ ) → ( ( 𝑐 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑑 ) ↑ 2 ) ) = ( ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) · ( 𝑐 − ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) )
83 36 40 82 syl2anc ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑐 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑑 ) ↑ 2 ) ) = ( ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) · ( 𝑐 − ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) )
84 81 83 oveq12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) ) · ( ( 𝑐 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑑 ) ↑ 2 ) ) ) = ( ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) · ( ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) · ( 𝑐 − ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) ) )
85 29 32 sqmuld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) = ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑏 ↑ 2 ) ) )
86 85 oveq2d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) ) = ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑏 ↑ 2 ) ) ) )
87 29 39 sqmuld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( √ ‘ 𝐷 ) · 𝑑 ) ↑ 2 ) = ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑑 ↑ 2 ) ) )
88 87 oveq2d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑐 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑑 ) ↑ 2 ) ) = ( ( 𝑐 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑑 ↑ 2 ) ) ) )
89 86 88 oveq12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) ) · ( ( 𝑐 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) · 𝑑 ) ↑ 2 ) ) ) = ( ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑏 ↑ 2 ) ) ) · ( ( 𝑐 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑑 ↑ 2 ) ) ) ) )
90 79 84 89 3eqtr2d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) · ( ( 𝑎 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) · ( 𝑐 − ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) ) = ( ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑏 ↑ 2 ) ) ) · ( ( 𝑐 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑑 ↑ 2 ) ) ) ) )
91 58 oveq1d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑏 ↑ 2 ) ) = ( 𝐷 · ( 𝑏 ↑ 2 ) ) )
92 91 oveq2d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑏 ↑ 2 ) ) ) = ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) )
93 58 oveq1d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑑 ↑ 2 ) ) = ( 𝐷 · ( 𝑑 ↑ 2 ) ) )
94 93 oveq2d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑐 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑑 ↑ 2 ) ) ) = ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) )
95 92 94 oveq12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑏 ↑ 2 ) ) ) · ( ( 𝑐 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑑 ↑ 2 ) ) ) ) = ( ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) · ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) ) )
96 simprr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 )
97 96 ad2antrr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 )
98 simprr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 )
99 97 98 oveq12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) · ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) ) = ( 1 · 1 ) )
100 1t1e1 ⊢ ( 1 · 1 ) = 1
101 100 a1i ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( 1 · 1 ) = 1 )
102 95 99 101 3eqtrd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( 𝑎 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑏 ↑ 2 ) ) ) · ( ( 𝑐 ↑ 2 ) − ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑑 ↑ 2 ) ) ) ) = 1 )
103 74 90 102 3eqtrd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) ) ) = 1 )
104 oveq1 ⊢ ( 𝑒 = ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) → ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) )
105 104 eqeq2d ⊢ ( 𝑒 = ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) → ( ( 𝐴 · 𝐵 ) = ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ↔ ( 𝐴 · 𝐵 ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ) )
106 oveq1 ⊢ ( 𝑒 = ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) → ( 𝑒 ↑ 2 ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) )
107 106 oveq1d ⊢ ( 𝑒 = ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) → ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) )
108 107 eqeq1d ⊢ ( 𝑒 = ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) → ( ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ↔ ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) )
109 105 108 anbi12d ⊢ ( 𝑒 = ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) → ( ( ( 𝐴 · 𝐵 ) = ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) ↔ ( ( 𝐴 · 𝐵 ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) ) )
110 oveq2 ⊢ ( 𝑓 = ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) → ( ( √ ‘ 𝐷 ) · 𝑓 ) = ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) )
111 110 oveq2d ⊢ ( 𝑓 = ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) → ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) )
112 111 eqeq2d ⊢ ( 𝑓 = ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) → ( ( 𝐴 · 𝐵 ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ↔ ( 𝐴 · 𝐵 ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) ) )
113 oveq1 ⊢ ( 𝑓 = ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) → ( 𝑓 ↑ 2 ) = ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) )
114 113 oveq2d ⊢ ( 𝑓 = ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) → ( 𝐷 · ( 𝑓 ↑ 2 ) ) = ( 𝐷 · ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) ) )
115 114 oveq2d ⊢ ( 𝑓 = ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) → ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) ) ) )
116 115 eqeq1d ⊢ ( 𝑓 = ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) → ( ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ↔ ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) ) ) = 1 ) )
117 112 116 anbi12d ⊢ ( 𝑓 = ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) → ( ( ( 𝐴 · 𝐵 ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) ↔ ( ( 𝐴 · 𝐵 ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) ∧ ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) ) ) = 1 ) ) )
118 109 117 rspc2ev ⊢ ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ∈ ℤ ∧ ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ∈ ℤ ∧ ( ( 𝐴 · 𝐵 ) = ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) + ( ( √ ‘ 𝐷 ) · ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ) ) ∧ ( ( ( ( 𝑎 · 𝑐 ) + ( 𝐷 · ( 𝑑 · 𝑏 ) ) ) ↑ 2 ) − ( 𝐷 · ( ( ( 𝑎 · 𝑑 ) + ( 𝑐 · 𝑏 ) ) ↑ 2 ) ) ) = 1 ) ) → ∃ 𝑒 ∈ ℤ ∃ 𝑓 ∈ ℤ ( ( 𝐴 · 𝐵 ) = ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) )
119 16 19 55 103 118 syl112anc ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ∃ 𝑒 ∈ ℤ ∃ 𝑓 ∈ ℤ ( ( 𝐴 · 𝐵 ) = ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) )
120 2 119 jca ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) ∧ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ ∃ 𝑒 ∈ ℤ ∃ 𝑓 ∈ ℤ ( ( 𝐴 · 𝐵 ) = ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) ) )
121 120 ex ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝑐 ∈ ℤ ∧ 𝑑 ∈ ℤ ) ) → ( ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ ∃ 𝑒 ∈ ℤ ∃ 𝑓 ∈ ℤ ( ( 𝐴 · 𝐵 ) = ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) ) ) )
122 121 rexlimdvva ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ ∃ 𝑒 ∈ ℤ ∃ 𝑓 ∈ ℤ ( ( 𝐴 · 𝐵 ) = ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) ) ) )
123 122 ex ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ ∃ 𝑒 ∈ ℤ ∃ 𝑓 ∈ ℤ ( ( 𝐴 · 𝐵 ) = ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) ) ) ) )
124 123 rexlimdvva ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ ∃ 𝑒 ∈ ℤ ∃ 𝑓 ∈ ℤ ( ( 𝐴 · 𝐵 ) = ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) ) ) ) )
125 124 impd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → ( ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ ∃ 𝑒 ∈ ℤ ∃ 𝑓 ∈ ℤ ( ( 𝐴 · 𝐵 ) = ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) ) ) )
126 125 expimpd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) ) → ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ ∃ 𝑒 ∈ ℤ ∃ 𝑓 ∈ ℤ ( ( 𝐴 · 𝐵 ) = ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) ) ) )
127 elpell1234qr ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
128 elpell1234qr ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ↔ ( 𝐵 ∈ ℝ ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) ) )
129 127 128 anbi12d ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ) ↔ ( ( 𝐴 ∈ ℝ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝐵 ∈ ℝ ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) ) ) )
130 an4 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ∧ ( 𝐵 ∈ ℝ ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) ) ↔ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) ) )
131 129 130 bitrdi ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ) ↔ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ∧ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ ( 𝐵 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) ) ) )
132 elpell1234qr ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝐴 · 𝐵 ) ∈ ( Pell1234QR ‘ 𝐷 ) ↔ ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ ∃ 𝑒 ∈ ℤ ∃ 𝑓 ∈ ℤ ( ( 𝐴 · 𝐵 ) = ( 𝑒 + ( ( √ ‘ 𝐷 ) · 𝑓 ) ) ∧ ( ( 𝑒 ↑ 2 ) − ( 𝐷 · ( 𝑓 ↑ 2 ) ) ) = 1 ) ) ) )
133 126 131 132 3imtr4d ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ) → ( 𝐴 · 𝐵 ) ∈ ( Pell1234QR ‘ 𝐷 ) ) )
134 133 3impib ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ∧ 𝐵 ∈ ( Pell1234QR ‘ 𝐷 ) ) → ( 𝐴 · 𝐵 ) ∈ ( Pell1234QR ‘ 𝐷 ) )