Theorem lgsquadlem3 15406

Description: Lemma for lgsquad 15407. (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 2453	. . . . 5 |- ( ph -> Q =/= P )
5		lgsquad.5	. . . . 5 |- N = ( ( Q - 1 ) / 2 )
6		lgsquad.4	. . . . 5 |- M = ( ( P - 1 ) / 2 )
7		eleq1w 2257	. . . . . . . . . 10 |- ( x = z -> ( x e. ( 1 ... M ) <-> z e. ( 1 ... M ) ) )
8		eleq1w 2257	. . . . . . . . . 10 |- ( y = w -> ( y e. ( 1 ... N ) <-> w e. ( 1 ... N ) ) )
9	7, 8	bi2anan9 606	. . . . . . . . 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 5932	. . . . . . . . 9 |- ( x = z -> ( x x. Q ) = ( z x. Q ) )
12		oveq1 5932	. . . . . . . . 9 |- ( y = w -> ( y x. P ) = ( w x. P ) )
13	11, 12	breqan12d 4050	. . . . . . . 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 4106	. . . . 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 15405	. . . 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 4791	. . . . . . . 8 |- Rel { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) }
19		eqid 2196	. . . . . . . . 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 9372	. . . . . . . . . 10 |- ( ph -> 1 e. ZZ )
21	2, 6	gausslemma2dlem0b 15377	. . . . . . . . . . 11 |- ( ph -> M e. NN )
22	21	nnzd 9466	. . . . . . . . . 10 |- ( ph -> M e. ZZ )
23	20, 22	fzfigd 10542	. . . . . . . . 9 |- ( ph -> ( 1 ... M ) e. Fin )
24	1, 5	gausslemma2dlem0b 15377	. . . . . . . . . . 11 |- ( ph -> N e. NN )
25	24	nnzd 9466	. . . . . . . . . 10 |- ( ph -> N e. ZZ )
26	20, 25	fzfigd 10542	. . . . . . . . 9 |- ( ph -> ( 1 ... N ) e. Fin )
27		elfznn 10148	. . . . . . . . . . . . . 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 3168	. . . . . . . . . . . . . . 15 |- ( ph -> Q e. Prime )
30	29	adantr 276	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q e. Prime )
31		prmnn 12305	. . . . . . . . . . . . . 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 9058	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. NN )
34	33	nnzd 9466	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. ZZ )
35		elfznn 10148	. . . . . . . . . . . . . 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 15376	. . . . . . . . . . . . . 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 9058	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. NN )
40	39	nnzd 9466	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. ZZ )
41		zdclt 9422	. . . . . . . . . . 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 2579	. . . . . . . . 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 7008	. . . . . . . 8 |- ( ph -> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin )
45		cnven 6876	. . . . . . . 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 5072	. . . . . . 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 4075	. . . . . 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 15402	. . . . . . 7 |- ( ph -> { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin )
50		hashen 10895	. . . . . . 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 5941	. . . 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 2232	. . 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 15405	. . 3 |- ( ph -> ( Q /L P ) = ( -u 1 ^ (♯ ` S ) ) )
57	54, 56	oveq12d 5943	. 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 9114	. . . 4 |- -u 1 e. CC
59	58	a1i 9	. . 3 |- ( ph -> -u 1 e. CC )
60	2, 1, 3, 6, 5, 55	lgsquadlemsfi 15402	. . . 4 |- ( ph -> S e. Fin )
61		hashcl 10892	. . . 4 |- ( S e. Fin -> (♯ ` S ) e. NN0 )
62	60, 61	syl 14	. . 3 |- ( ph -> (♯ ` S ) e. NN0 )
63		hashcl 10892	. . . 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 10786	. 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 9466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. ZZ )
68		prmz 12306	. . . . . . . . . . . . . . . . . . . 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 9383	. . . . . . . . . . . . . . . . . . 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 9022	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. RR )
73	71	zred 9467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. RR )
74		prmuz2 12326	. . . . . . . . . . . . . . . . . . . . . . . 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 9698	. . . . . . . . . . . . . . . . . . . . . . 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 9788	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. RR+ )
79		rphalflt 9777	. . . . . . . . . . . . . . . . . . . . 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 4069	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N < ( Q - 1 ) )
82	72, 73, 81	ltled 8164	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N <_ ( Q - 1 ) )
83		eluz2 9626	. . . . . . . . . . . . . . . . . 18 |- ( ( Q - 1 ) e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ ( Q - 1 ) e. ZZ /\ N <_ ( Q - 1 ) ) )
84	67, 71, 82, 83	syl3anbrc 1183	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. ( ZZ>= ` N ) )
85		fzss2 10158	. . . . . . . . . . . . . . . . 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 3185	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. ( 1 ... ( Q - 1 ) ) )
89		fzm1ndvds 12040	. . . . . . . . . . . . . . 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 3168	. . . . . . . . . . . . . . . . . 18 |- ( ph -> P e. Prime )
93	92	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. Prime )
94		prmrp 12340	. . . . . . . . . . . . . . . . 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 12306	. . . . . . . . . . . . . . . . 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 10119	. . . . . . . . . . . . . . . . 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 12287	. . . . . . . . . . . . . . . 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 1249	. . . . . . . . . . . . . . 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 664	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. Q || ( P x. y ) )
105	38	nncnd 9023	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. CC )
106	36	nncnd 9023	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. CC )
107	105, 106	mulcomd 8067	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( P x. y ) = ( y x. P ) )
108	107	breq2d 4046	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q || ( P x. y ) <-> Q || ( y x. P ) ) )
109	104, 108	mtbid 673	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. Q || ( y x. P ) )
110		elfzelz 10119	. . . . . . . . . . . . . . . 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 11998	. . . . . . . . . . . . . . 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 4038	. . . . . . . . . . . . . 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 2410	. . . . . . . . . . . 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 9726	. . . . . . . . . . . . 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 9726	. . . . . . . . . . . . 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 9734	. . . . . . . . . . . 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 4100	. . . . . 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 4113	. . . . . . 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 3315	. . . . . . 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 819	. . . . . . . 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 4101	. . . . . . 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 2227	. . . . . 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 4670	. . . . . 6 |- ( ( 1 ... M ) X. ( 1 ... N ) ) = { <. x , y >. | ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) }
136	129, 134, 135	3eqtr4g 2254	. . . . 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 5565	. . . 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 4799	. . . . . . 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 3362	. . . . . . 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 590	. . . . . . . 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 4101	. . . . . . 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 2227	. . . . . 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 9022	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. RR )
144	39	nnred 9022	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. RR )
145		ltnsym2 8136	. . . . . . . . . . . . 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 691	. . . . . . . . . . 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 1955	. . . . . . . . 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 1955	. . . . . . . 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 4316	. . . . . . . 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 678	. . . . . . 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 3472	. . . . . . 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 2241	. . . . 5 |- ( ph -> ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } i^i S ) = (/) )
157		hashun 10916	. . . . 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 1249	. . . 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 10937	. . . . . 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 9321	. . . . . . 7 |- ( ph -> M e. NN0 )
162		hashfz1 10894	. . . . . . 7 |- ( M e. NN0 -> (♯ ` ( 1 ... M ) ) = M )
163	161, 162	syl 14	. . . . . 6 |- ( ph -> (♯ ` ( 1 ... M ) ) = M )
164	24	nnnn0d 9321	. . . . . . 7 |- ( ph -> N e. NN0 )
165		hashfz1 10894	. . . . . . 7 |- ( N e. NN0 -> (♯ ` ( 1 ... N ) ) = N )
166	164, 165	syl 14	. . . . . 6 |- ( ph -> (♯ ` ( 1 ... N ) ) = N )
167	163, 166	oveq12d 5943	. . . . 5 |- ( ph -> ( (♯ ` ( 1 ... M ) ) x. (♯ ` ( 1 ... N ) ) ) = ( M x. N ) )
168	160, 167	eqtrd 2229	. . . 4 |- ( ph -> (♯ ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) = ( M x. N ) )
169	137, 158, 168	3eqtr3d 2237	. . 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 5941	. 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 2235	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 709  DECID wdc 835   = wceq 1364   E.wex 1506   e. wcel 2167   =/= wne 2367   \ cdif 3154   u. cun 3155   i^i cin 3156   C_ wss 3157   (/)c0 3451   {csn 3623   class class class wbr 4034   {copab 4094   X. cxp 4662   `'ccnv 4663   Rel wrel 4669   ` cfv 5259  (class class class)co 5925   ~~ cen 6806   Fincfn 6808   CCcc 7896   RRcr 7897   1c1 7899   + caddc 7901   x. cmul 7903   < clt 8080   <_ cle 8081   - cmin 8216   -ucneg 8217   / cdiv 8718   NNcn 9009   2c2 9060   NN0cn0 9268   ZZcz 9345   ZZ>=cuz 9620   QQcq 9712   RR+crp 9747   ...cfz 10102   ^cexp 10649  ♯chash 10886   || cdvds 11971   gcd cgcd 12147   Primecprime 12302   /Lclgs 15324

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4149  ax-sep 4152  ax-nul 4160  ax-pow 4208  ax-pr 4243  ax-un 4469  ax-setind 4574  ax-iinf 4625  ax-cnex 7989  ax-resscn 7990  ax-1cn 7991  ax-1re 7992  ax-icn 7993  ax-addcl 7994  ax-addrcl 7995  ax-mulcl 7996  ax-mulrcl 7997  ax-addcom 7998  ax-mulcom 7999  ax-addass 8000  ax-mulass 8001  ax-distr 8002  ax-i2m1 8003  ax-0lt1 8004  ax-1rid 8005  ax-0id 8006  ax-rnegex 8007  ax-precex 8008  ax-cnre 8009  ax-pre-ltirr 8010  ax-pre-ltwlin 8011  ax-pre-lttrn 8012  ax-pre-apti 8013  ax-pre-ltadd 8014  ax-pre-mulgt0 8015  ax-pre-mulext 8016  ax-arch 8017  ax-caucvg 8018  ax-addf 8020  ax-mulf 8021

This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-xor 1387  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rmo 2483  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3452  df-if 3563  df-pw 3608  df-sn 3629  df-pr 3630  df-tp 3631  df-op 3632  df-uni 3841  df-int 3876  df-iun 3919  df-disj 4012  df-br 4035  df-opab 4096  df-mpt 4097  df-tr 4133  df-id 4329  df-po 4332  df-iso 4333  df-iord 4402  df-on 4404  df-ilim 4405  df-suc 4407  df-iom 4628  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-rn 4675  df-res 4676  df-ima 4677  df-iota 5220  df-fun 5261  df-fn 5262  df-f 5263  df-f1 5264  df-fo 5265  df-f1o 5266  df-fv 5267  df-isom 5268  df-riota 5880  df-ov 5928  df-oprab 5929  df-mpo 5930  df-of 6139  df-1st 6207  df-2nd 6208  df-tpos 6312  df-recs 6372  df-irdg 6437  df-frec 6458  df-1o 6483  df-2o 6484  df-oadd 6487  df-er 6601  df-ec 6603  df-qs 6607  df-map 6718  df-en 6809  df-dom 6810  df-fin 6811  df-sup 7059  df-inf 7060  df-pnf 8082  df-mnf 8083  df-xr 8084  df-ltxr 8085  df-le 8086  df-sub 8218  df-neg 8219  df-reap 8621  df-ap 8628  df-div 8719  df-inn 9010  df-2 9068  df-3 9069  df-4 9070  df-5 9071  df-6 9072  df-7 9073  df-8 9074  df-9 9075  df-n0 9269  df-z 9346  df-dec 9477  df-uz 9621  df-q 9713  df-rp 9748  df-fz 10103  df-fzo 10237  df-fl 10379  df-mod 10434  df-seqfrec 10559  df-exp 10650  df-ihash 10887  df-cj 11026  df-re 11027  df-im 11028  df-rsqrt 11182  df-abs 11183  df-clim 11463  df-sumdc 11538  df-proddc 11735  df-dvds 11972  df-gcd 12148  df-prm 12303  df-phi 12406  df-pc 12481  df-struct 12707  df-ndx 12708  df-slot 12709  df-base 12711  df-sets 12712  df-iress 12713  df-plusg 12795  df-mulr 12796  df-starv 12797  df-sca 12798  df-vsca 12799  df-ip 12800  df-tset 12801  df-ple 12802  df-ds 12804  df-unif 12805  df-0g 12962  df-igsum 12963  df-topgen 12964  df-iimas 13006  df-qus 13007  df-mgm 13060  df-sgrp 13106  df-mnd 13121  df-mhm 13163  df-submnd 13164  df-grp 13207  df-minusg 13208  df-sbg 13209  df-mulg 13328  df-subg 13378  df-nsg 13379  df-eqg 13380  df-ghm 13449  df-cmn 13494  df-abl 13495  df-mgp 13555  df-rng 13567  df-ur 13594  df-srg 13598  df-ring 13632  df-cring 13633  df-oppr 13702  df-dvdsr 13723  df-unit 13724  df-invr 13755  df-dvr 13766  df-rhm 13786  df-nzr 13814  df-subrg 13853  df-domn 13893  df-idom 13894  df-lmod 13923  df-lssm 13987  df-lsp 14021  df-sra 14069  df-rgmod 14070  df-lidl 14103  df-rsp 14104  df-2idl 14134  df-bl 14180  df-mopn 14181  df-fg 14183  df-metu 14184  df-cnfld 14191  df-zring 14225  df-zrh 14248  df-zn 14250  df-lgs 15325

This theorem is referenced by:  lgsquad  15407