Theorem lgsquadlem3 15944

Description: Lemma for lgsquad 15945. (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 2498	. . . . 5 |- ( ph -> Q =/= P )
5		lgsquad.5	. . . . 5 |- N = ( ( Q - 1 ) / 2 )
6		lgsquad.4	. . . . 5 |- M = ( ( P - 1 ) / 2 )
7		eleq1w 2293	. . . . . . . . . 10 |- ( x = z -> ( x e. ( 1 ... M ) <-> z e. ( 1 ... M ) ) )
8		eleq1w 2293	. . . . . . . . . 10 |- ( y = w -> ( y e. ( 1 ... N ) <-> w e. ( 1 ... N ) ) )
9	7, 8	bi2anan9 610	. . . . . . . . 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 6056	. . . . . . . . 9 |- ( x = z -> ( x x. Q ) = ( z x. Q ) )
12		oveq1 6056	. . . . . . . . 9 |- ( y = w -> ( y x. P ) = ( w x. P ) )
13	11, 12	breqan12d 4124	. . . . . . . 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 4181	. . . . 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 15943	. . . 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 4878	. . . . . . . 8 |- Rel { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) }
19		eqid 2232	. . . . . . . . 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 9603	. . . . . . . . . 10 |- ( ph -> 1 e. ZZ )
21	2, 6	gausslemma2dlem0b 15915	. . . . . . . . . . 11 |- ( ph -> M e. NN )
22	21	nnzd 9698	. . . . . . . . . 10 |- ( ph -> M e. ZZ )
23	20, 22	fzfigd 10792	. . . . . . . . 9 |- ( ph -> ( 1 ... M ) e. Fin )
24	1, 5	gausslemma2dlem0b 15915	. . . . . . . . . . 11 |- ( ph -> N e. NN )
25	24	nnzd 9698	. . . . . . . . . 10 |- ( ph -> N e. ZZ )
26	20, 25	fzfigd 10792	. . . . . . . . 9 |- ( ph -> ( 1 ... N ) e. Fin )
27		elfznn 10387	. . . . . . . . . . . . . 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 3221	. . . . . . . . . . . . . . 15 |- ( ph -> Q e. Prime )
30	29	adantr 276	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q e. Prime )
31		prmnn 12803	. . . . . . . . . . . . . 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 9285	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. NN )
34	33	nnzd 9698	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. ZZ )
35		elfznn 10387	. . . . . . . . . . . . . 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 15914	. . . . . . . . . . . . . 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 9285	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. NN )
40	39	nnzd 9698	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. ZZ )
41		zdclt 9654	. . . . . . . . . . 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 2624	. . . . . . . . 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 7199	. . . . . . . 8 |- ( ph -> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin )
45		cnven 7048	. . . . . . . 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 5163	. . . . . . 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 4149	. . . . . 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 15940	. . . . . . 7 |- ( ph -> { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin )
50		hashen 11145	. . . . . . 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 6065	. . . 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 2268	. . 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 15943	. . 3 |- ( ph -> ( Q /L P ) = ( -u 1 ^ (♯ ` S ) ) )
57	54, 56	oveq12d 6067	. 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 9341	. . . 4 |- -u 1 e. CC
59	58	a1i 9	. . 3 |- ( ph -> -u 1 e. CC )
60	2, 1, 3, 6, 5, 55	lgsquadlemsfi 15940	. . . 4 |- ( ph -> S e. Fin )
61		hashcl 11142	. . . 4 |- ( S e. Fin -> (♯ ` S ) e. NN0 )
62	60, 61	syl 14	. . 3 |- ( ph -> (♯ ` S ) e. NN0 )
63		hashcl 11142	. . . 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 11036	. 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 9698	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. ZZ )
68		prmz 12804	. . . . . . . . . . . . . . . . . . . 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 9614	. . . . . . . . . . . . . . . . . . 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 9249	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. RR )
73	71	zred 9699	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. RR )
74		prmuz2 12824	. . . . . . . . . . . . . . . . . . . . . . . 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 9936	. . . . . . . . . . . . . . . . . . . . . . 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 10026	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. RR+ )
79		rphalflt 10015	. . . . . . . . . . . . . . . . . . . . 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 4143	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N < ( Q - 1 ) )
82	72, 73, 81	ltled 8391	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N <_ ( Q - 1 ) )
83		eluz2 9858	. . . . . . . . . . . . . . . . . 18 |- ( ( Q - 1 ) e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ ( Q - 1 ) e. ZZ /\ N <_ ( Q - 1 ) ) )
84	67, 71, 82, 83	syl3anbrc 1208	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. ( ZZ>= ` N ) )
85		fzss2 10397	. . . . . . . . . . . . . . . . 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 533	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. ( 1 ... N ) )
88	86, 87	sseldd 3238	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. ( 1 ... ( Q - 1 ) ) )
89		fzm1ndvds 12538	. . . . . . . . . . . . . . 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 3221	. . . . . . . . . . . . . . . . . 18 |- ( ph -> P e. Prime )
93	92	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. Prime )
94		prmrp 12838	. . . . . . . . . . . . . . . . 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 12804	. . . . . . . . . . . . . . . . 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 10358	. . . . . . . . . . . . . . . . 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 12785	. . . . . . . . . . . . . . . 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 1274	. . . . . . . . . . . . . . 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 669	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. Q || ( P x. y ) )
105	38	nncnd 9250	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. CC )
106	36	nncnd 9250	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. CC )
107	105, 106	mulcomd 8294	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( P x. y ) = ( y x. P ) )
108	107	breq2d 4120	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q || ( P x. y ) <-> Q || ( y x. P ) ) )
109	104, 108	mtbid 679	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. Q || ( y x. P ) )
110		elfzelz 10358	. . . . . . . . . . . . . . . 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 12496	. . . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . 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 2455	. . . . . . . . . . . 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 9964	. . . . . . . . . . . . 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 9964	. . . . . . . . . . . . 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 9972	. . . . . . . . . . . 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 4175	. . . . . 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 4188	. . . . . . 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 3369	. . . . . . 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 826	. . . . . . . 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 4176	. . . . . . 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 2263	. . . . . 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 4754	. . . . . 6 |- ( ( 1 ... M ) X. ( 1 ... N ) ) = { <. x , y >. | ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) }
136	129, 134, 135	3eqtr4g 2290	. . . . 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 5673	. . . 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 4886	. . . . . . 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 3418	. . . . . . 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 594	. . . . . . . 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 4176	. . . . . . 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 2263	. . . . . 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 9249	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. RR )
144	39	nnred 9249	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. RR )
145		ltnsym2 8363	. . . . . . . . . . . . 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 697	. . . . . . . . . . 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 1990	. . . . . . . . 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 1990	. . . . . . . 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 4398	. . . . . . . 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 684	. . . . . . 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 3528	. . . . . . 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 2277	. . . . 5 |- ( ph -> ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } i^i S ) = (/) )
157		hashun 11167	. . . . 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 1274	. . . 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 11189	. . . . . 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 9552	. . . . . . 7 |- ( ph -> M e. NN0 )
162		hashfz1 11144	. . . . . . 7 |- ( M e. NN0 -> (♯ ` ( 1 ... M ) ) = M )
163	161, 162	syl 14	. . . . . 6 |- ( ph -> (♯ ` ( 1 ... M ) ) = M )
164	24	nnnn0d 9552	. . . . . . 7 |- ( ph -> N e. NN0 )
165		hashfz1 11144	. . . . . . 7 |- ( N e. NN0 -> (♯ ` ( 1 ... N ) ) = N )
166	164, 165	syl 14	. . . . . 6 |- ( ph -> (♯ ` ( 1 ... N ) ) = N )
167	163, 166	oveq12d 6067	. . . . 5 |- ( ph -> ( (♯ ` ( 1 ... M ) ) x. (♯ ` ( 1 ... N ) ) ) = ( M x. N ) )
168	160, 167	eqtrd 2265	. . . 4 |- ( ph -> (♯ ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) = ( M x. N ) )
169	137, 158, 168	3eqtr3d 2273	. . 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 6065	. 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 2271	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 716  DECID wdc 842   = wceq 1398   E.wex 1541   e. wcel 2203   =/= wne 2412   \ cdif 3207   u. cun 3208   i^i cin 3209   C_ wss 3210   (/)c0 3507   {csn 3688   class class class wbr 4108   {copab 4169   X. cxp 4746   `'ccnv 4747   Rel wrel 4753   ` cfv 5351  (class class class)co 6049   ~~ cen 6972   Fincfn 6974   CCcc 8124   RRcr 8125   1c1 8127   + caddc 8129   x. cmul 8131   < clt 8307   <_ cle 8308   - cmin 8443   -ucneg 8444   / cdiv 8945   NNcn 9236   2c2 9287   NN0cn0 9495   ZZcz 9576   ZZ>=cuz 9852   QQcq 9950   RR+crp 9985   ...cfz 10341   ^cexp 10899  ♯chash 11136   || cdvds 12469   gcd cgcd 12645   Primecprime 12800   /Lclgs 15862

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-coll 4224  ax-sep 4227  ax-nul 4235  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-setind 4658  ax-iinf 4709  ax-cnex 8217  ax-resscn 8218  ax-1cn 8219  ax-1re 8220  ax-icn 8221  ax-addcl 8222  ax-addrcl 8223  ax-mulcl 8224  ax-mulrcl 8225  ax-addcom 8226  ax-mulcom 8227  ax-addass 8228  ax-mulass 8229  ax-distr 8230  ax-i2m1 8231  ax-0lt1 8232  ax-1rid 8233  ax-0id 8234  ax-rnegex 8235  ax-precex 8236  ax-cnre 8237  ax-pre-ltirr 8238  ax-pre-ltwlin 8239  ax-pre-lttrn 8240  ax-pre-apti 8241  ax-pre-ltadd 8242  ax-pre-mulgt0 8243  ax-pre-mulext 8244  ax-arch 8245  ax-caucvg 8246  ax-addf 8248  ax-mulf 8249

This theorem depends on definitions:  df-bi 117  df-stab 839  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-xor 1421  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rmo 2528  df-rab 2529  df-v 2814  df-sbc 3042  df-csb 3138  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-nul 3508  df-if 3620  df-pw 3670  df-sn 3694  df-pr 3695  df-tp 3696  df-op 3697  df-uni 3914  df-int 3949  df-iun 3992  df-disj 4085  df-br 4109  df-opab 4171  df-mpt 4172  df-tr 4208  df-id 4413  df-po 4416  df-iso 4417  df-iord 4486  df-on 4488  df-ilim 4489  df-suc 4491  df-iom 4712  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-rn 4759  df-res 4760  df-ima 4761  df-iota 5311  df-fun 5353  df-fn 5354  df-f 5355  df-f1 5356  df-fo 5357  df-f1o 5358  df-fv 5359  df-isom 5360  df-riota 6002  df-ov 6052  df-oprab 6053  df-mpo 6054  df-of 6265  df-1st 6333  df-2nd 6334  df-tpos 6475  df-recs 6535  df-irdg 6600  df-frec 6621  df-1o 6646  df-2o 6647  df-oadd 6650  df-er 6766  df-ec 6768  df-qs 6772  df-map 6883  df-en 6975  df-dom 6976  df-fin 6977  df-sup 7274  df-inf 7275  df-pnf 8309  df-mnf 8310  df-xr 8311  df-ltxr 8312  df-le 8313  df-sub 8445  df-neg 8446  df-reap 8848  df-ap 8855  df-div 8946  df-inn 9237  df-2 9295  df-3 9296  df-4 9297  df-5 9298  df-6 9299  df-7 9300  df-8 9301  df-9 9302  df-n0 9496  df-z 9577  df-dec 9709  df-uz 9853  df-q 9951  df-rp 9986  df-fz 10342  df-fzo 10476  df-fl 10629  df-mod 10684  df-seqfrec 10809  df-exp 10900  df-ihash 11137  df-cj 11523  df-re 11524  df-im 11525  df-rsqrt 11679  df-abs 11680  df-clim 11960  df-sumdc 12035  df-proddc 12233  df-dvds 12470  df-gcd 12646  df-prm 12801  df-phi 12904  df-pc 12979  df-struct 13206  df-ndx 13207  df-slot 13208  df-base 13210  df-sets 13211  df-iress 13212  df-plusg 13295  df-mulr 13296  df-starv 13297  df-sca 13298  df-vsca 13299  df-ip 13300  df-tset 13301  df-ple 13302  df-ds 13304  df-unif 13305  df-0g 13463  df-igsum 13464  df-topgen 13465  df-iimas 13507  df-qus 13508  df-mgm 13561  df-sgrp 13607  df-mnd 13622  df-mhm 13664  df-submnd 13665  df-grp 13708  df-minusg 13709  df-sbg 13710  df-mulg 13829  df-subg 13879  df-nsg 13880  df-eqg 13881  df-ghm 13950  df-cmn 13995  df-abl 13996  df-mgp 14057  df-rng 14069  df-ur 14096  df-srg 14100  df-ring 14134  df-cring 14135  df-oppr 14204  df-dvdsr 14225  df-unit 14226  df-invr 14258  df-dvr 14269  df-rhm 14289  df-nzr 14317  df-subrg 14356  df-domn 14396  df-idom 14397  df-lmod 14429  df-lssm 14493  df-lsp 14527  df-sra 14575  df-rgmod 14576  df-lidl 14609  df-rsp 14610  df-2idl 14640  df-bl 14686  df-mopn 14687  df-fg 14689  df-metu 14690  df-cnfld 14697  df-zring 14731  df-zrh 14754  df-zn 14756  df-lgs 15863

This theorem is referenced by:  lgsquad  15945