Theorem rmydioph

Description: jm2.27 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

	Ref	Expression
Assertion	rmydioph	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) } e. ( Dioph ` 3 )

Proof

Step	Hyp	Ref	Expression
1		elmapi	|- ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> a : ( 1 ... 3 ) --> NN0 )
2		2nn	|- 2 e. NN
3	2	jm2.27dlem3	|- 2 e. ( 1 ... 2 )
4		df-3	|- 3 = ( 2 + 1 )
5	3 4 2	jm2.27dlem2	|- 2 e. ( 1 ... 3 )
6		ffvelrn	|- ( ( a : ( 1 ... 3 ) --> NN0 /\ 2 e. ( 1 ... 3 ) ) -> ( a ` 2 ) e. NN0 )
7	1 5 6	sylancl	|- ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> ( a ` 2 ) e. NN0 )
8		elnn0	|- ( ( a ` 2 ) e. NN0 <-> ( ( a ` 2 ) e. NN \/ ( a ` 2 ) = 0 ) )
9	7 8	sylib	|- ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> ( ( a ` 2 ) e. NN \/ ( a ` 2 ) = 0 ) )
10		iba	|- ( ( ( a ` 2 ) e. NN \/ ( a ` 2 ) = 0 ) -> ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) <-> ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( ( a ` 2 ) e. NN \/ ( a ` 2 ) = 0 ) ) ) )
11		andi	|- ( ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( ( a ` 2 ) e. NN \/ ( a ` 2 ) = 0 ) ) <-> ( ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) = 0 ) ) )
12	10 11	bitrdi	|- ( ( ( a ` 2 ) e. NN \/ ( a ` 2 ) = 0 ) -> ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) <-> ( ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) = 0 ) ) ) )
13	12	anbi2d	|- ( ( ( a ` 2 ) e. NN \/ ( a ` 2 ) = 0 ) -> ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) <-> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) = 0 ) ) ) ) )
14	9 13	syl	|- ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) <-> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) = 0 ) ) ) ) )
15		simplr	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> ( a ` 1 ) e. ( ZZ>= ` 2 ) )
16		nnz	|- ( ( a ` 2 ) e. NN -> ( a ` 2 ) e. ZZ )
17	16	adantl	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> ( a ` 2 ) e. ZZ )
18		frmy	|- rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
19	18	fovcl	|- ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 2 ) e. ZZ ) -> ( ( a ` 1 ) rmY ( a ` 2 ) ) e. ZZ )
20	15 17 19	syl2anc	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> ( ( a ` 1 ) rmY ( a ` 2 ) ) e. ZZ )
21		rmy0	|- ( ( a ` 1 ) e. ( ZZ>= ` 2 ) -> ( ( a ` 1 ) rmY 0 ) = 0 )
22	21	ad2antlr	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> ( ( a ` 1 ) rmY 0 ) = 0 )
23		nngt0	|- ( ( a ` 2 ) e. NN -> 0 < ( a ` 2 ) )
24	23	adantl	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> 0 < ( a ` 2 ) )
25		0zd	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> 0 e. ZZ )
26		ltrmy	|- ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ 0 e. ZZ /\ ( a ` 2 ) e. ZZ ) -> ( 0 < ( a ` 2 ) <-> ( ( a ` 1 ) rmY 0 ) < ( ( a ` 1 ) rmY ( a ` 2 ) ) ) )
27	15 25 17 26	syl3anc	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> ( 0 < ( a ` 2 ) <-> ( ( a ` 1 ) rmY 0 ) < ( ( a ` 1 ) rmY ( a ` 2 ) ) ) )
28	24 27	mpbid	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> ( ( a ` 1 ) rmY 0 ) < ( ( a ` 1 ) rmY ( a ` 2 ) ) )
29	22 28	eqbrtrrd	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> 0 < ( ( a ` 1 ) rmY ( a ` 2 ) ) )
30		elnnz	|- ( ( ( a ` 1 ) rmY ( a ` 2 ) ) e. NN <-> ( ( ( a ` 1 ) rmY ( a ` 2 ) ) e. ZZ /\ 0 < ( ( a ` 1 ) rmY ( a ` 2 ) ) ) )
31	20 29 30	sylanbrc	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> ( ( a ` 1 ) rmY ( a ` 2 ) ) e. NN )
32		eleq1	|- ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) -> ( ( a ` 3 ) e. NN <-> ( ( a ` 1 ) rmY ( a ` 2 ) ) e. NN ) )
33	31 32	syl5ibrcom	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) -> ( a ` 3 ) e. NN ) )
34	33	pm4.71rd	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) <-> ( ( a ` 3 ) e. NN /\ ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) ) )
35		simpllr	|- ( ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) /\ ( a ` 3 ) e. NN ) -> ( a ` 1 ) e. ( ZZ>= ` 2 ) )
36		simplr	|- ( ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) /\ ( a ` 3 ) e. NN ) -> ( a ` 2 ) e. NN )
37		simpr	|- ( ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) /\ ( a ` 3 ) e. NN ) -> ( a ` 3 ) e. NN )
38		jm2.27	|- ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 2 ) e. NN /\ ( a ` 3 ) e. NN ) -> ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) <-> E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) )
39	35 36 37 38	syl3anc	|- ( ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) /\ ( a ` 3 ) e. NN ) -> ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) <-> E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) )
40	39	pm5.32da	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> ( ( ( a ` 3 ) e. NN /\ ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) <-> ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) ) )
41	34 40	bitrd	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) e. NN ) -> ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) <-> ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) ) )
42	41	ex	|- ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) -> ( ( a ` 2 ) e. NN -> ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) <-> ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) ) ) )
43	42	pm5.32rd	|- ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) -> ( ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) e. NN ) <-> ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) ) )
44		oveq2	|- ( ( a ` 2 ) = 0 -> ( ( a ` 1 ) rmY ( a ` 2 ) ) = ( ( a ` 1 ) rmY 0 ) )
45	44	adantl	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) = 0 ) -> ( ( a ` 1 ) rmY ( a ` 2 ) ) = ( ( a ` 1 ) rmY 0 ) )
46	21	ad2antlr	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) = 0 ) -> ( ( a ` 1 ) rmY 0 ) = 0 )
47	45 46	eqtrd	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) = 0 ) -> ( ( a ` 1 ) rmY ( a ` 2 ) ) = 0 )
48	47	eqeq2d	|- ( ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) /\ ( a ` 2 ) = 0 ) -> ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) <-> ( a ` 3 ) = 0 ) )
49	48	ex	|- ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) -> ( ( a ` 2 ) = 0 -> ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) <-> ( a ` 3 ) = 0 ) ) )
50	49	pm5.32rd	|- ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) -> ( ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) = 0 ) <-> ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) ) )
51	43 50	orbi12d	|- ( ( a e. ( NN0 ^m ( 1 ... 3 ) ) /\ ( a ` 1 ) e. ( ZZ>= ` 2 ) ) -> ( ( ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) = 0 ) ) <-> ( ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) ) ) )
52	51	pm5.32da	|- ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) /\ ( a ` 2 ) = 0 ) ) ) <-> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) ) ) ) )
53	14 52	bitrd	|- ( a e. ( NN0 ^m ( 1 ... 3 ) ) -> ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) <-> ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) ) ) ) )
54	53	rabbiia	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) } = { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) ) ) }
55		3nn0	|- 3 e. NN0
56		2z	|- 2 e. ZZ
57		ovex	|- ( 1 ... 3 ) e. _V
58		1nn	|- 1 e. NN
59	58	jm2.27dlem3	|- 1 e. ( 1 ... 1 )
60		df-2	|- 2 = ( 1 + 1 )
61	59 60 58	jm2.27dlem2	|- 1 e. ( 1 ... 2 )
62	61 4 2	jm2.27dlem2	|- 1 e. ( 1 ... 3 )
63		mzpproj	|- ( ( ( 1 ... 3 ) e. _V /\ 1 e. ( 1 ... 3 ) ) -> ( a e. ( ZZ ^m ( 1 ... 3 ) ) |-> ( a ` 1 ) ) e. ( mzPoly ` ( 1 ... 3 ) ) )
64	57 62 63	mp2an	|- ( a e. ( ZZ ^m ( 1 ... 3 ) ) |-> ( a ` 1 ) ) e. ( mzPoly ` ( 1 ... 3 ) )
65		eluzrabdioph	|- ( ( 3 e. NN0 /\ 2 e. ZZ /\ ( a e. ( ZZ ^m ( 1 ... 3 ) ) |-> ( a ` 1 ) ) e. ( mzPoly ` ( 1 ... 3 ) ) ) -> { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 1 ) e. ( ZZ>= ` 2 ) } e. ( Dioph ` 3 ) )
66	55 56 64 65	mp3an	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 1 ) e. ( ZZ>= ` 2 ) } e. ( Dioph ` 3 )
67		3nn	|- 3 e. NN
68	67	jm2.27dlem3	|- 3 e. ( 1 ... 3 )
69		mzpproj	|- ( ( ( 1 ... 3 ) e. _V /\ 3 e. ( 1 ... 3 ) ) -> ( a e. ( ZZ ^m ( 1 ... 3 ) ) |-> ( a ` 3 ) ) e. ( mzPoly ` ( 1 ... 3 ) ) )
70	57 68 69	mp2an	|- ( a e. ( ZZ ^m ( 1 ... 3 ) ) |-> ( a ` 3 ) ) e. ( mzPoly ` ( 1 ... 3 ) )
71		elnnrabdioph	|- ( ( 3 e. NN0 /\ ( a e. ( ZZ ^m ( 1 ... 3 ) ) |-> ( a ` 3 ) ) e. ( mzPoly ` ( 1 ... 3 ) ) ) -> { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 3 ) e. NN } e. ( Dioph ` 3 ) )
72	55 70 71	mp2an	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 3 ) e. NN } e. ( Dioph ` 3 )
73		fvex	|- ( i ` 8 ) e. _V
74		fvex	|- ( i ` 9 ) e. _V
75		fvex	|- ( i ` ; 1 0 ) e. _V
76		oveq1	|- ( g = ( i ` 9 ) -> ( g ^ 2 ) = ( ( i ` 9 ) ^ 2 ) )
77		oveq1	|- ( f = ( i ` 8 ) -> ( f ^ 2 ) = ( ( i ` 8 ) ^ 2 ) )
78	77	oveq2d	|- ( f = ( i ` 8 ) -> ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) = ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) )
79	76 78	oveqan12rd	|- ( ( f = ( i ` 8 ) /\ g = ( i ` 9 ) ) -> ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) )
80	79	eqeq1d	|- ( ( f = ( i ` 8 ) /\ g = ( i ` 9 ) ) -> ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 <-> ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 ) )
81	80	3adant3	|- ( ( f = ( i ` 8 ) /\ g = ( i ` 9 ) /\ h = ( i ` ; 1 0 ) ) -> ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 <-> ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 ) )
82		oveq1	|- ( h = ( i ` ; 1 0 ) -> ( h + 1 ) = ( ( i ` ; 1 0 ) + 1 ) )
83	82	oveq1d	|- ( h = ( i ` ; 1 0 ) -> ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) )
84	83	eqeq2d	|- ( h = ( i ` ; 1 0 ) -> ( c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) <-> c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) ) )
85	84	3ad2ant3	|- ( ( f = ( i ` 8 ) /\ g = ( i ` 9 ) /\ h = ( i ` ; 1 0 ) ) -> ( c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) <-> c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) ) )
86	81 85	3anbi12d	|- ( ( f = ( i ` 8 ) /\ g = ( i ` 9 ) /\ h = ( i ` ; 1 0 ) ) -> ( ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) <-> ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) )
87	86	anbi2d	|- ( ( f = ( i ` 8 ) /\ g = ( i ` 9 ) /\ h = ( i ` ; 1 0 ) ) -> ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) <-> ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) ) )
88		oveq1	|- ( f = ( i ` 8 ) -> ( f - ( a ` 3 ) ) = ( ( i ` 8 ) - ( a ` 3 ) ) )
89	88	breq2d	|- ( f = ( i ` 8 ) -> ( d || ( f - ( a ` 3 ) ) <-> d || ( ( i ` 8 ) - ( a ` 3 ) ) ) )
90	89	anbi2d	|- ( f = ( i ` 8 ) -> ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) <-> ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) ) )
91		oveq1	|- ( f = ( i ` 8 ) -> ( f - ( a ` 2 ) ) = ( ( i ` 8 ) - ( a ` 2 ) ) )
92	91	breq2d	|- ( f = ( i ` 8 ) -> ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) <-> ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) ) )
93	92	anbi1d	|- ( f = ( i ` 8 ) -> ( ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) <-> ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) )
94	90 93	anbi12d	|- ( f = ( i ` 8 ) -> ( ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) <-> ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
95	94	3ad2ant1	|- ( ( f = ( i ` 8 ) /\ g = ( i ` 9 ) /\ h = ( i ` ; 1 0 ) ) -> ( ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) <-> ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
96	87 95	anbi12d	|- ( ( f = ( i ` 8 ) /\ g = ( i ` 9 ) /\ h = ( i ` ; 1 0 ) ) -> ( ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) )
97	73 74 75 96	sbc3ie	|- ( [. ( i ` 8 ) / f ]. [. ( i ` 9 ) / g ]. [. ( i ` ; 1 0 ) / h ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
98	97	sbcbii	|- ( [. ( i ` 7 ) / e ]. [. ( i ` 8 ) / f ]. [. ( i ` 9 ) / g ]. [. ( i ` ; 1 0 ) / h ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> [. ( i ` 7 ) / e ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
99	98	sbcbii	|- ( [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. [. ( i ` 8 ) / f ]. [. ( i ` 9 ) / g ]. [. ( i ` ; 1 0 ) / h ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
100	99	sbcbii	|- ( [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. [. ( i ` 8 ) / f ]. [. ( i ` 9 ) / g ]. [. ( i ` ; 1 0 ) / h ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
101	100	sbcbii	|- ( [. ( i ` 4 ) / b ]. [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. [. ( i ` 8 ) / f ]. [. ( i ` 9 ) / g ]. [. ( i ` ; 1 0 ) / h ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> [. ( i ` 4 ) / b ]. [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
102	101	sbcbii	|- ( [. ( i |` ( 1 ... 3 ) ) / a ]. [. ( i ` 4 ) / b ]. [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. [. ( i ` 8 ) / f ]. [. ( i ` 9 ) / g ]. [. ( i ` ; 1 0 ) / h ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> [. ( i |` ( 1 ... 3 ) ) / a ]. [. ( i ` 4 ) / b ]. [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
103		fvex	|- ( i ` 5 ) e. _V
104		fvex	|- ( i ` 6 ) e. _V
105		fvex	|- ( i ` 7 ) e. _V
106		oveq1	|- ( d = ( i ` 6 ) -> ( d ^ 2 ) = ( ( i ` 6 ) ^ 2 ) )
107	106	3ad2ant2	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( d ^ 2 ) = ( ( i ` 6 ) ^ 2 ) )
108		oveq1	|- ( c = ( i ` 5 ) -> ( c ^ 2 ) = ( ( i ` 5 ) ^ 2 ) )
109	108	oveq2d	|- ( c = ( i ` 5 ) -> ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) = ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) )
110	109	3ad2ant1	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) = ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) )
111	107 110	oveq12d	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) )
112	111	eqeq1d	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 <-> ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 ) )
113		eleq1	|- ( e = ( i ` 7 ) -> ( e e. ( ZZ>= ` 2 ) <-> ( i ` 7 ) e. ( ZZ>= ` 2 ) ) )
114	113	3ad2ant3	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( e e. ( ZZ>= ` 2 ) <-> ( i ` 7 ) e. ( ZZ>= ` 2 ) ) )
115	112 114	3anbi23d	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) <-> ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) ) )
116		oveq1	|- ( e = ( i ` 7 ) -> ( e ^ 2 ) = ( ( i ` 7 ) ^ 2 ) )
117	116	oveq1d	|- ( e = ( i ` 7 ) -> ( ( e ^ 2 ) - 1 ) = ( ( ( i ` 7 ) ^ 2 ) - 1 ) )
118	117	oveq1d	|- ( e = ( i ` 7 ) -> ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) = ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) )
119	118	oveq2d	|- ( e = ( i ` 7 ) -> ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) )
120	119	eqeq1d	|- ( e = ( i ` 7 ) -> ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 <-> ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 ) )
121	120	3ad2ant3	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 <-> ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 ) )
122		eqeq1	|- ( c = ( i ` 5 ) -> ( c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) <-> ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) ) )
123	122	3ad2ant1	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) <-> ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) ) )
124		simp2	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> d = ( i ` 6 ) )
125		oveq1	|- ( e = ( i ` 7 ) -> ( e - ( a ` 1 ) ) = ( ( i ` 7 ) - ( a ` 1 ) ) )
126	125	3ad2ant3	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( e - ( a ` 1 ) ) = ( ( i ` 7 ) - ( a ` 1 ) ) )
127	124 126	breq12d	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( d || ( e - ( a ` 1 ) ) <-> ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) ) )
128	121 123 127	3anbi123d	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) <-> ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) ) ) )
129	115 128	anbi12d	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) <-> ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) ) ) ) )
130		oveq1	|- ( e = ( i ` 7 ) -> ( e - 1 ) = ( ( i ` 7 ) - 1 ) )
131	130	breq2d	|- ( e = ( i ` 7 ) -> ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) <-> ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) ) )
132		breq1	|- ( d = ( i ` 6 ) -> ( d || ( ( i ` 8 ) - ( a ` 3 ) ) <-> ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) )
133	131 132	bi2anan9r	|- ( ( d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) <-> ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) ) )
134	133	anbi1d	|- ( ( d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) <-> ( ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
135	134	3adant1	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) <-> ( ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
136	129 135	anbi12d	|- ( ( c = ( i ` 5 ) /\ d = ( i ` 6 ) /\ e = ( i ` 7 ) ) -> ( ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) )
137	103 104 105 136	sbc3ie	|- ( [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
138	137	sbcbii	|- ( [. ( i ` 4 ) / b ]. [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> [. ( i ` 4 ) / b ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
139	138	sbcbii	|- ( [. ( i |` ( 1 ... 3 ) ) / a ]. [. ( i ` 4 ) / b ]. [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ c = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> [. ( i |` ( 1 ... 3 ) ) / a ]. [. ( i ` 4 ) / b ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) )
140		vex	|- i e. _V
141	140	resex	|- ( i |` ( 1 ... 3 ) ) e. _V
142		fvex	|- ( i ` 4 ) e. _V
143		oveq1	|- ( b = ( i ` 4 ) -> ( b ^ 2 ) = ( ( i ` 4 ) ^ 2 ) )
144	62	jm2.27dlem1	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( a ` 1 ) = ( i ` 1 ) )
145	144	oveq1d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( a ` 1 ) ^ 2 ) = ( ( i ` 1 ) ^ 2 ) )
146	145	oveq1d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( ( a ` 1 ) ^ 2 ) - 1 ) = ( ( ( i ` 1 ) ^ 2 ) - 1 ) )
147	68	jm2.27dlem1	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( a ` 3 ) = ( i ` 3 ) )
148	147	oveq1d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( a ` 3 ) ^ 2 ) = ( ( i ` 3 ) ^ 2 ) )
149	146 148	oveq12d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) = ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) )
150	143 149	oveqan12rd	|- ( ( a = ( i |` ( 1 ... 3 ) ) /\ b = ( i ` 4 ) ) -> ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) )
151	150	eqeq1d	|- ( ( a = ( i |` ( 1 ... 3 ) ) /\ b = ( i ` 4 ) ) -> ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 <-> ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 ) )
152	146	oveq1d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) = ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) )
153	152	oveq2d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) )
154	153	eqeq1d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 <-> ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 ) )
155	154	adantr	|- ( ( a = ( i |` ( 1 ... 3 ) ) /\ b = ( i ` 4 ) ) -> ( ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 <-> ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 ) )
156	151 155	3anbi12d	|- ( ( a = ( i |` ( 1 ... 3 ) ) /\ b = ( i ` 4 ) ) -> ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) <-> ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) ) )
157	148	oveq2d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( 2 x. ( ( a ` 3 ) ^ 2 ) ) = ( 2 x. ( ( i ` 3 ) ^ 2 ) ) )
158	157	oveq2d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) )
159	158	eqeq2d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) <-> ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) ) )
160	144	oveq2d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( i ` 7 ) - ( a ` 1 ) ) = ( ( i ` 7 ) - ( i ` 1 ) ) )
161	160	breq2d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) <-> ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) )
162	159 161	3anbi23d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) ) <-> ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) ) )
163	162	adantr	|- ( ( a = ( i |` ( 1 ... 3 ) ) /\ b = ( i ` 4 ) ) -> ( ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) ) <-> ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) ) )
164	156 163	anbi12d	|- ( ( a = ( i |` ( 1 ... 3 ) ) /\ b = ( i ` 4 ) ) -> ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) ) ) <-> ( ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) ) ) )
165	147	oveq2d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( 2 x. ( a ` 3 ) ) = ( 2 x. ( i ` 3 ) ) )
166	165	breq1d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) <-> ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) ) )
167	147	oveq2d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( i ` 8 ) - ( a ` 3 ) ) = ( ( i ` 8 ) - ( i ` 3 ) ) )
168	167	breq2d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) <-> ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) )
169	166 168	anbi12d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) <-> ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) ) )
170	5	jm2.27dlem1	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( a ` 2 ) = ( i ` 2 ) )
171	170	oveq2d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( i ` 8 ) - ( a ` 2 ) ) = ( ( i ` 8 ) - ( i ` 2 ) ) )
172	165 171	breq12d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) <-> ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) ) )
173	170 147	breq12d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( a ` 2 ) <_ ( a ` 3 ) <-> ( i ` 2 ) <_ ( i ` 3 ) ) )
174	172 173	anbi12d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) <-> ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) ) )
175	169 174	anbi12d	|- ( a = ( i |` ( 1 ... 3 ) ) -> ( ( ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) <-> ( ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) /\ ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) ) ) )
176	175	adantr	|- ( ( a = ( i |` ( 1 ... 3 ) ) /\ b = ( i ` 4 ) ) -> ( ( ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) <-> ( ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) /\ ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) ) ) )
177	164 176	anbi12d	|- ( ( a = ( i |` ( 1 ... 3 ) ) /\ b = ( i ` 4 ) ) -> ( ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> ( ( ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) ) /\ ( ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) /\ ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) ) ) ) )
178	141 142 177	sbc2ie	|- ( [. ( i |` ( 1 ... 3 ) ) / a ]. [. ( i ` 4 ) / b ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( ( i ` 8 ) - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> ( ( ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) ) /\ ( ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) /\ ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) ) ) )
179	102 139 178	3bitri	|- ( [. ( i |` ( 1 ... 3 ) ) / a ]. [. ( i ` 4 ) / b ]. [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. [. ( i ` 8 ) / f ]. [. ( i ` 9 ) / g ]. [. ( i ` ; 1 0 ) / h ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) <-> ( ( ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) ) /\ ( ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) /\ ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) ) ) )
180	179	rabbii	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | [. ( i |` ( 1 ... 3 ) ) / a ]. [. ( i ` 4 ) / b ]. [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. [. ( i ` 8 ) / f ]. [. ( i ` 9 ) / g ]. [. ( i ` ; 1 0 ) / h ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) } = { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) ) /\ ( ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) /\ ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) ) ) }
181		10nn0	|- ; 1 0 e. NN0
182		ovex	|- ( 1 ... ; 1 0 ) e. _V
183		df-5	|- 5 = ( 4 + 1 )
184		df-6	|- 6 = ( 5 + 1 )
185		df-7	|- 7 = ( 6 + 1 )
186		df-8	|- 8 = ( 7 + 1 )
187		df-9	|- 9 = ( 8 + 1 )
188		9p1e10	|- ( 9 + 1 ) = ; 1 0
189	188	eqcomi	|- ; 1 0 = ( 9 + 1 )
190		ssid	|- ( 1 ... ; 1 0 ) C_ ( 1 ... ; 1 0 )
191	189 190	jm2.27dlem5	|- ( 1 ... 9 ) C_ ( 1 ... ; 1 0 )
192	187 191	jm2.27dlem5	|- ( 1 ... 8 ) C_ ( 1 ... ; 1 0 )
193	186 192	jm2.27dlem5	|- ( 1 ... 7 ) C_ ( 1 ... ; 1 0 )
194	185 193	jm2.27dlem5	|- ( 1 ... 6 ) C_ ( 1 ... ; 1 0 )
195	184 194	jm2.27dlem5	|- ( 1 ... 5 ) C_ ( 1 ... ; 1 0 )
196	183 195	jm2.27dlem5	|- ( 1 ... 4 ) C_ ( 1 ... ; 1 0 )
197		4nn	|- 4 e. NN
198	197	jm2.27dlem3	|- 4 e. ( 1 ... 4 )
199	196 198	sselii	|- 4 e. ( 1 ... ; 1 0 )
200		mzpproj	|- ( ( ( 1 ... ; 1 0 ) e. _V /\ 4 e. ( 1 ... ; 1 0 ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 4 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
201	182 199 200	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 4 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
202		2nn0	|- 2 e. NN0
203		mzpexpmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 4 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ 2 e. NN0 ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 4 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
204	201 202 203	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 4 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
205		df-4	|- 4 = ( 3 + 1 )
206	205 196	jm2.27dlem5	|- ( 1 ... 3 ) C_ ( 1 ... ; 1 0 )
207	4 206	jm2.27dlem5	|- ( 1 ... 2 ) C_ ( 1 ... ; 1 0 )
208	60 207	jm2.27dlem5	|- ( 1 ... 1 ) C_ ( 1 ... ; 1 0 )
209	208 59	sselii	|- 1 e. ( 1 ... ; 1 0 )
210		mzpproj	|- ( ( ( 1 ... ; 1 0 ) e. _V /\ 1 e. ( 1 ... ; 1 0 ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
211	182 209 210	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
212		mzpexpmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ 2 e. NN0 ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 1 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
213	211 202 212	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 1 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
214		1z	|- 1 e. ZZ
215		mzpconstmpt	|- ( ( ( 1 ... ; 1 0 ) e. _V /\ 1 e. ZZ ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
216	182 214 215	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
217		mzpsubmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 1 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 1 ) ^ 2 ) - 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
218	213 216 217	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 1 ) ^ 2 ) - 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
219	206 68	sselii	|- 3 e. ( 1 ... ; 1 0 )
220		mzpproj	|- ( ( ( 1 ... ; 1 0 ) e. _V /\ 3 e. ( 1 ... ; 1 0 ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 3 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
221	182 219 220	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 3 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
222		mzpexpmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 3 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ 2 e. NN0 ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 3 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
223	221 202 222	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 3 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
224		mzpmulmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 1 ) ^ 2 ) - 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 3 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
225	218 223 224	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
226		mzpsubmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 4 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
227	204 225 226	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
228		eqrabdioph	|- ( ( ; 1 0 e. NN0 /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 } e. ( Dioph ` ; 1 0 ) )
229	181 227 216 228	mp3an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 } e. ( Dioph ` ; 1 0 )
230		6nn	|- 6 e. NN
231	230	jm2.27dlem3	|- 6 e. ( 1 ... 6 )
232	194 231	sselii	|- 6 e. ( 1 ... ; 1 0 )
233		mzpproj	|- ( ( ( 1 ... ; 1 0 ) e. _V /\ 6 e. ( 1 ... ; 1 0 ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 6 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
234	182 232 233	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 6 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
235		mzpexpmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 6 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ 2 e. NN0 ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 6 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
236	234 202 235	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 6 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
237		5nn	|- 5 e. NN
238	237	jm2.27dlem3	|- 5 e. ( 1 ... 5 )
239	195 238	sselii	|- 5 e. ( 1 ... ; 1 0 )
240		mzpproj	|- ( ( ( 1 ... ; 1 0 ) e. _V /\ 5 e. ( 1 ... ; 1 0 ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 5 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
241	182 239 240	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 5 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
242		mzpexpmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 5 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ 2 e. NN0 ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 5 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
243	241 202 242	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 5 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
244		mzpmulmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 1 ) ^ 2 ) - 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 5 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
245	218 243 244	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
246		mzpsubmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 6 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
247	236 245 246	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
248		eqrabdioph	|- ( ( ; 1 0 e. NN0 /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 } e. ( Dioph ` ; 1 0 ) )
249	181 247 216 248	mp3an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 } e. ( Dioph ` ; 1 0 )
250		7nn	|- 7 e. NN
251	250	jm2.27dlem3	|- 7 e. ( 1 ... 7 )
252	193 251	sselii	|- 7 e. ( 1 ... ; 1 0 )
253		mzpproj	|- ( ( ( 1 ... ; 1 0 ) e. _V /\ 7 e. ( 1 ... ; 1 0 ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 7 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
254	182 252 253	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 7 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
255		eluzrabdioph	|- ( ( ; 1 0 e. NN0 /\ 2 e. ZZ /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 7 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 7 ) e. ( ZZ>= ` 2 ) } e. ( Dioph ` ; 1 0 ) )
256	181 56 254 255	mp3an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 7 ) e. ( ZZ>= ` 2 ) } e. ( Dioph ` ; 1 0 )
257		3anrabdioph	|- ( ( { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 } e. ( Dioph ` ; 1 0 ) /\ { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 } e. ( Dioph ` ; 1 0 ) /\ { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 7 ) e. ( ZZ>= ` 2 ) } e. ( Dioph ` ; 1 0 ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) } e. ( Dioph ` ; 1 0 ) )
258	229 249 256 257	mp3an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) } e. ( Dioph ` ; 1 0 )
259		9nn	|- 9 e. NN
260	259	jm2.27dlem3	|- 9 e. ( 1 ... 9 )
261	260 189 259	jm2.27dlem2	|- 9 e. ( 1 ... ; 1 0 )
262		mzpproj	|- ( ( ( 1 ... ; 1 0 ) e. _V /\ 9 e. ( 1 ... ; 1 0 ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 9 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
263	182 261 262	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 9 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
264		mzpexpmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 9 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ 2 e. NN0 ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 9 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
265	263 202 264	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 9 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
266		mzpexpmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 7 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ 2 e. NN0 ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 7 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
267	254 202 266	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 7 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
268		mzpsubmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 7 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 7 ) ^ 2 ) - 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
269	267 216 268	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 7 ) ^ 2 ) - 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
270		8nn	|- 8 e. NN
271	270	jm2.27dlem3	|- 8 e. ( 1 ... 8 )
272	192 271	sselii	|- 8 e. ( 1 ... ; 1 0 )
273		mzpproj	|- ( ( ( 1 ... ; 1 0 ) e. _V /\ 8 e. ( 1 ... ; 1 0 ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 8 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
274	182 272 273	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 8 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
275		mzpexpmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 8 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ 2 e. NN0 ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 8 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
276	274 202 275	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 8 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
277		mzpmulmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 7 ) ^ 2 ) - 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 8 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
278	269 276 277	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
279		mzpsubmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 9 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
280	265 278 279	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
281		eqrabdioph	|- ( ( ; 1 0 e. NN0 /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 } e. ( Dioph ` ; 1 0 ) )
282	181 280 216 281	mp3an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 } e. ( Dioph ` ; 1 0 )
283		10nn	|- ; 1 0 e. NN
284	283	jm2.27dlem3	|- ; 1 0 e. ( 1 ... ; 1 0 )
285		mzpproj	|- ( ( ( 1 ... ; 1 0 ) e. _V /\ ; 1 0 e. ( 1 ... ; 1 0 ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` ; 1 0 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
286	182 284 285	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` ; 1 0 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
287		mzpaddmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` ; 1 0 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` ; 1 0 ) + 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
288	286 216 287	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` ; 1 0 ) + 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
289		mzpconstmpt	|- ( ( ( 1 ... ; 1 0 ) e. _V /\ 2 e. ZZ ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 2 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
290	182 56 289	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 2 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
291		mzpmulmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 2 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 3 ) ^ 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
292	290 223 291	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
293		mzpmulmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` ; 1 0 ) + 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
294	288 292 293	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
295		eqrabdioph	|- ( ( ; 1 0 e. NN0 /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 5 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) } e. ( Dioph ` ; 1 0 ) )
296	181 241 294 295	mp3an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) } e. ( Dioph ` ; 1 0 )
297		mzpsubmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 7 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 7 ) - ( i ` 1 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
298	254 211 297	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 7 ) - ( i ` 1 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
299		dvdsrabdioph	|- ( ( ; 1 0 e. NN0 /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 6 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 7 ) - ( i ` 1 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) } e. ( Dioph ` ; 1 0 ) )
300	181 234 298 299	mp3an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) } e. ( Dioph ` ; 1 0 )
301		3anrabdioph	|- ( ( { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 } e. ( Dioph ` ; 1 0 ) /\ { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) } e. ( Dioph ` ; 1 0 ) /\ { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) } e. ( Dioph ` ; 1 0 ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) } e. ( Dioph ` ; 1 0 ) )
302	282 296 300 301	mp3an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) } e. ( Dioph ` ; 1 0 )
303		anrabdioph	|- ( ( { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) } e. ( Dioph ` ; 1 0 ) /\ { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) } e. ( Dioph ` ; 1 0 ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) ) } e. ( Dioph ` ; 1 0 ) )
304	258 302 303	mp2an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) ) } e. ( Dioph ` ; 1 0 )
305		mzpmulmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 2 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 3 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( 2 x. ( i ` 3 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
306	290 221 305	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( 2 x. ( i ` 3 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
307		mzpsubmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 7 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> 1 ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 7 ) - 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
308	254 216 307	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 7 ) - 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
309		dvdsrabdioph	|- ( ( ; 1 0 e. NN0 /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( 2 x. ( i ` 3 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 7 ) - 1 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) } e. ( Dioph ` ; 1 0 ) )
310	181 306 308 309	mp3an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) } e. ( Dioph ` ; 1 0 )
311		mzpsubmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 8 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 3 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 8 ) - ( i ` 3 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
312	274 221 311	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 8 ) - ( i ` 3 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
313		dvdsrabdioph	|- ( ( ; 1 0 e. NN0 /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 6 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 8 ) - ( i ` 3 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) } e. ( Dioph ` ; 1 0 ) )
314	181 234 312 313	mp3an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) } e. ( Dioph ` ; 1 0 )
315		anrabdioph	|- ( ( { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) } e. ( Dioph ` ; 1 0 ) /\ { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) } e. ( Dioph ` ; 1 0 ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) } e. ( Dioph ` ; 1 0 ) )
316	310 314 315	mp2an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) } e. ( Dioph ` ; 1 0 )
317	207 3	sselii	|- 2 e. ( 1 ... ; 1 0 )
318		mzpproj	|- ( ( ( 1 ... ; 1 0 ) e. _V /\ 2 e. ( 1 ... ; 1 0 ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
319	182 317 318	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
320		mzpsubmpt	|- ( ( ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 8 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 8 ) - ( i ` 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) )
321	274 319 320	mp2an	|- ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 8 ) - ( i ` 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) )
322		dvdsrabdioph	|- ( ( ; 1 0 e. NN0 /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( 2 x. ( i ` 3 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( ( i ` 8 ) - ( i ` 2 ) ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) } e. ( Dioph ` ; 1 0 ) )
323	181 306 321 322	mp3an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) } e. ( Dioph ` ; 1 0 )
324		lerabdioph	|- ( ( ; 1 0 e. NN0 /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 2 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) /\ ( i e. ( ZZ ^m ( 1 ... ; 1 0 ) ) |-> ( i ` 3 ) ) e. ( mzPoly ` ( 1 ... ; 1 0 ) ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 2 ) <_ ( i ` 3 ) } e. ( Dioph ` ; 1 0 ) )
325	181 319 221 324	mp3an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 2 ) <_ ( i ` 3 ) } e. ( Dioph ` ; 1 0 )
326		anrabdioph	|- ( ( { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) } e. ( Dioph ` ; 1 0 ) /\ { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( i ` 2 ) <_ ( i ` 3 ) } e. ( Dioph ` ; 1 0 ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) } e. ( Dioph ` ; 1 0 ) )
327	323 325 326	mp2an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) } e. ( Dioph ` ; 1 0 )
328		anrabdioph	|- ( ( { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) } e. ( Dioph ` ; 1 0 ) /\ { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) } e. ( Dioph ` ; 1 0 ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) /\ ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) ) } e. ( Dioph ` ; 1 0 ) )
329	316 327 328	mp2an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) /\ ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) ) } e. ( Dioph ` ; 1 0 )
330		anrabdioph	|- ( ( { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) ) } e. ( Dioph ` ; 1 0 ) /\ { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) /\ ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) ) } e. ( Dioph ` ; 1 0 ) ) -> { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) ) /\ ( ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) /\ ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) ) ) } e. ( Dioph ` ; 1 0 ) )
331	304 329 330	mp2an	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | ( ( ( ( ( ( i ` 4 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( ( i ` 6 ) ^ 2 ) - ( ( ( ( i ` 1 ) ^ 2 ) - 1 ) x. ( ( i ` 5 ) ^ 2 ) ) ) = 1 /\ ( i ` 7 ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( i ` 9 ) ^ 2 ) - ( ( ( ( i ` 7 ) ^ 2 ) - 1 ) x. ( ( i ` 8 ) ^ 2 ) ) ) = 1 /\ ( i ` 5 ) = ( ( ( i ` ; 1 0 ) + 1 ) x. ( 2 x. ( ( i ` 3 ) ^ 2 ) ) ) /\ ( i ` 6 ) || ( ( i ` 7 ) - ( i ` 1 ) ) ) ) /\ ( ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 7 ) - 1 ) /\ ( i ` 6 ) || ( ( i ` 8 ) - ( i ` 3 ) ) ) /\ ( ( 2 x. ( i ` 3 ) ) || ( ( i ` 8 ) - ( i ` 2 ) ) /\ ( i ` 2 ) <_ ( i ` 3 ) ) ) ) } e. ( Dioph ` ; 1 0 )
332	180 331	eqeltri	|- { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | [. ( i |` ( 1 ... 3 ) ) / a ]. [. ( i ` 4 ) / b ]. [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. [. ( i ` 8 ) / f ]. [. ( i ` 9 ) / g ]. [. ( i ` ; 1 0 ) / h ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) } e. ( Dioph ` ; 1 0 )
333	205 183 184 185 186 187 189	7rexfrabdioph	|- ( ( 3 e. NN0 /\ { i e. ( NN0 ^m ( 1 ... ; 1 0 ) ) | [. ( i |` ( 1 ... 3 ) ) / a ]. [. ( i ` 4 ) / b ]. [. ( i ` 5 ) / c ]. [. ( i ` 6 ) / d ]. [. ( i ` 7 ) / e ]. [. ( i ` 8 ) / f ]. [. ( i ` 9 ) / g ]. [. ( i ` ; 1 0 ) / h ]. ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) } e. ( Dioph ` ; 1 0 ) ) -> { a e. ( NN0 ^m ( 1 ... 3 ) ) | E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) } e. ( Dioph ` 3 ) )
334	55 332 333	mp2an	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) } e. ( Dioph ` 3 )
335		anrabdioph	|- ( ( { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 3 ) e. NN } e. ( Dioph ` 3 ) /\ { a e. ( NN0 ^m ( 1 ... 3 ) ) | E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) } e. ( Dioph ` 3 ) ) -> { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) } e. ( Dioph ` 3 ) )
336	72 334 335	mp2an	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) } e. ( Dioph ` 3 )
337		mzpproj	|- ( ( ( 1 ... 3 ) e. _V /\ 2 e. ( 1 ... 3 ) ) -> ( a e. ( ZZ ^m ( 1 ... 3 ) ) |-> ( a ` 2 ) ) e. ( mzPoly ` ( 1 ... 3 ) ) )
338	57 5 337	mp2an	|- ( a e. ( ZZ ^m ( 1 ... 3 ) ) |-> ( a ` 2 ) ) e. ( mzPoly ` ( 1 ... 3 ) )
339		elnnrabdioph	|- ( ( 3 e. NN0 /\ ( a e. ( ZZ ^m ( 1 ... 3 ) ) |-> ( a ` 2 ) ) e. ( mzPoly ` ( 1 ... 3 ) ) ) -> { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 2 ) e. NN } e. ( Dioph ` 3 ) )
340	55 338 339	mp2an	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 2 ) e. NN } e. ( Dioph ` 3 )
341		anrabdioph	|- ( ( { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) } e. ( Dioph ` 3 ) /\ { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 2 ) e. NN } e. ( Dioph ` 3 ) ) -> { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) } e. ( Dioph ` 3 ) )
342	336 340 341	mp2an	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) } e. ( Dioph ` 3 )
343		eq0rabdioph	|- ( ( 3 e. NN0 /\ ( a e. ( ZZ ^m ( 1 ... 3 ) ) |-> ( a ` 3 ) ) e. ( mzPoly ` ( 1 ... 3 ) ) ) -> { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 3 ) = 0 } e. ( Dioph ` 3 ) )
344	55 70 343	mp2an	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 3 ) = 0 } e. ( Dioph ` 3 )
345		eq0rabdioph	|- ( ( 3 e. NN0 /\ ( a e. ( ZZ ^m ( 1 ... 3 ) ) |-> ( a ` 2 ) ) e. ( mzPoly ` ( 1 ... 3 ) ) ) -> { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 2 ) = 0 } e. ( Dioph ` 3 ) )
346	55 338 345	mp2an	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 2 ) = 0 } e. ( Dioph ` 3 )
347		anrabdioph	|- ( ( { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 3 ) = 0 } e. ( Dioph ` 3 ) /\ { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 2 ) = 0 } e. ( Dioph ` 3 ) ) -> { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) } e. ( Dioph ` 3 ) )
348	344 346 347	mp2an	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) } e. ( Dioph ` 3 )
349		orrabdioph	|- ( ( { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) } e. ( Dioph ` 3 ) /\ { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) } e. ( Dioph ` 3 ) ) -> { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) ) } e. ( Dioph ` 3 ) )
350	342 348 349	mp2an	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) ) } e. ( Dioph ` 3 )
351		anrabdioph	|- ( ( { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 1 ) e. ( ZZ>= ` 2 ) } e. ( Dioph ` 3 ) /\ { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) ) } e. ( Dioph ` 3 ) ) -> { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) ) ) } e. ( Dioph ` 3 ) )
352	66 350 351	mp2an	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( ( ( ( a ` 3 ) e. NN /\ E. b e. NN0 E. c e. NN0 E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 ( ( ( ( ( b ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( ( a ` 3 ) ^ 2 ) ) ) = 1 /\ ( ( d ^ 2 ) - ( ( ( ( a ` 1 ) ^ 2 ) - 1 ) x. ( c ^ 2 ) ) ) = 1 /\ e e. ( ZZ>= ` 2 ) ) /\ ( ( ( g ^ 2 ) - ( ( ( e ^ 2 ) - 1 ) x. ( f ^ 2 ) ) ) = 1 /\ c = ( ( h + 1 ) x. ( 2 x. ( ( a ` 3 ) ^ 2 ) ) ) /\ d || ( e - ( a ` 1 ) ) ) ) /\ ( ( ( 2 x. ( a ` 3 ) ) || ( e - 1 ) /\ d || ( f - ( a ` 3 ) ) ) /\ ( ( 2 x. ( a ` 3 ) ) || ( f - ( a ` 2 ) ) /\ ( a ` 2 ) <_ ( a ` 3 ) ) ) ) ) /\ ( a ` 2 ) e. NN ) \/ ( ( a ` 3 ) = 0 /\ ( a ` 2 ) = 0 ) ) ) } e. ( Dioph ` 3 )
353	54 352	eqeltri	|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) rmY ( a ` 2 ) ) ) } e. ( Dioph ` 3 )