Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Color key:   Intuitionistic Logic Explorer  Intuitionistic Logic Explorer   User Mathboxes  User Mathboxes  

Last updated on 1-Jul-2020 at 12:34 PM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
24-Jun-2020nqprlu 6530 The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.)
(A Q → ⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ P)
 
15-Jun-2020imdivapd 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-2020redivapd 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-2020cjdivapd 9155 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))
 
15-Jun-2020riotaexg 5415 Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.)
(A 𝑉 → (x A ψ) V)
 
14-Jun-2020cjdivapi 9123 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
A     &   B        (B # 0 → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))
 
14-Jun-2020cjdivap 9097 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
((A B B # 0) → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))
 
14-Jun-2020cjap0 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-2020cjap 9094 Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
((A B ℂ) → ((∗‘A) # (∗‘B) ↔ A # B))
 
14-Jun-2020imdivap 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-2020redivap 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-2020mulreap 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-2020sqgt0apd 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-2020reexpclzapd 9018 Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
(φA ℝ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A𝑁) ℝ)
 
13-Jun-2020expdivapd 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-2020sqdivapd 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-2020expsubapd 9005 Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)    &   (φ𝑀 ℤ)       (φ → (A↑(𝑀𝑁)) = ((A𝑀) / (A𝑁)))
 
12-Jun-2020expm1apd 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-2020expp1zapd 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-2020exprecapd 9002 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → ((1 / A)↑𝑁) = (1 / (A𝑁)))
 
12-Jun-2020expnegapd 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-2020expap0d 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-2020expclzapd 8999 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A𝑁) ℂ)
 
12-Jun-2020sqrecapd 8998 Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)       (φ → ((1 / A)↑2) = (1 / (A↑2)))
 
12-Jun-2020sqgt0api 8952 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.)
A        (A # 0 → 0 < (A↑2))
 
12-Jun-2020sqdivapi 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-2020sqgt0ap 8935 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.)
((A A # 0) → 0 < (A↑2))
 
11-Jun-2020sqdivap 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-2020expdivap 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-2020expm1ap 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-2020expp1zap 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-2020expsubap 8916 Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
(((A A # 0) (𝑀 𝑁 ℤ)) → (A↑(𝑀𝑁)) = ((A𝑀) / (A𝑁)))
 
11-Jun-2020expmulzap 8915 Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
(((A A # 0) (𝑀 𝑁 ℤ)) → (A↑(𝑀 · 𝑁)) = ((A𝑀)↑𝑁))
 
10-Jun-2020expaddzap 8913 Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.)
(((A A # 0) (𝑀 𝑁 ℤ)) → (A↑(𝑀 + 𝑁)) = ((A𝑀) · (A𝑁)))
 
10-Jun-2020expaddzaplem 8912 Lemma for expaddzap 8913. (Contributed by Jim Kingdon, 10-Jun-2020.)
(((A A # 0) (𝑀 -𝑀 ℕ) 𝑁 0) → (A↑(𝑀 + 𝑁)) = ((A𝑀) · (A𝑁)))
 
10-Jun-2020exprecap 8910 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.)
((A A # 0 𝑁 ℤ) → ((1 / A)↑𝑁) = (1 / (A𝑁)))
 
10-Jun-2020mulexpzap 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-2020expap0i 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-2020expap0 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-2020mvllmulapd 7550 Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φA # 0)    &   (φ → (A · B) = 𝐶)       (φB = (𝐶 / A))
 
9-Jun-2020expclzap 8894 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.)
((A A # 0 𝑁 ℤ) → (A𝑁) ℂ)
 
9-Jun-2020expclzaplem 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-2020reexpclzap 8889 Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.)
((A A # 0 𝑁 ℤ) → (A𝑁) ℝ)
 
9-Jun-2020neg1ap0 7764 -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
-1 # 0
 
8-Jun-2020expcl2lemap 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 ℤ) → (AB) 𝐹)
 
8-Jun-2020expn1ap0 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-2020expineg2 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-2020expnegap0 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-2020expinnval 8872 Value of exponentiation to positive integer powers. (Contributed by Jim Kingdon, 8-Jun-2020.)
((A 𝑁 ℕ) → (A𝑁) = (seq1( · , (ℕ × {A}), ℂ)‘𝑁))
 
7-Jun-2020expival 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-2020expivallem 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-2020df-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-2020iseqfveq 8867 Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.)
(φ𝑁 (ℤ𝑀))    &   ((φ 𝑘 (𝑀...𝑁)) → (𝐹𝑘) = (𝐺𝑘))    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ x (ℤ𝑀)) → (𝐺x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)       (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝑀( + , 𝐺, 𝑆)‘𝑁))
 
3-Jun-2020iseqfeq2 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-2020iseqfveq2 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-2020iseqcl 8863 Closure properties of the recursive sequence builder. (Contributed by Jim Kingdon, 1-Jun-2020.)
(φ𝑁 (ℤ𝑀))    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)       (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) 𝑆)
 
1-Jun-2020fzdcel 8634 Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
((𝐾 𝑀 𝑁 ℤ) → DECID 𝐾 (𝑀...𝑁))
 
1-Jun-2020fztri3or 8633 Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
((𝐾 𝑀 𝑁 ℤ) → (𝐾 < 𝑀 𝐾 (𝑀...𝑁) 𝑁 < 𝐾))
 
1-Jun-2020zdclt 8054 Integer < is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
((A B ℤ) → DECID A < B)
 
31-May-2020iseqp1 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-2020iseq1 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-2020iseqovex 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-2020frecuzrdgcl 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-2020iseqfn 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-2020iseqval 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-2020nfiseq 8858 Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
x𝑀    &   x +    &   x𝐹    &   x𝑆       xseq𝑀( + , 𝐹, 𝑆)
 
30-May-2020iseqeq4 8857 Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
(𝑆 = 𝑇 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐹, 𝑇))
 
30-May-2020iseqeq3 8856 Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
(𝐹 = 𝐺 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐺, 𝑆))
 
30-May-2020iseqeq2 8855 Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
( + = 𝑄 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀(𝑄, 𝐹, 𝑆))
 
30-May-2020iseqeq1 8854 Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
(𝑀 = 𝑁 → seq𝑀( + , 𝐹, 𝑆) = seq𝑁( + , 𝐹, 𝑆))
 
30-May-2020nffrec 5921 Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
x𝐹    &   xA       xfrec(𝐹, A)
 
30-May-2020freceq2 5920 Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
(A = B → frec(𝐹, A) = frec(𝐹, B))
 
30-May-2020freceq1 5919 Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
(𝐹 = 𝐺 → frec(𝐹, A) = frec(𝐺, A))
 
29-May-2020df-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-2020frecuzrdgsuc 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-2020frecuzrdg0 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-2020frecuzrdgrrn 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-2020dffun5r 4857 A way of proving a relation is a function, analogous to mo2r 1949. (Contributed by Jim Kingdon, 27-May-2020.)
((Rel A xzy(⟨x, y Ay = z)) → Fun A)
 
26-May-2020frecuzrdgfn 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-2020frecuzrdglem 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-2020frecuzrdgrom 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-2020freccl 5932 Closure for finite recursion. (Contributed by Jim Kingdon, 25-May-2020.)
(φz(𝐹z) V)    &   (φA 𝑆)    &   ((φ z 𝑆) → (𝐹z) 𝑆)    &   (φB 𝜔)       (φ → (frec(𝐹, A)‘B) 𝑆)
 
24-May-2020frec2uzrdg 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-2020fzofig 8849 Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.)
((𝑀 𝑁 ℤ) → (𝑀..^𝑁) Fin)
 
21-May-2020fzfigd 8848 Deduction form of fzfig 8847. (Contributed by Jim Kingdon, 21-May-2020.)
(φ𝑀 ℤ)    &   (φ𝑁 ℤ)       (φ → (𝑀...𝑁) Fin)
 
19-May-2020fzfig 8847 A finite interval of integers is finite. (Contributed by Jim Kingdon, 19-May-2020.)
((𝑀 𝑁 ℤ) → (𝑀...𝑁) Fin)
 
19-May-2020frechashgf1o 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-2020ssfiexmid 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.)
xy((x Fin yx) → y Fin)       (φ ¬ φ)
 
19-May-2020enm 6230 A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.)
((AB x x A) → y y B)
 
18-May-2020frecfzen2 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-2020frecfzennn 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-2020frec2uzisod 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-2020frec2uzf1od 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-2020frec2uzrand 8832 Range of 𝐺 (see frec2uz0d 8826). (Contributed by Jim Kingdon, 17-May-2020.)
(φ𝐶 ℤ)    &   𝐺 = frec((x ℤ ↦ (x + 1)), 𝐶)       (φ → ran 𝐺 = (ℤ𝐶))
 
16-May-2020frec2uzlt2d 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-2020frec2uzltd 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-2020frec2uzuzd 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-2020frec2uzsucd 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-2020frec2uzzd 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-2020frec2uz0d 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]