# 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 ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell1234QR}\left({D}\right)\wedge {B}\in \mathrm{Pell1234QR}\left({D}\right)\right)\to {A}{B}\in \mathrm{Pell1234QR}\left({D}\right)$

### Proof

Step Hyp Ref Expression
1 remulcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{B}\in ℝ$
2 1 ad5antlr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {A}{B}\in ℝ$
3 simprl ${⊢}\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {a}\in ℤ$
4 3 ad3antrrr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}\in ℤ$
5 simplrl ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {c}\in ℤ$
6 4 5 zmulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{c}\in ℤ$
7 eldifi ${⊢}{D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\to {D}\in ℕ$
8 7 ad2antrr ${⊢}\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {D}\in ℕ$
9 8 nnzd ${⊢}\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {D}\in ℤ$
10 9 ad3antrrr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {D}\in ℤ$
11 simplrr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {d}\in ℤ$
12 simprr ${⊢}\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {b}\in ℤ$
13 12 ad3antrrr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {b}\in ℤ$
14 11 13 zmulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {d}{b}\in ℤ$
15 10 14 zmulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {D}{d}{b}\in ℤ$
16 6 15 zaddcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{c}+{D}{d}{b}\in ℤ$
17 4 11 zmulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{d}\in ℤ$
18 5 13 zmulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {c}{b}\in ℤ$
19 17 18 zaddcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{d}+{c}{b}\in ℤ$
20 simprl ${⊢}\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\to {A}={a}+\sqrt{{D}}{b}$
21 20 ad2antrr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {A}={a}+\sqrt{{D}}{b}$
22 simprl ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {B}={c}+\sqrt{{D}}{d}$
23 21 22 oveq12d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {A}{B}=\left({a}+\sqrt{{D}}{b}\right)\left({c}+\sqrt{{D}}{d}\right)$
24 zcn ${⊢}{a}\in ℤ\to {a}\in ℂ$
25 24 ad2antrl ${⊢}\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {a}\in ℂ$
26 25 ad3antrrr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}\in ℂ$
27 8 nncnd ${⊢}\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {D}\in ℂ$
28 27 ad3antrrr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {D}\in ℂ$
29 28 sqrtcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \sqrt{{D}}\in ℂ$
30 zcn ${⊢}{b}\in ℤ\to {b}\in ℂ$
31 30 ad2antll ${⊢}\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {b}\in ℂ$
32 31 ad3antrrr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {b}\in ℂ$
33 29 32 mulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \sqrt{{D}}{b}\in ℂ$
34 zcn ${⊢}{c}\in ℤ\to {c}\in ℂ$
35 34 adantr ${⊢}\left({c}\in ℤ\wedge {d}\in ℤ\right)\to {c}\in ℂ$
36 35 ad2antlr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {c}\in ℂ$
37 zcn ${⊢}{d}\in ℤ\to {d}\in ℂ$
38 37 adantl ${⊢}\left({c}\in ℤ\wedge {d}\in ℤ\right)\to {d}\in ℂ$
39 38 ad2antlr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {d}\in ℂ$
40 29 39 mulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \sqrt{{D}}{d}\in ℂ$
41 26 33 36 40 muladdd ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \left({a}+\sqrt{{D}}{b}\right)\left({c}+\sqrt{{D}}{d}\right)={a}{c}+\sqrt{{D}}{d}\sqrt{{D}}{b}+{a}\sqrt{{D}}{d}+{c}\sqrt{{D}}{b}$
42 29 39 29 32 mul4d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \sqrt{{D}}{d}\sqrt{{D}}{b}=\sqrt{{D}}\sqrt{{D}}{d}{b}$
43 28 msqsqrtd ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \sqrt{{D}}\sqrt{{D}}={D}$
44 43 oveq1d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \sqrt{{D}}\sqrt{{D}}{d}{b}={D}{d}{b}$
45 42 44 eqtrd ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \sqrt{{D}}{d}\sqrt{{D}}{b}={D}{d}{b}$
46 45 oveq2d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{c}+\sqrt{{D}}{d}\sqrt{{D}}{b}={a}{c}+{D}{d}{b}$
47 26 29 39 mul12d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}\sqrt{{D}}{d}=\sqrt{{D}}{a}{d}$
48 36 29 32 mul12d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {c}\sqrt{{D}}{b}=\sqrt{{D}}{c}{b}$
49 47 48 oveq12d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}\sqrt{{D}}{d}+{c}\sqrt{{D}}{b}=\sqrt{{D}}{a}{d}+\sqrt{{D}}{c}{b}$
50 26 39 mulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{d}\in ℂ$
51 36 32 mulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {c}{b}\in ℂ$
52 29 50 51 adddid ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \sqrt{{D}}\left({a}{d}+{c}{b}\right)=\sqrt{{D}}{a}{d}+\sqrt{{D}}{c}{b}$
53 49 52 eqtr4d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}\sqrt{{D}}{d}+{c}\sqrt{{D}}{b}=\sqrt{{D}}\left({a}{d}+{c}{b}\right)$
54 46 53 oveq12d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{c}+\sqrt{{D}}{d}\sqrt{{D}}{b}+{a}\sqrt{{D}}{d}+{c}\sqrt{{D}}{b}={a}{c}+{D}{d}{b}+\sqrt{{D}}\left({a}{d}+{c}{b}\right)$
55 23 41 54 3eqtrd ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {A}{B}={a}{c}+{D}{d}{b}+\sqrt{{D}}\left({a}{d}+{c}{b}\right)$
56 50 51 addcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{d}+{c}{b}\in ℂ$
57 29 56 sqmuld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {\sqrt{{D}}\left({a}{d}+{c}{b}\right)}^{2}={\sqrt{{D}}}^{2}{\left({a}{d}+{c}{b}\right)}^{2}$
58 28 sqsqrtd ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {\sqrt{{D}}}^{2}={D}$
59 58 oveq1d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {\sqrt{{D}}}^{2}{\left({a}{d}+{c}{b}\right)}^{2}={D}{\left({a}{d}+{c}{b}\right)}^{2}$
60 57 59 eqtr2d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {D}{\left({a}{d}+{c}{b}\right)}^{2}={\sqrt{{D}}\left({a}{d}+{c}{b}\right)}^{2}$
61 60 oveq2d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{\left({a}{d}+{c}{b}\right)}^{2}={\left({a}{c}+{D}{d}{b}\right)}^{2}-{\sqrt{{D}}\left({a}{d}+{c}{b}\right)}^{2}$
62 26 36 mulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{c}\in ℂ$
63 39 32 mulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {d}{b}\in ℂ$
64 28 63 mulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {D}{d}{b}\in ℂ$
65 62 64 addcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{c}+{D}{d}{b}\in ℂ$
66 29 56 mulcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \sqrt{{D}}\left({a}{d}+{c}{b}\right)\in ℂ$
67 subsq ${⊢}\left({a}{c}+{D}{d}{b}\in ℂ\wedge \sqrt{{D}}\left({a}{d}+{c}{b}\right)\in ℂ\right)\to {\left({a}{c}+{D}{d}{b}\right)}^{2}-{\sqrt{{D}}\left({a}{d}+{c}{b}\right)}^{2}=\left({a}{c}+{D}{d}{b}+\sqrt{{D}}\left({a}{d}+{c}{b}\right)\right)\left({a}{c}+{D}{d}{b}-\sqrt{{D}}\left({a}{d}+{c}{b}\right)\right)$
68 65 66 67 syl2anc ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {\left({a}{c}+{D}{d}{b}\right)}^{2}-{\sqrt{{D}}\left({a}{d}+{c}{b}\right)}^{2}=\left({a}{c}+{D}{d}{b}+\sqrt{{D}}\left({a}{d}+{c}{b}\right)\right)\left({a}{c}+{D}{d}{b}-\sqrt{{D}}\left({a}{d}+{c}{b}\right)\right)$
69 41 54 eqtr2d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{c}+{D}{d}{b}+\sqrt{{D}}\left({a}{d}+{c}{b}\right)=\left({a}+\sqrt{{D}}{b}\right)\left({c}+\sqrt{{D}}{d}\right)$
70 26 33 36 40 mulsubd ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \left({a}-\sqrt{{D}}{b}\right)\left({c}-\sqrt{{D}}{d}\right)={a}{c}+\sqrt{{D}}{d}\sqrt{{D}}{b}-\left({a}\sqrt{{D}}{d}+{c}\sqrt{{D}}{b}\right)$
71 46 53 oveq12d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{c}+\sqrt{{D}}{d}\sqrt{{D}}{b}-\left({a}\sqrt{{D}}{d}+{c}\sqrt{{D}}{b}\right)={a}{c}+{D}{d}{b}-\sqrt{{D}}\left({a}{d}+{c}{b}\right)$
72 70 71 eqtr2d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}{c}+{D}{d}{b}-\sqrt{{D}}\left({a}{d}+{c}{b}\right)=\left({a}-\sqrt{{D}}{b}\right)\left({c}-\sqrt{{D}}{d}\right)$
73 69 72 oveq12d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \left({a}{c}+{D}{d}{b}+\sqrt{{D}}\left({a}{d}+{c}{b}\right)\right)\left({a}{c}+{D}{d}{b}-\sqrt{{D}}\left({a}{d}+{c}{b}\right)\right)=\left({a}+\sqrt{{D}}{b}\right)\left({c}+\sqrt{{D}}{d}\right)\left({a}-\sqrt{{D}}{b}\right)\left({c}-\sqrt{{D}}{d}\right)$
74 61 68 73 3eqtrd ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{\left({a}{d}+{c}{b}\right)}^{2}=\left({a}+\sqrt{{D}}{b}\right)\left({c}+\sqrt{{D}}{d}\right)\left({a}-\sqrt{{D}}{b}\right)\left({c}-\sqrt{{D}}{d}\right)$
75 26 33 addcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}+\sqrt{{D}}{b}\in ℂ$
76 36 40 addcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {c}+\sqrt{{D}}{d}\in ℂ$
77 26 33 subcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {a}-\sqrt{{D}}{b}\in ℂ$
78 36 40 subcld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {c}-\sqrt{{D}}{d}\in ℂ$
79 75 76 77 78 mul4d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \left({a}+\sqrt{{D}}{b}\right)\left({c}+\sqrt{{D}}{d}\right)\left({a}-\sqrt{{D}}{b}\right)\left({c}-\sqrt{{D}}{d}\right)=\left({a}+\sqrt{{D}}{b}\right)\left({a}-\sqrt{{D}}{b}\right)\left({c}+\sqrt{{D}}{d}\right)\left({c}-\sqrt{{D}}{d}\right)$
80 subsq ${⊢}\left({a}\in ℂ\wedge \sqrt{{D}}{b}\in ℂ\right)\to {{a}}^{2}-{\sqrt{{D}}{b}}^{2}=\left({a}+\sqrt{{D}}{b}\right)\left({a}-\sqrt{{D}}{b}\right)$
81 26 33 80 syl2anc ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {{a}}^{2}-{\sqrt{{D}}{b}}^{2}=\left({a}+\sqrt{{D}}{b}\right)\left({a}-\sqrt{{D}}{b}\right)$
82 subsq ${⊢}\left({c}\in ℂ\wedge \sqrt{{D}}{d}\in ℂ\right)\to {{c}}^{2}-{\sqrt{{D}}{d}}^{2}=\left({c}+\sqrt{{D}}{d}\right)\left({c}-\sqrt{{D}}{d}\right)$
83 36 40 82 syl2anc ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {{c}}^{2}-{\sqrt{{D}}{d}}^{2}=\left({c}+\sqrt{{D}}{d}\right)\left({c}-\sqrt{{D}}{d}\right)$
84 81 83 oveq12d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \left({{a}}^{2}-{\sqrt{{D}}{b}}^{2}\right)\left({{c}}^{2}-{\sqrt{{D}}{d}}^{2}\right)=\left({a}+\sqrt{{D}}{b}\right)\left({a}-\sqrt{{D}}{b}\right)\left({c}+\sqrt{{D}}{d}\right)\left({c}-\sqrt{{D}}{d}\right)$
85 29 32 sqmuld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {\sqrt{{D}}{b}}^{2}={\sqrt{{D}}}^{2}{{b}}^{2}$
86 85 oveq2d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {{a}}^{2}-{\sqrt{{D}}{b}}^{2}={{a}}^{2}-{\sqrt{{D}}}^{2}{{b}}^{2}$
87 29 39 sqmuld ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {\sqrt{{D}}{d}}^{2}={\sqrt{{D}}}^{2}{{d}}^{2}$
88 87 oveq2d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {{c}}^{2}-{\sqrt{{D}}{d}}^{2}={{c}}^{2}-{\sqrt{{D}}}^{2}{{d}}^{2}$
89 86 88 oveq12d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \left({{a}}^{2}-{\sqrt{{D}}{b}}^{2}\right)\left({{c}}^{2}-{\sqrt{{D}}{d}}^{2}\right)=\left({{a}}^{2}-{\sqrt{{D}}}^{2}{{b}}^{2}\right)\left({{c}}^{2}-{\sqrt{{D}}}^{2}{{d}}^{2}\right)$
90 79 84 89 3eqtr2d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \left({a}+\sqrt{{D}}{b}\right)\left({c}+\sqrt{{D}}{d}\right)\left({a}-\sqrt{{D}}{b}\right)\left({c}-\sqrt{{D}}{d}\right)=\left({{a}}^{2}-{\sqrt{{D}}}^{2}{{b}}^{2}\right)\left({{c}}^{2}-{\sqrt{{D}}}^{2}{{d}}^{2}\right)$
91 58 oveq1d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {\sqrt{{D}}}^{2}{{b}}^{2}={D}{{b}}^{2}$
92 91 oveq2d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {{a}}^{2}-{\sqrt{{D}}}^{2}{{b}}^{2}={{a}}^{2}-{D}{{b}}^{2}$
93 58 oveq1d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {\sqrt{{D}}}^{2}{{d}}^{2}={D}{{d}}^{2}$
94 93 oveq2d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {{c}}^{2}-{\sqrt{{D}}}^{2}{{d}}^{2}={{c}}^{2}-{D}{{d}}^{2}$
95 92 94 oveq12d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \left({{a}}^{2}-{\sqrt{{D}}}^{2}{{b}}^{2}\right)\left({{c}}^{2}-{\sqrt{{D}}}^{2}{{d}}^{2}\right)=\left({{a}}^{2}-{D}{{b}}^{2}\right)\left({{c}}^{2}-{D}{{d}}^{2}\right)$
96 simprr ${⊢}\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\to {{a}}^{2}-{D}{{b}}^{2}=1$
97 96 ad2antrr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {{a}}^{2}-{D}{{b}}^{2}=1$
98 simprr ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {{c}}^{2}-{D}{{d}}^{2}=1$
99 97 98 oveq12d ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \left({{a}}^{2}-{D}{{b}}^{2}\right)\left({{c}}^{2}-{D}{{d}}^{2}\right)=1\cdot 1$
100 1t1e1 ${⊢}1\cdot 1=1$
101 100 a1i ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to 1\cdot 1=1$
102 95 99 101 3eqtrd ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \left({{a}}^{2}-{\sqrt{{D}}}^{2}{{b}}^{2}\right)\left({{c}}^{2}-{\sqrt{{D}}}^{2}{{d}}^{2}\right)=1$
103 74 90 102 3eqtrd ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to {\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{\left({a}{d}+{c}{b}\right)}^{2}=1$
104 oveq1 ${⊢}{e}={a}{c}+{D}{d}{b}\to {e}+\sqrt{{D}}{f}={a}{c}+{D}{d}{b}+\sqrt{{D}}{f}$
105 104 eqeq2d ${⊢}{e}={a}{c}+{D}{d}{b}\to \left({A}{B}={e}+\sqrt{{D}}{f}↔{A}{B}={a}{c}+{D}{d}{b}+\sqrt{{D}}{f}\right)$
106 oveq1 ${⊢}{e}={a}{c}+{D}{d}{b}\to {{e}}^{2}={\left({a}{c}+{D}{d}{b}\right)}^{2}$
107 106 oveq1d ${⊢}{e}={a}{c}+{D}{d}{b}\to {{e}}^{2}-{D}{{f}}^{2}={\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{{f}}^{2}$
108 107 eqeq1d ${⊢}{e}={a}{c}+{D}{d}{b}\to \left({{e}}^{2}-{D}{{f}}^{2}=1↔{\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{{f}}^{2}=1\right)$
109 105 108 anbi12d ${⊢}{e}={a}{c}+{D}{d}{b}\to \left(\left({A}{B}={e}+\sqrt{{D}}{f}\wedge {{e}}^{2}-{D}{{f}}^{2}=1\right)↔\left({A}{B}={a}{c}+{D}{d}{b}+\sqrt{{D}}{f}\wedge {\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{{f}}^{2}=1\right)\right)$
110 oveq2 ${⊢}{f}={a}{d}+{c}{b}\to \sqrt{{D}}{f}=\sqrt{{D}}\left({a}{d}+{c}{b}\right)$
111 110 oveq2d ${⊢}{f}={a}{d}+{c}{b}\to {a}{c}+{D}{d}{b}+\sqrt{{D}}{f}={a}{c}+{D}{d}{b}+\sqrt{{D}}\left({a}{d}+{c}{b}\right)$
112 111 eqeq2d ${⊢}{f}={a}{d}+{c}{b}\to \left({A}{B}={a}{c}+{D}{d}{b}+\sqrt{{D}}{f}↔{A}{B}={a}{c}+{D}{d}{b}+\sqrt{{D}}\left({a}{d}+{c}{b}\right)\right)$
113 oveq1 ${⊢}{f}={a}{d}+{c}{b}\to {{f}}^{2}={\left({a}{d}+{c}{b}\right)}^{2}$
114 113 oveq2d ${⊢}{f}={a}{d}+{c}{b}\to {D}{{f}}^{2}={D}{\left({a}{d}+{c}{b}\right)}^{2}$
115 114 oveq2d ${⊢}{f}={a}{d}+{c}{b}\to {\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{{f}}^{2}={\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{\left({a}{d}+{c}{b}\right)}^{2}$
116 115 eqeq1d ${⊢}{f}={a}{d}+{c}{b}\to \left({\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{{f}}^{2}=1↔{\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{\left({a}{d}+{c}{b}\right)}^{2}=1\right)$
117 112 116 anbi12d ${⊢}{f}={a}{d}+{c}{b}\to \left(\left({A}{B}={a}{c}+{D}{d}{b}+\sqrt{{D}}{f}\wedge {\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{{f}}^{2}=1\right)↔\left({A}{B}={a}{c}+{D}{d}{b}+\sqrt{{D}}\left({a}{d}+{c}{b}\right)\wedge {\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{\left({a}{d}+{c}{b}\right)}^{2}=1\right)\right)$
118 109 117 rspc2ev ${⊢}\left({a}{c}+{D}{d}{b}\in ℤ\wedge {a}{d}+{c}{b}\in ℤ\wedge \left({A}{B}={a}{c}+{D}{d}{b}+\sqrt{{D}}\left({a}{d}+{c}{b}\right)\wedge {\left({a}{c}+{D}{d}{b}\right)}^{2}-{D}{\left({a}{d}+{c}{b}\right)}^{2}=1\right)\right)\to \exists {e}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {f}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}{B}={e}+\sqrt{{D}}{f}\wedge {{e}}^{2}-{D}{{f}}^{2}=1\right)$
119 16 19 55 103 118 syl112anc ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \exists {e}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {f}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}{B}={e}+\sqrt{{D}}{f}\wedge {{e}}^{2}-{D}{{f}}^{2}=1\right)$
120 2 119 jca ${⊢}\left(\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\wedge \left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \left({A}{B}\in ℝ\wedge \exists {e}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {f}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}{B}={e}+\sqrt{{D}}{f}\wedge {{e}}^{2}-{D}{{f}}^{2}=1\right)\right)$
121 120 ex ${⊢}\left(\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({c}\in ℤ\wedge {d}\in ℤ\right)\right)\to \left(\left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\to \left({A}{B}\in ℝ\wedge \exists {e}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {f}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}{B}={e}+\sqrt{{D}}{f}\wedge {{e}}^{2}-{D}{{f}}^{2}=1\right)\right)\right)$
122 121 rexlimdvva ${⊢}\left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\to \left(\exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\to \left({A}{B}\in ℝ\wedge \exists {e}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {f}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}{B}={e}+\sqrt{{D}}{f}\wedge {{e}}^{2}-{D}{{f}}^{2}=1\right)\right)\right)$
123 122 ex ${⊢}\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left(\left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\to \left(\exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\to \left({A}{B}\in ℝ\wedge \exists {e}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {f}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}{B}={e}+\sqrt{{D}}{f}\wedge {{e}}^{2}-{D}{{f}}^{2}=1\right)\right)\right)\right)$
124 123 rexlimdvva ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\to \left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\to \left(\exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\to \left({A}{B}\in ℝ\wedge \exists {e}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {f}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}{B}={e}+\sqrt{{D}}{f}\wedge {{e}}^{2}-{D}{{f}}^{2}=1\right)\right)\right)\right)$
125 124 impd ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\right)\to \left(\left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\wedge \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\to \left({A}{B}\in ℝ\wedge \exists {e}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {f}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}{B}={e}+\sqrt{{D}}{f}\wedge {{e}}^{2}-{D}{{f}}^{2}=1\right)\right)\right)$
126 125 expimpd ${⊢}{D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \left(\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\wedge \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\right)\to \left({A}{B}\in ℝ\wedge \exists {e}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {f}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}{B}={e}+\sqrt{{D}}{f}\wedge {{e}}^{2}-{D}{{f}}^{2}=1\right)\right)\right)$
127 elpell1234qr ${⊢}{D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \left({A}\in \mathrm{Pell1234QR}\left({D}\right)↔\left({A}\in ℝ\wedge \exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\right)$
128 elpell1234qr ${⊢}{D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \left({B}\in \mathrm{Pell1234QR}\left({D}\right)↔\left({B}\in ℝ\wedge \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\right)$
129 127 128 anbi12d ${⊢}{D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \left(\left({A}\in \mathrm{Pell1234QR}\left({D}\right)\wedge {B}\in \mathrm{Pell1234QR}\left({D}\right)\right)↔\left(\left({A}\in ℝ\wedge \exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({B}\in ℝ\wedge \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\right)\right)$
130 an4 ${⊢}\left(\left({A}\in ℝ\wedge \exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\right)\wedge \left({B}\in ℝ\wedge \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\right)↔\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\wedge \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\right)$
131 129 130 syl6bb ${⊢}{D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \left(\left({A}\in \mathrm{Pell1234QR}\left({D}\right)\wedge {B}\in \mathrm{Pell1234QR}\left({D}\right)\right)↔\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}={a}+\sqrt{{D}}{b}\wedge {{a}}^{2}-{D}{{b}}^{2}=1\right)\wedge \exists {c}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({B}={c}+\sqrt{{D}}{d}\wedge {{c}}^{2}-{D}{{d}}^{2}=1\right)\right)\right)\right)$
132 elpell1234qr ${⊢}{D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \left({A}{B}\in \mathrm{Pell1234QR}\left({D}\right)↔\left({A}{B}\in ℝ\wedge \exists {e}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {f}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}{B}={e}+\sqrt{{D}}{f}\wedge {{e}}^{2}-{D}{{f}}^{2}=1\right)\right)\right)$
133 126 131 132 3imtr4d ${⊢}{D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \left(\left({A}\in \mathrm{Pell1234QR}\left({D}\right)\wedge {B}\in \mathrm{Pell1234QR}\left({D}\right)\right)\to {A}{B}\in \mathrm{Pell1234QR}\left({D}\right)\right)$
134 133 3impib ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell1234QR}\left({D}\right)\wedge {B}\in \mathrm{Pell1234QR}\left({D}\right)\right)\to {A}{B}\in \mathrm{Pell1234QR}\left({D}\right)$