pellex - Mathbox for Stefan O'Rear

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

Theorem pellex 29129

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 29127	. 2 $/\$ $/\$ $/\$ $/\$
2		fzfi 11786	. . . . . . . . . 10
3		xpfi 7575	. . . . . . . . . 10 $/\$
4	2, 2, 3	mp2an 672	. . . . . . . . 9
5		isfinite 7850	. . . . . . . . 9
6	4, 5	mpbi 208	. . . . . . . 8
7		nnenom 11794	. . . . . . . . 9
8	7	ensymi 7351	. . . . . . . 8
9		sdomentr 7437	. . . . . . . 8 $/\$
10	6, 8, 9	mp2an 672	. . . . . . 7
11		ensym 7350	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
12	11	ad2antll 728	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		sdomentr 7437	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
14	10, 12, 13	sylancr 663	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		opabssxp 4906	. . . . . . . . . 10 $/\$ $/\$
16	15	sseli 3347	. . . . . . . . 9 $/\$ $/\$
17		simprrl 763	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	17	nnzd 10738	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simpllr 758	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		simplr 754	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		nnabscl 12805	. . . . . . . . . . . . . 14 $/\$
22	19, 20, 21	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
23		zmodfz 11721	. . . . . . . . . . . . 13 $/\$
24	18, 22, 23	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25		simprrr 764	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	25	nnzd 10738	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27		zmodfz 11721	. . . . . . . . . . . . 13 $/\$
28	26, 22, 27	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	24, 28	jca 532	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31		elxp7 6604	. . . . . . . . . 10 $/\$ $/\$
32		opelxp 4864	. . . . . . . . . 10 $/\$
33	30, 31, 32	3imtr4g 270	. . . . . . . . 9 $/\$ $/\$ $/\$
34	16, 33	syl5 32	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
35	34	imp 429	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36	35	adantlrr 720	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37		fveq2 5686	. . . . . . . 8
38	37	oveq1d 6101	. . . . . . 7
39		fveq2 5686	. . . . . . . 8
40	39	oveq1d 6101	. . . . . . 7
41	38, 40	opeq12d 4062	. . . . . 6
42	14, 36, 41	fphpd 29108	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43		eleq1 2498	. . . . . . . . . . . . . 14
44		eleq1 2498	. . . . . . . . . . . . . 14
45	43, 44	bi2anan9 868	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
46		oveq1 6093	. . . . . . . . . . . . . . 15
47		oveq1 6093	. . . . . . . . . . . . . . . 16
48	47	oveq2d 6102	. . . . . . . . . . . . . . 15
49	46, 48	oveqan12d 6105	. . . . . . . . . . . . . 14 $/\$
50	49	eqeq1d 2446	. . . . . . . . . . . . 13 $/\$
51	45, 50	anbi12d 710	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
52	51	cbvopabv 4356	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
53	52	eleq2i 2502	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
54	53	biimpi 194	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
55		elopab 4592	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
56		elopab 4592	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
57		simp3ll 1059	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	57	3expb 1188	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	3ad2ant1 1009	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		simp3lr 1060	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	60	3expb 1188	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	61	3ad2ant1 1009	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp1lr 1052	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	63	3adant1r 1211	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65		simp-4l 765	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	65	3ad2ant1 1009	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67		simp-4r 766	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68	67	3ad2ant1 1009	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		simp2ll 1055	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	69	3adant2l 1212	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71		simp2lr 1056	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	71	3adant2l 1212	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		simp2l 1014	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74		simp1rl 1053	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		simp3l 1016	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76		simp3 990	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
77		simp2 989	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
78		simp1 988	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
79	76, 77, 78	3netr3d 2629	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
80		vex 2970	. . . . . . . . . . . . . . . . . . . . 21
81		vex 2970	. . . . . . . . . . . . . . . . . . . . 21
82	80, 81	opth 4561	. . . . . . . . . . . . . . . . . . . 20 $/\$
83	82	necon3abii 2633	. . . . . . . . . . . . . . . . . . 19 $/\$
84	79, 83	sylib 196	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	73, 74, 75, 84	syl3anc 1218	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		simp1lr 1052	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87		simp1rr 1054	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	87	3adant1l 1210	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		simp2rr 1058	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		simp3r 1017	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91		simp3 990	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
92		ovex 6111	. . . . . . . . . . . . . . . . . . . . . 22
93		ovex 6111	. . . . . . . . . . . . . . . . . . . . . 22
94	92, 93	opth 4561	. . . . . . . . . . . . . . . . . . . . 21 $/\$
95	91, 94	sylib 196	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
96		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
97		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
98	97	fveq2d 5690	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
99	80, 81	op1st 6580	. . . . . . . . . . . . . . . . . . . . . . . . . 26
100	98, 99	syl6eq 2486	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
101	100	oveq1d 6101	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
102		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
103	102	fveq2d 5690	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
104		vex 2970	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105		vex 2970	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
106	104, 105	op1st 6580	. . . . . . . . . . . . . . . . . . . . . . . . . 26
107	103, 106	syl6eq 2486	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
108	107	oveq1d 6101	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
109	96, 101, 108	3eqtr3d 2478	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
110		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
111	97	fveq2d 5690	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
112	80, 81	op2nd 6581	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113	111, 112	syl6eq 2486	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
114	113	oveq1d 6101	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
115	102	fveq2d 5690	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
116	104, 105	op2nd 6581	. . . . . . . . . . . . . . . . . . . . . . . . . 26
117	115, 116	syl6eq 2486	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
118	117	oveq1d 6101	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
119	110, 114, 118	3eqtr3d 2478	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
120	109, 119	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
121	120	ex 434	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
122	121	3adant3 1008	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
123	95, 122	mpd 15	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
124	74, 73, 90, 123	syl3anc 1218	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125	124	simpld 459	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	124	simprd 463	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	59, 62, 64, 66, 68, 70, 72, 85, 86, 88, 89, 125, 126	pellexlem6 29128	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128	127	3exp 1186	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	128	exlimdvv 1691	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130	56, 129	syl5bi 217	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131	130	ex 434	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	131	exlimdvv 1691	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	55, 132	syl5bi 217	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	133	impd 431	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	54, 134	sylan2i 655	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	rexlimdvv 2842	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	136	imp 429	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
138	137	adantlrr 720	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
139	42, 138	mpdan 668	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140	139	ex 434	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
141	140	rexlimdva 2836	. 2 $/\$ $/\$ $/\$ $/\$
142	1, 141	mpd 15	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wex 1586

wcel 1756

wne 2601

wrex 2711

cvv 2967

cop 3878 class class class wbr 4287

copab 4344

cxp 4833

cfv 5413 (class class class)co 6086

com 6471

c1st 6570

c2nd 6571

cen 7299

csdm 7301

cfn 7302

cc0 9274

c1 9275

cmul 9279

cmin 9587

cn 10314

c2 10363

cz 10638

cq 10945

cfz 11429

cmo 11700

cexp 11857

csqr 12714

cabs 12715

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 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-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-1o 6912 df-oadd 6916 df-omul 6917 df-er 7093 df-map 7208 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-sup 7683 df-oi 7716 df-card 8101 df-acn 8104 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-n0 10572 df-z 10639 df-uz 10854 df-q 10946 df-rp 10984 df-ico 11298 df-fz 11430 df-fl 11634 df-mod 11701 df-seq 11799 df-exp 11858 df-hash 12096 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-dvds 13528 df-gcd 13683 df-numer 13805 df-denom 13806

This theorem is referenced by: pellqrex 29173

W3C validator