Home | Metamath
Proof Explorer Theorem List (p. 414 of 426) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imarnf1pr 41301 | The image of the range of a function 𝐹 under a function 𝐸 if 𝐹 is a function of a pair into the domain of 𝐸. (Contributed by Alexander van der Vekens, 2-Feb-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (((𝐹:{𝑋, 𝑌}⟶dom 𝐸 ∧ 𝐸:dom 𝐸⟶𝑅) ∧ ((𝐸‘(𝐹‘𝑋)) = 𝐴 ∧ (𝐸‘(𝐹‘𝑌)) = 𝐵)) → (𝐸 “ ran 𝐹) = {𝐴, 𝐵})) | ||
Theorem | funop1 41302* | A function is an ordered pair iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.) |
⊢ (∃𝑥∃𝑦 𝐹 = 〈𝑥, 𝑦〉 → (Fun 𝐹 ↔ ∃𝑥∃𝑦 𝐹 = {〈𝑥, 𝑦〉})) | ||
Theorem | fun2dmnopgexmpl 41303 | A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020.) |
⊢ (𝐺 = {〈0, 1〉, 〈1, 1〉} → ¬ 𝐺 ∈ (V × V)) | ||
Theorem | opabresex0d 41304* | A collection of ordered pairs, the class of all possible second components being a set, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 1-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝜃) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → {𝑦 ∣ 𝜃} ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥𝑅𝑦 ∧ 𝜓)} ∈ V) | ||
Theorem | opabbrfex0d 41305* | A collection of ordered pairs, the class of all possible second components being a set, is a set. (Contributed by AV, 15-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝜃) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → {𝑦 ∣ 𝜃} ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} ∈ V) | ||
Theorem | opabresexd 41306* | A collection of ordered pairs, the second component being a function, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 15-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥𝑅𝑦 ∧ 𝜓)} ∈ V) | ||
Theorem | opabbrfexd 41307* | A collection of ordered pairs, the second component being a function, is a set. (Contributed by AV, 15-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} ∈ V) | ||
Theorem | leltletr 41308 | Transitive law, weaker form of lelttr 10128. (Contributed by AV, 14-Oct-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶)) | ||
Theorem | cnambpcma 41309 | ((a-b)+c)-a = c-a holds for complex numbers a,b,c. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) − 𝐴) = (𝐶 − 𝐵)) | ||
Theorem | cnapbmcpd 41310 | ((a+b)-c)+d = ((a+d)+b)-c holds for complex numbers a,b,c,d. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 + 𝐵) − 𝐶) + 𝐷) = (((𝐴 + 𝐷) + 𝐵) − 𝐶)) | ||
Theorem | leaddsuble 41311 | Addition and subtraction on one side of 'less or equal'. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ ((𝐴 + 𝐵) − 𝐶) ≤ 𝐴)) | ||
Theorem | 2leaddle2 41312 | If two real numbers are less than a third real number, the sum of the real numbers is less than twice the third real number. (Contributed by Alexander van der Vekens, 21-May-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐶) → (𝐴 + 𝐵) < (2 · 𝐶))) | ||
Theorem | ltnltne 41313 | Variant of trichotomy law for 'less than'. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (¬ 𝐵 < 𝐴 ∧ ¬ 𝐵 = 𝐴))) | ||
Theorem | p1lep2 41314 | A real number increasd by 1 is less than or equal to the number increased by 2. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ≤ (𝑁 + 2)) | ||
Theorem | ltsubsubaddltsub 41315 | If the result of subtracting two numbers is greater than a number, the result of adding one of these subtracted numbers to the number is less than the result of subtracting the other subtracted number only. (Contributed by Alexander van der Vekens, 9-Jun-2018.) |
⊢ ((𝐽 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → (𝐽 < ((𝐿 − 𝑀) − 𝑁) ↔ (𝐽 + 𝑀) < (𝐿 − 𝑁))) | ||
Theorem | zm1nn 41316 | An integer minus 1 is positive under certain circumstances. (Contributed by Alexander van der Vekens, 9-Jun-2018.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝐽 ∈ ℝ ∧ 0 ≤ 𝐽 ∧ 𝐽 < ((𝐿 − 𝑁) − 1)) → (𝐿 − 1) ∈ ℕ)) | ||
Theorem | nn0resubcl 41317 | Closure law for subtraction of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 − 𝐵) ∈ ℝ) | ||
Theorem | zgeltp1eq 41318 | If an integer is between another integer and its successor, the integer is equal to the other integer. (Contributed by AV, 30-May-2020.) |
⊢ ((𝐼 ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 ≤ 𝐼 ∧ 𝐼 < (𝐴 + 1)) → 𝐼 = 𝐴)) | ||
Theorem | 1t10e1p1e11 41319 | 11 is 1 times 10 to the power of 1, plus 1. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
⊢ ;11 = ((1 · (;10↑1)) + 1) | ||
Theorem | 1t10e1p1e11OLD 41320 | Obsolete version of 1t10e1p1e11 41319 as of 9-Sep-2021. (Contributed by AV, 4-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ;11 = ((1 · (10↑1)) + 1) | ||
Theorem | deccarry 41321 | Add 1 to a 2 digit number with carry. This is a special case of decsucc 11550, but in closed form. As observed by ML, this theorem allows for carrying the 1 down multiple decimal constructors, so we can carry the 1 multiple times down a multi-digit number, e.g. by applying this theorem three times we get (;;999 + 1) = ;;;1000. (Contributed by AV, 4-Aug-2020.) (Revised by ML, 8-Aug-2020.) (Proof shortened by AV, 10-Sep-2021.) |
⊢ (𝐴 ∈ ℕ → (;𝐴9 + 1) = ;(𝐴 + 1)0) | ||
Theorem | eluzge0nn0 41322 | If an integer is greater than or equal to a nonnegative integer, then it is a nonnegative integer. (Contributed by Alexander van der Vekens, 27-Aug-2018.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (0 ≤ 𝑀 → 𝑁 ∈ ℕ0)) | ||
Theorem | nltle2tri 41323 | Negated extended trichotomy law for 'less than' and 'less than or equal to'. (Contributed by AV, 18-Jul-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴)) | ||
Theorem | ssfz12 41324 | Subset relationship for finite sets of sequential integers. (Contributed by Alexander van der Vekens, 16-Mar-2018.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) | ||
Theorem | elfz2z 41325 | Membership of an integer in a finite set of sequential integers starting at 0. (Contributed by Alexander van der Vekens, 25-May-2018.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ (0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | 2elfz3nn0 41326 | If there are two elements in a finite set of sequential integers starting at 0, these two elements as well as the upper bound are nonnegative integers. (Contributed by Alexander van der Vekens, 7-Apr-2018.) |
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) | ||
Theorem | fz0addcom 41327 | The addition of two members of a finite set of sequential integers starting at 0 is commutative. (Contributed by Alexander van der Vekens, 22-May-2018.) (Revised by Alexander van der Vekens, 9-Jun-2018.) |
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | 2elfz2melfz 41328 | If the sum of two integers of a 0 based finite set of sequential integers is greater than the upper bound, the difference between one of the integers and the difference between the upper bound and the other integer is in the 0 based finite set of sequential integers with the first integer as upper bound. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.) |
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁 − 𝐴)) ∈ (0...𝐴))) | ||
Theorem | fz0addge0 41329 | The sum of two integers in 0 based finite sets of sequential integers is greater than or equal to zero. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ ((𝐴 ∈ (0...𝑀) ∧ 𝐵 ∈ (0...𝑁)) → 0 ≤ (𝐴 + 𝐵)) | ||
Theorem | elfzlble 41330 | Membership of an integer in a finite set of sequential integers with the integer as upper bound and a lower bound less than or equal to the integer. (Contributed by AV, 21-Oct-2018.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ((𝑁 − 𝑀)...𝑁)) | ||
Theorem | elfzelfzlble 41331 | Membership of an element of a finite set of sequential integers in a finite set of sequential integers with the same upper bound and a lower bound less than the upper bound. (Contributed by AV, 21-Oct-2018.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁) ∧ 𝑁 < (𝑀 + 𝐾)) → 𝐾 ∈ ((𝑁 − 𝑀)...𝑁)) | ||
Theorem | fzopred 41332 | Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 12557. (Contributed by AV, 14-Jul-2020.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → (𝑀..^𝑁) = ({𝑀} ∪ ((𝑀 + 1)..^𝑁))) | ||
Theorem | fzopredsuc 41333 | Join a predecessor and a successor to the beginning and the end of an open integer interval. This theorem holds even if 𝑁 = 𝑀 (then (𝑀...𝑁) = {𝑀} = ({𝑀} ∪ ∅) ∪ {𝑀}). (Contributed by AV, 14-Jul-2020.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁})) | ||
Theorem | 1fzopredsuc 41334 | Join 0 and a successor to the beginning and the end of an open integer interval starting at 1. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝑁 ∈ ℕ0 → (0...𝑁) = (({0} ∪ (1..^𝑁)) ∪ {𝑁})) | ||
Theorem | el1fzopredsuc 41335 | An element of an open integer interval starting at 1 joined by 0 and a successor at the beginning and the end is either 0 or an element of the open integer interval or the successor. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝑁 ∈ ℕ0 → (𝐼 ∈ (0...𝑁) ↔ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁))) | ||
Theorem | subsubelfzo0 41336 | Subtracting a difference from a number which is not less than the difference results in a bounded nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.) |
⊢ ((𝐴 ∈ (0..^𝑁) ∧ 𝐼 ∈ (0..^𝑁) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → (𝐼 − (𝑁 − 𝐴)) ∈ (0..^𝐴)) | ||
Theorem | fzoopth 41337 | A half-open integer range can represent an ordered pair, analogous to fzopth 12378. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) = (𝐽..^𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾))) | ||
Theorem | 2ffzoeq 41338* | Two functions over a half-open range of nonnegative integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) | ||
Theorem | m1mod0mod1 41339 | An integer decreased by 1 is 0 modulo a positive integer iff the integer is 1 modulo the same modulus. (Contributed by AV, 6-Jun-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 < 𝑁) → (((𝐴 − 1) mod 𝑁) = 0 ↔ (𝐴 mod 𝑁) = 1)) | ||
Theorem | elmod2 41340 | An integer modulo 2 is either 0 or 1. (Contributed by AV, 24-May-2020.) (Proof shortened by OpenAI, 3-Jul-2020.) |
⊢ (𝑁 ∈ ℤ → (𝑁 mod 2) ∈ {0, 1}) | ||
Theorem | smonoord 41341* | Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord 12831 (except that the case 𝑀 = 𝑁 must be excluded). Duplicate of monoords 39511? (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘𝑁)) | ||
Theorem | fsummsndifre 41342* | A finite sum with one of its integer summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∖ {𝑋})𝐵 ∈ ℝ) | ||
Theorem | fsumsplitsndif 41343* | Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
⊢ ((𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ 𝐴 𝐵 = (Σ𝑘 ∈ (𝐴 ∖ {𝑋})𝐵 + ⦋𝑋 / 𝑘⦌𝐵)) | ||
Theorem | fsummmodsndifre 41344* | A finite sum of summands modulo a positive number with one of its summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∖ {𝑋})(𝐵 mod 𝑁) ∈ ℝ) | ||
Theorem | fsummmodsnunz 41345* | A finite sum of summands modulo a positive number with an additional summand is an integer. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∪ {𝑧})(𝐵 mod 𝑁) ∈ ℤ) | ||
Theorem | setsidel 41346 | The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑅 = (𝑆 sSet 〈𝐴, 𝐵〉) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ 𝑅) | ||
Theorem | setsnidel 41347 | The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑅 = (𝑆 sSet 〈𝐴, 𝐵〉) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ 𝑅) | ||
Theorem | setsv 41348 | The value of the structure replacement function is a set. (Contributed by AV, 10-Nov-2021.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet 〈𝐴, 𝐵〉) ∈ V) | ||
Based on the theorems of the fourierdlem* series of GS's mathbox. | ||
Syntax | ciccp 41349 | Extend class notation with the partitions of a closed interval of extended reals. |
class RePart | ||
Definition | df-iccp 41350* | Define partitions of a closed interval of extended reals. Such partitions are finite increasing sequences of extended reals. (Contributed by AV, 8-Jul-2020.) |
⊢ RePart = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ* ↑𝑚 (0...𝑚)) ∣ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))}) | ||
Theorem | iccpval 41351* | Partition consisting of a fixed number 𝑀 of parts. (Contributed by AV, 9-Jul-2020.) |
⊢ (𝑀 ∈ ℕ → (RePart‘𝑀) = {𝑝 ∈ (ℝ* ↑𝑚 (0...𝑀)) ∣ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))}) | ||
Theorem | iccpart 41352* | A special partition. Corresponds to fourierdlem2 40326 in GS's mathbox. (Contributed by AV, 9-Jul-2020.) |
⊢ (𝑀 ∈ ℕ → (𝑃 ∈ (RePart‘𝑀) ↔ (𝑃 ∈ (ℝ* ↑𝑚 (0...𝑀)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑃‘𝑖) < (𝑃‘(𝑖 + 1))))) | ||
Theorem | iccpartimp 41353 | Implications for a class being a partition. (Contributed by AV, 11-Jul-2020.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘𝑀) ∧ 𝐼 ∈ (0..^𝑀)) → (𝑃 ∈ (ℝ* ↑𝑚 (0...𝑀)) ∧ (𝑃‘𝐼) < (𝑃‘(𝐼 + 1)))) | ||
Theorem | iccpartres 41354 | The restriction of a partition is a partition. (Contributed by AV, 16-Jul-2020.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘(𝑀 + 1))) → (𝑃 ↾ (0...𝑀)) ∈ (RePart‘𝑀)) | ||
Theorem | iccpartxr 41355 | If there is a partition, then all intermediate points and bounds are extended real numbers. (Contributed by AV, 11-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝐼 ∈ (0...𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘𝐼) ∈ ℝ*) | ||
Theorem | iccpartgtprec 41356 | If there is a partition, then all intermediate points and the upper bound are strictly greater than the preceeding intermediate points or lower bound. (Contributed by AV, 11-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘(𝐼 − 1)) < (𝑃‘𝐼)) | ||
Theorem | iccpartipre 41357 | If there is a partition, then all intermediate points are real numbers. (Contributed by AV, 11-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘𝐼) ∈ ℝ) | ||
Theorem | iccpartiltu 41358* | If there is a partition, then all intermediate points are strictly less than the upper bound. (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀)) | ||
Theorem | iccpartigtl 41359* | If there is a partition, then all intermediate points are strictly greater than the lower bound. (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (1..^𝑀)(𝑃‘0) < (𝑃‘𝑖)) | ||
Theorem | iccpartlt 41360 | If there is a partition, then the lower bound is strictly less than the upper bound. Corresponds to fourierdlem11 40335 in GS's mathbox. (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘0) < (𝑃‘𝑀)) | ||
Theorem | iccpartltu 41361* | If there is a partition, then all intermediate points and the lower bound are strictly less than the upper bound. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀)) | ||
Theorem | iccpartgtl 41362* | If there is a partition, then all intermediate points and the upper bound are strictly greater than the lower bound. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)(𝑃‘0) < (𝑃‘𝑖)) | ||
Theorem | iccpartgt 41363* | If there is a partition, then all intermediate points and the bounds are strictly ordered. (Contributed by AV, 18-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)∀𝑗 ∈ (0...𝑀)(𝑖 < 𝑗 → (𝑃‘𝑖) < (𝑃‘𝑗))) | ||
Theorem | iccpartleu 41364* | If there is a partition, then all intermediate points and the lower and the upper bound are less than or equal to the upper bound. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘𝑖) ≤ (𝑃‘𝑀)) | ||
Theorem | iccpartgel 41365* | If there is a partition, then all intermediate points and the upper and the lower bound are greater than or equal to the lower bound. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑖)) | ||
Theorem | iccpartrn 41366 | If there is a partition, then all intermediate points and bounds are contained in an closed interval of extended reals. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ran 𝑃 ⊆ ((𝑃‘0)[,](𝑃‘𝑀))) | ||
Theorem | iccpartf 41367 | The range of the partition is between its starting point and its ending point. Corresponds to fourierdlem15 40339 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → 𝑃:(0...𝑀)⟶((𝑃‘0)[,](𝑃‘𝑀))) | ||
Theorem | iccpartel 41368 | If there is a partition, then all intermediate points and bounds are contained in an closed interval of extended reals. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝐼 ∈ (0...𝑀)) → (𝑃‘𝐼) ∈ ((𝑃‘0)[,](𝑃‘𝑀))) | ||
Theorem | iccelpart 41369* | An element of any partitioned half opened interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020.) |
⊢ (𝑀 ∈ ℕ → ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) | ||
Theorem | iccpartiun 41370* | A half opened interval of extended reals is the union of the parts of its partition. (Contributed by AV, 18-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ((𝑃‘0)[,)(𝑃‘𝑀)) = ∪ 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) | ||
Theorem | icceuelpartlem 41371 | Lemma for icceuelpart 41372. (Contributed by AV, 19-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀)) → (𝐼 < 𝐽 → (𝑃‘(𝐼 + 1)) ≤ (𝑃‘𝐽)))) | ||
Theorem | icceuelpart 41372* | An element of a partitioned half opened interval of extended reals is an element of exactly one part of the partition. (Contributed by AV, 19-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ ((𝑃‘0)[,)(𝑃‘𝑀))) → ∃!𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) | ||
Theorem | iccpartdisj 41373* | The segments of a partitioned half opened interval of extended reals are a disjoint collection. (Contributed by AV, 19-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → Disj 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) | ||
Theorem | iccpartnel 41374 | A point of a partition is not an element of any open interval determined by the partition. Corresponds to fourierdlem12 40336 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 8-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑃) ⇒ ⊢ ((𝜑 ∧ 𝐼 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑃‘𝐼)(,)(𝑃‘(𝐼 + 1)))) | ||
Theorem | fargshiftfv 41375* | If a class is a function, then the values of the "shifted function" correspond to the function values of the class. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → (𝑋 ∈ (0..^𝑁) → (𝐺‘𝑋) = (𝐹‘(𝑋 + 1)))) | ||
Theorem | fargshiftf 41376* | If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → 𝐺:(0..^(#‘𝐹))⟶dom 𝐸) | ||
Theorem | fargshiftf1 41377* | If a function is 1-1, then also the shifted function is 1-1. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–1-1→dom 𝐸) → 𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸) | ||
Theorem | fargshiftfo 41378* | If a function is onto, then also the shifted function is onto. (Contributed by Alexander van der Vekens, 24-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–onto→dom 𝐸) → 𝐺:(0..^(#‘𝐹))–onto→dom 𝐸) | ||
Theorem | fargshiftfva 41379* | The values of a shifted function correspond to the value of the original function. (Contributed by Alexander van der Vekens, 24-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → (∀𝑘 ∈ (1...𝑁)(𝐸‘(𝐹‘𝑘)) = ⦋𝑘 / 𝑥⦌𝑃 → ∀𝑙 ∈ (0..^𝑁)(𝐸‘(𝐺‘𝑙)) = ⦋(𝑙 + 1) / 𝑥⦌𝑃)) | ||
Theorem | lswn0 41380 | The last symbol of a not empty word exists. The empty set must be excluded as symbol, because otherwise, it cannot be distinguished between valid cases (∅ is the last symbol) and invalid cases (∅ means that no last symbol exists. This is because of the special definition of a function in set.mm. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∅ ∉ 𝑉 ∧ (#‘𝑊) ≠ 0) → ( lastS ‘𝑊) ≠ ∅) | ||
In https://www.allacronyms.com/prefix/abbreviated, "pfx" is proposed as abbreviation for "prefix". Regarding the meaning of "prefix", it is different in computer science (automata theory/formal languages) compared with linguistics: in linguistics, a prefix has a meaning (see Wikipedia "Prefix" https://en.wikipedia.org/wiki/Prefix), whereas in computer science, a prefix is an arbitrary substring/subword starting at the beginning of a string/word (see Wikipedia "Substring" https://en.wikipedia.org/wiki/Substring#Prefix or https://math.stackexchange.com/questions/2190559/ is-there-standard-terminology-notation-for-the-prefix-of-a-word ). | ||
Syntax | cpfx 41381 | Syntax for the prefix operator. |
class prefix | ||
Definition | df-pfx 41382* | Define an operation which extracts prefixes of words, i.e. subwords starting at the beginning of a word. Definition in section 9.1 of [AhoHopUll] p. 318. "pfx" is used as label fragment. (Contributed by AV, 2-May-2020.) |
⊢ prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr 〈0, 𝑙〉)) | ||
Theorem | pfxval 41383 | Value of a prefix. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 prefix 𝐿) = (𝑆 substr 〈0, 𝐿〉)) | ||
Theorem | pfx00 41384 | A zero length prefix. (Contributed by AV, 2-May-2020.) |
⊢ (𝑆 prefix 0) = ∅ | ||
Theorem | pfx0 41385 | A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.) |
⊢ (∅ prefix 𝐿) = ∅ | ||
Theorem | pfxcl 41386 | Closure of the prefix extractor. (Contributed by AV, 2-May-2020.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐿) ∈ Word 𝐴) | ||
Theorem | pfxmpt 41387* | Value of the prefix extractor as mapping. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (𝑆 prefix 𝐿) = (𝑥 ∈ (0..^𝐿) ↦ (𝑆‘𝑥))) | ||
Theorem | pfxres 41388 | Value of the prefix extractor as restriction. Could replace swrd0val 13421. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (𝑆 prefix 𝐿) = (𝑆 ↾ (0..^𝐿))) | ||
Theorem | pfxf 41389 | A prefix of a word is a function from a half-open range of nonnegative integers of the same length as the prefix to the set of symbols for the original word. Could replace swrd0f 13427. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑊))) → (𝑊 prefix 𝐿):(0..^𝐿)⟶𝑉) | ||
Theorem | pfxfn 41390 | Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (𝑆 prefix 𝐿) Fn (0..^𝐿)) | ||
Theorem | pfxlen 41391 | Length of a prefix. Could replace swrd0len 13422. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (#‘(𝑆 prefix 𝐿)) = 𝐿) | ||
Theorem | pfxid 41392 | A word is a prefix of itself. (Contributed by AV, 2-May-2020.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix (#‘𝑆)) = 𝑆) | ||
Theorem | pfxrn 41393 | The range of a prefix of a word is a subset of the set of symbols for the word. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑊))) → ran (𝑊 prefix 𝐿) ⊆ 𝑉) | ||
Theorem | pfxn0 41394 | A prefix consisting of at least one symbol is not empty. Could replace swrdn0 13430. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ ∧ 𝐿 ≤ (#‘𝑊)) → (𝑊 prefix 𝐿) ≠ ∅) | ||
Theorem | pfxnd 41395 | The value of the prefix extractor is the empty set (undefined) if the argument is not within the range of the word. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (#‘𝑊) < 𝐿) → (𝑊 prefix 𝐿) = ∅) | ||
Theorem | pfxlen0 41396 | Length of a prefix of a word reduced by a single symbol. Could replace swrd0len0 13436. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (#‘𝑊) = (𝐿 + 1)) → (#‘(𝑊 prefix 𝐿)) = 𝐿) | ||
Theorem | addlenrevpfx 41397 | The sum of the lengths of two reversed parts of a word is the length of the word. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → ((#‘(𝑊 substr 〈𝑀, (#‘𝑊)〉)) + (#‘(𝑊 prefix 𝑀))) = (#‘𝑊)) | ||
Theorem | addlenpfx 41398 | The sum of the lengths of two parts of a word is the length of the word. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → ((#‘(𝑊 prefix 𝑀)) + (#‘(𝑊 substr 〈𝑀, (#‘𝑊)〉))) = (#‘𝑊)) | ||
Theorem | pfxfv 41399 | A symbol in a prefix of a word, indexed using the prefix' indices. Could replace swrd0fv 13439. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | pfxfv0 41400 | The first symbol in a prefix of a word. Could replace swrd0fv0 13440. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (1...(#‘𝑊))) → ((𝑊 prefix 𝐿)‘0) = (𝑊‘0)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |