P. 164 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16301-16400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gausslemma2dlem1f1o 16301*	Lemma for gausslemma2dlem1 16302. (Contributed by Jim Kingdon, 9-Aug-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   =>    |- ( ph -> R : ( 1 ... H ) -1-1-onto-> ( 1 ... H ) )
Theorem	gausslemma2dlem1 16302*	Lemma 1 for gausslemma2d 16310. (Contributed by AV, 5-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   =>    |- ( ph -> ( ! ` H ) = prod_ k e. ( 1 ... H ) ( R ` k ) )
Theorem	gausslemma2dlem2 16303*	Lemma 2 for gausslemma2d 16310. (Contributed by AV, 4-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   =>    |- ( ph -> A. k e. ( 1 ... M ) ( R ` k ) = ( k x. 2 ) )
Theorem	gausslemma2dlem3 16304*	Lemma 3 for gausslemma2d 16310. (Contributed by AV, 4-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   =>    |- ( ph -> A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) )
Theorem	gausslemma2dlem4 16305*	Lemma 4 for gausslemma2d 16310. (Contributed by AV, 16-Jun-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   =>    |- ( ph -> ( ! ` H ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )
Theorem	gausslemma2dlem5a 16306*	Lemma for gausslemma2dlem5 16307. (Contributed by AV, 8-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   =>    |- ( ph -> ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) = ( prod_ k e. ( ( M + 1 ) ... H ) ( -u 1 x. ( k x. 2 ) ) mod P ) )
Theorem	gausslemma2dlem5 16307*	Lemma 5 for gausslemma2d 16310. (Contributed by AV, 9-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- N = ( H - M )   =>    |- ( ph -> ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) = ( ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) mod P ) )
Theorem	gausslemma2dlem6 16308*	Lemma 6 for gausslemma2d 16310. (Contributed by AV, 16-Jun-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- N = ( H - M )   =>    |- ( ph -> ( ( ! ` H ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) mod P ) )
Theorem	gausslemma2dlem7 16309*	Lemma 7 for gausslemma2d 16310. (Contributed by AV, 13-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- N = ( H - M )   =>    |- ( ph -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = 1 )
Theorem	gausslemma2d 16310*	Gauss' Lemma (see also theorem 9.6 in [ApostolNT] p. 182) for integer 2: Let p be an odd prime. Let S = {2, 4, 6, ..., p - 1}. Let n denote the number of elements of S whose least positive residue modulo p is greater than p/2. Then ( 2 | p ) = (-1)^n. (Contributed by AV, 14-Jul-2021.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- M = ( |_ ` ( P / 4 ) )   &    |- N = ( H - M )   =>    |- ( ph -> ( 2 /L P ) = ( -u 1 ^ N ) )
11.4.7  Quadratic reciprocity
Theorem	lgseisenlem1 16311*	Lemma for lgseisen 16315. If R ( u ) = ( Q x. u ) mod P and M ( u ) = ( -u 1 ^ R ( u ) ) x. R ( u ), then for any even 1 <_ u <_ P - 1, M ( u ) is also an even integer 1 <_ M ( u ) <_ P - 1. To simplify these statements, we divide all the even numbers by 2, so that it becomes the statement that M ( x / 2 ) = ( -u 1 ^ R ( x / 2 ) ) x. R ( x / 2 ) / 2 is an integer between 1 and ( P - 1 ) / 2. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- R = ( ( Q x. ( 2 x. x ) ) mod P )   &    |- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )   =>    |- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) )
Theorem	lgseisenlem2 16312*	Lemma for lgseisen 16315. The function M is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 17-Jun-2015.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- R = ( ( Q x. ( 2 x. x ) ) mod P )   &    |- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )   &    |- S = ( ( Q x. ( 2 x. y ) ) mod P )   =>    |- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( 1 ... ( ( P - 1 ) / 2 ) ) )
Theorem	lgseisenlem3 16313*	Lemma for lgseisen 16315. (Contributed by Mario Carneiro, 17-Jun-2015.) (Proof shortened by AV, 28-Jul-2019.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- R = ( ( Q x. ( 2 x. x ) ) mod P )   &    |- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )   &    |- S = ( ( Q x. ( 2 x. y ) ) mod P )   &    |- Y = (ℤ/nℤ ` P )   &    |- G = (mulGrp ` Y )   &    |- L = ( ZRHom ` Y )   =>    |- ( ph -> ( G gsumg ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) = ( 1r ` Y ) )
Theorem	lgseisenlem4 16314*	Lemma for lgseisen 16315. (Contributed by Mario Carneiro, 18-Jun-2015.) (Proof shortened by AV, 15-Jun-2019.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- R = ( ( Q x. ( 2 x. x ) ) mod P )   &    |- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )   &    |- S = ( ( Q x. ( 2 x. y ) ) mod P )   &    |- Y = (ℤ/nℤ ` P )   &    |- G = (mulGrp ` Y )   &    |- L = ( ZRHom ` Y )   =>    |- ( ph -> ( ( Q ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) mod P ) )
Theorem	lgseisen 16315*	Eisenstein's lemma, an expression for ( P /L Q ) when P , Q are distinct odd primes. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   =>    |- ( ph -> ( Q /L P ) = ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
Theorem	lgsquadlemsfi 16316*	Lemma for lgsquad 16321. S is finite. (Contributed by Jim Kingdon, 16-Sep-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> S e. Fin )
Theorem	lgsquadlemofi 16317*	Lemma for lgsquad 16321. There are finitely many members of S with odd first part. (Contributed by Jim Kingdon, 16-Sep-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> { z e. S | -. 2 || ( 1st ` z ) } e. Fin )
Theorem	lgsquadlem1 16318*	Lemma for lgsquad 16321. Count the members of S with odd coordinates. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) )
Theorem	lgsquadlem2 16319*	Lemma for lgsquad 16321. Count the members of S with even coordinates, and combine with lgsquadlem1 16318 to get the total count of lattice points in S (up to parity). (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> ( Q /L P ) = ( -u 1 ^ (♯ ` S ) ) )
Theorem	lgsquadlem3 16320*	Lemma for lgsquad 16321. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> ( ( P /L Q ) x. ( Q /L P ) ) = ( -u 1 ^ ( M x. N ) ) )
Theorem	lgsquad 16321	The Law of Quadratic Reciprocity, see also theorem 9.8 in [ApostolNT] p. 185. If P and Q are distinct odd primes, then the product of the Legendre symbols ( P /L Q ) and ( Q /L P ) is the parity of ( ( P - 1 ) / 2 ) x. ( ( Q - 1 ) / 2 ). This uses Eisenstein's proof, which also has a nice geometric interpretation - see https://en.wikipedia.org/wiki/Proofs_of_quadratic_reciprocity. This is Metamath 100 proof #7. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( ( P e. ( Prime \ { 2 } ) /\ Q e. ( Prime \ { 2 } ) /\ P =/= Q ) -> ( ( P /L Q ) x. ( Q /L P ) ) = ( -u 1 ^ ( ( ( P - 1 ) / 2 ) x. ( ( Q - 1 ) / 2 ) ) ) )
Theorem	lgsquad2lem1 16322	Lemma for lgsquad2 16324. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( ph -> M e. NN )   &    |- ( ph -> -. 2 || M )   &    |- ( ph -> N e. NN )   &    |- ( ph -> -. 2 || N )   &    |- ( ph -> ( M gcd N ) = 1 )   &    |- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> ( A x. B ) = M )   &    |- ( ph -> ( ( A /L N ) x. ( N /L A ) ) = ( -u 1 ^ ( ( ( A - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )   &    |- ( ph -> ( ( B /L N ) x. ( N /L B ) ) = ( -u 1 ^ ( ( ( B - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )   =>    |- ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
Theorem	lgsquad2lem2 16323*	Lemma for lgsquad2 16324. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( ph -> M e. NN )   &    |- ( ph -> -. 2 || M )   &    |- ( ph -> N e. NN )   &    |- ( ph -> -. 2 || N )   &    |- ( ph -> ( M gcd N ) = 1 )   &    |- ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )   &    |- ( ps <-> A. x e. ( 1 ... k ) ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )   =>    |- ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
Theorem	lgsquad2 16324	Extend lgsquad 16321 to coprime odd integers (the domain of the Jacobi symbol). (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( ph -> M e. NN )   &    |- ( ph -> -. 2 || M )   &    |- ( ph -> N e. NN )   &    |- ( ph -> -. 2 || N )   &    |- ( ph -> ( M gcd N ) = 1 )   =>    |- ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
Theorem	lgsquad3 16325	Extend lgsquad2 16324 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( ( ( M e. NN /\ -. 2 || M ) /\ ( N e. NN /\ -. 2 || N ) ) -> ( M /L N ) = ( ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) x. ( N /L M ) ) )
Theorem	m1lgs 16326	The first supplement to the law of quadratic reciprocity. Negative one is a square mod an odd prime P iff P == 1 (mod 4). See first case of theorem 9.4 in [ApostolNT] p. 181. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- ( P e. ( Prime \ { 2 } ) -> ( ( -u 1 /L P ) = 1 <-> ( P mod 4 ) = 1 ) )
Theorem	2lgslem1a1 16327*	Lemma 1 for 2lgslem1a 16329. (Contributed by AV, 16-Jun-2021.)
|- ( ( P e. NN /\ -. 2 || P ) -> A. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( i x. 2 ) = ( ( i x. 2 ) mod P ) )
Theorem	2lgslem1a2 16328	Lemma 2 for 2lgslem1a 16329. (Contributed by AV, 18-Jun-2021.)
|- ( ( N e. ZZ /\ I e. ZZ ) -> ( ( |_ ` ( N / 4 ) ) < I <-> ( N / 2 ) < ( I x. 2 ) ) )
Theorem	2lgslem1a 16329*	Lemma 1 for 2lgslem1 16332. (Contributed by AV, 18-Jun-2021.)
|- ( ( P e. Prime /\ -. 2 || P ) -> { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } = { x e. ZZ | E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) } )
Theorem	2lgslem1b 16330*	Lemma 2 for 2lgslem1 16332. (Contributed by AV, 18-Jun-2021.)
|- I = ( A ... B )   &    |- F = ( j e. I |-> ( j x. 2 ) )   =>    |- F : I -1-1-onto-> { x e. ZZ | E. i e. I x = ( i x. 2 ) }
Theorem	2lgslem1c 16331	Lemma 3 for 2lgslem1 16332. (Contributed by AV, 19-Jun-2021.)
|- ( ( P e. Prime /\ -. 2 || P ) -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) )
Theorem	2lgslem1 16332*	Lemma 1 for 2lgs 16345. (Contributed by AV, 19-Jun-2021.)
|- ( ( P e. Prime /\ -. 2 || P ) -> (♯ ` { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } ) = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) )
Theorem	2lgslem2 16333	Lemma 2 for 2lgs 16345. (Contributed by AV, 20-Jun-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. Prime /\ -. 2 || P ) -> N e. ZZ )
Theorem	2lgslem3a 16334	Lemma for 2lgslem3a1 16338. (Contributed by AV, 14-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 1 ) ) -> N = ( 2 x. K ) )
Theorem	2lgslem3b 16335	Lemma for 2lgslem3b1 16339. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 3 ) ) -> N = ( ( 2 x. K ) + 1 ) )
Theorem	2lgslem3c 16336	Lemma for 2lgslem3c1 16340. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 5 ) ) -> N = ( ( 2 x. K ) + 1 ) )
Theorem	2lgslem3d 16337	Lemma for 2lgslem3d1 16341. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 7 ) ) -> N = ( ( 2 x. K ) + 2 ) )
Theorem	2lgslem3a1 16338	Lemma 1 for 2lgslem3 16342. (Contributed by AV, 15-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ ( P mod 8 ) = 1 ) -> ( N mod 2 ) = 0 )
Theorem	2lgslem3b1 16339	Lemma 2 for 2lgslem3 16342. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ ( P mod 8 ) = 3 ) -> ( N mod 2 ) = 1 )
Theorem	2lgslem3c1 16340	Lemma 3 for 2lgslem3 16342. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ ( P mod 8 ) = 5 ) -> ( N mod 2 ) = 1 )
Theorem	2lgslem3d1 16341	Lemma 4 for 2lgslem3 16342. (Contributed by AV, 15-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ ( P mod 8 ) = 7 ) -> ( N mod 2 ) = 0 )
Theorem	2lgslem3 16342	Lemma 3 for 2lgs 16345. (Contributed by AV, 16-Jul-2021.)
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )   =>    |- ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) )
Theorem	2lgs2 16343	The Legendre symbol for 2 at 2 is 0. (Contributed by AV, 20-Jun-2021.)
|- ( 2 /L 2 ) = 0
Theorem	2lgslem4 16344	Lemma 4 for 2lgs 16345: special case of 2lgs 16345 for P = 2. (Contributed by AV, 20-Jun-2021.)
|- ( ( 2 /L 2 ) = 1 <-> ( 2 mod 8 ) e. { 1 , 7 } )
Theorem	2lgs 16345	The second supplement to the law of quadratic reciprocity (for the Legendre symbol extended to arbitrary primes as second argument). Two is a square modulo a prime P iff P == pm 1 (mod 8), see first case of theorem 9.5 in [ApostolNT] p. 181. This theorem justifies our definition of ( N /L 2 ) (lgs2 16258) to some degree, by demanding that reciprocity extend to the case Q = 2. (Proposed by Mario Carneiro, 19-Jun-2015.) (Contributed by AV, 16-Jul-2021.)
|- ( P e. Prime -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )
Theorem	2lgsoddprmlem1 16346	Lemma 1 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021.)
|- ( ( A e. ZZ /\ B e. ZZ /\ N = ( ( 8 x. A ) + B ) ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) = ( ( ( 8 x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) + ( ( ( B ^ 2 ) - 1 ) / 8 ) ) )
Theorem	2lgsoddprmlem2 16347	Lemma 2 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021.)
|- ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) ) )
Theorem	2lgsoddprmlem3a 16348	Lemma 1 for 2lgsoddprmlem3 16352. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 1 ^ 2 ) - 1 ) / 8 ) = 0
Theorem	2lgsoddprmlem3b 16349	Lemma 2 for 2lgsoddprmlem3 16352. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 3 ^ 2 ) - 1 ) / 8 ) = 1
Theorem	2lgsoddprmlem3c 16350	Lemma 3 for 2lgsoddprmlem3 16352. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 5 ^ 2 ) - 1 ) / 8 ) = 3
Theorem	2lgsoddprmlem3d 16351	Lemma 4 for 2lgsoddprmlem3 16352. (Contributed by AV, 20-Jul-2021.)
|- ( ( ( 7 ^ 2 ) - 1 ) / 8 ) = ( 2 x. 3 )
Theorem	2lgsoddprmlem3 16352	Lemma 3 for 2lgsoddprm . (Contributed by AV, 20-Jul-2021.)
|- ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) <-> R e. { 1 , 7 } ) )
Theorem	2lgsoddprmlem4 16353	Lemma 4 for 2lgsoddprm . (Contributed by AV, 20-Jul-2021.)
|- ( ( N e. ZZ /\ -. 2 || N ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> ( N mod 8 ) e. { 1 , 7 } ) )
Theorem	2lgsoddprm 16354	The second supplement to the law of quadratic reciprocity for odd primes (common representation, see theorem 9.5 in [ApostolNT] p. 181): The Legendre symbol for 2 at an odd prime is minus one to the power of the square of the odd prime minus one divided by eight ( ( 2 /L P ) = -1^(((P^2)-1)/8) ). (Contributed by AV, 20-Jul-2021.)
|- ( P e. ( Prime \ { 2 } ) -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )
11.4.8  All primes 4n+1 are the sum of two squares
Theorem	2sqlem1 16355*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   =>    |- ( A e. S <-> E. x e. ZZ[_i] A = ( ( abs ` x ) ^ 2 ) )
Theorem	2sqlem2 16356*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   =>    |- ( A e. S <-> E. x e. ZZ E. y e. ZZ A = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
Theorem	mul2sq 16357	Fibonacci's identity (actually due to Diophantus). The product of two sums of two squares is also a sum of two squares. We can take advantage of Gaussian integers here to trivialize the proof. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   =>    |- ( ( A e. S /\ B e. S ) -> ( A x. B ) e. S )
Theorem	2sqlem3 16358	Lemma for 2sqlem5 16360. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- ( ph -> ( N x. P ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )   &    |- ( ph -> P = ( ( C ^ 2 ) + ( D ^ 2 ) ) )   &    |- ( ph -> P || ( ( C x. B ) + ( A x. D ) ) )   =>    |- ( ph -> N e. S )
Theorem	2sqlem4 16359	Lemma for 2sqlem5 16360. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- ( ph -> ( N x. P ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )   &    |- ( ph -> P = ( ( C ^ 2 ) + ( D ^ 2 ) ) )   =>    |- ( ph -> N e. S )
Theorem	2sqlem5 16360	Lemma for 2sq . If a number that is a sum of two squares is divisible by a prime that is a sum of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( N x. P ) e. S )   &    |- ( ph -> P e. S )   =>    |- ( ph -> N e. S )
Theorem	2sqlem6 16361*	Lemma for 2sq . If a number that is a sum of two squares is divisible by a number whose prime divisors are all sums of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> A. p e. Prime ( p || B -> p e. S ) )   &    |- ( ph -> ( A x. B ) e. S )   =>    |- ( ph -> A e. S )
Theorem	2sqlem7 16362*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   =>    |- Y C_ ( S i^i NN )
Theorem	2sqlem8a 16363*	Lemma for 2sqlem8 16364. (Contributed by Mario Carneiro, 4-Jun-2016.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   &    |- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )   &    |- ( ph -> M || N )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> ( A gcd B ) = 1 )   &    |- ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) )   &    |- C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   =>    |- ( ph -> ( C gcd D ) e. NN )
Theorem	2sqlem8 16364*	Lemma for 2sq . (Contributed by Mario Carneiro, 20-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   &    |- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )   &    |- ( ph -> M || N )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> ( A gcd B ) = 1 )   &    |- ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) )   &    |- C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- E = ( C / ( C gcd D ) )   &    |- F = ( D / ( C gcd D ) )   =>    |- ( ph -> M e. S )
Theorem	2sqlem9 16365*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   &    |- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )   &    |- ( ph -> M || N )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. Y )   =>    |- ( ph -> M e. S )
Theorem	2sqlem10 16366*	Lemma for 2sq . Every factor of a "proper" sum of two squares (where the summands are coprime) is a sum of two squares. (Contributed by Mario Carneiro, 19-Jun-2015.)
|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )   &    |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }   =>    |- ( ( A e. Y /\ B e. NN /\ B || A ) -> B e. S )
PART 12  GRAPH THEORY
12.1  Vertices and edges
12.1.1  The edge function extractor for extensible structures
Syntax	cedgf 16367	Extend class notation with an edge function.
class .ef
Definition	df-edgf 16368	Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020.) Use its index-independent form edgfid 16369 instead. (New usage is discouraged.)
|- .ef = Slot ; 1 8
Theorem	edgfid 16369	Utility theorem: index-independent form of df-edgf 16368. (Contributed by AV, 16-Nov-2021.)
|- .ef = Slot (.ef ` ndx )
Theorem	edgfndx 16370	Index value of the df-edgf 16368 slot. (Contributed by AV, 13-Oct-2024.) (New usage is discouraged.)
|- (.ef ` ndx ) = ; 1 8
Theorem	edgfndxnn 16371	The index value of the edge function extractor is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 13-Oct-2024.)
|- (.ef ` ndx ) e. NN
Theorem	edgfndxid 16372	The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 28-Oct-2024.)
|- ( G e. V -> (.ef ` G ) = ( G ` (.ef ` ndx ) ) )
Theorem	basendxltedgfndx 16373	The index value of the Base slot is less than the index value of the .ef slot. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 30-Oct-2024.)
|- ( Base ` ndx ) < (.ef ` ndx )
Theorem	basendxnedgfndx 16374	The slots Base and .ef are different. (Contributed by AV, 21-Sep-2020.)
|- ( Base ` ndx ) =/= (.ef ` ndx )
12.1.2  Vertices and indexed edges
12.1.2.1  Definitions and basic properties
Syntax	cvtx 16375	Extend class notation with the vertices of "graphs".
class Vtx
Syntax	ciedg 16376	Extend class notation with the indexed edges of "graphs".
class iEdg
Definition	df-vtx 16377	Define the function mapping a graph to the set of its vertices. This definition is very general: It defines the set of vertices for any ordered pair as its first component, and for any other class as its "base set". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure representing a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 20-Sep-2020.)
|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
Definition	df-iedg 16378	Define the function mapping a graph to its indexed edges. This definition is very general: It defines the indexed edges for any ordered pair as its second component, and for any other class as its "edge function". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure (containing a slot for "edge functions") representing a graph. (Contributed by AV, 20-Sep-2020.)
|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
Theorem	vtxvalg 16379	The set of vertices of a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.)
|- ( G e. V -> (Vtx ` G ) = if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) ) )
Theorem	iedgvalg 16380	The set of indexed edges of a graph. (Contributed by AV, 21-Sep-2020.)
|- ( G e. V -> (iEdg ` G ) = if ( G e. ( _V X. _V ) , ( 2nd ` G ) , (.ef ` G ) ) )
Theorem	vtxex 16381	Applying the vertex function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
|- ( G e. V -> (Vtx ` G ) e. _V )
Theorem	iedgex 16382	Applying the indexed edge function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
|- ( G e. V -> (iEdg ` G ) e. _V )
Theorem	1vgrex 16383	A graph with at least one vertex is a set. (Contributed by AV, 2-Mar-2021.)
|- V = (Vtx ` G )   =>    |- ( N e. V -> G e. _V )
12.1.2.2  The vertices and edges of a graph represented as ordered pair
Theorem	opvtxval 16384	The set of vertices of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.)
|- ( G e. ( _V X. _V ) -> (Vtx ` G ) = ( 1st ` G ) )
Theorem	opvtxfv 16385	The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020.)
|- ( ( V e. X /\ E e. Y ) -> (Vtx ` <. V , E >. ) = V )
Theorem	opvtxov 16386	The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as operation value. (Contributed by AV, 21-Sep-2020.)
|- ( ( V e. X /\ E e. Y ) -> ( VVtx E ) = V )
Theorem	opiedgval 16387	The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 21-Sep-2020.)
|- ( G e. ( _V X. _V ) -> (iEdg ` G ) = ( 2nd ` G ) )
Theorem	opiedgfv 16388	The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020.)
|- ( ( V e. X /\ E e. Y ) -> (iEdg ` <. V , E >. ) = E )
Theorem	opiedgov 16389	The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as operation value. (Contributed by AV, 21-Sep-2020.)
|- ( ( V e. X /\ E e. Y ) -> ( ViEdg E ) = E )
Theorem	opvtxfvi 16390	The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 4-Mar-2021.)
|- V e. _V   &    |- E e. _V   =>    |- (Vtx ` <. V , E >. ) = V
Theorem	opiedgfvi 16391	The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 4-Mar-2021.)
|- V e. _V   &    |- E e. _V   =>    |- (iEdg ` <. V , E >. ) = E
12.1.2.3  The vertices and edges of a graph represented as extensible structure
Theorem	funvtxdm2domval 16392	The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by Jim Kingdon, 11-Dec-2025.)
|- ( ( G e. V /\ Fun ( G \ { (/) } ) /\ 2o ~<_ dom G ) -> (Vtx ` G ) = ( Base ` G ) )
Theorem	funiedgdm2domval 16393	The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by Jim Kingdon, 11-Dec-2025.)
|- ( ( G e. V /\ Fun ( G \ { (/) } ) /\ 2o ~<_ dom G ) -> (iEdg ` G ) = (.ef ` G ) )
Theorem	funvtxdm2vald 16394	The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 11-Dec-2025.)
|- A e. _V   &    |- B e. _V   &    |- ( ph -> G e. X )   &    |- ( ph -> Fun ( G \ { (/) } ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> { A , B } C_ dom G )   =>    |- ( ph -> (Vtx ` G ) = ( Base ` G ) )
Theorem	funiedgdm2vald 16395	The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 12-Dec-2025.)
|- A e. _V   &    |- B e. _V   &    |- ( ph -> G e. X )   &    |- ( ph -> Fun ( G \ { (/) } ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> { A , B } C_ dom G )   =>    |- ( ph -> (iEdg ` G ) = (.ef ` G ) )
Theorem	funvtxval0d 16396	The set of vertices of an extensible structure with a base set and (at least) another slot. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.)
|- S e. _V   &    |- ( ph -> G e. V )   &    |- ( ph -> Fun ( G \ { (/) } ) )   &    |- ( ph -> S =/= ( Base ` ndx ) )   &    |- ( ph -> { ( Base ` ndx ) , S } C_ dom G )   =>    |- ( ph -> (Vtx ` G ) = ( Base ` G ) )
Theorem	basvtxval2dom 16397	The set of vertices of a graph represented as an extensible structure with the set of vertices as base set. (Contributed by AV, 14-Oct-2020.) (Revised by AV, 12-Nov-2021.)
|- ( ph -> G Struct X )   &    |- ( ph -> 2o ~<_ dom G )   &    |- ( ph -> V e. Y )   &    |- ( ph -> <. ( Base ` ndx ) , V >. e. G )   =>    |- ( ph -> (Vtx ` G ) = V )
Theorem	edgfiedgval2dom 16398	The set of indexed edges of a graph represented as an extensible structure with the indexed edges in the slot for edge functions. (Contributed by AV, 14-Oct-2020.) (Revised by AV, 12-Nov-2021.)
|- ( ph -> G Struct X )   &    |- ( ph -> 2o ~<_ dom G )   &    |- ( ph -> E e. Y )   &    |- ( ph -> <. (.ef ` ndx ) , E >. e. G )   =>    |- ( ph -> (iEdg ` G ) = E )
Theorem	funvtxvalg 16399	The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.)
|- ( ( G e. V /\ Fun ( G \ { (/) } ) /\ { ( Base ` ndx ) , (.ef ` ndx ) } C_ dom G ) -> (Vtx ` G ) = ( Base ` G ) )
Theorem	funiedgvalg 16400	The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.)
|- ( ( G e. V /\ Fun ( G \ { (/) } ) /\ { ( Base ` ndx ) , (.ef ` ndx ) } C_ dom G ) -> (iEdg ` G ) = (.ef ` G ) )