Theorem lgsquadlem3 16320

Description: Lemma for lgsquad 16321. (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 2506	. . . . 5 |- ( ph -> Q =/= P )
5		lgsquad.5	. . . . 5 |- N = ( ( Q - 1 ) / 2 )
6		lgsquad.4	. . . . 5 |- M = ( ( P - 1 ) / 2 )
7		eleq1w 2299	. . . . . . . . . 10 |- ( x = z -> ( x e. ( 1 ... M ) <-> z e. ( 1 ... M ) ) )
8		eleq1w 2299	. . . . . . . . . 10 |- ( y = w -> ( y e. ( 1 ... N ) <-> w e. ( 1 ... N ) ) )
9	7, 8	bi2anan9 614	. . . . . . . . 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 6092	. . . . . . . . 9 |- ( x = z -> ( x x. Q ) = ( z x. Q ) )
12		oveq1 6092	. . . . . . . . 9 |- ( y = w -> ( y x. P ) = ( w x. P ) )
13	11, 12	breqan12d 4146	. . . . . . . 8 |- ( ( x = z /\ y = w ) -> ( ( x x. Q ) < ( y x. P ) <-> ( z x. Q ) < ( w x. P ) ) )
14	10, 13	anbi12d 477	. . . . . . 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 4203	. . . . 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 16319	. . . 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 4904	. . . . . . . 8 |- Rel { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) }
19		eqid 2238	. . . . . . . . 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 9676	. . . . . . . . . 10 |- ( ph -> 1 e. ZZ )
21	2, 6	gausslemma2dlem0b 16291	. . . . . . . . . . 11 |- ( ph -> M e. NN )
22	21	nnzd 9772	. . . . . . . . . 10 |- ( ph -> M e. ZZ )
23	20, 22	fzfigd 10882	. . . . . . . . 9 |- ( ph -> ( 1 ... M ) e. Fin )
24	1, 5	gausslemma2dlem0b 16291	. . . . . . . . . . 11 |- ( ph -> N e. NN )
25	24	nnzd 9772	. . . . . . . . . 10 |- ( ph -> N e. ZZ )
26	20, 25	fzfigd 10882	. . . . . . . . 9 |- ( ph -> ( 1 ... N ) e. Fin )
27		elfznn 10471	. . . . . . . . . . . . . 14 |- ( x e. ( 1 ... M ) -> x e. NN )
28	27	ad2antrl 494	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> x e. NN )
29	1	eldifad 3231	. . . . . . . . . . . . . . 15 |- ( ph -> Q e. Prime )
30	29	adantr 276	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q e. Prime )
31		prmnn 12906	. . . . . . . . . . . . . 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 9356	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. NN )
34	33	nnzd 9772	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. ZZ )
35		elfznn 10471	. . . . . . . . . . . . . 14 |- ( y e. ( 1 ... N ) -> y e. NN )
36	35	ad2antll 495	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. NN )
37	2	gausslemma2dlem0a 16290	. . . . . . . . . . . . . 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 9356	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. NN )
40	39	nnzd 9772	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. ZZ )
41		zdclt 9727	. . . . . . . . . . 11 |- ( ( ( x x. Q ) e. ZZ /\ ( y x. P ) e. ZZ ) -> DECID ( x x. Q ) < ( y x. P ) )
42	34, 40, 41	syl2anc 415	. . . . . . . . . 10 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> DECID ( x x. Q ) < ( y x. P ) )
43	42	ralrimivva 2632	. . . . . . . . 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 7247	. . . . . . . 8 |- ( ph -> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin )
45		cnven 7096	. . . . . . . 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 418	. . . . . . 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 5189	. . . . . . 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 4171	. . . . . 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 16316	. . . . . . 7 |- ( ph -> { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin )
50		hashen 11238	. . . . . . 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 415	. . . . . 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 6101	. . . 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 2274	. . 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 16319	. . 3 |- ( ph -> ( Q /L P ) = ( -u 1 ^ (♯ ` S ) ) )
57	54, 56	oveq12d 6103	. 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 9412	. . . 4 |- -u 1 e. CC
59	58	a1i 9	. . 3 |- ( ph -> -u 1 e. CC )
60	2, 1, 3, 6, 5, 55	lgsquadlemsfi 16316	. . . 4 |- ( ph -> S e. Fin )
61		hashcl 11235	. . . 4 |- ( S e. Fin -> (♯ ` S ) e. NN0 )
62	60, 61	syl 14	. . 3 |- ( ph -> (♯ ` S ) e. NN0 )
63		hashcl 11235	. . . 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 11127	. 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 9772	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. ZZ )
68		prmz 12907	. . . . . . . . . . . . . . . . . . . 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 9687	. . . . . . . . . . . . . . . . . . 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 9320	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. RR )
73	71	zred 9773	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. RR )
74		prmuz2 12928	. . . . . . . . . . . . . . . . . . . . . . . 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 10015	. . . . . . . . . . . . . . . . . . . . . . 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 10106	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. RR+ )
79		rphalflt 10095	. . . . . . . . . . . . . . . . . . . . 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 4165	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N < ( Q - 1 ) )
82	72, 73, 81	ltled 8447	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N <_ ( Q - 1 ) )
83		eluz2 9937	. . . . . . . . . . . . . . . . . 18 |- ( ( Q - 1 ) e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ ( Q - 1 ) e. ZZ /\ N <_ ( Q - 1 ) ) )
84	67, 71, 82, 83	syl3anbrc 1212	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. ( ZZ>= ` N ) )
85		fzss2 10481	. . . . . . . . . . . . . . . . 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 537	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. ( 1 ... N ) )
88	86, 87	sseldd 3249	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. ( 1 ... ( Q - 1 ) ) )
89		fzm1ndvds 12641	. . . . . . . . . . . . . . 15 |- ( ( Q e. NN /\ y e. ( 1 ... ( Q - 1 ) ) ) -> -. Q || y )
90	32, 88, 89	syl2anc 415	. . . . . . . . . . . . . 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 3231	. . . . . . . . . . . . . . . . . 18 |- ( ph -> P e. Prime )
93	92	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. Prime )
94		prmrp 12942	. . . . . . . . . . . . . . . . 17 |- ( ( Q e. Prime /\ P e. Prime ) -> ( ( Q gcd P ) = 1 <-> Q =/= P ) )
95	30, 93, 94	syl2anc 415	. . . . . . . . . . . . . . . 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 12907	. . . . . . . . . . . . . . . . 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 10439	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 1 ... N ) -> y e. ZZ )
100	99	ad2antll 495	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. ZZ )
101		coprmdvds 12888	. . . . . . . . . . . . . . . 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 1278	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( ( Q || ( P x. y ) /\ ( Q gcd P ) = 1 ) -> Q || y ) )
103	96, 102	mpan2d 432	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q || ( P x. y ) -> Q || y ) )
104	90, 103	mtod 673	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. Q || ( P x. y ) )
105	38	nncnd 9321	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. CC )
106	36	nncnd 9321	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. CC )
107	105, 106	mulcomd 8348	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( P x. y ) = ( y x. P ) )
108	107	breq2d 4142	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q || ( P x. y ) <-> Q || ( y x. P ) ) )
109	104, 108	mtbid 683	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. Q || ( y x. P ) )
110		elfzelz 10439	. . . . . . . . . . . . . . . 16 |- ( x e. ( 1 ... M ) -> x e. ZZ )
111	110	ad2antrl 494	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> x e. ZZ )
112		dvdsmul2 12599	. . . . . . . . . . . . . . 15 |- ( ( x e. ZZ /\ Q e. ZZ ) -> Q || ( x x. Q ) )
113	111, 69, 112	syl2anc 415	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q || ( x x. Q ) )
114		breq2 4134	. . . . . . . . . . . . . 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 2463	. . . . . . . . . . . 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 10043	. . . . . . . . . . . . 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 10043	. . . . . . . . . . . . 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 10051	. . . . . . . . . . . 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 415	. . . . . . . . . . 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 398	. . . . . . . 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 4197	. . . . . 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 4210	. . . . . . 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 3380	. . . . . . 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 830	. . . . . . . 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 4198	. . . . . . 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 2269	. . . . . 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 4780	. . . . . 6 |- ( ( 1 ... M ) X. ( 1 ... N ) ) = { <. x , y >. | ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) }
136	129, 134, 135	3eqtr4g 2296	. . . . 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 5699	. . . 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 4912	. . . . . . 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 3429	. . . . . . 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 598	. . . . . . . 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 4198	. . . . . . 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 2269	. . . . . 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 9320	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. RR )
144	39	nnred 9320	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. RR )
145		ltnsym2 8417	. . . . . . . . . . . . 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 415	. . . . . . . . . . . 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 701	. . . . . . . . . . 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 1996	. . . . . . . . 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 1996	. . . . . . . 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 4423	. . . . . . . 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 688	. . . . . . 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 3542	. . . . . . 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 2283	. . . . 5 |- ( ph -> ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } i^i S ) = (/) )
157		hashun 11260	. . . . 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 1278	. . . 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 11282	. . . . . 6 |- ( ( ( 1 ... M ) e. Fin /\ ( 1 ... N ) e. Fin ) -> (♯ ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) = ( (♯ ` ( 1 ... M ) ) x. (♯ ` ( 1 ... N ) ) ) )
160	23, 26, 159	syl2anc 415	. . . . 5 |- ( ph -> (♯ ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) = ( (♯ ` ( 1 ... M ) ) x. (♯ ` ( 1 ... N ) ) ) )
161	21	nnnn0d 9625	. . . . . . 7 |- ( ph -> M e. NN0 )
162		hashfz1 11237	. . . . . . 7 |- ( M e. NN0 -> (♯ ` ( 1 ... M ) ) = M )
163	161, 162	syl 14	. . . . . 6 |- ( ph -> (♯ ` ( 1 ... M ) ) = M )
164	24	nnnn0d 9625	. . . . . . 7 |- ( ph -> N e. NN0 )
165		hashfz1 11237	. . . . . . 7 |- ( N e. NN0 -> (♯ ` ( 1 ... N ) ) = N )
166	164, 165	syl 14	. . . . . 6 |- ( ph -> (♯ ` ( 1 ... N ) ) = N )
167	163, 166	oveq12d 6103	. . . . 5 |- ( ph -> ( (♯ ` ( 1 ... M ) ) x. (♯ ` ( 1 ... N ) ) ) = ( M x. N ) )
168	160, 167	eqtrd 2271	. . . 4 |- ( ph -> (♯ ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) = ( M x. N ) )
169	137, 158, 168	3eqtr3d 2279	. . 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 6101	. 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 2277	1 |- ( ph -> ( ( P /L Q ) x. ( Q /L P ) ) = ( -u 1 ^ ( M x. N ) ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 720  DECID wdc 846   = wceq 1402   E.wex 1545   e. wcel 2209   =/= wne 2420   \ cdif 3217   u. cun 3218   i^i cin 3219   C_ wss 3220   (/)c0 3520   {csn 3709   class class class wbr 4130   {copab 4191   X. cxp 4772   `'ccnv 4773   Rel wrel 4779   ` cfv 5377  (class class class)co 6085   ~~ cen 7020   Fincfn 7022   CCcc 8178   RRcr 8179   1c1 8181   + caddc 8183   x. cmul 8185   < clt 8361   <_ cle 8362   - cmin 8499   -ucneg 8500   / cdiv 9005   NNcn 9307   2c2 9358   NN0cn0 9568   ZZcz 9649   ZZ>=cuz 9931   QQcq 10029   RR+crp 10065   ...cfz 10422   ^cexp 10989  ♯chash 11229   || cdvds 12572   gcd cgcd 12748   Primecprime 12903   /Lclgs 16238

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735  ax-cnex 8271  ax-resscn 8272  ax-1cn 8273  ax-1re 8274  ax-icn 8275  ax-addcl 8276  ax-addrcl 8277  ax-mulcl 8278  ax-mulrcl 8279  ax-addcom 8280  ax-mulcom 8281  ax-addass 8282  ax-mulass 8283  ax-distr 8284  ax-i2m1 8285  ax-0lt1 8286  ax-1rid 8287  ax-0id 8288  ax-rnegex 8289  ax-precex 8290  ax-cnre 8291  ax-pre-ltirr 8292  ax-pre-ltwlin 8293  ax-pre-lttrn 8294  ax-pre-apti 8295  ax-pre-ltadd 8296  ax-pre-mulgt0 8297  ax-pre-mulext 8298  ax-arch 8299  ax-caucvg 8300  ax-addf 8302  ax-mulf 8303

This proof depends on definitions:  df-bi 117  df-stab 843  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-xor 1425  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-tp 3717  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-disj 4107  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-id 4438  df-po 4441  df-iso 4442  df-iord 4511  df-on 4513  df-ilim 4514  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-isom 5386  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-of 6302  df-1st 6374  df-2nd 6375  df-tpos 6516  df-recs 6576  df-irdg 6641  df-frec 6662  df-1o 6687  df-2o 6688  df-oadd 6691  df-er 6807  df-ec 6809  df-qs 6813  df-map 6924  df-en 7023  df-dom 7024  df-fin 7025  df-sup 7325  df-inf 7326  df-pnf 8363  df-mnf 8364  df-xr 8365  df-ltxr 8366  df-le 8367  df-sub 8501  df-neg 8502  df-reap 8906  df-ap 8913  df-div 9006  df-inn 9308  df-2 9366  df-3 9367  df-4 9368  df-5 9369  df-6 9370  df-7 9371  df-8 9372  df-9 9373  df-n0 9569  df-z 9650  df-dec 9783  df-uz 9932  df-q 10030  df-rp 10066  df-fz 10423  df-fzo 10561  df-fl 10716  df-mod 10774  df-seqfrec 10899  df-exp 10990  df-ihash 11230  df-cj 11622  df-re 11623  df-im 11624  df-rsqrt 11779  df-abs 11780  df-clim 12063  df-sumdc 12138  df-proddc 12336  df-dvds 12573  df-gcd 12749  df-prm 12904  df-phi 13011  df-pc 13086  df-struct 13405  df-ndx 13406  df-slot 13407  df-base 13409  df-sets 13410  df-iress 13411  df-plusg 13495  df-mulr 13496  df-starv 13497  df-sca 13498  df-vsca 13499  df-ip 13500  df-tset 13501  df-ple 13502  df-ds 13504  df-unif 13505  df-0g 13663  df-gzsum 13664  df-topgen 13665  df-iimas 13675  df-qus 13676  df-mgm 13727  df-sgrp 13768  df-mnd 13781  df-mhm 13817  df-submnd 13818  df-grp 13859  df-minusg 13860  df-sbg 13861  df-mulg 13974  df-subg 14024  df-nsg 14025  df-eqg 14026  df-ghm 14095  df-cmn 14140  df-abl 14141  df-gsumfi 14202  df-mgp 14269  df-rng 14283  df-ur 14314  df-srg 14319  df-ring 14353  df-cring 14354  df-oppr 14424  df-dvdsr 14446  df-unit 14447  df-invr 14479  df-dvr 14490  df-rhm 14510  df-nzr 14538  df-subrg 14578  df-domn 14618  df-idom 14619  df-lmod 14676  df-lssm 14741  df-lsp 14775  df-sra 14823  df-rgmod 14824  df-lidl 14857  df-rsp 14858  df-2idl 14888  df-bl 14934  df-mopn 14935  df-fg 14937  df-metu 14938  df-cnfld 14945  df-zring 14977  df-zrh 15000  df-zn 15002  df-lgs 16239

This theorem is used by:  lgsquad  16321