pell1qrgaplem

		Ref	Expression
	Assertion	pell1qrgaplem	$⊢ ((D \in ℕ \land (A \in ℕ_{0} \land B \in ℕ_{0})) \land (1 < A + \sqrt{D} B \land A^{2} - D B^{2} = 1)) \to \sqrt{D + 1} + \sqrt{D} \leq A + \sqrt{D} B$

Proof

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

Metamath Proof Explorer

Theorem pell1qrgaplem

Proof