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 35650

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 12192	. . . . . . . 8
2		xpfi 7852	. . . . . . . 8 $/\$
3	1, 1, 2	mp2an 676	. . . . . . 7
4		isfinite 8167	. . . . . . 7
5	3, 4	mpbi 211	. . . . . 6
6		nnenom 12200	. . . . . . 7
7	6	ensymi 7630	. . . . . 6
8		sdomentr 7716	. . . . . 6 $/\$
9	5, 7, 8	mp2an 676	. . . . 5
10		ensym 7629	. . . . . 6 $/\$ $/\$ $/\$ $/\$
11	10	ad2antll 733	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		sdomentr 7716	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
13	9, 11, 12	sylancr 667	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		opabssxp 4928	. . . . . . . 8 $/\$ $/\$
15	14	sseli 3460	. . . . . . 7 $/\$ $/\$
16		simprrl 772	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17	16	nnzd 11047	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18		simpllr 767	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simplr 760	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		nnabscl 13389	. . . . . . . . . . . 12 $/\$
21	18, 19, 20	syl2anc 665	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		zmodfz 12125	. . . . . . . . . . 11 $/\$
23	17, 21, 22	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		simprrr 773	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	24	nnzd 11047	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26		zmodfz 12125	. . . . . . . . . . 11 $/\$
27	25, 21, 26	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	23, 27	jca 534	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	28	ex 435	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		elxp7 6841	. . . . . . . 8 $/\$ $/\$
31		opelxp 4883	. . . . . . . 8 $/\$
32	29, 30, 31	3imtr4g 273	. . . . . . 7 $/\$ $/\$ $/\$
33	15, 32	syl5 33	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
34	33	imp 430	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	34	adantlrr 725	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		fveq2 5882	. . . . . 6
37	36	oveq1d 6321	. . . . 5
38		fveq2 5882	. . . . . 6
39	38	oveq1d 6321	. . . . 5
40	37, 39	opeq12d 4195	. . . 4
41	13, 35, 40	fphpd 35629	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		eleq1 2495	. . . . . . . . . . . 12
43		eleq1 2495	. . . . . . . . . . . 12
44	42, 43	bi2anan9 881	. . . . . . . . . . 11 $/\$ $/\$ $/\$
45		oveq1 6313	. . . . . . . . . . . . 13
46		oveq1 6313	. . . . . . . . . . . . . 14
47	46	oveq2d 6322	. . . . . . . . . . . . 13
48	45, 47	oveqan12d 6325	. . . . . . . . . . . 12 $/\$
49	48	eqeq1d 2424	. . . . . . . . . . 11 $/\$
50	44, 49	anbi12d 715	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
51	50	cbvopabv 4493	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
52	51	eleq2i 2499	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
53	52	biimpi 197	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
54		elopab 4728	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
55		elopab 4728	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
56		simp3ll 1076	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	3expb 1206	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	57	3ad2ant1 1026	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		simp3lr 1077	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	59	3expb 1206	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	60	3ad2ant1 1026	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		simp1lr 1069	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	62	3adant1r 1257	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		simp-4l 774	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	64	3ad2ant1 1026	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66		simp-4r 775	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	66	3ad2ant1 1026	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		simp2ll 1072	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69	68	3adant2l 1258	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		simp2lr 1073	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	70	3adant2l 1258	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72		simp2l 1031	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		simp1rl 1070	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74		simp3l 1033	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		simp3 1007	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
76		simp2 1006	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
77		simp1 1005	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
78	75, 76, 77	3netr3d 2723	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
79		vex 3083	. . . . . . . . . . . . . . . . . . 19
80		vex 3083	. . . . . . . . . . . . . . . . . . 19
81	79, 80	opth 4695	. . . . . . . . . . . . . . . . . 18 $/\$
82	81	necon3abii 2680	. . . . . . . . . . . . . . . . 17 $/\$
83	78, 82	sylib 199	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
84	72, 73, 74, 83	syl3anc 1264	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		simp1lr 1069	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		simp1rr 1071	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	86	3adant1l 1256	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88		simp2rr 1075	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		simp3r 1034	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		simp3 1007	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
91		ovex 6334	. . . . . . . . . . . . . . . . . . . 20
92		ovex 6334	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	opth 4695	. . . . . . . . . . . . . . . . . . 19 $/\$
94	90, 93	sylib 199	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
95		simprl 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
96		simpll 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
97	96	fveq2d 5886	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
98	79, 80	op1st 6816	. . . . . . . . . . . . . . . . . . . . . . . 24
99	97, 98	syl6eq 2479	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
100	99	oveq1d 6321	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
101		simplr 760	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
102	101	fveq2d 5886	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
103		vex 3083	. . . . . . . . . . . . . . . . . . . . . . . . 25
104		vex 3083	. . . . . . . . . . . . . . . . . . . . . . . . 25
105	103, 104	op1st 6816	. . . . . . . . . . . . . . . . . . . . . . . 24
106	102, 105	syl6eq 2479	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
107	106	oveq1d 6321	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
108	95, 100, 107	3eqtr3d 2471	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
109		simprr 764	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
110	96	fveq2d 5886	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
111	79, 80	op2nd 6817	. . . . . . . . . . . . . . . . . . . . . . . 24
112	110, 111	syl6eq 2479	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
113	112	oveq1d 6321	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
114	101	fveq2d 5886	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
115	103, 104	op2nd 6817	. . . . . . . . . . . . . . . . . . . . . . . 24
116	114, 115	syl6eq 2479	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
117	116	oveq1d 6321	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
118	109, 113, 117	3eqtr3d 2471	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
119	108, 118	jca 534	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
120	119	ex 435	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
121	120	3adant3 1025	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
122	94, 121	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
123	73, 72, 89, 122	syl3anc 1264	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
124	123	simpld 460	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125	123	simprd 464	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	58, 61, 63, 65, 67, 69, 71, 84, 85, 87, 88, 124, 125	pellexlem6 35649	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	126	3exp 1204	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128	127	exlimdvv 1773	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	55, 128	syl5bi 220	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130	129	ex 435	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131	130	exlimdvv 1773	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	54, 131	syl5bi 220	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	132	impd 432	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	53, 133	sylan2i 659	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	134	rexlimdvv 2920	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	imp 430	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	136	adantlrr 725	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
138	41, 137	mpdan 672	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
139		pellexlem5 35648	. 2 $/\$ $/\$ $/\$ $/\$
140	138, 139	r19.29a 2967	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wex 1657

wcel 1872

wne 2614

wrex 2772

cvv 3080

cop 4004 class class class wbr 4423

copab 4481

cxp 4851

cfv 5601 (class class class)co 6306

com 6707

c1st 6806

c2nd 6807

cen 7578

csdm 7580

cfn 7581

cc0 9547

c1 9548

cmul 9552

cmin 9868

cn 10617

c2 10667

cz 10945

cq 11272

cfz 11792

cmo 12103

cexp 12279

csqrt 13297

cabs 13298

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6598 ax-inf2 8156 ax-cnex 9603 ax-resscn 9604 ax-1cn 9605 ax-icn 9606 ax-addcl 9607 ax-addrcl 9608 ax-mulcl 9609 ax-mulrcl 9610 ax-mulcom 9611 ax-addass 9612 ax-mulass 9613 ax-distr 9614 ax-i2m1 9615 ax-1ne0 9616 ax-1rid 9617 ax-rnegex 9618 ax-rrecex 9619 ax-cnre 9620 ax-pre-lttri 9621 ax-pre-lttrn 9622 ax-pre-ltadd 9623 ax-pre-mulgt0 9624 ax-pre-sup 9625

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-nel 2617 df-ral 2776 df-rex 2777 df-reu 2778 df-rmo 2779 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4220 df-int 4256 df-iun 4301 df-br 4424 df-opab 4483 df-mpt 4484 df-tr 4519 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-se 4813 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6268 df-ov 6309 df-oprab 6310 df-mpt2 6311 df-om 6708 df-1st 6808 df-2nd 6809 df-wrecs 7040 df-recs 7102 df-rdg 7140 df-1o 7194 df-oadd 7198 df-omul 7199 df-er 7375 df-map 7486 df-en 7582 df-dom 7583 df-sdom 7584 df-fin 7585 df-sup 7966 df-inf 7967 df-oi 8035 df-card 8382 df-acn 8385 df-pnf 9685 df-mnf 9686 df-xr 9687 df-ltxr 9688 df-le 9689 df-sub 9870 df-neg 9871 df-div 10278 df-nn 10618 df-2 10676 df-3 10677 df-n0 10878 df-z 10946 df-uz 11168 df-q 11273 df-rp 11311 df-ico 11649 df-fz 11793 df-fl 12035 df-mod 12104 df-seq 12221 df-exp 12280 df-hash 12523 df-cj 13163 df-re 13164 df-im 13165 df-sqrt 13299 df-abs 13300 df-dvds 14306 df-gcd 14469 df-numer 14684 df-denom 14685

This theorem is referenced by: pellqrex 35697

W3C validator