P. 157 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15601-15700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lgsquad 15601	The Law of Quadratic Reciprocity, see also theorem 9.8 in [ApostolNT] p. 185. If 𝑃 and 𝑄 are distinct odd primes, then the product of the Legendre symbols (𝑃 /L 𝑄) and (𝑄 /L 𝑃) is the parity of ((𝑃 − 1) / 2) · ((𝑄 − 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.)
⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑄 ∈ (ℙ ∖ {2}) ∧ 𝑃 ≠ 𝑄) → ((𝑃 /L 𝑄) · (𝑄 /L 𝑃)) = (-1↑(((𝑃 − 1) / 2) · ((𝑄 − 1) / 2))))
Theorem	lgsquad2lem1 15602	Lemma for lgsquad2 15604. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑁)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = 𝑀)    &   ⊢ (𝜑 → ((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) = (-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))))    &   ⊢ (𝜑 → ((𝐵 /L 𝑁) · (𝑁 /L 𝐵)) = (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2))))    ⇒   ⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))))
Theorem	lgsquad2lem2 15603*	Lemma for lgsquad2 15604. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑁)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    &   ⊢ ((𝜑 ∧ (𝑚 ∈ (ℙ ∖ {2}) ∧ (𝑚 gcd 𝑁) = 1)) → ((𝑚 /L 𝑁) · (𝑁 /L 𝑚)) = (-1↑(((𝑚 − 1) / 2) · ((𝑁 − 1) / 2))))    &   ⊢ (𝜓 ↔ ∀𝑥 ∈ (1...𝑘)((𝑥 gcd (2 · 𝑁)) = 1 → ((𝑥 /L 𝑁) · (𝑁 /L 𝑥)) = (-1↑(((𝑥 − 1) / 2) · ((𝑁 − 1) / 2)))))    ⇒   ⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))))
Theorem	lgsquad2 15604	Extend lgsquad 15601 to coprime odd integers (the domain of the Jacobi symbol). (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑁)    &   ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)    ⇒   ⊢ (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))))
Theorem	lgsquad3 15605	Extend lgsquad2 15604 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (((𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀) ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) → (𝑀 /L 𝑁) = ((-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) · (𝑁 /L 𝑀)))
Theorem	m1lgs 15606	The first supplement to the law of quadratic reciprocity. Negative one is a square mod an odd prime 𝑃 iff 𝑃≡1 (mod 4). See first case of theorem 9.4 in [ApostolNT] p. 181. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /L 𝑃) = 1 ↔ (𝑃 mod 4) = 1))
Theorem	2lgslem1a1 15607*	Lemma 1 for 2lgslem1a 15609. (Contributed by AV, 16-Jun-2021.)
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → ∀𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑖 · 2) = ((𝑖 · 2) mod 𝑃))
Theorem	2lgslem1a2 15608	Lemma 2 for 2lgslem1a 15609. (Contributed by AV, 18-Jun-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ) → ((⌊‘(𝑁 / 4)) < 𝐼 ↔ (𝑁 / 2) < (𝐼 · 2)))
Theorem	2lgslem1a 15609*	Lemma 1 for 2lgslem1 15612. (Contributed by AV, 18-Jun-2021.)
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))} = {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)})
Theorem	2lgslem1b 15610*	Lemma 2 for 2lgslem1 15612. (Contributed by AV, 18-Jun-2021.)
⊢ 𝐼 = (𝐴...𝐵)    &   ⊢ 𝐹 = (𝑗 ∈ 𝐼 ↦ (𝑗 · 2))    ⇒   ⊢ 𝐹:𝐼–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)}
Theorem	2lgslem1c 15611	Lemma 3 for 2lgslem1 15612. (Contributed by AV, 19-Jun-2021.)
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2))
Theorem	2lgslem1 15612*	Lemma 1 for 2lgs 15625. (Contributed by AV, 19-Jun-2021.)
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → (♯‘{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))}) = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4))))
Theorem	2lgslem2 15613	Lemma 2 for 2lgs 15625. (Contributed by AV, 20-Jun-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃) → 𝑁 ∈ ℤ)
Theorem	2lgslem3a 15614	Lemma for 2lgslem3a1 15618. (Contributed by AV, 14-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 1)) → 𝑁 = (2 · 𝐾))
Theorem	2lgslem3b 15615	Lemma for 2lgslem3b1 15619. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 3)) → 𝑁 = ((2 · 𝐾) + 1))
Theorem	2lgslem3c 15616	Lemma for 2lgslem3c1 15620. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 5)) → 𝑁 = ((2 · 𝐾) + 1))
Theorem	2lgslem3d 15617	Lemma for 2lgslem3d1 15621. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑃 = ((8 · 𝐾) + 7)) → 𝑁 = ((2 · 𝐾) + 2))
Theorem	2lgslem3a1 15618	Lemma 1 for 2lgslem3 15622. (Contributed by AV, 15-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 1) → (𝑁 mod 2) = 0)
Theorem	2lgslem3b1 15619	Lemma 2 for 2lgslem3 15622. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 3) → (𝑁 mod 2) = 1)
Theorem	2lgslem3c1 15620	Lemma 3 for 2lgslem3 15622. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 5) → (𝑁 mod 2) = 1)
Theorem	2lgslem3d1 15621	Lemma 4 for 2lgslem3 15622. (Contributed by AV, 15-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ (𝑃 mod 8) = 7) → (𝑁 mod 2) = 0)
Theorem	2lgslem3 15622	Lemma 3 for 2lgs 15625. (Contributed by AV, 16-Jul-2021.)
⊢ 𝑁 = (((𝑃 − 1) / 2) − (⌊‘(𝑃 / 4)))    ⇒   ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑁 mod 2) = if((𝑃 mod 8) ∈ {1, 7}, 0, 1))
Theorem	2lgs2 15623	The Legendre symbol for 2 at 2 is 0. (Contributed by AV, 20-Jun-2021.)
⊢ (2 /L 2) = 0
Theorem	2lgslem4 15624	Lemma 4 for 2lgs 15625: special case of 2lgs 15625 for 𝑃 = 2. (Contributed by AV, 20-Jun-2021.)
⊢ ((2 /L 2) = 1 ↔ (2 mod 8) ∈ {1, 7})
Theorem	2lgs 15625	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 𝑃 iff 𝑃≡±1 (mod 8), see first case of theorem 9.5 in [ApostolNT] p. 181. This theorem justifies our definition of (𝑁 /L 2) (lgs2 15538) to some degree, by demanding that reciprocity extend to the case 𝑄 = 2. (Proposed by Mario Carneiro, 19-Jun-2015.) (Contributed by AV, 16-Jul-2021.)
⊢ (𝑃 ∈ ℙ → ((2 /L 𝑃) = 1 ↔ (𝑃 mod 8) ∈ {1, 7}))
Theorem	2lgsoddprmlem1 15626	Lemma 1 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 = ((8 · 𝐴) + 𝐵)) → (((𝑁↑2) − 1) / 8) = (((8 · (𝐴↑2)) + (2 · (𝐴 · 𝐵))) + (((𝐵↑2) − 1) / 8)))
Theorem	2lgsoddprmlem2 15627	Lemma 2 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((𝑅↑2) − 1) / 8)))
Theorem	2lgsoddprmlem3a 15628	Lemma 1 for 2lgsoddprmlem3 15632. (Contributed by AV, 20-Jul-2021.)
⊢ (((1↑2) − 1) / 8) = 0
Theorem	2lgsoddprmlem3b 15629	Lemma 2 for 2lgsoddprmlem3 15632. (Contributed by AV, 20-Jul-2021.)
⊢ (((3↑2) − 1) / 8) = 1
Theorem	2lgsoddprmlem3c 15630	Lemma 3 for 2lgsoddprmlem3 15632. (Contributed by AV, 20-Jul-2021.)
⊢ (((5↑2) − 1) / 8) = 3
Theorem	2lgsoddprmlem3d 15631	Lemma 4 for 2lgsoddprmlem3 15632. (Contributed by AV, 20-Jul-2021.)
⊢ (((7↑2) − 1) / 8) = (2 · 3)
Theorem	2lgsoddprmlem3 15632	Lemma 3 for 2lgsoddprm . (Contributed by AV, 20-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑅↑2) − 1) / 8) ↔ 𝑅 ∈ {1, 7}))
Theorem	2lgsoddprmlem4 15633	Lemma 4 for 2lgsoddprm . (Contributed by AV, 20-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ (𝑁 mod 8) ∈ {1, 7}))
Theorem	2lgsoddprm 15634	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 𝑃) = -1^(((P^2)-1)/8) ). (Contributed by AV, 20-Jul-2021.)
⊢ (𝑃 ∈ (ℙ ∖ {2}) → (2 /L 𝑃) = (-1↑(((𝑃↑2) − 1) / 8)))
11.3.7  All primes 4n+1 are the sum of two squares
Theorem	2sqlem1 15635*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ[i] 𝐴 = ((abs‘𝑥)↑2))
Theorem	2sqlem2 15636*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝐴 = ((𝑥↑2) + (𝑦↑2)))
Theorem	mul2sq 15637	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.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 · 𝐵) ∈ 𝑆)
Theorem	2sqlem3 15638	Lemma for 2sqlem5 15640. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2)))    &   ⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2)))    &   ⊢ (𝜑 → 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷)))    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝑆)
Theorem	2sqlem4 15639	Lemma for 2sqlem5 15640. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2)))    &   ⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2)))    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝑆)
Theorem	2sqlem5 15640	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.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (𝑁 · 𝑃) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝑆)
Theorem	2sqlem6 15641*	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.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆))    &   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑆)
Theorem	2sqlem7 15642*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}    ⇒   ⊢ 𝑌 ⊆ (𝑆 ∩ ℕ)
Theorem	2sqlem8a 15643*	Lemma for 2sqlem8 15644. (Contributed by Mario Carneiro, 4-Jun-2016.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}    &   ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))    &   ⊢ (𝜑 → 𝑀 ∥ 𝑁)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2)))    &   ⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ)
Theorem	2sqlem8 15644*	Lemma for 2sq . (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}    &   ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))    &   ⊢ (𝜑 → 𝑀 ∥ 𝑁)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2)))    &   ⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐸 = (𝐶 / (𝐶 gcd 𝐷))    &   ⊢ 𝐹 = (𝐷 / (𝐶 gcd 𝐷))    ⇒   ⊢ (𝜑 → 𝑀 ∈ 𝑆)
Theorem	2sqlem9 15645*	Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}    &   ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))    &   ⊢ (𝜑 → 𝑀 ∥ 𝑁)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑌)    ⇒   ⊢ (𝜑 → 𝑀 ∈ 𝑆)
Theorem	2sqlem10 15646*	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.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}    ⇒   ⊢ ((𝐴 ∈ 𝑌 ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴) → 𝐵 ∈ 𝑆)
PART 12  GRAPH THEORY
12.1  Vertices and edges
12.1.1  The edge function extractor for extensible structures
Syntax	cedgf 15647	Extend class notation with an edge function.
class .ef
Definition	df-edgf 15648	Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020.) Use its index-independent form edgfid 15649 instead. (New usage is discouraged.)
⊢ .ef = Slot ;18
Theorem	edgfid 15649	Utility theorem: index-independent form of df-edgf 15648. (Contributed by AV, 16-Nov-2021.)
⊢ .ef = Slot (.ef‘ndx)
Theorem	edgfndx 15650	Index value of the df-edgf 15648 slot. (Contributed by AV, 13-Oct-2024.) (New usage is discouraged.)
⊢ (.ef‘ndx) = ;18
Theorem	edgfndxnn 15651	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) ∈ ℕ
Theorem	edgfndxid 15652	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.)
⊢ (𝐺 ∈ 𝑉 → (.ef‘𝐺) = (𝐺‘(.ef‘ndx)))
Theorem	basendxltedgfndx 15653	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 15654	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 15655	Extend class notation with the vertices of "graphs".
class Vtx
Syntax	ciedg 15656	Extend class notation with the indexed edges of "graphs".
class iEdg
Definition	df-vtx 15657	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 = (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (1st ‘𝑔), (Base‘𝑔)))
Definition	df-iedg 15658	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 = (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (2nd ‘𝑔), (.ef‘𝑔)))
Theorem	vtxvalg 15659	The set of vertices of a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.)
⊢ (𝐺 ∈ 𝑉 → (Vtx‘𝐺) = if(𝐺 ∈ (V × V), (1st ‘𝐺), (Base‘𝐺)))
Theorem	iedgvalg 15660	The set of indexed edges of a graph. (Contributed by AV, 21-Sep-2020.)
⊢ (𝐺 ∈ 𝑉 → (iEdg‘𝐺) = if(𝐺 ∈ (V × V), (2nd ‘𝐺), (.ef‘𝐺)))
Theorem	vtxex 15661	Applying the vertex function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
⊢ (𝐺 ∈ 𝑉 → (Vtx‘𝐺) ∈ V)
Theorem	iedgex 15662	Applying the indexed edge function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
⊢ (𝐺 ∈ 𝑉 → (iEdg‘𝐺) ∈ V)
Theorem	1vgrex 15663	A graph with at least one vertex is a set. (Contributed by AV, 2-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝐺 ∈ V)
12.1.2.2  The vertices and edges of a graph represented as ordered pair
Theorem	opvtxval 15664	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.)
⊢ (𝐺 ∈ (V × V) → (Vtx‘𝐺) = (1st ‘𝐺))
Theorem	opvtxfv 15665	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.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = 𝑉)
Theorem	opvtxov 15666	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.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉Vtx𝐸) = 𝑉)
Theorem	opiedgval 15667	The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 21-Sep-2020.)
⊢ (𝐺 ∈ (V × V) → (iEdg‘𝐺) = (2nd ‘𝐺))
Theorem	opiedgfv 15668	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.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘⟨𝑉, 𝐸⟩) = 𝐸)
Theorem	opiedgov 15669	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.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉iEdg𝐸) = 𝐸)
Theorem	opvtxfvi 15670	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    &   ⊢ 𝐸 ∈ V    ⇒   ⊢ (Vtx‘⟨𝑉, 𝐸⟩) = 𝑉
Theorem	opiedgfvi 15671	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    &   ⊢ 𝐸 ∈ V    ⇒   ⊢ (iEdg‘⟨𝑉, 𝐸⟩) = 𝐸
12.1.2.3  The vertices and edges of a graph represented as extensible structure
Theorem	funvtxdm2domval 15672	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.)
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅}) ∧ 2o ≼ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺))
Theorem	funiedgdm2domval 15673	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.)
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅}) ∧ 2o ≼ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺))
Theorem	funvtxdm2vald 15674	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.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ (𝜑 → Fun (𝐺 ∖ {∅}))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → {𝐴, 𝐵} ⊆ dom 𝐺)    ⇒   ⊢ (𝜑 → (Vtx‘𝐺) = (Base‘𝐺))
Theorem	funiedgdm2vald 15675	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.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ (𝜑 → Fun (𝐺 ∖ {∅}))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → {𝐴, 𝐵} ⊆ dom 𝐺)    ⇒   ⊢ (𝜑 → (iEdg‘𝐺) = (.ef‘𝐺))
Theorem	funvtxval0d 15676	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.)
⊢ 𝑆 ∈ V    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → Fun (𝐺 ∖ {∅}))    &   ⊢ (𝜑 → 𝑆 ≠ (Base‘ndx))    &   ⊢ (𝜑 → {(Base‘ndx), 𝑆} ⊆ dom 𝐺)    ⇒   ⊢ (𝜑 → (Vtx‘𝐺) = (Base‘𝐺))
Theorem	basvtxval2dom 15677	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.)
⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → 2o ≼ dom 𝐺)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → ⟨(Base‘ndx), 𝑉⟩ ∈ 𝐺)    ⇒   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)
Theorem	edgfiedgval2dom 15678	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.)
⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → 2o ≼ dom 𝐺)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑌)    &   ⊢ (𝜑 → ⟨(.ef‘ndx), 𝐸⟩ ∈ 𝐺)    ⇒   ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸)
Theorem	funvtxvalg 15679	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.)
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺))
Theorem	funiedgvalg 15680	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.)
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺))
Theorem	struct2slots2dom 15681	There are at least two elements in an extensible structure with a base set and another slot. (Contributed by AV, 23-Sep-2020.) (Revised by AV, 12-Nov-2021.)
⊢ 𝑆 ∈ ℕ    &   ⊢ (Base‘ndx) < 𝑆    &   ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨𝑆, 𝐸⟩}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 2o ≼ dom 𝐺)
Theorem	structvtxval 15682	The set of vertices of an extensible structure with a base set and another slot. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.)
⊢ 𝑆 ∈ ℕ    &   ⊢ (Base‘ndx) < 𝑆    &   ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨𝑆, 𝐸⟩}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘𝐺) = 𝑉)
Theorem	structiedg0val 15683	The set of indexed edges of an extensible structure with a base set and another slot not being the slot for edge functions is empty. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.)
⊢ 𝑆 ∈ ℕ    &   ⊢ (Base‘ndx) < 𝑆    &   ⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨𝑆, 𝐸⟩}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → (iEdg‘𝐺) = ∅)
Theorem	structgr2slots2dom 15684	There are at least two elements in a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.)
⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑍)    &   ⊢ (𝜑 → {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⊆ 𝐺)    ⇒   ⊢ (𝜑 → 2o ≼ dom 𝐺)
Theorem	structgrssvtx 15685	The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.)
⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑍)    &   ⊢ (𝜑 → {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⊆ 𝐺)    ⇒   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)
Theorem	structgrssiedg 15686	The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.)
⊢ (𝜑 → 𝐺 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑍)    &   ⊢ (𝜑 → {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩} ⊆ 𝐺)    ⇒   ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸)
Theorem	struct2grstrg 15687	A graph represented as an extensible structure with vertices as base set and indexed edges is actually an extensible structure. (Contributed by AV, 23-Nov-2020.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐺 Struct ⟨(Base‘ndx), (.ef‘ndx)⟩)
Theorem	struct2grvtx 15688	The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘𝐺) = 𝑉)
Theorem	struct2griedg 15689	The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘𝐺) = 𝐸)
Theorem	gropd 15690*	If any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property 𝜓, then the ordered pair ⟨𝑉, 𝐸⟩ of the set of vertices and the set of edges (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. (Contributed by AV, 11-Oct-2020.)
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝜓))    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    ⇒   ⊢ (𝜑 → [⟨𝑉, 𝐸⟩ / 𝑔]𝜓)
Theorem	grstructd2dom 15691*	If any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property 𝜓, then any structure with base set 𝑉 and value 𝐸 in the slot for edge functions (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.)
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝜓))    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    &   ⊢ (𝜑 → Fun (𝑆 ∖ {∅}))    &   ⊢ (𝜑 → 2o ≼ dom 𝑆)    &   ⊢ (𝜑 → (Base‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (.ef‘𝑆) = 𝐸)    ⇒   ⊢ (𝜑 → [𝑆 / 𝑔]𝜓)
Theorem	gropeld 15692*	If any representation of a graph with vertices 𝑉 and edges 𝐸 is an element of an arbitrary class 𝐶, then the ordered pair ⟨𝑉, 𝐸⟩ of the set of vertices and the set of edges (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) is an element of this class 𝐶. (Contributed by AV, 11-Oct-2020.)
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝑔 ∈ 𝐶))    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ⟨𝑉, 𝐸⟩ ∈ 𝐶)
Theorem	grstructeld2dom 15693*	If any representation of a graph with vertices 𝑉 and edges 𝐸 is an element of an arbitrary class 𝐶, then any structure with base set 𝑉 and value 𝐸 in the slot for edge functions (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) is an element of this class 𝐶. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.)
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝑔 ∈ 𝐶))    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    &   ⊢ (𝜑 → Fun (𝑆 ∖ {∅}))    &   ⊢ (𝜑 → 2o ≼ dom 𝑆)    &   ⊢ (𝜑 → (Base‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (.ef‘𝑆) = 𝐸)    ⇒   ⊢ (𝜑 → 𝑆 ∈ 𝐶)
12.1.2.4  Degenerated cases of representations of graphs
Theorem	vtxval0 15694	Degenerated case 1 for vertices: The set of vertices of the empty set is the empty set. (Contributed by AV, 24-Sep-2020.)
⊢ (Vtx‘∅) = ∅
Theorem	iedgval0 15695	Degenerated case 1 for edges: The set of indexed edges of the empty set is the empty set. (Contributed by AV, 24-Sep-2020.)
⊢ (iEdg‘∅) = ∅
Theorem	vtxvalprc 15696	Degenerated case 4 for vertices: The set of vertices of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.)
⊢ (𝐶 ∉ V → (Vtx‘𝐶) = ∅)
Theorem	iedgvalprc 15697	Degenerated case 4 for edges: The set of indexed edges of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.)
⊢ (𝐶 ∉ V → (iEdg‘𝐶) = ∅)
12.1.3  Edges as range of the edge function
Syntax	cedg 15698	Extend class notation with the set of edges (of an undirected simple (hyper-/pseudo-)graph).
class Edg
Definition	df-edg 15699	Define the class of edges of a graph, see also definition "E = E(G)" in section I.1 of [Bollobas] p. 1. This definition is very general: It defines edges of a class as the range of its edge function (which does not even need to be a function). Therefore, this definition could also be used for hypergraphs, pseudographs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. In some cases, this is no problem, so theorems with Edg are meaningful nevertheless. Usually, however, this definition is used only for undirected simple (hyper-/pseudo-)graphs (with or without loops). (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.)
⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
Theorem	edgvalg 15700	The edges of a graph. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) (Revised by AV, 8-Dec-2021.)
⊢ (𝐺 ∈ 𝑉 → (Edg‘𝐺) = ran (iEdg‘𝐺))