pellex - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pellex		Unicode version

Theorem pellex 26788

Description: Every Pell equation has a nontrivial solution. Theorem 62 in [vandenDries] p. 43. (Contributed by Stefan O'Rear, 19-Oct-2014.)

**Assertion**
Ref	Expression
pellex	$/\$

Distinct variable group:

Proof of Theorem pellex Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pellexlem5 26786	. 2 $/\$ $/\$ $/\$ $/\$
2		fzfi 11266	. . . . . . . . . 10
3		xpfi 7337	. . . . . . . . . 10 $/\$
4	2, 2, 3	mp2an 654	. . . . . . . . 9
5		isfinite 7563	. . . . . . . . 9
6	4, 5	mpbi 200	. . . . . . . 8
7		nnenom 11274	. . . . . . . . 9
8	7	ensymi 7116	. . . . . . . 8
9		sdomentr 7200	. . . . . . . 8 $/\$
10	6, 8, 9	mp2an 654	. . . . . . 7
11		ensym 7115	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
12	11	ad2antll 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		sdomentr 7200	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
14	10, 12, 13	sylancr 645	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		opabssxp 4909	. . . . . . . . . 10 $/\$ $/\$
16	15	sseli 3304	. . . . . . . . 9 $/\$ $/\$
17		simprrl 741	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	17	nnzd 10330	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simpllr 736	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		simplr 732	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		nnabscl 12084	. . . . . . . . . . . . . 14 $/\$
22	19, 20, 21	syl2anc 643	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
23		zmodfz 11223	. . . . . . . . . . . . 13 $/\$
24	18, 22, 23	syl2anc 643	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25		simprrr 742	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	25	nnzd 10330	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27		zmodfz 11223	. . . . . . . . . . . . 13 $/\$
28	26, 22, 27	syl2anc 643	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	24, 28	jca 519	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ex 424	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31		elxp7 6338	. . . . . . . . . 10 $/\$ $/\$
32		opelxp 4867	. . . . . . . . . 10 $/\$
33	30, 31, 32	3imtr4g 262	. . . . . . . . 9 $/\$ $/\$ $/\$
34	16, 33	syl5 30	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
35	34	imp 419	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36	35	adantlrr 702	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37		fveq2 5687	. . . . . . . 8
38	37	oveq1d 6055	. . . . . . 7
39		fveq2 5687	. . . . . . . 8
40	39	oveq1d 6055	. . . . . . 7
41	38, 40	opeq12d 3952	. . . . . 6
42	14, 36, 41	fphpd 26767	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43		eleq1 2464	. . . . . . . . . . . . . 14
44		eleq1 2464	. . . . . . . . . . . . . 14
45	43, 44	bi2anan9 844	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
46		oveq1 6047	. . . . . . . . . . . . . . 15
47		oveq1 6047	. . . . . . . . . . . . . . . 16
48	47	oveq2d 6056	. . . . . . . . . . . . . . 15
49	46, 48	oveqan12d 6059	. . . . . . . . . . . . . 14 $/\$
50	49	eqeq1d 2412	. . . . . . . . . . . . 13 $/\$
51	45, 50	anbi12d 692	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
52	51	cbvopabv 4237	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
53	52	eleq2i 2468	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
54	53	biimpi 187	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
55		elopab 4422	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
56		elopab 4422	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
57		simp3ll 1028	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	57	3expb 1154	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	3ad2ant1 978	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		simp3lr 1029	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	60	3expb 1154	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	61	3ad2ant1 978	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp1lr 1021	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	63	3adant1r 1177	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65		simp-4l 743	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	65	3ad2ant1 978	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67		simp-4r 744	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68	67	3ad2ant1 978	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		simp2ll 1024	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	69	3adant2l 1178	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71		simp2lr 1025	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	71	3adant2l 1178	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		simp2l 983	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74		simp1rl 1022	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		simp3l 985	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76		simp3 959	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
77		simp2 958	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
78		simp1 957	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
79	76, 77, 78	3netr3d 2593	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
80		vex 2919	. . . . . . . . . . . . . . . . . . . . 21
81		vex 2919	. . . . . . . . . . . . . . . . . . . . 21
82	80, 81	opth 4395	. . . . . . . . . . . . . . . . . . . 20 $/\$
83	82	necon3abii 2597	. . . . . . . . . . . . . . . . . . 19 $/\$
84	79, 83	sylib 189	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	73, 74, 75, 84	syl3anc 1184	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		simp1lr 1021	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87		simp1rr 1023	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	87	3adant1l 1176	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		simp2rr 1027	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		simp3r 986	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91		simp3 959	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
92		ovex 6065	. . . . . . . . . . . . . . . . . . . . . 22
93		ovex 6065	. . . . . . . . . . . . . . . . . . . . . 22
94	92, 93	opth 4395	. . . . . . . . . . . . . . . . . . . . 21 $/\$
95	91, 94	sylib 189	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
96		simprl 733	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
97		simpll 731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
98	97	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
99	80, 81	op1st 6314	. . . . . . . . . . . . . . . . . . . . . . . . . 26
100	98, 99	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
101	100	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
102		simplr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
103	102	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
104		vex 2919	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105		vex 2919	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
106	104, 105	op1st 6314	. . . . . . . . . . . . . . . . . . . . . . . . . 26
107	103, 106	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
108	107	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
109	96, 101, 108	3eqtr3d 2444	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
110		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
111	97	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
112	80, 81	op2nd 6315	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113	111, 112	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
114	113	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
115	102	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
116	104, 105	op2nd 6315	. . . . . . . . . . . . . . . . . . . . . . . . . 26
117	115, 116	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
118	117	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
119	110, 114, 118	3eqtr3d 2444	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
120	109, 119	jca 519	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
121	120	ex 424	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
122	121	3adant3 977	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
123	95, 122	mpd 15	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
124	74, 73, 90, 123	syl3anc 1184	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125	124	simpld 446	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	124	simprd 450	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	59, 62, 64, 66, 68, 70, 72, 85, 86, 88, 89, 125, 126	pellexlem6 26787	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128	127	3exp 1152	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	128	exlimdvv 1644	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130	56, 129	syl5bi 209	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131	130	ex 424	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	131	exlimdvv 1644	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	55, 132	syl5bi 209	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	133	imp3a 421	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	54, 134	sylan2i 637	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	rexlimdvv 2796	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	136	imp 419	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
138	137	adantlrr 702	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
139	42, 138	mpdan 650	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140	139	ex 424	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
141	140	rexlimdva 2790	. 2 $/\$ $/\$ $/\$ $/\$
142	1, 141	mpd 15	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 359 $/\$ w3a 936

wex 1547

wceq 1649

wcel 1721

wne 2567

wrex 2667

cvv 2916

cop 3777 class class class wbr 4172

copab 4225

com 4804

cxp 4835

cfv 5413 (class class class)co 6040

c1st 6306

c2nd 6307

cen 7065

csdm 7067

cfn 7068

cc0 8946

c1 8947

cmul 8951

cmin 9247

cn 9956

c2 10005

cz 10238

cq 10530

cfz 10999

cmo 11205

cexp 11337

csqr 11993

cabs 11994

This theorem is referenced by: pellqrex 26832

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-omul 6688 df-er 6864 df-map 6979 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-oi 7435 df-card 7782 df-acn 7785 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-q 10531 df-rp 10569 df-ico 10878 df-fz 11000 df-fl 11157 df-mod 11206 df-seq 11279 df-exp 11338 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-dvds 12808 df-gcd 12962 df-numer 13082 df-denom 13083

W3C validator