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 30933

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 12084	. . . . . . . 8
2		xpfi 7809	. . . . . . . 8 $/\$
3	1, 1, 2	mp2an 672	. . . . . . 7
4		isfinite 8086	. . . . . . 7
5	3, 4	mpbi 208	. . . . . 6
6		nnenom 12092	. . . . . . 7
7	6	ensymi 7584	. . . . . 6
8		sdomentr 7670	. . . . . 6 $/\$
9	5, 7, 8	mp2an 672	. . . . 5
10		ensym 7583	. . . . . 6 $/\$ $/\$ $/\$ $/\$
11	10	ad2antll 728	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		sdomentr 7670	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
13	9, 11, 12	sylancr 663	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		opabssxp 5083	. . . . . . . 8 $/\$ $/\$
15	14	sseli 3495	. . . . . . 7 $/\$ $/\$
16		simprrl 765	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17	16	nnzd 10989	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18		simpllr 760	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simplr 755	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		nnabscl 13169	. . . . . . . . . . . 12 $/\$
21	18, 19, 20	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		zmodfz 12019	. . . . . . . . . . 11 $/\$
23	17, 21, 22	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		simprrr 766	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	24	nnzd 10989	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26		zmodfz 12019	. . . . . . . . . . 11 $/\$
27	25, 21, 26	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	23, 27	jca 532	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	28	ex 434	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		elxp7 6832	. . . . . . . 8 $/\$ $/\$
31		opelxp 5038	. . . . . . . 8 $/\$
32	29, 30, 31	3imtr4g 270	. . . . . . 7 $/\$ $/\$ $/\$
33	15, 32	syl5 32	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
34	33	imp 429	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	34	adantlrr 720	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		fveq2 5872	. . . . . 6
37	36	oveq1d 6311	. . . . 5
38		fveq2 5872	. . . . . 6
39	38	oveq1d 6311	. . . . 5
40	37, 39	opeq12d 4227	. . . 4
41	13, 35, 40	fphpd 30912	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		eleq1 2529	. . . . . . . . . . . 12
43		eleq1 2529	. . . . . . . . . . . 12
44	42, 43	bi2anan9 873	. . . . . . . . . . 11 $/\$ $/\$ $/\$
45		oveq1 6303	. . . . . . . . . . . . 13
46		oveq1 6303	. . . . . . . . . . . . . 14
47	46	oveq2d 6312	. . . . . . . . . . . . 13
48	45, 47	oveqan12d 6315	. . . . . . . . . . . 12 $/\$
49	48	eqeq1d 2459	. . . . . . . . . . 11 $/\$
50	44, 49	anbi12d 710	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
51	50	cbvopabv 4526	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
52	51	eleq2i 2535	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
53	52	biimpi 194	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
54		elopab 4764	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
55		elopab 4764	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
56		simp3ll 1067	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	3expb 1197	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	57	3ad2ant1 1017	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		simp3lr 1068	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	59	3expb 1197	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	60	3ad2ant1 1017	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		simp1lr 1060	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	62	3adant1r 1221	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		simp-4l 767	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	64	3ad2ant1 1017	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66		simp-4r 768	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	66	3ad2ant1 1017	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		simp2ll 1063	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69	68	3adant2l 1222	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		simp2lr 1064	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	70	3adant2l 1222	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72		simp2l 1022	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		simp1rl 1061	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74		simp3l 1024	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		simp3 998	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
76		simp2 997	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
77		simp1 996	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
78	75, 76, 77	3netr3d 2760	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
79		vex 3112	. . . . . . . . . . . . . . . . . . 19
80		vex 3112	. . . . . . . . . . . . . . . . . . 19
81	79, 80	opth 4730	. . . . . . . . . . . . . . . . . 18 $/\$
82	81	necon3abii 2717	. . . . . . . . . . . . . . . . 17 $/\$
83	78, 82	sylib 196	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
84	72, 73, 74, 83	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		simp1lr 1060	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		simp1rr 1062	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	86	3adant1l 1220	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88		simp2rr 1066	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		simp3r 1025	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		simp3 998	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
91		ovex 6324	. . . . . . . . . . . . . . . . . . . 20
92		ovex 6324	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	opth 4730	. . . . . . . . . . . . . . . . . . 19 $/\$
94	90, 93	sylib 196	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
95		simprl 756	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
96		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
97	96	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
98	79, 80	op1st 6807	. . . . . . . . . . . . . . . . . . . . . . . 24
99	97, 98	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
100	99	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
101		simplr 755	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
102	101	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
103		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . . 25
104		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . . 25
105	103, 104	op1st 6807	. . . . . . . . . . . . . . . . . . . . . . . 24
106	102, 105	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
107	106	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
108	95, 100, 107	3eqtr3d 2506	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
109		simprr 757	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
110	96	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
111	79, 80	op2nd 6808	. . . . . . . . . . . . . . . . . . . . . . . 24
112	110, 111	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
113	112	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
114	101	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
115	103, 104	op2nd 6808	. . . . . . . . . . . . . . . . . . . . . . . 24
116	114, 115	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
117	116	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
118	109, 113, 117	3eqtr3d 2506	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
119	108, 118	jca 532	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
120	119	ex 434	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
121	120	3adant3 1016	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
122	94, 121	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
123	73, 72, 89, 122	syl3anc 1228	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
124	123	simpld 459	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125	123	simprd 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	58, 61, 63, 65, 67, 69, 71, 84, 85, 87, 88, 124, 125	pellexlem6 30932	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	126	3exp 1195	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128	127	exlimdvv 1726	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	55, 128	syl5bi 217	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130	129	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131	130	exlimdvv 1726	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	54, 131	syl5bi 217	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	132	impd 431	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134	53, 133	sylan2i 655	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	134	rexlimdvv 2955	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	imp 429	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137	136	adantlrr 720	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
138	41, 137	mpdan 668	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
139		pellexlem5 30931	. 2 $/\$ $/\$ $/\$ $/\$
140	138, 139	r19.29a 2999	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

wceq 1395

wex 1613

wcel 1819

wne 2652

wrex 2808

cvv 3109

cop 4038 class class class wbr 4456

copab 4514

cxp 5006

cfv 5594 (class class class)co 6296

com 6699

c1st 6797

c2nd 6798

cen 7532

csdm 7534

cfn 7535

cc0 9509

c1 9510

cmul 9514

cmin 9824

cn 10556

c2 10606

cz 10885

cq 11207

cfz 11697

cmo 11998

cexp 12168

csqrt 13077

cabs 13078

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-oadd 7152 df-omul 7153 df-er 7329 df-map 7440 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-oi 7953 df-card 8337 df-acn 8340 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-q 11208 df-rp 11246 df-ico 11560 df-fz 11698 df-fl 11931 df-mod 11999 df-seq 12110 df-exp 12169 df-hash 12408 df-cj 12943 df-re 12944 df-im 12945 df-sqrt 13079 df-abs 13080 df-dvds 13998 df-gcd 14156 df-numer 14279 df-denom 14280

This theorem is referenced by: pellqrex 30977

W3C validator