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 29317

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 29315	. 2 $/\$ $/\$ $/\$ $/\$
2		fzfi 11904	. . . . . . . . . 10
3		xpfi 7687	. . . . . . . . . 10 $/\$
4	2, 2, 3	mp2an 672	. . . . . . . . 9
5		isfinite 7962	. . . . . . . . 9
6	4, 5	mpbi 208	. . . . . . . 8
7		nnenom 11912	. . . . . . . . 9
8	7	ensymi 7462	. . . . . . . 8
9		sdomentr 7548	. . . . . . . 8 $/\$
10	6, 8, 9	mp2an 672	. . . . . . 7
11		ensym 7461	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
12	11	ad2antll 728	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		sdomentr 7548	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
14	10, 12, 13	sylancr 663	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		opabssxp 5012	. . . . . . . . . 10 $/\$ $/\$
16	15	sseli 3453	. . . . . . . . 9 $/\$ $/\$
17		simprrl 763	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	17	nnzd 10850	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simpllr 758	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		simplr 754	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		nnabscl 12924	. . . . . . . . . . . . . 14 $/\$
22	19, 20, 21	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
23		zmodfz 11839	. . . . . . . . . . . . 13 $/\$
24	18, 22, 23	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25		simprrr 764	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	25	nnzd 10850	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27		zmodfz 11839	. . . . . . . . . . . . 13 $/\$
28	26, 22, 27	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	24, 28	jca 532	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31		elxp7 6712	. . . . . . . . . 10 $/\$ $/\$
32		opelxp 4970	. . . . . . . . . 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 5792	. . . . . . . 8
38	37	oveq1d 6208	. . . . . . 7
39		fveq2 5792	. . . . . . . 8
40	39	oveq1d 6208	. . . . . . 7
41	38, 40	opeq12d 4168	. . . . . 6
42	14, 36, 41	fphpd 29296	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43		eleq1 2523	. . . . . . . . . . . . . 14
44		eleq1 2523	. . . . . . . . . . . . . 14
45	43, 44	bi2anan9 868	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
46		oveq1 6200	. . . . . . . . . . . . . . 15
47		oveq1 6200	. . . . . . . . . . . . . . . 16
48	47	oveq2d 6209	. . . . . . . . . . . . . . 15
49	46, 48	oveqan12d 6212	. . . . . . . . . . . . . 14 $/\$
50	49	eqeq1d 2453	. . . . . . . . . . . . 13 $/\$
51	45, 50	anbi12d 710	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
52	51	cbvopabv 4462	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
53	52	eleq2i 2529	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
54	53	biimpi 194	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
55		elopab 4698	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
56		elopab 4698	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
57		simp3ll 1059	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	57	3expb 1189	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	3ad2ant1 1009	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		simp3lr 1060	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	60	3expb 1189	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	61	3ad2ant1 1009	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp1lr 1052	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	63	3adant1r 1212	. . . . . . . . . . . . . . . . 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 1213	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71		simp2lr 1056	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	71	3adant2l 1213	. . . . . . . . . . . . . . . . 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 2751	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
80		vex 3074	. . . . . . . . . . . . . . . . . . . . 21
81		vex 3074	. . . . . . . . . . . . . . . . . . . . 21
82	80, 81	opth 4667	. . . . . . . . . . . . . . . . . . . 20 $/\$
83	82	necon3abii 2708	. . . . . . . . . . . . . . . . . . 19 $/\$
84	79, 83	sylib 196	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	73, 74, 75, 84	syl3anc 1219	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		simp1lr 1052	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87		simp1rr 1054	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	87	3adant1l 1211	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		simp2rr 1058	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		simp3r 1017	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91		simp3 990	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
92		ovex 6218	. . . . . . . . . . . . . . . . . . . . . 22
93		ovex 6218	. . . . . . . . . . . . . . . . . . . . . 22
94	92, 93	opth 4667	. . . . . . . . . . . . . . . . . . . . 21 $/\$
95	91, 94	sylib 196	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
96		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
97		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
98	97	fveq2d 5796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
99	80, 81	op1st 6688	. . . . . . . . . . . . . . . . . . . . . . . . . 26
100	98, 99	syl6eq 2508	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
101	100	oveq1d 6208	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
102		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
103	102	fveq2d 5796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
104		vex 3074	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105		vex 3074	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
106	104, 105	op1st 6688	. . . . . . . . . . . . . . . . . . . . . . . . . 26
107	103, 106	syl6eq 2508	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
108	107	oveq1d 6208	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
109	96, 101, 108	3eqtr3d 2500	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
110		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
111	97	fveq2d 5796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
112	80, 81	op2nd 6689	. . . . . . . . . . . . . . . . . . . . . . . . . 26
113	111, 112	syl6eq 2508	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
114	113	oveq1d 6208	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
115	102	fveq2d 5796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
116	104, 105	op2nd 6689	. . . . . . . . . . . . . . . . . . . . . . . . . 26
117	115, 116	syl6eq 2508	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
118	117	oveq1d 6208	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
119	110, 114, 118	3eqtr3d 2500	. . . . . . . . . . . . . . . . . . . . . . 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 1219	. . . . . . . . . . . . . . . . . 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 29316	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128	127	3exp 1187	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	128	exlimdvv 1692	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130	56, 129	syl5bi 217	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131	130	ex 434	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	131	exlimdvv 1692	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	55, 132	syl5bi 217	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	133	impd 431	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	54, 134	sylan2i 655	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	rexlimdvv 2946	. . . . . . 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 2940	. 2 $/\$ $/\$ $/\$ $/\$
142	1, 141	mpd 15	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

wceq 1370

wex 1587

wcel 1758

wne 2644

wrex 2796

cvv 3071

cop 3984 class class class wbr 4393

copab 4450

cxp 4939

cfv 5519 (class class class)co 6193

com 6579

c1st 6678

c2nd 6679

cen 7410

csdm 7412

cfn 7413

cc0 9386

c1 9387

cmul 9391

cmin 9699

cn 10426

c2 10475

cz 10750

cq 11057

cfz 11547

cmo 11818

cexp 11975

csqr 12833

cabs 12834

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4504 ax-sep 4514 ax-nul 4522 ax-pow 4571 ax-pr 4632 ax-un 6475 ax-inf2 7951 ax-cnex 9442 ax-resscn 9443 ax-1cn 9444 ax-icn 9445 ax-addcl 9446 ax-addrcl 9447 ax-mulcl 9448 ax-mulrcl 9449 ax-mulcom 9450 ax-addass 9451 ax-mulass 9452 ax-distr 9453 ax-i2m1 9454 ax-1ne0 9455 ax-1rid 9456 ax-rnegex 9457 ax-rrecex 9458 ax-cnre 9459 ax-pre-lttri 9460 ax-pre-lttrn 9461 ax-pre-ltadd 9462 ax-pre-mulgt0 9463 ax-pre-sup 9464

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3073 df-sbc 3288 df-csb 3390 df-dif 3432 df-un 3434 df-in 3436 df-ss 3443 df-pss 3445 df-nul 3739 df-if 3893 df-pw 3963 df-sn 3979 df-pr 3981 df-tp 3983 df-op 3985 df-uni 4193 df-int 4230 df-iun 4274 df-br 4394 df-opab 4452 df-mpt 4453 df-tr 4487 df-eprel 4733 df-id 4737 df-po 4742 df-so 4743 df-fr 4780 df-se 4781 df-we 4782 df-ord 4823 df-on 4824 df-lim 4825 df-suc 4826 df-xp 4947 df-rel 4948 df-cnv 4949 df-co 4950 df-dm 4951 df-rn 4952 df-res 4953 df-ima 4954 df-iota 5482 df-fun 5521 df-fn 5522 df-f 5523 df-f1 5524 df-fo 5525 df-f1o 5526 df-fv 5527 df-isom 5528 df-riota 6154 df-ov 6196 df-oprab 6197 df-mpt2 6198 df-om 6580 df-1st 6680 df-2nd 6681 df-recs 6935 df-rdg 6969 df-1o 7023 df-oadd 7027 df-omul 7028 df-er 7204 df-map 7319 df-en 7414 df-dom 7415 df-sdom 7416 df-fin 7417 df-sup 7795 df-oi 7828 df-card 8213 df-acn 8216 df-pnf 9524 df-mnf 9525 df-xr 9526 df-ltxr 9527 df-le 9528 df-sub 9701 df-neg 9702 df-div 10098 df-nn 10427 df-2 10484 df-3 10485 df-n0 10684 df-z 10751 df-uz 10966 df-q 11058 df-rp 11096 df-ico 11410 df-fz 11548 df-fl 11752 df-mod 11819 df-seq 11917 df-exp 11976 df-hash 12214 df-cj 12699 df-re 12700 df-im 12701 df-sqr 12835 df-abs 12836 df-dvds 13647 df-gcd 13802 df-numer 13924 df-denom 13925

This theorem is referenced by: pellqrex 29361

W3C validator