Theorem lgsquadlem3 15743

Description: Lemma for lgsquad 15744. (Contributed by Mario Carneiro, 18-Jun-2015.)

Hypotheses

Ref	Expression
lgseisen.1	|- ( ph -> P e. ( Prime \ { 2 } ) )
lgseisen.2	|- ( ph -> Q e. ( Prime \ { 2 } ) )
lgseisen.3	|- ( ph -> P =/= Q )
lgsquad.4	|- M = ( ( P - 1 ) / 2 )
lgsquad.5	|- N = ( ( Q - 1 ) / 2 )
lgsquad.6	|- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }

Assertion

Ref	Expression
lgsquadlem3	|- ( ph -> ( ( P /L Q ) x. ( Q /L P ) ) = ( -u 1 ^ ( M x. N ) ) )

Distinct variable groups:   x, y, P   ph, x, y   y, M   x, N, y   x, Q, y   x, S   x, M   y, S

Proof of Theorem lgsquadlem3

Dummy variables w z j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lgseisen.2	. . . . 5 |- ( ph -> Q e. ( Prime \ { 2 } ) )
2		lgseisen.1	. . . . 5 |- ( ph -> P e. ( Prime \ { 2 } ) )
3		lgseisen.3	. . . . . 6 |- ( ph -> P =/= Q )
4	3	necomd 2486	. . . . 5 |- ( ph -> Q =/= P )
5		lgsquad.5	. . . . 5 |- N = ( ( Q - 1 ) / 2 )
6		lgsquad.4	. . . . 5 |- M = ( ( P - 1 ) / 2 )
7		eleq1w 2290	. . . . . . . . . 10 |- ( x = z -> ( x e. ( 1 ... M ) <-> z e. ( 1 ... M ) ) )
8		eleq1w 2290	. . . . . . . . . 10 |- ( y = w -> ( y e. ( 1 ... N ) <-> w e. ( 1 ... N ) ) )
9	7, 8	bi2anan9 608	. . . . . . . . 9 |- ( ( x = z /\ y = w ) -> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) <-> ( z e. ( 1 ... M ) /\ w e. ( 1 ... N ) ) ) )
10	9	biancomd 271	. . . . . . . 8 |- ( ( x = z /\ y = w ) -> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) <-> ( w e. ( 1 ... N ) /\ z e. ( 1 ... M ) ) ) )
11		oveq1 6001	. . . . . . . . 9 |- ( x = z -> ( x x. Q ) = ( z x. Q ) )
12		oveq1 6001	. . . . . . . . 9 |- ( y = w -> ( y x. P ) = ( w x. P ) )
13	11, 12	breqan12d 4098	. . . . . . . 8 |- ( ( x = z /\ y = w ) -> ( ( x x. Q ) < ( y x. P ) <-> ( z x. Q ) < ( w x. P ) ) )
14	10, 13	anbi12d 473	. . . . . . 7 |- ( ( x = z /\ y = w ) -> ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) <-> ( ( w e. ( 1 ... N ) /\ z e. ( 1 ... M ) ) /\ ( z x. Q ) < ( w x. P ) ) ) )
15	14	ancoms 268	. . . . . 6 |- ( ( y = w /\ x = z ) -> ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) <-> ( ( w e. ( 1 ... N ) /\ z e. ( 1 ... M ) ) /\ ( z x. Q ) < ( w x. P ) ) ) )
16	15	cbvopabv 4155	. . . . 5 |- { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } = { <. w , z >. | ( ( w e. ( 1 ... N ) /\ z e. ( 1 ... M ) ) /\ ( z x. Q ) < ( w x. P ) ) }
17	1, 2, 4, 5, 6, 16	lgsquadlem2 15742	. . . 4 |- ( ph -> ( P /L Q ) = ( -u 1 ^ (♯ ` { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) ) )
18		relopabv 4843	. . . . . . . 8 |- Rel { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) }
19		eqid 2229	. . . . . . . . 9 |- { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) }
20		1zzd 9461	. . . . . . . . . 10 |- ( ph -> 1 e. ZZ )
21	2, 6	gausslemma2dlem0b 15714	. . . . . . . . . . 11 |- ( ph -> M e. NN )
22	21	nnzd 9556	. . . . . . . . . 10 |- ( ph -> M e. ZZ )
23	20, 22	fzfigd 10640	. . . . . . . . 9 |- ( ph -> ( 1 ... M ) e. Fin )
24	1, 5	gausslemma2dlem0b 15714	. . . . . . . . . . 11 |- ( ph -> N e. NN )
25	24	nnzd 9556	. . . . . . . . . 10 |- ( ph -> N e. ZZ )
26	20, 25	fzfigd 10640	. . . . . . . . 9 |- ( ph -> ( 1 ... N ) e. Fin )
27		elfznn 10238	. . . . . . . . . . . . . 14 |- ( x e. ( 1 ... M ) -> x e. NN )
28	27	ad2antrl 490	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> x e. NN )
29	1	eldifad 3208	. . . . . . . . . . . . . . 15 |- ( ph -> Q e. Prime )
30	29	adantr 276	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q e. Prime )
31		prmnn 12618	. . . . . . . . . . . . . 14 |- ( Q e. Prime -> Q e. NN )
32	30, 31	syl 14	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q e. NN )
33	28, 32	nnmulcld 9147	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. NN )
34	33	nnzd 9556	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. ZZ )
35		elfznn 10238	. . . . . . . . . . . . . 14 |- ( y e. ( 1 ... N ) -> y e. NN )
36	35	ad2antll 491	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. NN )
37	2	gausslemma2dlem0a 15713	. . . . . . . . . . . . . 14 |- ( ph -> P e. NN )
38	37	adantr 276	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. NN )
39	36, 38	nnmulcld 9147	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. NN )
40	39	nnzd 9556	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. ZZ )
41		zdclt 9512	. . . . . . . . . . 11 |- ( ( ( x x. Q ) e. ZZ /\ ( y x. P ) e. ZZ ) -> DECID ( x x. Q ) < ( y x. P ) )
42	34, 40, 41	syl2anc 411	. . . . . . . . . 10 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> DECID ( x x. Q ) < ( y x. P ) )
43	42	ralrimivva 2612	. . . . . . . . 9 |- ( ph -> A. x e. ( 1 ... M ) A. y e. ( 1 ... N )DECID ( x x. Q ) < ( y x. P ) )
44	19, 23, 26, 43	opabfi 7088	. . . . . . . 8 |- ( ph -> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin )
45		cnven 6951	. . . . . . . 8 |- ( ( Rel { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } /\ { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin ) -> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ~~ `' { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } )
46	18, 44, 45	sylancr 414	. . . . . . 7 |- ( ph -> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ~~ `' { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } )
47		cnvopab 5126	. . . . . . 7 |- `' { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } = { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) }
48	46, 47	breqtrdi 4123	. . . . . 6 |- ( ph -> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ~~ { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } )
49	1, 2, 4, 5, 6, 16	lgsquadlemsfi 15739	. . . . . . 7 |- ( ph -> { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin )
50		hashen 10993	. . . . . . 7 |- ( ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin /\ { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin ) -> ( (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) = (♯ ` { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) <-> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ~~ { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) )
51	44, 49, 50	syl2anc 411	. . . . . 6 |- ( ph -> ( (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) = (♯ ` { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) <-> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ~~ { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) )
52	48, 51	mpbird 167	. . . . 5 |- ( ph -> (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) = (♯ ` { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) )
53	52	oveq2d 6010	. . . 4 |- ( ph -> ( -u 1 ^ (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) ) = ( -u 1 ^ (♯ ` { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) ) )
54	17, 53	eqtr4d 2265	. . 3 |- ( ph -> ( P /L Q ) = ( -u 1 ^ (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) ) )
55		lgsquad.6	. . . 4 |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }
56	2, 1, 3, 6, 5, 55	lgsquadlem2 15742	. . 3 |- ( ph -> ( Q /L P ) = ( -u 1 ^ (♯ ` S ) ) )
57	54, 56	oveq12d 6012	. 2 |- ( ph -> ( ( P /L Q ) x. ( Q /L P ) ) = ( ( -u 1 ^ (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) ) x. ( -u 1 ^ (♯ ` S ) ) ) )
58		neg1cn 9203	. . . 4 |- -u 1 e. CC
59	58	a1i 9	. . 3 |- ( ph -> -u 1 e. CC )
60	2, 1, 3, 6, 5, 55	lgsquadlemsfi 15739	. . . 4 |- ( ph -> S e. Fin )
61		hashcl 10990	. . . 4 |- ( S e. Fin -> (♯ ` S ) e. NN0 )
62	60, 61	syl 14	. . 3 |- ( ph -> (♯ ` S ) e. NN0 )
63		hashcl 10990	. . . 4 |- ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin -> (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) e. NN0 )
64	44, 63	syl 14	. . 3 |- ( ph -> (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) e. NN0 )
65	59, 62, 64	expaddd 10884	. 2 |- ( ph -> ( -u 1 ^ ( (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) + (♯ ` S ) ) ) = ( ( -u 1 ^ (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) ) x. ( -u 1 ^ (♯ ` S ) ) ) )
66	24	adantr 276	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. NN )
67	66	nnzd 9556	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. ZZ )
68		prmz 12619	. . . . . . . . . . . . . . . . . . . 20 |- ( Q e. Prime -> Q e. ZZ )
69	30, 68	syl 14	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q e. ZZ )
70		peano2zm 9472	. . . . . . . . . . . . . . . . . . 19 |- ( Q e. ZZ -> ( Q - 1 ) e. ZZ )
71	69, 70	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. ZZ )
72	66	nnred 9111	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. RR )
73	71	zred 9557	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. RR )
74		prmuz2 12639	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( Q e. Prime -> Q e. ( ZZ>= ` 2 ) )
75	30, 74	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q e. ( ZZ>= ` 2 ) )
76		uz2m1nn 9788	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( Q e. ( ZZ>= ` 2 ) -> ( Q - 1 ) e. NN )
77	75, 76	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. NN )
78	77	nnrpd 9878	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. RR+ )
79		rphalflt 9867	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( Q - 1 ) e. RR+ -> ( ( Q - 1 ) / 2 ) < ( Q - 1 ) )
80	78, 79	syl 14	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( ( Q - 1 ) / 2 ) < ( Q - 1 ) )
81	5, 80	eqbrtrid 4117	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N < ( Q - 1 ) )
82	72, 73, 81	ltled 8253	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N <_ ( Q - 1 ) )
83		eluz2 9716	. . . . . . . . . . . . . . . . . 18 |- ( ( Q - 1 ) e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ ( Q - 1 ) e. ZZ /\ N <_ ( Q - 1 ) ) )
84	67, 71, 82, 83	syl3anbrc 1205	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. ( ZZ>= ` N ) )
85		fzss2 10248	. . . . . . . . . . . . . . . . 17 |- ( ( Q - 1 ) e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... ( Q - 1 ) ) )
86	84, 85	syl 14	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( 1 ... N ) C_ ( 1 ... ( Q - 1 ) ) )
87		simprr 531	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. ( 1 ... N ) )
88	86, 87	sseldd 3225	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. ( 1 ... ( Q - 1 ) ) )
89		fzm1ndvds 12353	. . . . . . . . . . . . . . 15 |- ( ( Q e. NN /\ y e. ( 1 ... ( Q - 1 ) ) ) -> -. Q || y )
90	32, 88, 89	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. Q || y )
91	4	adantr 276	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q =/= P )
92	2	eldifad 3208	. . . . . . . . . . . . . . . . . 18 |- ( ph -> P e. Prime )
93	92	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. Prime )
94		prmrp 12653	. . . . . . . . . . . . . . . . 17 |- ( ( Q e. Prime /\ P e. Prime ) -> ( ( Q gcd P ) = 1 <-> Q =/= P ) )
95	30, 93, 94	syl2anc 411	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( ( Q gcd P ) = 1 <-> Q =/= P ) )
96	91, 95	mpbird 167	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q gcd P ) = 1 )
97		prmz 12619	. . . . . . . . . . . . . . . . 17 |- ( P e. Prime -> P e. ZZ )
98	93, 97	syl 14	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. ZZ )
99		elfzelz 10209	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 1 ... N ) -> y e. ZZ )
100	99	ad2antll 491	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. ZZ )
101		coprmdvds 12600	. . . . . . . . . . . . . . . 16 |- ( ( Q e. ZZ /\ P e. ZZ /\ y e. ZZ ) -> ( ( Q || ( P x. y ) /\ ( Q gcd P ) = 1 ) -> Q || y ) )
102	69, 98, 100, 101	syl3anc 1271	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( ( Q || ( P x. y ) /\ ( Q gcd P ) = 1 ) -> Q || y ) )
103	96, 102	mpan2d 428	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q || ( P x. y ) -> Q || y ) )
104	90, 103	mtod 667	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. Q || ( P x. y ) )
105	38	nncnd 9112	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. CC )
106	36	nncnd 9112	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. CC )
107	105, 106	mulcomd 8156	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( P x. y ) = ( y x. P ) )
108	107	breq2d 4094	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q || ( P x. y ) <-> Q || ( y x. P ) ) )
109	104, 108	mtbid 676	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. Q || ( y x. P ) )
110		elfzelz 10209	. . . . . . . . . . . . . . . 16 |- ( x e. ( 1 ... M ) -> x e. ZZ )
111	110	ad2antrl 490	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> x e. ZZ )
112		dvdsmul2 12311	. . . . . . . . . . . . . . 15 |- ( ( x e. ZZ /\ Q e. ZZ ) -> Q || ( x x. Q ) )
113	111, 69, 112	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q || ( x x. Q ) )
114		breq2 4086	. . . . . . . . . . . . . 14 |- ( ( x x. Q ) = ( y x. P ) -> ( Q || ( x x. Q ) <-> Q || ( y x. P ) ) )
115	113, 114	syl5ibcom 155	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( ( x x. Q ) = ( y x. P ) -> Q || ( y x. P ) ) )
116	115	necon3bd 2443	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( -. Q || ( y x. P ) -> ( x x. Q ) =/= ( y x. P ) ) )
117	109, 116	mpd 13	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) =/= ( y x. P ) )
118		nnq 9816	. . . . . . . . . . . . 13 |- ( ( x x. Q ) e. NN -> ( x x. Q ) e. QQ )
119	33, 118	syl 14	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. QQ )
120		nnq 9816	. . . . . . . . . . . . 13 |- ( ( y x. P ) e. NN -> ( y x. P ) e. QQ )
121	39, 120	syl 14	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. QQ )
122		qlttri2 9824	. . . . . . . . . . . 12 |- ( ( ( x x. Q ) e. QQ /\ ( y x. P ) e. QQ ) -> ( ( x x. Q ) =/= ( y x. P ) <-> ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) ) )
123	119, 121, 122	syl2anc 411	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( ( x x. Q ) =/= ( y x. P ) <-> ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) ) )
124	117, 123	mpbid 147	. . . . . . . . . 10 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) )
125	124	ex 115	. . . . . . . . 9 |- ( ph -> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) -> ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) ) )
126	125	pm4.71rd 394	. . . . . . . 8 |- ( ph -> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) <-> ( ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) ) )
127		ancom 266	. . . . . . . 8 |- ( ( ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) <-> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) ) )
128	126, 127	bitr2di 197	. . . . . . 7 |- ( ph -> ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) ) <-> ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) )
129	128	opabbidv 4149	. . . . . 6 |- ( ph -> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) ) } = { <. x , y >. | ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) } )
130		unopab 4162	. . . . . . 7 |- ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } u. { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } ) = { <. x , y >. | ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) \/ ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) ) }
131	55	uneq2i 3355	. . . . . . 7 |- ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } u. S ) = ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } u. { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } )
132		andi 823	. . . . . . . 8 |- ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) ) <-> ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) \/ ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) ) )
133	132	opabbii 4150	. . . . . . 7 |- { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) ) } = { <. x , y >. | ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) \/ ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) ) }
134	130, 131, 133	3eqtr4i 2260	. . . . . 6 |- ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } u. S ) = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) ) }
135		df-xp 4722	. . . . . 6 |- ( ( 1 ... M ) X. ( 1 ... N ) ) = { <. x , y >. | ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) }
136	129, 134, 135	3eqtr4g 2287	. . . . 5 |- ( ph -> ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } u. S ) = ( ( 1 ... M ) X. ( 1 ... N ) ) )
137	136	fveq2d 5627	. . . 4 |- ( ph -> (♯ ` ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } u. S ) ) = (♯ ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) )
138		inopab 4851	. . . . . . 7 |- ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } i^i { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } ) = { <. x , y >. | ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) /\ ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) ) }
139	55	ineq2i 3402	. . . . . . 7 |- ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } i^i S ) = ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } i^i { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } )
140		anandi 592	. . . . . . . 8 |- ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) <-> ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) /\ ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) ) )
141	140	opabbii 4150	. . . . . . 7 |- { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) } = { <. x , y >. | ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) /\ ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) ) }
142	138, 139, 141	3eqtr4i 2260	. . . . . 6 |- ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } i^i S ) = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) }
143	33	nnred 9111	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. RR )
144	39	nnred 9111	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. RR )
145		ltnsym2 8225	. . . . . . . . . . . . 13 |- ( ( ( x x. Q ) e. RR /\ ( y x. P ) e. RR ) -> -. ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) )
146	143, 144, 145	syl2anc 411	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) )
147	146	ex 115	. . . . . . . . . . 11 |- ( ph -> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) -> -. ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) )
148		imnan 694	. . . . . . . . . . 11 |- ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) -> -. ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) <-> -. ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) )
149	147, 148	sylib 122	. . . . . . . . . 10 |- ( ph -> -. ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) )
150	149	nexdv 1987	. . . . . . . . 9 |- ( ph -> -. E. y ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) )
151	150	nexdv 1987	. . . . . . . 8 |- ( ph -> -. E. x E. y ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) )
152		opabm 4368	. . . . . . . 8 |- ( E. j j e. { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) } <-> E. x E. y ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) )
153	151, 152	sylnibr 681	. . . . . . 7 |- ( ph -> -. E. j j e. { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) } )
154		notm0 3512	. . . . . . 7 |- ( -. E. j j e. { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) } <-> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) } = (/) )
155	153, 154	sylib 122	. . . . . 6 |- ( ph -> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) } = (/) )
156	142, 155	eqtrid 2274	. . . . 5 |- ( ph -> ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } i^i S ) = (/) )
157		hashun 11014	. . . . 5 |- ( ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin /\ S e. Fin /\ ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } i^i S ) = (/) ) -> (♯ ` ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } u. S ) ) = ( (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) + (♯ ` S ) ) )
158	44, 60, 156, 157	syl3anc 1271	. . . 4 |- ( ph -> (♯ ` ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } u. S ) ) = ( (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) + (♯ ` S ) ) )
159		hashxp 11035	. . . . . 6 |- ( ( ( 1 ... M ) e. Fin /\ ( 1 ... N ) e. Fin ) -> (♯ ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) = ( (♯ ` ( 1 ... M ) ) x. (♯ ` ( 1 ... N ) ) ) )
160	23, 26, 159	syl2anc 411	. . . . 5 |- ( ph -> (♯ ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) = ( (♯ ` ( 1 ... M ) ) x. (♯ ` ( 1 ... N ) ) ) )
161	21	nnnn0d 9410	. . . . . . 7 |- ( ph -> M e. NN0 )
162		hashfz1 10992	. . . . . . 7 |- ( M e. NN0 -> (♯ ` ( 1 ... M ) ) = M )
163	161, 162	syl 14	. . . . . 6 |- ( ph -> (♯ ` ( 1 ... M ) ) = M )
164	24	nnnn0d 9410	. . . . . . 7 |- ( ph -> N e. NN0 )
165		hashfz1 10992	. . . . . . 7 |- ( N e. NN0 -> (♯ ` ( 1 ... N ) ) = N )
166	164, 165	syl 14	. . . . . 6 |- ( ph -> (♯ ` ( 1 ... N ) ) = N )
167	163, 166	oveq12d 6012	. . . . 5 |- ( ph -> ( (♯ ` ( 1 ... M ) ) x. (♯ ` ( 1 ... N ) ) ) = ( M x. N ) )
168	160, 167	eqtrd 2262	. . . 4 |- ( ph -> (♯ ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) = ( M x. N ) )
169	137, 158, 168	3eqtr3d 2270	. . 3 |- ( ph -> ( (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) + (♯ ` S ) ) = ( M x. N ) )
170	169	oveq2d 6010	. 2 |- ( ph -> ( -u 1 ^ ( (♯ ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) + (♯ ` S ) ) ) = ( -u 1 ^ ( M x. N ) ) )
171	57, 65, 170	3eqtr2d 2268	1 |- ( ph -> ( ( P /L Q ) x. ( Q /L P ) ) = ( -u 1 ^ ( M x. N ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 713  DECID wdc 839   = wceq 1395   E.wex 1538   e. wcel 2200   =/= wne 2400   \ cdif 3194   u. cun 3195   i^i cin 3196   C_ wss 3197   (/)c0 3491   {csn 3666   class class class wbr 4082   {copab 4143   X. cxp 4714   `'ccnv 4715   Rel wrel 4721   ` cfv 5314  (class class class)co 5994   ~~ cen 6875   Fincfn 6877   CCcc 7985   RRcr 7986   1c1 7988   + caddc 7990   x. cmul 7992   < clt 8169   <_ cle 8170   - cmin 8305   -ucneg 8306   / cdiv 8807   NNcn 9098   2c2 9149   NN0cn0 9357   ZZcz 9434   ZZ>=cuz 9710   QQcq 9802   RR+crp 9837   ...cfz 10192   ^cexp 10747  ♯chash 10984   || cdvds 12284   gcd cgcd 12460   Primecprime 12615   /Lclgs 15661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4198  ax-sep 4201  ax-nul 4209  ax-pow 4257  ax-pr 4292  ax-un 4521  ax-setind 4626  ax-iinf 4677  ax-cnex 8078  ax-resscn 8079  ax-1cn 8080  ax-1re 8081  ax-icn 8082  ax-addcl 8083  ax-addrcl 8084  ax-mulcl 8085  ax-mulrcl 8086  ax-addcom 8087  ax-mulcom 8088  ax-addass 8089  ax-mulass 8090  ax-distr 8091  ax-i2m1 8092  ax-0lt1 8093  ax-1rid 8094  ax-0id 8095  ax-rnegex 8096  ax-precex 8097  ax-cnre 8098  ax-pre-ltirr 8099  ax-pre-ltwlin 8100  ax-pre-lttrn 8101  ax-pre-apti 8102  ax-pre-ltadd 8103  ax-pre-mulgt0 8104  ax-pre-mulext 8105  ax-arch 8106  ax-caucvg 8107  ax-addf 8109  ax-mulf 8110

This theorem depends on definitions:  df-bi 117  df-stab 836  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-xor 1418  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rmo 2516  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-if 3603  df-pw 3651  df-sn 3672  df-pr 3673  df-tp 3674  df-op 3675  df-uni 3888  df-int 3923  df-iun 3966  df-disj 4059  df-br 4083  df-opab 4145  df-mpt 4146  df-tr 4182  df-id 4381  df-po 4384  df-iso 4385  df-iord 4454  df-on 4456  df-ilim 4457  df-suc 4459  df-iom 4680  df-xp 4722  df-rel 4723  df-cnv 4724  df-co 4725  df-dm 4726  df-rn 4727  df-res 4728  df-ima 4729  df-iota 5274  df-fun 5316  df-fn 5317  df-f 5318  df-f1 5319  df-fo 5320  df-f1o 5321  df-fv 5322  df-isom 5323  df-riota 5947  df-ov 5997  df-oprab 5998  df-mpo 5999  df-of 6208  df-1st 6276  df-2nd 6277  df-tpos 6381  df-recs 6441  df-irdg 6506  df-frec 6527  df-1o 6552  df-2o 6553  df-oadd 6556  df-er 6670  df-ec 6672  df-qs 6676  df-map 6787  df-en 6878  df-dom 6879  df-fin 6880  df-sup 7139  df-inf 7140  df-pnf 8171  df-mnf 8172  df-xr 8173  df-ltxr 8174  df-le 8175  df-sub 8307  df-neg 8308  df-reap 8710  df-ap 8717  df-div 8808  df-inn 9099  df-2 9157  df-3 9158  df-4 9159  df-5 9160  df-6 9161  df-7 9162  df-8 9163  df-9 9164  df-n0 9358  df-z 9435  df-dec 9567  df-uz 9711  df-q 9803  df-rp 9838  df-fz 10193  df-fzo 10327  df-fl 10477  df-mod 10532  df-seqfrec 10657  df-exp 10748  df-ihash 10985  df-cj 11339  df-re 11340  df-im 11341  df-rsqrt 11495  df-abs 11496  df-clim 11776  df-sumdc 11851  df-proddc 12048  df-dvds 12285  df-gcd 12461  df-prm 12616  df-phi 12719  df-pc 12794  df-struct 13020  df-ndx 13021  df-slot 13022  df-base 13024  df-sets 13025  df-iress 13026  df-plusg 13109  df-mulr 13110  df-starv 13111  df-sca 13112  df-vsca 13113  df-ip 13114  df-tset 13115  df-ple 13116  df-ds 13118  df-unif 13119  df-0g 13277  df-igsum 13278  df-topgen 13279  df-iimas 13321  df-qus 13322  df-mgm 13375  df-sgrp 13421  df-mnd 13436  df-mhm 13478  df-submnd 13479  df-grp 13522  df-minusg 13523  df-sbg 13524  df-mulg 13643  df-subg 13693  df-nsg 13694  df-eqg 13695  df-ghm 13764  df-cmn 13809  df-abl 13810  df-mgp 13870  df-rng 13882  df-ur 13909  df-srg 13913  df-ring 13947  df-cring 13948  df-oppr 14017  df-dvdsr 14038  df-unit 14039  df-invr 14070  df-dvr 14081  df-rhm 14101  df-nzr 14129  df-subrg 14168  df-domn 14208  df-idom 14209  df-lmod 14238  df-lssm 14302  df-lsp 14336  df-sra 14384  df-rgmod 14385  df-lidl 14418  df-rsp 14419  df-2idl 14449  df-bl 14495  df-mopn 14496  df-fg 14498  df-metu 14499  df-cnfld 14506  df-zring 14540  df-zrh 14563  df-zn 14565  df-lgs 15662

This theorem is referenced by:  lgsquad  15744