Home | Metamath
Proof Explorer Theorem List (p. 400 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | afvres 39901 | The value of a restricted function, analogous to fvres 6117. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)'''𝐴) = (𝐹'''𝐴)) | ||
Theorem | tz6.12-afv 39902* | Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12 6121. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ ((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐹'''𝐴) = 𝑦) | ||
Theorem | tz6.12-1-afv 39903* | Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12-1 6120. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹'''𝐴) = 𝑦) | ||
Theorem | dmfcoafv 39904 | Domains of a function composition, analogous to dmfco 6182. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺'''𝐴) ∈ dom 𝐹)) | ||
Theorem | afvco2 39905 | Value of a function composition, analogous to fvco2 6183. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)'''𝑋) = (𝐹'''(𝐺'''𝑋))) | ||
Theorem | rlimdmafv 39906 | Two ways to express that a function has a limit, analogous to rlimdm 14130. (Contributed by Alexander van der Vekens, 27-Nov-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 '''𝐹))) | ||
Theorem | aoveq123d 39907 | Equality deduction for operation value, analogous to oveq123d 6570. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐶)) = ((𝐵𝐺𝐷)) ) | ||
Theorem | nfaov 39908 | Bound-variable hypothesis builder for operation value, analogous to nfov 6575. To prove a deduction version of this analogous to nfovd 6574 is not quickly possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of alternative operation values is based on are not available (see nfafv 39865). (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 ((𝐴𝐹𝐵)) | ||
Theorem | csbaovg 39909 | Move class substitution in and out of an operation. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌ ((𝐵𝐹𝐶)) = ((⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝐹⦋𝐴 / 𝑥⦌𝐶)) ) | ||
Theorem | aovfundmoveq 39910 | If a class is a function restricted to an ordered pair of its domain, then the value of the operation on this pair is equal for both definitions. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐹 defAt 〈𝐴, 𝐵〉 → ((𝐴𝐹𝐵)) = (𝐴𝐹𝐵)) | ||
Theorem | aovnfundmuv 39911 | If an ordered pair is not in the domain of a class or the class is not a function restricted to the ordered pair, then the operation value for this pair is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (¬ 𝐹 defAt 〈𝐴, 𝐵〉 → ((𝐴𝐹𝐵)) = V) | ||
Theorem | ndmaov 39912 | The value of an operation outside its domain, analogous to ndmafv 39869. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (¬ 〈𝐴, 𝐵〉 ∈ dom 𝐹 → ((𝐴𝐹𝐵)) = V) | ||
Theorem | ndmaovg 39913 | The value of an operation outside its domain, analogous to ndmovg 6715. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((dom 𝐹 = (𝑅 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → ((𝐴𝐹𝐵)) = V) | ||
Theorem | aovvdm 39914 | If the operation value of a class for an ordered pair is a set, the ordered pair is contained in the domain of the class. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 → 〈𝐴, 𝐵〉 ∈ dom 𝐹) | ||
Theorem | nfunsnaov 39915 | If the restriction of a class to a singleton is not a function, its operation value is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (¬ Fun (𝐹 ↾ {〈𝐴, 𝐵〉}) → ((𝐴𝐹𝐵)) = V) | ||
Theorem | aovvfunressn 39916 | If the operation value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 → Fun (𝐹 ↾ {〈𝐴, 𝐵〉})) | ||
Theorem | aovprc 39917 | The value of an operation when the one of the arguments is a proper class, analogous to ovprc 6581. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Rel dom 𝐹 ⇒ ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴𝐹𝐵)) = V) | ||
Theorem | aovrcl 39918 | Reverse closure for an operation value, analogous to afvvv 39874. In contrast to ovrcl 6584, elementhood of the operation's value in a set is required, not containing an element. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Rel dom 𝐹 ⇒ ⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | aovpcov0 39919 | If the alternative value of the operation on an ordered pair is the universal class, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ( ((𝐴𝐹𝐵)) = V → (𝐴𝐹𝐵) = ∅) | ||
Theorem | aovnuoveq 39920 | The alternative value of the operation on an ordered pair equals the operation's value at this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ( ((𝐴𝐹𝐵)) ≠ V → ((𝐴𝐹𝐵)) = (𝐴𝐹𝐵)) | ||
Theorem | aovvoveq 39921 | The alternative value of the operation on an ordered pair equals the operation's value on this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 → ((𝐴𝐹𝐵)) = (𝐴𝐹𝐵)) | ||
Theorem | aov0ov0 39922 | If the alternative value of the operation on an ordered pair is the empty set, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ( ((𝐴𝐹𝐵)) = ∅ → (𝐴𝐹𝐵) = ∅) | ||
Theorem | aovovn0oveq 39923 | If the operation's value at an argument is not the empty set, it equals the value of the alternative operation at this argument. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐴𝐹𝐵) ≠ ∅ → ((𝐴𝐹𝐵)) = (𝐴𝐹𝐵)) | ||
Theorem | aov0nbovbi 39924 | The operation's value on an ordered pair is an element of a set if and only if the alternative value of the operation on this ordered pair is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (∅ ∉ 𝐶 → ( ((𝐴𝐹𝐵)) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶)) | ||
Theorem | aovov0bi 39925 | The operation's value on an ordered pair is the empty set if and only if the alternative value of the operation on this ordered pair is either the empty set or the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐴𝐹𝐵) = ∅ ↔ ( ((𝐴𝐹𝐵)) = ∅ ∨ ((𝐴𝐹𝐵)) = V)) | ||
Theorem | rspceaov 39926* | A frequently used special case of rspc2ev 3295 for operation values, analogous to rspceov 6590. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = ((𝐶𝐹𝐷)) ) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = ((𝑥𝐹𝑦)) ) | ||
Theorem | fnotaovb 39927 | Equivalence of operation value and ordered triple membership, analogous to fnopfvb 6147. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ( ((𝐶𝐹𝐷)) = 𝑅 ↔ 〈𝐶, 𝐷, 𝑅〉 ∈ 𝐹)) | ||
Theorem | ffnaov 39928* | An operation maps to a class to which all values belong, analogous to ffnov 6662. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑥𝐹𝑦)) ∈ 𝐶)) | ||
Theorem | faovcl 39929 | Closure law for an operation, analogous to fovcl 6663. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶 ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵)) ∈ 𝐶) | ||
Theorem | aovmpt4g 39930* | Value of a function given by the "maps to" notation, analogous to ovmpt4g 6681. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → ((𝑥𝐹𝑦)) = 𝐶) | ||
Theorem | aoprssdm 39931* | Domain of closure of an operation. In contrast to oprssdm 6713, no additional property for S (¬ ∅ ∈ 𝑆) is required! (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦)) ∈ 𝑆) ⇒ ⊢ (𝑆 × 𝑆) ⊆ dom 𝐹 | ||
Theorem | ndmaovcl 39932 | The "closure" of an operation outside its domain, when the operation's value is a set in contrast to ndmovcl 6717 where it is required that the domain contains the empty set (∅ ∈ 𝑆). (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵)) ∈ 𝑆) & ⊢ ((𝐴𝐹𝐵)) ∈ V ⇒ ⊢ ((𝐴𝐹𝐵)) ∈ 𝑆 | ||
Theorem | ndmaovrcl 39933 | Reverse closure law, in contrast to ndmovrcl 6718 where it is required that the operation's domain doesn't contain the empty set (¬ ∅ ∈ 𝑆), no additional asumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) ⇒ ⊢ ( ((𝐴𝐹𝐵)) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) | ||
Theorem | ndmaovcom 39934 | Any operation is commutative outside its domain, analogous to ndmovcom 6719. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵)) = ((𝐵𝐹𝐴)) ) | ||
Theorem | ndmaovass 39935 | Any operation is associative outside its domain. In contrast to ndmovass 6720 where it is required that the operation's domain doesn't contain the empty set (¬ ∅ ∈ 𝑆), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (( ((𝐴𝐹𝐵)) 𝐹𝐶)) = ((𝐴𝐹 ((𝐵𝐹𝐶)) )) ) | ||
Theorem | ndmaovdistr 39936 | Any operation is distributive outside its domain. In contrast to ndmovdistr 6721 where it is required that the operation's domain doesn't contain the empty set (¬ ∅ ∈ 𝑆), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ dom 𝐺 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) ) | ||
Theorem | 1t10e1p1e11 39937 | 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 39938 | Obsolete version of 1t10e1p1e11 39937 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 | elprneb 39939 | An element of a proper unordered pair is the first element iff it is not the second element. (Contributed by AV, 18-Jun-2020.) |
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐵 ≠ 𝐶) → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶)) | ||
Theorem | leltletr 39940 | Transitive law, weaker form of lelttr 10007. (Contributed by AV, 14-Oct-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶)) | ||
Theorem | deccarry 39941 | Add 1 to a 2 digit number with carry. This is a special case of decsucc 11426, 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 | nltle2tri 39942 | Negated extended trichotomy law for 'less than' and 'less than or equal to'. (Contributed by AV, 18-Jul-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴)) | ||
Theorem | zgeltp1eq 39943 | 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 | smonoord 39944* | Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord 12693 (except that the case 𝑀 = 𝑁 must be excluded). Duplicate of monoords 38452? (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘𝑁)) | ||
Theorem | fzopred 39945 | Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 12424. (Contributed by AV, 14-Jul-2020.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → (𝑀..^𝑁) = ({𝑀} ∪ ((𝑀 + 1)..^𝑁))) | ||
Theorem | fzopredsuc 39946 | 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 39947 | 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 39948 | 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 | m1mod0mod1 39949 | 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 39950 | 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}) | ||
Based on the theorems of the fourierdlem* series of GS's mathbox. | ||
Syntax | ciccp 39951 | Extend class notation with the partitions of a closed interval of extended reals. |
class RePart | ||
Definition | df-iccp 39952* | 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 39953* | Partition consisting of a fixed number 𝑀 of parts. (Contributed by AV, 9-Jul-2020.) |
⊢ (𝑀 ∈ ℕ → (RePart‘𝑀) = {𝑝 ∈ (ℝ* ↑𝑚 (0...𝑀)) ∣ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))}) | ||
Theorem | iccpart 39954* | A special partition. Corresponds to fourierdlem2 39002 in GS's mathbox. (Contributed by AV, 9-Jul-2020.) |
⊢ (𝑀 ∈ ℕ → (𝑃 ∈ (RePart‘𝑀) ↔ (𝑃 ∈ (ℝ* ↑𝑚 (0...𝑀)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑃‘𝑖) < (𝑃‘(𝑖 + 1))))) | ||
Theorem | iccpartimp 39955 | Implications for a class being a partition. (Contributed by AV, 11-Jul-2020.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘𝑀) ∧ 𝐼 ∈ (0..^𝑀)) → (𝑃 ∈ (ℝ* ↑𝑚 (0...𝑀)) ∧ (𝑃‘𝐼) < (𝑃‘(𝐼 + 1)))) | ||
Theorem | iccpartres 39956 | The restriction of a partition is a partition. (Contributed by AV, 16-Jul-2020.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘(𝑀 + 1))) → (𝑃 ↾ (0...𝑀)) ∈ (RePart‘𝑀)) | ||
Theorem | iccpartxr 39957 | 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 39958 | 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 39959 | If there is a partition, then all intermediate points are real numbers. (Contributed by AV, 11-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘𝐼) ∈ ℝ) | ||
Theorem | iccpartiltu 39960* | 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 39961* | 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 39962 | If there is a partition, then the lower bound is strictly less than the upper bound. Corresponds to fourierdlem11 39011 in GS's mathbox. (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘0) < (𝑃‘𝑀)) | ||
Theorem | iccpartltu 39963* | 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 39964* | 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 39965* | 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 39966* | 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 39967* | 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 39968 | 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 39969 | The range of the partition is between its starting point and its ending point. Corresponds to fourierdlem15 39015 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → 𝑃:(0...𝑀)⟶((𝑃‘0)[,](𝑃‘𝑀))) | ||
Theorem | iccpartel 39970 | 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 39971* | 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 39972* | 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 39973 | Lemma for icceuelpart 39974. (Contributed by AV, 19-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀)) → (𝐼 < 𝐽 → (𝑃‘(𝐼 + 1)) ≤ (𝑃‘𝐽)))) | ||
Theorem | icceuelpart 39974* | 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 39975* | 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 39976 | A point of a partition is not an element of any open interval determined by the partition. Corresponds to fourierdlem12 39012 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 8-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑃) ⇒ ⊢ ((𝜑 ∧ 𝐼 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑃‘𝐼)(,)(𝑃‘(𝐼 + 1)))) | ||
At first, the (sequence of) Fermat numbers FermatNo (the 𝑛-th Fermat number is denoted as (FermatNo‘𝑛)) is defined, see df-fmtno 39978, and basic theorems are provided. Afterwards, it is shown that the first five Fermat numbers are prime, the (first) five Fermat primes, see fmtnofz04prm 40027, but that the 5th Fermat number (counting starts at 0!) is not prime, see fmtno5nprm 40033. The 4th Fermat number (i.e. the 5th Fermat prime) (FermatNo‘4) = ;;;;65537 is currently the biggest number proven to be prime in set.mm, see 65537prm 40026 (previously, it was ;;;4001, see 4001prm 15690). Another important result of this section is Goldbach's theorem goldbachth 39997, showing that two different Fermut numbers are coprime. By this, it can be proven that there is an infinite number of primes, see prminf2 40038. Finally, it is shown that every prime of the form ((2↑𝑘) + 1) must be a Fermat number (i.e. a Fermat prime), see 2pwp1prmfmtno 40042. | ||
Syntax | cfmtno 39977 | Extend class notation with the Fermat numbers. |
class FermatNo | ||
Definition | df-fmtno 39978 | Define the function that enumerates the Fermat numbers, see definition in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ FermatNo = (𝑛 ∈ ℕ0 ↦ ((2↑(2↑𝑛)) + 1)) | ||
Theorem | fmtno 39979 | The 𝑁 th Fermat number. (Contributed by AV, 13-Jun-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1)) | ||
Theorem | fmtnoge3 39980 | Each Fermat number is greater than or equal to 3. (Contributed by AV, 4-Aug-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ (ℤ≥‘3)) | ||
Theorem | fmtnonn 39981 | Each Fermat number is a positive integer. (Contributed by AV, 26-Jul-2021.) (Proof shortened by AV, 4-Aug-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ ℕ) | ||
Theorem | fmtnom1nn 39982 | A Fermat number minus one is a power of a power of two. (Contributed by AV, 29-Jul-2021.) |
⊢ (𝑁 ∈ ℕ0 → ((FermatNo‘𝑁) − 1) = (2↑(2↑𝑁))) | ||
Theorem | fmtnoodd 39983 | Each Fermat number is odd. (Contributed by AV, 26-Jul-2021.) |
⊢ (𝑁 ∈ ℕ0 → ¬ 2 ∥ (FermatNo‘𝑁)) | ||
Theorem | fmtnorn 39984* | A Fermat number is a function value of the enumeration of the Fermat numbers. (Contributed by AV, 3-Aug-2021.) |
⊢ (𝐹 ∈ ran FermatNo ↔ ∃𝑛 ∈ ℕ0 (FermatNo‘𝑛) = 𝐹) | ||
Theorem | fmtnof1 39985 | The enumeration of the Fermat numbers is a one-one function into the positive integers. (Contributed by AV, 3-Aug-2021.) |
⊢ FermatNo:ℕ0–1-1→ℕ | ||
Theorem | fmtnoinf 39986 | The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021.) |
⊢ ran FermatNo ∉ Fin | ||
Theorem | fmtnorec1 39987 | The first recurrence relation for Fermat numbers, see Wikipedia "Fermat number", https://en.wikipedia.org/wiki/Fermat_number#Basic_properties, 22-Jul-2021. (Contributed by AV, 22-Jul-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘(𝑁 + 1)) = ((((FermatNo‘𝑁) − 1)↑2) + 1)) | ||
Theorem | sqrtpwpw2p 39988 | The floor of the square root of 2 to the power of 2 to the power of a positive integer plus a bounded nonnegative integer. (Contributed by AV, 28-Jul-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < ((2↑((2↑(𝑁 − 1)) + 1)) + 1)) → (⌊‘(√‘((2↑(2↑𝑁)) + 𝑀))) = (2↑(2↑(𝑁 − 1)))) | ||
Theorem | fmtnosqrt 39989 | The floor of the square root of a Fermat number. (Contributed by AV, 28-Jul-2021.) |
⊢ (𝑁 ∈ ℕ → (⌊‘(√‘(FermatNo‘𝑁))) = (2↑(2↑(𝑁 − 1)))) | ||
Theorem | fmtno0 39990 | The 0 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘0) = 3 | ||
Theorem | fmtno1 39991 | The 1 st Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘1) = 5 | ||
Theorem | fmtnorec2lem 39992* | Lemma for fmtnorec2 39993 (induction step). (Contributed by AV, 29-Jul-2021.) |
⊢ (𝑦 ∈ ℕ0 → ((FermatNo‘(𝑦 + 1)) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) → (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2))) | ||
Theorem | fmtnorec2 39993* | The second recurrence relation for Fermat numbers, see ProofWiki "Product of Sequence of Fermat Numbers plus 2", 29-Jul-2021, https://proofwiki.org/wiki/Product_of_Sequence_of_Fermat_Numbers_plus_2 or Wikipedia "Fermat number", 29-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 29-Jul-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘(𝑁 + 1)) = (∏𝑛 ∈ (0...𝑁)(FermatNo‘𝑛) + 2)) | ||
Theorem | fmtnodvds 39994 | Any Fermat number divides a greater Fermat number minus 2. Corrolary of fmtnorec2 39993, see ProofWiki "Product of Sequence of Fermat Numbers plus 2/Corollary", 31-Jul-2021. (Contributed by AV, 1-Aug-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ) → (FermatNo‘𝑁) ∥ ((FermatNo‘(𝑁 + 𝑀)) − 2)) | ||
Theorem | goldbachthlem1 39995 | Lemma 1 for goldbachth 39997. (Contributed by AV, 1-Aug-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → (FermatNo‘𝑀) ∥ ((FermatNo‘𝑁) − 2)) | ||
Theorem | goldbachthlem2 39996 | Lemma 2 for goldbachth 39997. (Contributed by AV, 1-Aug-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1) | ||
Theorem | goldbachth 39997 | Goldbach's theorem: Two different Fermat numbers are coprime. See ProofWiki "Goldbach's theorem", 31-Jul-2021, https://proofwiki.org/wiki/Goldbach%27s_Theorem or Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 1-Aug-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ≠ 𝑀) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1) | ||
Theorem | fmtnorec3 39998* | The third recurrence relation for Fermat numbers, see Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 2-Aug-2021.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → (FermatNo‘𝑁) = ((FermatNo‘(𝑁 − 1)) + ((2↑(2↑(𝑁 − 1))) · ∏𝑛 ∈ (0...(𝑁 − 2))(FermatNo‘𝑛)))) | ||
Theorem | fmtnorec4 39999 | The fourth recurrence relation for Fermat numbers, see Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 31-Jul-2021.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → (FermatNo‘𝑁) = (((FermatNo‘(𝑁 − 1))↑2) − (2 · (((FermatNo‘(𝑁 − 2)) − 1)↑2)))) | ||
Theorem | fmtno2 40000 | The 2 nd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘2) = ;17 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |