P. 362 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36101-36200   *Has distinct variable group(s)

Type	Label	Description
Statement
21.11.18.6  Segment less than or equal to
Syntax	csegle 36101	Declare the constant for the segment less than or equal to relationship.
class Seg≤
Definition	df-segle 36102*	Define the segment length comparison relationship. This relationship expresses that the segment 𝐴𝐵 is no longer than 𝐶𝐷. In this section, we establish various properties of this relationship showing that it is a transitive, reflexive relationship on pairs of points that is substitutive under congruence. Definition 5.4 of [Schwabhauser] p. 41. (Contributed by Scott Fenton, 11-Oct-2013.)
⊢ Seg≤ = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
Theorem	brsegle 36103*	Binary relation form of the segment comparison relationship. (Contributed by Scott Fenton, 11-Oct-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩ Seg≤ ⟨𝐶, 𝐷⟩ ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)))
Theorem	brsegle2 36104*	Alternate characterization of segment comparison. Theorem 5.5 of [Schwabhauser] p. 41-42. (Contributed by Scott Fenton, 11-Oct-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩ Seg≤ ⟨𝐶, 𝐷⟩ ↔ ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)))
Theorem	seglecgr12im 36105	Substitution law for segment comparison under congruence. Theorem 5.6 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.)
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩ ∧ ⟨𝐴, 𝐵⟩ Seg≤ ⟨𝐶, 𝐷⟩) → ⟨𝐸, 𝐹⟩ Seg≤ ⟨𝐺, 𝐻⟩))
Theorem	seglecgr12 36106	Substitution law for segment comparison under congruence. Biconditional version. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩) → (⟨𝐴, 𝐵⟩ Seg≤ ⟨𝐶, 𝐷⟩ ↔ ⟨𝐸, 𝐹⟩ Seg≤ ⟨𝐺, 𝐻⟩)))
Theorem	seglerflx 36107	Segment comparison is reflexive. Theorem 5.7 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ⟨𝐴, 𝐵⟩ Seg≤ ⟨𝐴, 𝐵⟩)
Theorem	seglemin 36108	Any segment is at least as long as a degenerate segment. Theorem 5.11 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ⟨𝐴, 𝐴⟩ Seg≤ ⟨𝐵, 𝐶⟩)
Theorem	segletr 36109	Segment less than is transitive. Theorem 5.8 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 11-Oct-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩ Seg≤ ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ Seg≤ ⟨𝐸, 𝐹⟩) → ⟨𝐴, 𝐵⟩ Seg≤ ⟨𝐸, 𝐹⟩))
Theorem	segleantisym 36110	Antisymmetry law for segment comparison. Theorem 5.9 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩ Seg≤ ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ Seg≤ ⟨𝐴, 𝐵⟩) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩))
Theorem	seglelin 36111	Linearity law for segment comparison. Theorem 5.10 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩ Seg≤ ⟨𝐶, 𝐷⟩ ∨ ⟨𝐶, 𝐷⟩ Seg≤ ⟨𝐴, 𝐵⟩))
Theorem	btwnsegle 36112	If 𝐵 falls between 𝐴 and 𝐶, then 𝐴𝐵 is no longer than 𝐴𝐶. (Contributed by Scott Fenton, 16-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐵 Btwn ⟨𝐴, 𝐶⟩ → ⟨𝐴, 𝐵⟩ Seg≤ ⟨𝐴, 𝐶⟩))
Theorem	colinbtwnle 36113	Given three colinear points 𝐴, 𝐵, and 𝐶, 𝐵 falls in the middle iff the two segments to 𝐵 are no longer than 𝐴𝐶. Theorem 5.12 of [Schwabhauser] p. 42. (Contributed by Scott Fenton, 15-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Colinear ⟨𝐵, 𝐶⟩ → (𝐵 Btwn ⟨𝐴, 𝐶⟩ ↔ (⟨𝐴, 𝐵⟩ Seg≤ ⟨𝐴, 𝐶⟩ ∧ ⟨𝐵, 𝐶⟩ Seg≤ ⟨𝐴, 𝐶⟩))))
21.11.18.7  Outside-of relationship
Syntax	coutsideof 36114	Declare the syntax for the outside of constant.
class OutsideOf
Definition	df-outsideof 36115	The outside of relationship. This relationship expresses that 𝑃, 𝐴, and 𝐵 fall on a line, but 𝑃 is not on the segment 𝐴𝐵. This definition is taken from theorem 6.4 of [Schwabhauser] p. 43, since it requires no dummy variables. (Contributed by Scott Fenton, 17-Oct-2013.)
⊢ OutsideOf = ( Colinear ∖ Btwn )
Theorem	broutsideof 36116	Binary relation form of OutsideOf. Theorem 6.4 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 17-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝑃OutsideOf⟨𝐴, 𝐵⟩ ↔ (𝑃 Colinear ⟨𝐴, 𝐵⟩ ∧ ¬ 𝑃 Btwn ⟨𝐴, 𝐵⟩))
Theorem	broutsideof2 36117	Alternate form of OutsideOf. Definition 6.1 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 17-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝐴, 𝐵⟩ ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn ⟨𝑃, 𝐵⟩ ∨ 𝐵 Btwn ⟨𝑃, 𝐴⟩))))
Theorem	outsidene1 36118	Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝐴, 𝐵⟩ → 𝐴 ≠ 𝑃))
Theorem	outsidene2 36119	Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝐴, 𝐵⟩ → 𝐵 ≠ 𝑃))
Theorem	btwnoutside 36120	A principle linking outsideness to betweenness. Theorem 6.2 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝑃 Btwn ⟨𝐴, 𝐶⟩) → (𝑃 Btwn ⟨𝐵, 𝐶⟩ ↔ 𝑃OutsideOf⟨𝐴, 𝐵⟩)))
Theorem	broutsideof3 36121*	Characterization of outsideness in terms of relationship to a fourth point. Theorem 6.3 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝐴, 𝐵⟩ ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑃 Btwn ⟨𝐵, 𝑐⟩))))
Theorem	outsideofrflx 36122	Reflexivity of outsideness. Theorem 6.5 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐴 ≠ 𝑃 → 𝑃OutsideOf⟨𝐴, 𝐴⟩))
Theorem	outsideofcom 36123	Commutativity law for outsideness. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝐴, 𝐵⟩ ↔ 𝑃OutsideOf⟨𝐵, 𝐴⟩))
Theorem	outsideoftr 36124	Transitivity law for outsideness. Theorem 6.7 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝑃OutsideOf⟨𝐴, 𝐵⟩ ∧ 𝑃OutsideOf⟨𝐵, 𝐶⟩) → 𝑃OutsideOf⟨𝐴, 𝐶⟩))
Theorem	outsideofeq 36125	Uniqueness law for OutsideOf. Analogue of segconeq 36005. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁) ∧ 𝑌 ∈ (𝔼‘𝑁))) → (((𝐴OutsideOf⟨𝑋, 𝑅⟩ ∧ ⟨𝐴, 𝑋⟩Cgr⟨𝐵, 𝐶⟩) ∧ (𝐴OutsideOf⟨𝑌, 𝑅⟩ ∧ ⟨𝐴, 𝑌⟩Cgr⟨𝐵, 𝐶⟩)) → 𝑋 = 𝑌))
Theorem	outsideofeu 36126*	Given a nondegenerate ray, there is a unique point congruent to the segment 𝐵𝐶 lying on the ray 𝐴𝑅. Theorem 6.11 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 23-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) → ∃!𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf⟨𝑥, 𝑅⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐵, 𝐶⟩)))
Theorem	outsidele 36127	Relate OutsideOf to Seg≤. Theorem 6.13 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝐴, 𝐵⟩ → (⟨𝑃, 𝐴⟩ Seg≤ ⟨𝑃, 𝐵⟩ ↔ 𝐴 Btwn ⟨𝑃, 𝐵⟩)))
Theorem	outsideofcol 36128	Outside of implies colinearity. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝑃OutsideOf⟨𝑄, 𝑅⟩ → 𝑃 Colinear ⟨𝑄, 𝑅⟩)
21.11.18.8  Lines and Rays
Syntax	cline2 36129	Declare the constant for the line function.
class Line
Syntax	cray 36130	Declare the constant for the ray function.
class Ray
Syntax	clines2 36131	Declare the constant for the set of all lines.
class LinesEE
Definition	df-line2 36132*	Define the Line function. This function generates the line passing through the distinct points 𝑎 and 𝑏. Adapted from definition 6.14 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 25-Oct-2013.)
⊢ Line = {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}
Definition	df-ray 36133*	Define the Ray function. This function generates the set of all points that lie on the ray starting at 𝑝 and passing through 𝑎. Definition 6.8 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 21-Oct-2013.)
⊢ Ray = {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})}
Definition	df-lines2 36134	Define the set of all lines. Definition 6.14, part 2 of [Schwabhauser] p. 45. See ellines 36147 for membership. (Contributed by Scott Fenton, 28-Oct-2013.)
⊢ LinesEE = ran Line
Theorem	funray 36135	Show that the Ray relationship is a function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Fun Ray
Theorem	fvray 36136*	Calculate the value of the Ray function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴)) → (𝑃Ray𝐴) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})
Theorem	funline 36137	Show that the Line relationship is a function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Fun Line
Theorem	linedegen 36138	When Line is applied with the same argument, the result is the empty set. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝐴Line𝐴) = ∅
Theorem	fvline 36139*	Calculate the value of the Line function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = {𝑥 ∣ 𝑥 Colinear ⟨𝐴, 𝐵⟩})
Theorem	liness 36140	A line is a subset of the space its two points lie in. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) ⊆ (𝔼‘𝑁))
Theorem	fvline2 36141*	Alternate definition of a line. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝐴, 𝐵⟩})
Theorem	lineunray 36142	A line is composed of a point and the two rays emerging from it. Theorem 6.15 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 Btwn ⟨𝑄, 𝑅⟩ → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅))))
Theorem	lineelsb2 36143	If 𝑆 lies on 𝑃𝑄, then 𝑃𝑄 = 𝑃𝑆. Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑆 ∈ (𝑃Line𝑄) → (𝑃Line𝑄) = (𝑃Line𝑆)))
Theorem	linerflx1 36144	Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → 𝑃 ∈ (𝑃Line𝑄))
Theorem	linecom 36145	Commutativity law for lines. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Line𝑄) = (𝑄Line𝑃))
Theorem	linerflx2 36146	Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → 𝑄 ∈ (𝑃Line𝑄))
Theorem	ellines 36147*	Membership in the set of all lines. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝐴 ∈ LinesEE ↔ ∃𝑛 ∈ ℕ ∃𝑝 ∈ (𝔼‘𝑛)∃𝑞 ∈ (𝔼‘𝑛)(𝑝 ≠ 𝑞 ∧ 𝐴 = (𝑝Line𝑞)))
Theorem	linethru 36148	If 𝐴 is a line containing two distinct points 𝑃 and 𝑄, then 𝐴 is the line through 𝑃 and 𝑄. Theorem 6.18 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ LinesEE ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝐴 = (𝑃Line𝑄))
Theorem	hilbert1.1 36149*	There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → ∃𝑥 ∈ LinesEE (𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥))
Theorem	hilbert1.2 36150*	There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by NM, 17-Jun-2017.)
⊢ (𝑃 ≠ 𝑄 → ∃*𝑥 ∈ LinesEE (𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥))
Theorem	linethrueu 36151*	There is a unique line going through any two distinct points. Theorem 6.19 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → ∃!𝑥 ∈ LinesEE (𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥))
Theorem	lineintmo 36152*	Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ LinesEE ∧ 𝐵 ∈ LinesEE ∧ 𝐴 ≠ 𝐵) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
21.11.19  Forward difference
Syntax	cfwddif 36153	Declare the syntax for the forward difference operator.
class △
Definition	df-fwddif 36154*	Define the forward difference operator. This is a discrete analogue of the derivative operator. Definition 2.42 of [GramKnuthPat], p. 47. (Contributed by Scott Fenton, 18-May-2020.)
⊢ △ = (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥))))
Syntax	cfwddifn 36155	Declare the syntax for the nth forward difference operator.
class △n
Definition	df-fwddifn 36156*	Define the nth forward difference operator. This works out to be the forward difference operator iterated 𝑛 times. (Contributed by Scott Fenton, 28-May-2020.)
⊢ △n = (𝑛 ∈ ℕ0, 𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))))
Theorem	fwddifval 36157	Calculate the value of the forward difference operator at a point. (Contributed by Scott Fenton, 18-May-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑋 + 1) ∈ 𝐴)    ⇒   ⊢ (𝜑 → (( △ ‘𝐹)‘𝑋) = ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋)))
Theorem	fwddifnval 36158*	The value of the forward difference operator at a point. (Contributed by Scott Fenton, 28-May-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + 𝑘) ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑁 △n 𝐹)‘𝑋) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))
Theorem	fwddifn0 36159	The value of the n-iterated forward difference operator at zero is just the function value. (Contributed by Scott Fenton, 28-May-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((0 △n 𝐹)‘𝑋) = (𝐹‘𝑋))
Theorem	fwddifnp1 36160*	The value of the n-iterated forward difference at a successor. (Contributed by Scott Fenton, 28-May-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑋 + 𝑘) ∈ 𝐴)    ⇒   ⊢ (𝜑 → (((𝑁 + 1) △n 𝐹)‘𝑋) = (((𝑁 △n 𝐹)‘(𝑋 + 1)) − ((𝑁 △n 𝐹)‘𝑋)))
21.11.20  Rank theorems
Theorem	rankung 36161	The rank of the union of two sets. Closed form of rankun 9816. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (rank‘(𝐴 ∪ 𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵)))
Theorem	ranksng 36162	The rank of a singleton. Closed form of ranksn 9814. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ (𝐴 ∈ 𝑉 → (rank‘{𝐴}) = suc (rank‘𝐴))
Theorem	rankelg 36163	The membership relation is inherited by the rank function. Closed form of rankel 9799. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝐵) → (rank‘𝐴) ∈ (rank‘𝐵))
Theorem	rankpwg 36164	The rank of a power set. Closed form of rankpw 9803. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ (𝐴 ∈ 𝑉 → (rank‘𝒫 𝐴) = suc (rank‘𝐴))
Theorem	rank0 36165	The rank of the empty set is ∅. (Contributed by Scott Fenton, 17-Jul-2015.)
⊢ (rank‘∅) = ∅
Theorem	rankeq1o 36166	The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.)
⊢ ((rank‘𝐴) = 1o ↔ 𝐴 = {∅})
21.11.21  Hereditarily Finite Sets
Syntax	chf 36167	The constant Hf is a class.
class Hf
Definition	df-hf 36168	Define the hereditarily finite sets. These are the finite sets whose elements are finite, and so forth. (Contributed by Scott Fenton, 9-Jul-2015.)
⊢ Hf = ∪ (𝑅1 “ ω)
Theorem	elhf 36169*	Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015.)
⊢ (𝐴 ∈ Hf ↔ ∃𝑥 ∈ ω 𝐴 ∈ (𝑅1‘𝑥))
Theorem	elhf2 36170	Alternate form of membership in the hereditarily finite sets. (Contributed by Scott Fenton, 13-Jul-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Hf ↔ (rank‘𝐴) ∈ ω)
Theorem	elhf2g 36171	Hereditarily finiteness via rank. Closed form of elhf2 36170. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Hf ↔ (rank‘𝐴) ∈ ω))
Theorem	0hf 36172	The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015.)
⊢ ∅ ∈ Hf
Theorem	hfun 36173	The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ 𝐵) ∈ Hf )
Theorem	hfsn 36174	The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ (𝐴 ∈ Hf → {𝐴} ∈ Hf )
Theorem	hfadj 36175	Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ {𝐵}) ∈ Hf )
Theorem	hfelhf 36176	Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ Hf ) → 𝐴 ∈ Hf )
Theorem	hftr 36177	The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ Tr Hf
Theorem	hfext 36178*	Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ Hf (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)))
Theorem	hfuni 36179	The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ (𝐴 ∈ Hf → ∪ 𝐴 ∈ Hf )
Theorem	hfpw 36180	The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ (𝐴 ∈ Hf → 𝒫 𝐴 ∈ Hf )
Theorem	hfninf 36181	ω is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ¬ ω ∈ Hf
21.12  Mathbox for Gino Giotto
21.12.1  Equality theorems.
21.12.1.1  Inference versions.
Theorem	rmoeqi 36182	Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓)
Theorem	rmoeqbii 36183	Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒)
Theorem	reueqi 36184	Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜓)
Theorem	reueqbii 36185	Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒)
Theorem	sbceqbii 36186	Formula-building inference for class substitution. General version of sbcbii 3813. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜓)
Theorem	disjeq1i 36187	Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)
Theorem	disjeq12i 36188	Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷)
Theorem	rabeqbii 36189	Equality theorem for restricted class abstractions. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓}
Theorem	iuneq12i 36190	Equality theorem for indexed union. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷
Theorem	iineq1i 36191	Equality theorem for indexed intersection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶
Theorem	iineq12i 36192	Equality theorem for indexed intersection. Inference version. General version of iineq1i 36191. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷
Theorem	riotaeqbii 36193	Equivalent wff's and equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓)
Theorem	riotaeqi 36194	Equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑)
Theorem	ixpeq1i 36195	Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶
Theorem	ixpeq12i 36196	Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷
Theorem	sumeq2si 36197	Equality inference for sum. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶
Theorem	sumeq12si 36198	Equality inference for sum. General version of sumeq2si 36197. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ Σ𝑥 ∈ 𝐴 𝐶 = Σ𝑥 ∈ 𝐵 𝐷
Theorem	prodeq2si 36199	Equality inference for product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶
Theorem	prodeq12si 36200	Equality inference for product. General version of prodeq2si 36199. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∏𝑥 ∈ 𝐴 𝐶 = ∏𝑥 ∈ 𝐵 𝐷