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 Visualization version Unicode version

Theorem pellex 35750

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		fzfi 12223	. . . . . . . 8
2		xpfi 7860	. . . . . . . 8 $/\$
3	1, 1, 2	mp2an 686	. . . . . . 7
4		isfinite 8175	. . . . . . 7
5	3, 4	mpbi 213	. . . . . 6
6		nnenom 12231	. . . . . . 7
7	6	ensymi 7637	. . . . . 6
8		sdomentr 7724	. . . . . 6 $/\$
9	5, 7, 8	mp2an 686	. . . . 5
10		ensym 7636	. . . . . 6 $/\$ $/\$ $/\$ $/\$
11	10	ad2antll 743	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		sdomentr 7724	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
13	9, 11, 12	sylancr 676	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		opabssxp 4914	. . . . . . . 8 $/\$ $/\$
15	14	sseli 3414	. . . . . . 7 $/\$ $/\$
16		simprrl 782	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17	16	nnzd 11062	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18		simpllr 777	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simplr 770	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		nnabscl 13465	. . . . . . . . . . . 12 $/\$
21	18, 19, 20	syl2anc 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		zmodfz 12151	. . . . . . . . . . 11 $/\$
23	17, 21, 22	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		simprrr 783	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	24	nnzd 11062	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26		zmodfz 12151	. . . . . . . . . . 11 $/\$
27	25, 21, 26	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	23, 27	jca 541	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	28	ex 441	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		elxp7 6845	. . . . . . . 8 $/\$ $/\$
31		opelxp 4869	. . . . . . . 8 $/\$
32	29, 30, 31	3imtr4g 278	. . . . . . 7 $/\$ $/\$ $/\$
33	15, 32	syl5 32	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
34	33	imp 436	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	34	adantlrr 735	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		fveq2 5879	. . . . . 6
37	36	oveq1d 6323	. . . . 5
38		fveq2 5879	. . . . . 6
39	38	oveq1d 6323	. . . . 5
40	37, 39	opeq12d 4166	. . . 4
41	13, 35, 40	fphpd 35730	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		eleq1 2537	. . . . . . . . . . . 12
43		eleq1 2537	. . . . . . . . . . . 12
44	42, 43	bi2anan9 890	. . . . . . . . . . 11 $/\$ $/\$ $/\$
45		oveq1 6315	. . . . . . . . . . . . 13
46		oveq1 6315	. . . . . . . . . . . . . 14
47	46	oveq2d 6324	. . . . . . . . . . . . 13
48	45, 47	oveqan12d 6327	. . . . . . . . . . . 12 $/\$
49	48	eqeq1d 2473	. . . . . . . . . . 11 $/\$
50	44, 49	anbi12d 725	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
51	50	cbvopabv 4465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
52	51	eleq2i 2541	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
53	52	biimpi 199	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
54		elopab 4709	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
55		elopab 4709	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
56		simp3ll 1101	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	3expb 1232	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	57	3ad2ant1 1051	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		simp3lr 1102	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	59	3expb 1232	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	60	3ad2ant1 1051	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		simp1lr 1094	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	62	3adant1r 1285	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		simp-4l 784	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	64	3ad2ant1 1051	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66		simp-4r 785	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	66	3ad2ant1 1051	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		simp2ll 1097	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69	68	3adant2l 1286	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		simp2lr 1098	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	70	3adant2l 1286	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72		simp2l 1056	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		simp1rl 1095	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74		simp3l 1058	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		simp3 1032	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
76		simp2 1031	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
77		simp1 1030	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
78	75, 76, 77	3netr3d 2719	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
79		vex 3034	. . . . . . . . . . . . . . . . . . 19
80		vex 3034	. . . . . . . . . . . . . . . . . . 19
81	79, 80	opth 4676	. . . . . . . . . . . . . . . . . 18 $/\$
82	81	necon3abii 2689	. . . . . . . . . . . . . . . . 17 $/\$
83	78, 82	sylib 201	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
84	72, 73, 74, 83	syl3anc 1292	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		simp1lr 1094	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		simp1rr 1096	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	86	3adant1l 1284	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88		simp2rr 1100	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		simp3r 1059	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		simp3 1032	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
91		ovex 6336	. . . . . . . . . . . . . . . . . . . 20
92		ovex 6336	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	opth 4676	. . . . . . . . . . . . . . . . . . 19 $/\$
94	90, 93	sylib 201	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
95		simprl 772	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
96		simpll 768	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
97	96	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
98	79, 80	op1st 6820	. . . . . . . . . . . . . . . . . . . . . . . 24
99	97, 98	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
100	99	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
101		simplr 770	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
102	101	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
103		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . 25
104		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . 25
105	103, 104	op1st 6820	. . . . . . . . . . . . . . . . . . . . . . . 24
106	102, 105	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
107	106	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
108	95, 100, 107	3eqtr3d 2513	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
109		simprr 774	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
110	96	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
111	79, 80	op2nd 6821	. . . . . . . . . . . . . . . . . . . . . . . 24
112	110, 111	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
113	112	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
114	101	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
115	103, 104	op2nd 6821	. . . . . . . . . . . . . . . . . . . . . . . 24
116	114, 115	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
117	116	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
118	109, 113, 117	3eqtr3d 2513	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
119	108, 118	jca 541	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
120	119	ex 441	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
121	120	3adant3 1050	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
122	94, 121	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
123	73, 72, 89, 122	syl3anc 1292	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
124	123	simpld 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125	123	simprd 470	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	58, 61, 63, 65, 67, 69, 71, 84, 85, 87, 88, 124, 125	pellexlem6 35749	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	126	3exp 1230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128	127	exlimdvv 1788	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	55, 128	syl5bi 225	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130	129	ex 441	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131	130	exlimdvv 1788	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	54, 131	syl5bi 225	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	132	impd 438	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	53, 133	sylan2i 667	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	134	rexlimdvv 2877	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	imp 436	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	136	adantlrr 735	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
138	41, 137	mpdan 681	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
139		pellexlem5 35748	. 2 $/\$ $/\$ $/\$ $/\$
140	138, 139	r19.29a 2918	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wex 1671

wcel 1904

wne 2641

wrex 2757

cvv 3031

cop 3965 class class class wbr 4395

copab 4453

cxp 4837

cfv 5589 (class class class)co 6308

com 6711

c1st 6810

c2nd 6811

cen 7584

csdm 7586

cfn 7587

cc0 9557

c1 9558

cmul 9562

cmin 9880

cn 10631

c2 10681

cz 10961

cq 11287

cfz 11810

cmo 12129

cexp 12310

csqrt 13373

cabs 13374

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-omul 7205 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-acn 8394 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-q 11288 df-rp 11326 df-ico 11666 df-fz 11811 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-dvds 14383 df-gcd 14548 df-numer 14763 df-denom 14764

This theorem is referenced by: pellqrex 35797

W3C validator