Theorem rmspecsqrtnq

Description: The discriminant used to define the X and Y sequences has an irrational square root. (Contributed by Stefan O'Rear, 21-Sep-2014) (Proof shortened by AV, 2-Aug-2021)

	Ref	Expression
Assertion	rmspecsqrtnq	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \sqrt{A^2-1}\in \left(ℂ\setminus \mathbb{Q}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eluzelcn	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in ℂ$$
2	1	sqcld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2\in ℂ$$
3		ax-1cn	$$⊢1\in ℂ$$
4		subcl	$$⊢\left(A^2\in ℂ\wedge 1\in ℂ\right)\to A^2-1\in ℂ$$
5	2 3 4	sylancl	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1\in ℂ$$
6	5	sqrtcld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \sqrt{A^2-1}\in ℂ$$
7		eluz2nn	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{N}$$
8	7	nnsqcld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2\in \mathbb{N}$$
9		nnm1nn0	$$⊢A^2\in \mathbb{N}\to A^2-1\in {\mathbb{N}}_0$$
10	8 9	syl	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1\in {\mathbb{N}}_0$$
11		nnm1nn0	$$⊢A\in \mathbb{N}\to A-1\in {\mathbb{N}}_0$$
12	7 11	syl	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A-1\in {\mathbb{N}}_0$$
13		binom2sub1	$$⊢A\in ℂ\to {\left(A-1\right)}^2=A^2-2A+1$$
14	1 13	syl	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to {\left(A-1\right)}^2=A^2-2A+1$$
15		2cnd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 2\in ℂ$$
16	15 1	mulcld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 2A\in ℂ$$
17	3	a1i	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1\in ℂ$$
18	2 16 17	subsubd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-\left(2A-1\right)=A^2-2A+1$$
19	14 18	eqtr4d	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to {\left(A-1\right)}^2=A^2-\left(2A-1\right)$$
20		1red	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1\in ℝ$$
21		2re	$$⊢2\in ℝ$$
22	21	a1i	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 2\in ℝ$$
23		eluzelre	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in ℝ$$
24	22 23	remulcld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 2A\in ℝ$$
25	24 20	resubcld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 2A-1\in ℝ$$
26	8	nnred	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2\in ℝ$$
27		eluz2gt1	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1<A$$
28	20 20 23 27 27	lt2addmuld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1+1<2A$$
29		remulcl	$$⊢\left(2\in ℝ\wedge A\in ℝ\right)\to 2A\in ℝ$$
30	21 23 29	sylancr	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 2A\in ℝ$$
31	20 20 30	ltaddsubd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(1+1<2A\leftrightarrow 1<2A-1\right)$$
32	28 31	mpbid	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1<2A-1$$
33	20 25 26 32	ltsub2dd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-\left(2A-1\right)<A^2-1$$
34	19 33	eqbrtrd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to {\left(A-1\right)}^2<A^2-1$$
35	26	ltm1d	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1<A^2$$
36		npcan	$$⊢\left(A\in ℂ\wedge 1\in ℂ\right)\to A-1+1=A$$
37	1 3 36	sylancl	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A-1+1=A$$
38	37	oveq1d	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to {\left(A-1+1\right)}^2=A^2$$
39	35 38	breqtrrd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1<{\left(A-1+1\right)}^2$$
40		nonsq	$$⊢\left(\left(A^2-1\in {\mathbb{N}}_0\wedge A-1\in {\mathbb{N}}_0\right)\wedge \left({\left(A-1\right)}^2<A^2-1\wedge A^2-1<{\left(A-1+1\right)}^2\right)\right)\to \neg \sqrt{A^2-1}\in \mathbb{Q}$$
41	10 12 34 39 40	syl22anc	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \neg \sqrt{A^2-1}\in \mathbb{Q}$$
42	6 41	eldifd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \sqrt{A^2-1}\in \left(ℂ\setminus \mathbb{Q}\right)$$