Metamath Proof Explorer


Theorem pell1qrgaplem

Description: Lemma for pell1qrgap . (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell1qrgaplem D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + 1 + D A + D B

Proof

Step Hyp Ref Expression
1 nnrp D D +
2 1 ad2antrr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D +
3 1rp 1 +
4 3 a1i D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1 +
5 2 4 rpaddcld D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + 1 +
6 5 rpsqrtcld D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + 1 +
7 6 rpred D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + 1
8 2 rpsqrtcld D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D +
9 8 rpred D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D
10 nn0re A 0 A
11 10 adantr A 0 B 0 A
12 11 ad2antlr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 A
13 nn0re B 0 B
14 13 adantl A 0 B 0 B
15 14 ad2antlr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B
16 9 15 remulcld D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D B
17 2 rpred D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D
18 1re 1
19 18 a1i D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1
20 15 resqcld D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B 2
21 19 20 resubcld D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1 B 2
22 17 21 remulcld D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D 1 B 2
23 0red D A 0 B 0 1 < A + D B A 2 D B 2 = 1 0
24 17 23 remulcld D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D 0
25 12 resqcld D A 0 B 0 1 < A + D B A 2 D B 2 = 1 A 2
26 sq1 1 2 = 1
27 26 a1i D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1 2 = 1
28 nnge1 B 1 B
29 28 adantl D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B 1 B
30 simplrl D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 1 < A + D B
31 oveq1 B = 0 B 2 = 0 2
32 31 adantl D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 B 2 = 0 2
33 sq0 0 2 = 0
34 32 33 eqtrdi D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 B 2 = 0
35 34 oveq2d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 D B 2 = D 0
36 2 rpcnd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D
37 36 adantr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 D
38 37 mul01d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 D 0 = 0
39 35 38 eqtrd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 D B 2 = 0
40 39 oveq2d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 A 2 D B 2 = A 2 0
41 simplrr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 A 2 D B 2 = 1
42 12 recnd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 A
43 42 sqcld D A 0 B 0 1 < A + D B A 2 D B 2 = 1 A 2
44 43 adantr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 A 2
45 44 subid1d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 A 2 0 = A 2
46 40 41 45 3eqtr3d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 1 = A 2
47 26 46 eqtr2id D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 A 2 = 1 2
48 nn0ge0 A 0 0 A
49 48 adantr A 0 B 0 0 A
50 49 ad2antlr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 0 A
51 0le1 0 1
52 51 a1i D A 0 B 0 1 < A + D B A 2 D B 2 = 1 0 1
53 sq11 A 0 A 1 0 1 A 2 = 1 2 A = 1
54 12 50 19 52 53 syl22anc D A 0 B 0 1 < A + D B A 2 D B 2 = 1 A 2 = 1 2 A = 1
55 54 adantr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 A 2 = 1 2 A = 1
56 47 55 mpbid D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 A = 1
57 simpr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 B = 0
58 57 oveq2d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 D B = D 0
59 8 rpcnd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D
60 59 adantr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 D
61 60 mul01d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 D 0 = 0
62 58 61 eqtrd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 D B = 0
63 56 62 oveq12d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 A + D B = 1 + 0
64 1p0e1 1 + 0 = 1
65 63 64 eqtrdi D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 A + D B = 1
66 30 65 breqtrd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 1 < 1
67 18 ltnri ¬ 1 < 1
68 pm2.24 1 < 1 ¬ 1 < 1 1 B
69 66 67 68 mpisyl D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B = 0 1 B
70 simplrr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B 0
71 elnn0 B 0 B B = 0
72 70 71 sylib D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B B = 0
73 29 69 72 mpjaodan D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1 B
74 nn0ge0 B 0 0 B
75 74 adantl A 0 B 0 0 B
76 75 ad2antlr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 0 B
77 19 15 52 76 le2sqd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1 B 1 2 B 2
78 73 77 mpbid D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1 2 B 2
79 27 78 eqbrtrrd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1 B 2
80 19 20 suble0d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1 B 2 0 1 B 2
81 79 80 mpbird D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1 B 2 0
82 21 23 2 lemul2d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1 B 2 0 D 1 B 2 D 0
83 81 82 mpbid D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D 1 B 2 D 0
84 22 24 25 83 leadd2dd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 A 2 + D 1 B 2 A 2 + D 0
85 5 rpcnd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + 1
86 85 sqsqrtd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + 1 2 = D + 1
87 simprr D A 0 B 0 1 < A + D B A 2 D B 2 = 1 A 2 D B 2 = 1
88 87 eqcomd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1 = A 2 D B 2
89 88 oveq2d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + 1 = D + A 2 - D B 2
90 15 recnd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B
91 90 sqcld D A 0 B 0 1 < A + D B A 2 D B 2 = 1 B 2
92 36 91 mulcld D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D B 2
93 36 43 92 addsub12d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + A 2 - D B 2 = A 2 + D - D B 2
94 19 recnd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1
95 36 94 91 subdid D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D 1 B 2 = D 1 D B 2
96 36 mulid1d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D 1 = D
97 96 oveq1d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D 1 D B 2 = D D B 2
98 95 97 eqtr2d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D D B 2 = D 1 B 2
99 98 oveq2d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 A 2 + D - D B 2 = A 2 + D 1 B 2
100 93 99 eqtrd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + A 2 - D B 2 = A 2 + D 1 B 2
101 86 89 100 3eqtrd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + 1 2 = A 2 + D 1 B 2
102 36 mul01d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D 0 = 0
103 102 oveq2d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 A 2 + D 0 = A 2 + 0
104 43 addid1d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 A 2 + 0 = A 2
105 103 104 eqtr2d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 A 2 = A 2 + D 0
106 84 101 105 3brtr4d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + 1 2 A 2
107 6 rpge0d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 0 D + 1
108 7 12 107 50 le2sqd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + 1 A D + 1 2 A 2
109 106 108 mpbird D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + 1 A
110 59 mulid1d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D 1 = D
111 19 15 8 lemul2d D A 0 B 0 1 < A + D B A 2 D B 2 = 1 1 B D 1 D B
112 73 111 mpbid D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D 1 D B
113 110 112 eqbrtrrd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D D B
114 7 9 12 16 109 113 le2addd D A 0 B 0 1 < A + D B A 2 D B 2 = 1 D + 1 + D A + D B