Theorem lgsquadlem3 16181

Description: Lemma for lgsquad 16182. (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 6086	. . . . . . . . 9 |- ( x = z -> ( x x. Q ) = ( z x. Q ) )
12		oveq1 6086	. . . . . . . . 9 |- ( y = w -> ( y x. P ) = ( w x. P ) )
13	11, 12	breqan12d 4144	. . . . . . . 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 4201	. . . . 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 16180	. . . 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 4902	. . . . . . . 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 9654	. . . . . . . . . 10 |- ( ph -> 1 e. ZZ )
21	2, 6	gausslemma2dlem0b 16152	. . . . . . . . . . 11 |- ( ph -> M e. NN )
22	21	nnzd 9750	. . . . . . . . . 10 |- ( ph -> M e. ZZ )
23	20, 22	fzfigd 10851	. . . . . . . . 9 |- ( ph -> ( 1 ... M ) e. Fin )
24	1, 5	gausslemma2dlem0b 16152	. . . . . . . . . . 11 |- ( ph -> N e. NN )
25	24	nnzd 9750	. . . . . . . . . 10 |- ( ph -> N e. ZZ )
26	20, 25	fzfigd 10851	. . . . . . . . 9 |- ( ph -> ( 1 ... N ) e. Fin )
27		elfznn 10443	. . . . . . . . . . . . . 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 12871	. . . . . . . . . . . . . 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 9336	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. NN )
34	33	nnzd 9750	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. ZZ )
35		elfznn 10443	. . . . . . . . . . . . . 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 16151	. . . . . . . . . . . . . 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 9336	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. NN )
40	39	nnzd 9750	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. ZZ )
41		zdclt 9705	. . . . . . . . . . 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 7241	. . . . . . . 8 |- ( ph -> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin )
45		cnven 7090	. . . . . . . 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 5187	. . . . . . 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 4169	. . . . . 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 16177	. . . . . . 7 |- ( ph -> { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin )
50		hashen 11206	. . . . . . 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 6095	. . . 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 16180	. . 3 |- ( ph -> ( Q /L P ) = ( -u 1 ^ (♯ ` S ) ) )
57	54, 56	oveq12d 6097	. 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 9392	. . . 4 |- -u 1 e. CC
59	58	a1i 9	. . 3 |- ( ph -> -u 1 e. CC )
60	2, 1, 3, 6, 5, 55	lgsquadlemsfi 16177	. . . 4 |- ( ph -> S e. Fin )
61		hashcl 11203	. . . 4 |- ( S e. Fin -> (♯ ` S ) e. NN0 )
62	60, 61	syl 14	. . 3 |- ( ph -> (♯ ` S ) e. NN0 )
63		hashcl 11203	. . . 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 11096	. 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 9750	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. ZZ )
68		prmz 12872	. . . . . . . . . . . . . . . . . . . 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 9665	. . . . . . . . . . . . . . . . . . 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 9300	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. RR )
73	71	zred 9751	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. RR )
74		prmuz2 12892	. . . . . . . . . . . . . . . . . . . . . . . 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 9988	. . . . . . . . . . . . . . . . . . . . . . 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 10078	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. RR+ )
79		rphalflt 10067	. . . . . . . . . . . . . . . . . . . . 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 4163	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N < ( Q - 1 ) )
82	72, 73, 81	ltled 8439	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N <_ ( Q - 1 ) )
83		eluz2 9910	. . . . . . . . . . . . . . . . . 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 10453	. . . . . . . . . . . . . . . . 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 12606	. . . . . . . . . . . . . . 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 12906	. . . . . . . . . . . . . . . . 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 12872	. . . . . . . . . . . . . . . . 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 10411	. . . . . . . . . . . . . . . . 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 12853	. . . . . . . . . . . . . . . 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 9301	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. CC )
106	36	nncnd 9301	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. CC )
107	105, 106	mulcomd 8341	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( P x. y ) = ( y x. P ) )
108	107	breq2d 4140	. . . . . . . . . . . . 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 10411	. . . . . . . . . . . . . . . 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 12564	. . . . . . . . . . . . . . 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 4132	. . . . . . . . . . . . . 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 10016	. . . . . . . . . . . . 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 10016	. . . . . . . . . . . . 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 10024	. . . . . . . . . . . 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 4195	. . . . . 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 4208	. . . . . . 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 4196	. . . . . . 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 4778	. . . . . 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 5697	. . . 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 4910	. . . . . . 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 4196	. . . . . . 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 9300	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. RR )
144	39	nnred 9300	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. RR )
145		ltnsym2 8410	. . . . . . . . . . . . 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 4421	. . . . . . . 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 11228	. . . . 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 11250	. . . . . 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 9603	. . . . . . 7 |- ( ph -> M e. NN0 )
162		hashfz1 11205	. . . . . . 7 |- ( M e. NN0 -> (♯ ` ( 1 ... M ) ) = M )
163	161, 162	syl 14	. . . . . 6 |- ( ph -> (♯ ` ( 1 ... M ) ) = M )
164	24	nnnn0d 9603	. . . . . . 7 |- ( ph -> N e. NN0 )
165		hashfz1 11205	. . . . . . 7 |- ( N e. NN0 -> (♯ ` ( 1 ... N ) ) = N )
166	164, 165	syl 14	. . . . . 6 |- ( ph -> (♯ ` ( 1 ... N ) ) = N )
167	163, 166	oveq12d 6097	. . . . 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 6095	. 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 ) ) )

Syntax hints:   -. 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 3708   class class class wbr 4128   {copab 4189   X. cxp 4770   `'ccnv 4771   Rel wrel 4777   ` cfv 5375  (class class class)co 6079   ~~ cen 7014   Fincfn 7016   CCcc 8171   RRcr 8172   1c1 8174   + caddc 8176   x. cmul 8178   < clt 8354   <_ cle 8355   - cmin 8491   -ucneg 8492   / cdiv 8996   NNcn 9287   2c2 9338   NN0cn0 9546   ZZcz 9627   ZZ>=cuz 9904   QQcq 10002   RR+crp 10037   ...cfz 10394   ^cexp 10958  ♯chash 11197   || cdvds 12537   gcd cgcd 12713   Primecprime 12868   /Lclgs 16099

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 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 4244  ax-sep 4247  ax-nul 4257  ax-pow 4309  ax-pr 4344  ax-un 4576  ax-setind 4682  ax-iinf 4733  ax-cnex 8264  ax-resscn 8265  ax-1cn 8266  ax-1re 8267  ax-icn 8268  ax-addcl 8269  ax-addrcl 8270  ax-mulcl 8271  ax-mulrcl 8272  ax-addcom 8273  ax-mulcom 8274  ax-addass 8275  ax-mulass 8276  ax-distr 8277  ax-i2m1 8278  ax-0lt1 8279  ax-1rid 8280  ax-0id 8281  ax-rnegex 8282  ax-precex 8283  ax-cnre 8284  ax-pre-ltirr 8285  ax-pre-ltwlin 8286  ax-pre-lttrn 8287  ax-pre-apti 8288  ax-pre-ltadd 8289  ax-pre-mulgt0 8290  ax-pre-mulext 8291  ax-arch 8292  ax-caucvg 8293  ax-addf 8295  ax-mulf 8296

This theorem 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 3714  df-pr 3715  df-tp 3716  df-op 3717  df-uni 3934  df-int 3969  df-iun 4012  df-disj 4105  df-br 4129  df-opab 4191  df-mpt 4192  df-tr 4228  df-id 4436  df-po 4439  df-iso 4440  df-iord 4509  df-on 4511  df-ilim 4512  df-suc 4514  df-iom 4736  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-rn 4783  df-res 4784  df-ima 4785  df-iota 5335  df-fun 5377  df-fn 5378  df-f 5379  df-f1 5380  df-fo 5381  df-f1o 5382  df-fv 5383  df-isom 5384  df-riota 6032  df-ov 6082  df-oprab 6083  df-mpo 6084  df-of 6296  df-1st 6368  df-2nd 6369  df-tpos 6510  df-recs 6570  df-irdg 6635  df-frec 6656  df-1o 6681  df-2o 6682  df-oadd 6685  df-er 6801  df-ec 6803  df-qs 6807  df-map 6918  df-en 7017  df-dom 7018  df-fin 7019  df-sup 7318  df-inf 7319  df-pnf 8356  df-mnf 8357  df-xr 8358  df-ltxr 8359  df-le 8360  df-sub 8493  df-neg 8494  df-reap 8897  df-ap 8904  df-div 8997  df-inn 9288  df-2 9346  df-3 9347  df-4 9348  df-5 9349  df-6 9350  df-7 9351  df-8 9352  df-9 9353  df-n0 9547  df-z 9628  df-dec 9761  df-uz 9905  df-q 10003  df-rp 10038  df-fz 10395  df-fzo 10533  df-fl 10688  df-mod 10743  df-seqfrec 10868  df-exp 10959  df-ihash 11198  df-cj 11590  df-re 11591  df-im 11592  df-rsqrt 11747  df-abs 11748  df-clim 12028  df-sumdc 12103  df-proddc 12301  df-dvds 12538  df-gcd 12714  df-prm 12869  df-phi 12972  df-pc 13047  df-struct 13337  df-ndx 13338  df-slot 13339  df-base 13341  df-sets 13342  df-iress 13343  df-plusg 13427  df-mulr 13428  df-starv 13429  df-sca 13430  df-vsca 13431  df-ip 13432  df-tset 13433  df-ple 13434  df-ds 13436  df-unif 13437  df-0g 13595  df-gzsum 13596  df-topgen 13597  df-iimas 13607  df-qus 13608  df-mgm 13659  df-sgrp 13700  df-mnd 13713  df-mhm 13749  df-submnd 13750  df-grp 13791  df-minusg 13792  df-sbg 13793  df-mulg 13906  df-subg 13956  df-nsg 13957  df-eqg 13958  df-ghm 14027  df-cmn 14072  df-abl 14073  df-gsumfi 14134  df-mgp 14201  df-rng 14215  df-ur 14246  df-srg 14251  df-ring 14285  df-cring 14286  df-oppr 14356  df-dvdsr 14378  df-unit 14379  df-invr 14411  df-dvr 14422  df-rhm 14442  df-nzr 14470  df-subrg 14510  df-domn 14550  df-idom 14551  df-lmod 14608  df-lssm 14673  df-lsp 14707  df-sra 14755  df-rgmod 14756  df-lidl 14789  df-rsp 14790  df-2idl 14820  df-bl 14866  df-mopn 14867  df-fg 14869  df-metu 14870  df-cnfld 14877  df-zring 14909  df-zrh 14932  df-zn 14934  df-lgs 16100

This theorem is referenced by:  lgsquad  16182