Metamath Proof Explorer

Theorem pell1qrgaplem

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

Ref Expression
Assertion pell1qrgaplem 
|- ( ( ( D e. NN /\ ( A e. NN0 /\ B e. NN0 ) ) /\ ( 1 < ( A + ( ( sqrt ` D ) x. B ) ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ ( A + ( ( sqrt ` D ) x. B ) ) )

Proof

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