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 D A Pell1234QR D B Pell1234QR D A B Pell1234QR D

Proof

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