Most Recent Proofs
|
|
Intuitionistic Logic Explorer Most Recent Proofs |
|
| Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 | |
See the MPE Most Recent Proofs page for news and some useful links.
| Color key: |
Intuitionistic Logic Explorer |
 User Mathboxes |
| Date | Label | Description |
|---|---|---|
| Theorem | ||
| 24-Jun-2020 | nqprlu 6530 | The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.) |
| ⊢ (A ∈ Q → ⟨{𝑙 ∣ 𝑙 <Q A}, {u ∣ A <Q u}⟩ ∈ P) | ||
| 15-Jun-2020 | imdivapd 9162 | Imaginary part of a division. Related to remul2 9061. (Contributed by Jim Kingdon, 15-Jun-2020.) |
| ⊢ (φ → A ∈ ℝ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → A # 0) ⇒ ⊢ (φ → (ℑ‘(B / A)) = ((ℑ‘B) / A)) | ||
| 15-Jun-2020 | redivapd 9161 | Real part of a division. Related to remul2 9061. (Contributed by Jim Kingdon, 15-Jun-2020.) |
| ⊢ (φ → A ∈ ℝ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → A # 0) ⇒ ⊢ (φ → (ℜ‘(B / A)) = ((ℜ‘B) / A)) | ||
| 15-Jun-2020 | cjdivapd 9155 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → B # 0) ⇒ ⊢ (φ → (∗‘(A / B)) = ((∗‘A) / (∗‘B))) | ||
| 15-Jun-2020 | riotaexg 5415 | Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.) |
| ⊢ (A ∈ 𝑉 → (℩x ∈ A ψ) ∈ V) | ||
| 14-Jun-2020 | cjdivapi 9123 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ A ∈ ℂ & ⊢ B ∈ ℂ ⇒ ⊢ (B # 0 → (∗‘(A / B)) = ((∗‘A) / (∗‘B))) | ||
| 14-Jun-2020 | cjdivap 9097 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ B # 0) → (∗‘(A / B)) = ((∗‘A) / (∗‘B))) | ||
| 14-Jun-2020 | cjap0 9095 | A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ (A ∈ ℂ → (A # 0 ↔ (∗‘A) # 0)) | ||
| 14-Jun-2020 | cjap 9094 | Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((∗‘A) # (∗‘B) ↔ A # B)) | ||
| 14-Jun-2020 | imdivap 9069 | Imaginary part of a division. Related to immul2 9068. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (ℑ‘(A / B)) = ((ℑ‘A) / B)) | ||
| 14-Jun-2020 | redivap 9062 | Real part of a division. Related to remul2 9061. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (ℜ‘(A / B)) = ((ℜ‘A) / B)) | ||
| 14-Jun-2020 | mulreap 9052 | A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ B ∈ ℝ ∧ B # 0) → (A ∈ ℝ ↔ (B · A) ∈ ℝ)) | ||
| 13-Jun-2020 | sqgt0apd 9021 | The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.) |
| ⊢ (φ → A ∈ ℝ) & ⊢ (φ → A # 0) ⇒ ⊢ (φ → 0 < (A↑2)) | ||
| 13-Jun-2020 | reexpclzapd 9018 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.) |
| ⊢ (φ → A ∈ ℝ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑𝑁) ∈ ℝ) | ||
| 13-Jun-2020 | expdivapd 9008 | Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → B # 0) & ⊢ (φ → 𝑁 ∈ ℕ0) ⇒ ⊢ (φ → ((A / B)↑𝑁) = ((A↑𝑁) / (B↑𝑁))) | ||
| 13-Jun-2020 | sqdivapd 9007 | Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → B # 0) ⇒ ⊢ (φ → ((A / B)↑2) = ((A↑2) / (B↑2))) | ||
| 12-Jun-2020 | expsubapd 9005 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) & ⊢ (φ → 𝑀 ∈ ℤ) ⇒ ⊢ (φ → (A↑(𝑀 − 𝑁)) = ((A↑𝑀) / (A↑𝑁))) | ||
| 12-Jun-2020 | expm1apd 9004 | Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑(𝑁 − 1)) = ((A↑𝑁) / A)) | ||
| 12-Jun-2020 | expp1zapd 9003 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑(𝑁 + 1)) = ((A↑𝑁) · A)) | ||
| 12-Jun-2020 | exprecapd 9002 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → ((1 / A)↑𝑁) = (1 / (A↑𝑁))) | ||
| 12-Jun-2020 | expnegapd 9001 | Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑-𝑁) = (1 / (A↑𝑁))) | ||
| 12-Jun-2020 | expap0d 9000 | Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑𝑁) # 0) | ||
| 12-Jun-2020 | expclzapd 8999 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (A↑𝑁) ∈ ℂ) | ||
| 12-Jun-2020 | sqrecapd 8998 | Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → A # 0) ⇒ ⊢ (φ → ((1 / A)↑2) = (1 / (A↑2))) | ||
| 12-Jun-2020 | sqgt0api 8952 | The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ A ∈ ℝ ⇒ ⊢ (A # 0 → 0 < (A↑2)) | ||
| 12-Jun-2020 | sqdivapi 8950 | Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| ⊢ A ∈ ℂ & ⊢ B ∈ ℂ & ⊢ B # 0 ⇒ ⊢ ((A / B)↑2) = ((A↑2) / (B↑2)) | ||
| 11-Jun-2020 | sqgt0ap 8935 | The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ ((A ∈ ℝ ∧ A # 0) → 0 < (A↑2)) | ||
| 11-Jun-2020 | sqdivap 8932 | Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ B # 0) → ((A / B)↑2) = ((A↑2) / (B↑2))) | ||
| 11-Jun-2020 | expdivap 8919 | Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ (B ∈ ℂ ∧ B # 0) ∧ 𝑁 ∈ ℕ0) → ((A / B)↑𝑁) = ((A↑𝑁) / (B↑𝑁))) | ||
| 11-Jun-2020 | expm1ap 8918 | Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑(𝑁 − 1)) = ((A↑𝑁) / A)) | ||
| 11-Jun-2020 | expp1zap 8917 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑(𝑁 + 1)) = ((A↑𝑁) · A)) | ||
| 11-Jun-2020 | expsubap 8916 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (A↑(𝑀 − 𝑁)) = ((A↑𝑀) / (A↑𝑁))) | ||
| 11-Jun-2020 | expmulzap 8915 | Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| ⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (A↑(𝑀 · 𝑁)) = ((A↑𝑀)↑𝑁)) | ||
| 10-Jun-2020 | expaddzap 8913 | Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (A↑(𝑀 + 𝑁)) = ((A↑𝑀) · (A↑𝑁))) | ||
| 10-Jun-2020 | expaddzaplem 8912 | Lemma for expaddzap 8913. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑(𝑀 + 𝑁)) = ((A↑𝑀) · (A↑𝑁))) | ||
| 10-Jun-2020 | exprecap 8910 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → ((1 / A)↑𝑁) = (1 / (A↑𝑁))) | ||
| 10-Jun-2020 | mulexpzap 8909 | Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ (((A ∈ ℂ ∧ A # 0) ∧ (B ∈ ℂ ∧ B # 0) ∧ 𝑁 ∈ ℤ) → ((A · B)↑𝑁) = ((A↑𝑁) · (B↑𝑁))) | ||
| 10-Jun-2020 | expap0i 8901 | Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) # 0) | ||
| 10-Jun-2020 | expap0 8899 | Positive integer exponentiation is apart from zero iff its mantissa is apart from zero. That it is easier to prove this first, and then prove expeq0 8900 in terms of it, rather than the other way around, is perhaps an illustration of the maxim "In constructive analysis, the apartness is more basic [ than ] equality." ([Geuvers], p. 1). (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((A↑𝑁) # 0 ↔ A # 0)) | ||
| 10-Jun-2020 | mvllmulapd 7550 | Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| ⊢ (φ → A ∈ ℂ) & ⊢ (φ → B ∈ ℂ) & ⊢ (φ → A # 0) & ⊢ (φ → (A · B) = 𝐶) ⇒ ⊢ (φ → B = (𝐶 / A)) | ||
| 9-Jun-2020 | expclzap 8894 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ ℂ) | ||
| 9-Jun-2020 | expclzaplem 8893 | Closure law for integer exponentiation. Lemma for expclzap 8894 and expap0i 8901. (Contributed by Jim Kingdon, 9-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ {z ∈ ℂ ∣ z # 0}) | ||
| 9-Jun-2020 | reexpclzap 8889 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.) |
| ⊢ ((A ∈ ℝ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ ℝ) | ||
| 9-Jun-2020 | neg1ap0 7764 | -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.) |
| ⊢ -1 # 0 | ||
| 8-Jun-2020 | expcl2lemap 8881 | Lemma for proving integer exponentiation closure laws. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| ⊢ 𝐹 ⊆ ℂ & ⊢ ((x ∈ 𝐹 ∧ y ∈ 𝐹) → (x · y) ∈ 𝐹) & ⊢ 1 ∈ 𝐹 & ⊢ ((x ∈ 𝐹 ∧ x # 0) → (1 / x) ∈ 𝐹) ⇒ ⊢ ((A ∈ 𝐹 ∧ A # 0 ∧ B ∈ ℤ) → (A↑B) ∈ 𝐹) | ||
| 8-Jun-2020 | expn1ap0 8879 | A number to the negative one power is the reciprocal. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0) → (A↑-1) = (1 / A)) | ||
| 8-Jun-2020 | expineg2 8878 | Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| ⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)) → (A↑𝑁) = (1 / (A↑-𝑁))) | ||
| 8-Jun-2020 | expnegap0 8877 | Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℕ0) → (A↑-𝑁) = (1 / (A↑𝑁))) | ||
| 8-Jun-2020 | expinnval 8872 | Value of exponentiation to positive integer powers. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ) → (A↑𝑁) = (seq1( · , (ℕ × {A}), ℂ)‘𝑁)) | ||
| 7-Jun-2020 | expival 8871 | Value of exponentiation to integer powers. (Contributed by Jim Kingdon, 7-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (A # 0 ∨ 0 ≤ 𝑁)) → (A↑𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {A}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {A}), ℂ)‘-𝑁))))) | ||
| 7-Jun-2020 | expivallem 8870 | Lemma for expival 8871. If we take a complex number apart from zero and raise it to a positive integer power, the result is apart from zero. (Contributed by Jim Kingodon, 7-Jun-2020.) |
| ⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℕ) → (seq1( · , (ℕ × {A}), ℂ)‘𝑁) # 0) | ||
| 7-Jun-2020 | df-iexp 8869 | Define exponentiation to nonnegative integer powers. This definition is not meant to be used directly; instead, exp0 8873 and expp1 8876 provide the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we don't have superscripts. 10-Jun-2005: The definition was extended to include zero exponents, so that 0↑0 = 1 per the convention of Definition 10-4.1 of [Gleason] p. 134. 4-Jun-2014: The definition was extended to include negative integer exponents. The case x = 0, y < 0 gives the value (1 / 0), so we will avoid this case in our theorems. (Contributed by Jim Kingodon, 7-Jun-2020.) |
| ⊢ ↑ = (x ∈ ℂ, y ∈ ℤ ↦ if(y = 0, 1, if(0 < y, (seq1( · , (ℕ × {x}), ℂ)‘y), (1 / (seq1( · , (ℕ × {x}), ℂ)‘-y))))) | ||
| 4-Jun-2020 | iseqfveq 8867 | Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.) |
| ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((φ ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘)) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐺‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝑀( + , 𝐺, 𝑆)‘𝑁)) | ||
| 3-Jun-2020 | iseqfeq2 8866 | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) |
| ⊢ (φ → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (𝐺‘𝐾)) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝐾)) → (𝐺‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) & ⊢ ((φ ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆) ↾ (ℤ≥‘𝐾)) = seq𝐾( + , 𝐺, 𝑆)) | ||
| 3-Jun-2020 | iseqfveq2 8865 | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) |
| ⊢ (φ → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (𝐺‘𝐾)) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝐾)) → (𝐺‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) & ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝐾)) & ⊢ ((φ ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝐾( + , 𝐺, 𝑆)‘𝑁)) | ||
| 1-Jun-2020 | iseqcl 8863 | Closure properties of the recursive sequence builder. (Contributed by Jim Kingdon, 1-Jun-2020.) |
| ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) ∈ 𝑆) | ||
| 1-Jun-2020 | fzdcel 8634 | Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝐾 ∈ (𝑀...𝑁)) | ||
| 1-Jun-2020 | fztri3or 8633 | Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾)) | ||
| 1-Jun-2020 | zdclt 8054 | Integer < is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.) |
| ⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → DECID A < B) | ||
| 31-May-2020 | iseqp1 8864 | Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 31-May-2020.) |
| ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁) + (𝐹‘(𝑁 + 1)))) | ||
| 31-May-2020 | iseq1 8862 | Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 31-May-2020.) |
| ⊢ (φ → 𝑀 ∈ ℤ) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (𝐹‘𝑀)) | ||
| 31-May-2020 | iseqovex 8859 | Closure of a function used in proving sequence builder theorems. This can be thought of as a lemma for the small number of sequence builder theorems which need it. (Contributed by Jim Kingdon, 31-May-2020.) |
| ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝑀) ∧ y ∈ 𝑆)) → (x(z ∈ (ℤ≥‘𝑀), w ∈ 𝑆 ↦ (w + (𝐹‘(z + 1))))y) ∈ 𝑆) | ||
| 31-May-2020 | frecuzrdgcl 8840 | Closure law for the recursive definition generator on upper integers. See comment in frec2uz0d 8826 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 31-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩) & ⊢ (φ → 𝑇 = ran 𝑅) ⇒ ⊢ ((φ ∧ B ∈ (ℤ≥‘𝐶)) → (𝑇‘B) ∈ 𝑆) | ||
| 30-May-2020 | iseqfn 8861 | The sequence builder function is a function. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ (φ → 𝑀 ∈ ℤ) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → seq𝑀( + , 𝐹, 𝑆) Fn (ℤ≥‘𝑀)) | ||
| 30-May-2020 | iseqval 8860 | Value of the sequence builder function. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝑀), y ∈ 𝑆 ↦ ⟨(x + 1), (x(z ∈ (ℤ≥‘𝑀), w ∈ 𝑆 ↦ (w + (𝐹‘(z + 1))))y)⟩), ⟨𝑀, (𝐹‘𝑀)⟩) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → seq𝑀( + , 𝐹, 𝑆) = ran 𝑅) | ||
| 30-May-2020 | nfiseq 8858 | Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ Ⅎx𝑀 & ⊢ Ⅎx + & ⊢ Ⅎx𝐹 & ⊢ Ⅎx𝑆 ⇒ ⊢ Ⅎxseq𝑀( + , 𝐹, 𝑆) | ||
| 30-May-2020 | iseqeq4 8857 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ (𝑆 = 𝑇 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐹, 𝑇)) | ||
| 30-May-2020 | iseqeq3 8856 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ (𝐹 = 𝐺 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐺, 𝑆)) | ||
| 30-May-2020 | iseqeq2 8855 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ ( + = 𝑄 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀(𝑄, 𝐹, 𝑆)) | ||
| 30-May-2020 | iseqeq1 8854 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ (𝑀 = 𝑁 → seq𝑀( + , 𝐹, 𝑆) = seq𝑁( + , 𝐹, 𝑆)) | ||
| 30-May-2020 | nffrec 5921 | Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ Ⅎx𝐹 & ⊢ ℲxA ⇒ ⊢ Ⅎxfrec(𝐹, A) | ||
| 30-May-2020 | freceq2 5920 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ (A = B → frec(𝐹, A) = frec(𝐹, B)) | ||
| 30-May-2020 | freceq1 5919 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
| ⊢ (𝐹 = 𝐺 → frec(𝐹, A) = frec(𝐺, A)) | ||
| 29-May-2020 | df-iseq 8853 |
Define a general-purpose operation that builds a recursive sequence
(i.e. a function on the positive integers ℕ or some other upper
integer set) whose value at an index is a function of its previous value
and the value of an input sequence at that index. This definition is
complicated, but fortunately it is not intended to be used directly.
Instead, the only purpose of this definition is to provide us with an
object that has the properties expressed by iseq1 8862 and at successors.
Typically, those are the main theorems that would be used in practice.
The first operand in the parentheses is the operation that is applied to the previous value and the value of the input sequence (second operand). The operand to the left of the parenthesis is the integer to start from. For example, for the operation +, an input sequence 𝐹 with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence seq1( + , 𝐹) with values 1, 3/2, 7/4, 15/8,.., so that (seq1( + , 𝐹)‘1) = 1, (seq1( + , 𝐹)‘2) = 3/2, etc. In other words, seq𝑀( + , 𝐹) transforms a sequence 𝐹 into an infinite series. Internally, the frec function generates as its values a set of ordered pairs starting at ⟨𝑀, (𝐹‘𝑀)⟩, with the first member of each pair incremented by one in each successive value. So, the range of frec is exactly the sequence we want, and we just extract the range and throw away the domain. (Contributed by Jim Kingdon, 29-May-2020.) |
| ⊢ seq𝑀( + , 𝐹, 𝑆) = ran frec((x ∈ (ℤ≥‘𝑀), y ∈ 𝑆 ↦ ⟨(x + 1), (y + (𝐹‘(x + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) | ||
| 28-May-2020 | frecuzrdgsuc 8842 | Successor value of a recursive definition generator on upper integers. See comment in frec2uz0d 8826 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 28-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩) & ⊢ (φ → 𝑇 = ran 𝑅) ⇒ ⊢ ((φ ∧ B ∈ (ℤ≥‘𝐶)) → (𝑇‘(B + 1)) = (B𝐹(𝑇‘B))) | ||
| 27-May-2020 | frecuzrdg0 8841 | Initial value of a recursive definition generator on upper integers. See comment in frec2uz0d 8826 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 27-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩) & ⊢ (φ → 𝑇 = ran 𝑅) ⇒ ⊢ (φ → (𝑇‘𝐶) = A) | ||
| 27-May-2020 | frecuzrdgrrn 8835 | The function 𝑅 (used in the definition of the recursive definition generator on upper integers) yields ordered pairs of integers and elements of 𝑆. (Contributed by Jim Kingdon, 27-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩) ⇒ ⊢ ((φ ∧ 𝐷 ∈ 𝜔) → (𝑅‘𝐷) ∈ ((ℤ≥‘𝐶) × 𝑆)) | ||
| 27-May-2020 | dffun5r 4857 | A way of proving a relation is a function, analogous to mo2r 1949. (Contributed by Jim Kingdon, 27-May-2020.) |
| ⊢ ((Rel A ∧ ∀x∃z∀y(⟨x, y⟩ ∈ A → y = z)) → Fun A) | ||
| 26-May-2020 | frecuzrdgfn 8839 | The recursive definition generator on upper integers is a function. See comment in frec2uz0d 8826 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 26-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩) & ⊢ (φ → 𝑇 = ran 𝑅) ⇒ ⊢ (φ → 𝑇 Fn (ℤ≥‘𝐶)) | ||
| 26-May-2020 | frecuzrdglem 8838 | A helper lemma for the value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 26-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩) & ⊢ (φ → B ∈ (ℤ≥‘𝐶)) ⇒ ⊢ (φ → ⟨B, (2nd ‘(𝑅‘(◡𝐺‘B)))⟩ ∈ ran 𝑅) | ||
| 26-May-2020 | frecuzrdgrom 8837 | The function 𝑅 (used in the definition of the recursive definition generator on upper integers) is a function defined for all natural numbers. (Contributed by Jim Kingdon, 26-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩) ⇒ ⊢ (φ → 𝑅 Fn 𝜔) | ||
| 25-May-2020 | freccl 5932 | Closure for finite recursion. (Contributed by Jim Kingdon, 25-May-2020.) |
| ⊢ (φ → ∀z(𝐹‘z) ∈ V) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ z ∈ 𝑆) → (𝐹‘z) ∈ 𝑆) & ⊢ (φ → B ∈ 𝜔) ⇒ ⊢ (φ → (frec(𝐹, A)‘B) ∈ 𝑆) | ||
| 24-May-2020 | frec2uzrdg 8836 | A helper lemma for the value of a recursive definition generator on upper integers (typically either ℕ or ℕ0) with characteristic function 𝐹(x, y) and initial value A. This lemma shows that evaluating 𝑅 at an element of 𝜔 gives an ordered pair whose first element is the index (translated from 𝜔 to (ℤ≥‘𝐶)). See comment in frec2uz0d 8826 which describes 𝐺 and the index translation. (Contributed by Jim Kingdon, 24-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩) & ⊢ (φ → B ∈ 𝜔) ⇒ ⊢ (φ → (𝑅‘B) = ⟨(𝐺‘B), (2nd ‘(𝑅‘B))⟩) | ||
| 21-May-2020 | fzofig 8849 | Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) ∈ Fin) | ||
| 21-May-2020 | fzfigd 8848 | Deduction form of fzfig 8847. (Contributed by Jim Kingdon, 21-May-2020.) |
| ⊢ (φ → 𝑀 ∈ ℤ) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (𝑀...𝑁) ∈ Fin) | ||
| 19-May-2020 | fzfig 8847 | A finite interval of integers is finite. (Contributed by Jim Kingdon, 19-May-2020.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ Fin) | ||
| 19-May-2020 | frechashgf1o 8846 | 𝐺 maps 𝜔 one-to-one onto ℕ0. (Contributed by Jim Kingdon, 19-May-2020.) |
| ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 0) ⇒ ⊢ 𝐺:𝜔–1-1-onto→ℕ0 | ||
| 19-May-2020 | ssfiexmid 6254 | If any subset of a finite set is finite, excluded middle follows. One direction of Theorem 2.1 of [Bauer], p. 485. (Contributed by Jim Kingdon, 19-May-2020.) |
| ⊢ ∀x∀y((x ∈ Fin ∧ y ⊆ x) → y ∈ Fin) ⇒ ⊢ (φ ∨ ¬ φ) | ||
| 19-May-2020 | enm 6230 | A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.) |
| ⊢ ((A ≈ B ∧ ∃x x ∈ A) → ∃y y ∈ B) | ||
| 18-May-2020 | frecfzen2 8845 | The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Jim Kingdon, 18-May-2020.) |
| ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 0) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡𝐺‘((𝑁 + 1) − 𝑀))) | ||
| 18-May-2020 | frecfzennn 8844 | The cardinality of a finite set of sequential integers. (See frec2uz0d 8826 for a description of the hypothesis.) (Contributed by Jim Kingdon, 18-May-2020.) |
| ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 0) ⇒ ⊢ (𝑁 ∈ ℕ0 → (1...𝑁) ≈ (◡𝐺‘𝑁)) | ||
| 17-May-2020 | frec2uzisod 8834 | 𝐺 (see frec2uz0d 8826) is an isomorphism from natural ordinals to upper integers. (Contributed by Jim Kingdon, 17-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) ⇒ ⊢ (φ → 𝐺 Isom E , < (𝜔, (ℤ≥‘𝐶))) | ||
| 17-May-2020 | frec2uzf1od 8833 | 𝐺 (see frec2uz0d 8826) is a one-to-one onto mapping. (Contributed by Jim Kingdon, 17-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) ⇒ ⊢ (φ → 𝐺:𝜔–1-1-onto→(ℤ≥‘𝐶)) | ||
| 17-May-2020 | frec2uzrand 8832 | Range of 𝐺 (see frec2uz0d 8826). (Contributed by Jim Kingdon, 17-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) ⇒ ⊢ (φ → ran 𝐺 = (ℤ≥‘𝐶)) | ||
| 16-May-2020 | frec2uzlt2d 8831 | The mapping 𝐺 (see frec2uz0d 8826) preserves order. (Contributed by Jim Kingdon, 16-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → A ∈ 𝜔) & ⊢ (φ → B ∈ 𝜔) ⇒ ⊢ (φ → (A ∈ B ↔ (𝐺‘A) < (𝐺‘B))) | ||
| 16-May-2020 | frec2uzltd 8830 | Less-than relation for 𝐺 (see frec2uz0d 8826). (Contributed by Jim Kingdon, 16-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → A ∈ 𝜔) & ⊢ (φ → B ∈ 𝜔) ⇒ ⊢ (φ → (A ∈ B → (𝐺‘A) < (𝐺‘B))) | ||
| 16-May-2020 | frec2uzuzd 8829 | The value 𝐺 (see frec2uz0d 8826) at an ordinal natural number is in the upper integers. (Contributed by Jim Kingdon, 16-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → A ∈ 𝜔) ⇒ ⊢ (φ → (𝐺‘A) ∈ (ℤ≥‘𝐶)) | ||
| 16-May-2020 | frec2uzsucd 8828 | The value of 𝐺 (see frec2uz0d 8826) at a successor. (Contributed by Jim Kingdon, 16-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → A ∈ 𝜔) ⇒ ⊢ (φ → (𝐺‘suc A) = ((𝐺‘A) + 1)) | ||
| 16-May-2020 | frec2uzzd 8827 | The value of 𝐺 (see frec2uz0d 8826) is an integer. (Contributed by Jim Kingdon, 16-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → A ∈ 𝜔) ⇒ ⊢ (φ → (𝐺‘A) ∈ ℤ) | ||
| 16-May-2020 | frec2uz0d 8826 | The mapping 𝐺 is a one-to-one mapping from 𝜔 onto upper integers that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number 𝐶 (normally 0 for the upper integers ℕ0 or 1 for the upper integers ℕ), 1 maps to 𝐶 + 1, etc. This theorem shows the value of 𝐺 at ordinal natural number zero. (Contributed by Jim Kingdon, 16-May-2020.) |
| ⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) ⇒ ⊢ (φ → (𝐺‘∅) = 𝐶) | ||
| Copyright terms: Public domain | W3C HTML validation [external] |