 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 User Mathboxes

Last updated on 9-Aug-2020 at 1:35 AM 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𝑁)))

(((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)), 𝐶)       (φ → (𝐺‘∅) = 𝐶)

15-May-2020nntri3 6014 A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-May-2020.)
((A 𝜔 B 𝜔) → (A = B ↔ (¬ A B ¬ B A)))

14-May-2020rdgifnon2 5907 The recursive definition generator is a function on ordinal numbers. (Contributed by Jim Kingdon, 14-May-2020.)
((z(𝐹z) V A 𝑉) → rec(𝐹, A) Fn On)

14-May-2020rdgtfr 5901 The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 14-May-2020.)
((z(𝐹z) V A 𝑉) → (Fun (g V ↦ (A x dom g(𝐹‘(gx)))) ((g V ↦ (A x dom g(𝐹‘(gx))))‘f) V))

13-May-2020frecfnom 5925 The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.)
((z(𝐹z) V A 𝑉) → frec(𝐹, A) Fn 𝜔)

13-May-2020frecabex 5923 The class abstraction from df-frec 5918 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.)
(φ𝑆 𝑉)    &   (φy(𝐹y) V)    &   (φA 𝑊)       (φ → {x ∣ (𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚))) (dom 𝑆 = ∅ x A))} V)

8-May-2020tfr0 5878 Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.)
𝐹 = recs(𝐺)       ((𝐺‘∅) 𝑉 → (𝐹‘∅) = (𝐺‘∅))

7-May-2020frec0g 5922 The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.)
(A 𝑉 → (frec(𝐹, A)‘∅) = A)

3-May-2020dcned 2209 Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
(φDECID A = B)       (φDECID AB)

2-May-2020ax-arch 6762 Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by theorem axarch 6733.

This axiom should not be used directly; instead use arch 7914 (which is the same, but stated in terms of and <). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.)

(A ℝ → 𝑛 {x ∣ (1 x y x (y + 1) x)}A < 𝑛)

30-Apr-2020ltexnqi 6392 Ordering on positive fractions in terms of existence of sum. (Contributed by Jim Kingdon, 30-Apr-2020.)
(A <Q Bx Q (A +Q x) = B)

28-Apr-2020addnqpr1lemiu 6540 Lemma for addnqpr1 6541. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 28-Apr-2020.)
(A Q → (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) ⊆ (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)))

28-Apr-2020addnqpr1lemil 6539 Lemma for addnqpr1 6541. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 28-Apr-2020.)
(A Q → (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩) ⊆ (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)))

28-Apr-2020addnqpr1lemru 6538 Lemma for addnqpr1 6541. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 28-Apr-2020.)
(A Q → (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)) ⊆ (2nd ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩))

28-Apr-2020addnqpr1lemrl 6537 Lemma for addnqpr1 6541. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 28-Apr-2020.)
(A Q → (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P)) ⊆ (1st ‘⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩))

26-Apr-2020pitonnlem1p1 6702 Lemma for pitonn 6704. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.)
(A P → [⟨(A +P (1P +P 1P)), (1P +P 1P)⟩] ~R = [⟨(A +P 1P), 1P⟩] ~R )

26-Apr-2020addnqpr1 6541 Addition of one to a fraction embedded into a positive real. One can either add the fraction one to the fraction, or the positive real one to the positive real, and get the same result. (Contributed by Jim Kingdon, 26-Apr-2020.)
(A Q → ⟨{𝑙𝑙 <Q (A +Q 1Q)}, {u ∣ (A +Q 1Q) <Q u}⟩ = (⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P 1P))

26-Apr-2020addpinq1 6446 Addition of one to the numerator of a fraction whose denominator is one. (Contributed by Jim Kingdon, 26-Apr-2020.)
(A N → [⟨(A +N 1𝑜), 1𝑜⟩] ~Q = ([⟨A, 1𝑜⟩] ~Q +Q 1Q))

26-Apr-2020nnnq 6405 The canonical embedding of positive integers into positive fractions. (Contributed by Jim Kingdon, 26-Apr-2020.)
(A N → [⟨A, 1𝑜⟩] ~Q Q)

24-Apr-2020pitonnlem2 6703 Lemma for pitonn 6704. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.)
(𝐾 N → (⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐾, 1𝑜⟩] ~Q }, {u ∣ [⟨𝐾, 1𝑜⟩] ~Q <Q u}⟩ +P 1P), 1P⟩] ~R , 0R⟩ + 1) = ⟨[⟨(⟨{𝑙𝑙 <Q [⟨(𝐾 +N 1𝑜), 1𝑜⟩] ~Q }, {u ∣ [⟨(𝐾 +N 1𝑜), 1𝑜⟩] ~Q <Q u}⟩ +P 1P), 1P⟩] ~R , 0R⟩)

24-Apr-2020pitonnlem1 6701 Lemma for pitonn 6704. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.)
⟨[⟨(⟨{𝑙𝑙 <Q [⟨1𝑜, 1𝑜⟩] ~Q }, {u ∣ [⟨1𝑜, 1𝑜⟩] ~Q <Q u}⟩ +P 1P), 1P⟩] ~R , 0R⟩ = 1

23-Apr-2020archsr 6668 For any signed real, there is an integer that is greater than it. This is also known as the "archimedean property". The expression [⟨(⟨{𝑙𝑙 <Q [⟨x, 1𝑜⟩] ~Q }, {u ∣ [⟨x, 1𝑜⟩] ~Q <Q u}⟩ +P 1P), 1P⟩] ~R is the embedding of the positive integer x into the signed reals. (Contributed by Jim Kingdon, 23-Apr-2020.)
(A Rx N A <R [⟨(⟨{𝑙𝑙 <Q [⟨x, 1𝑜⟩] ~Q }, {u ∣ [⟨x, 1𝑜⟩] ~Q <Q u}⟩ +P 1P), 1P⟩] ~R )

23-Apr-2020nnprlu 6533 The canonical embedding of positive integers into the positive reals. (Contributed by Jim Kingdon, 23-Apr-2020.)
(A N → ⟨{𝑙𝑙 <Q [⟨A, 1𝑜⟩] ~Q }, {u ∣ [⟨A, 1𝑜⟩] ~Q <Q u}⟩ P)

22-Apr-2020axarch 6733 Archimedean axiom. The Archimedean property is more naturally stated once we have defined . Unless we find another way to state it, we'll just use the right hand side of dfnn2 7657 in stating what we mean by "natural number" in the context of this axiom.

This construction-dependent theorem should not be referenced directly; instead, use ax-arch 6762. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.)

(A ℝ → 𝑛 {x ∣ (1 x y x (y + 1) x)}A < 𝑛)

22-Apr-2020pitonn 6704 Mapping from N to . (Contributed by Jim Kingdon, 22-Apr-2020.)
(𝑛 N → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑛, 1𝑜⟩] ~Q }, {u ∣ [⟨𝑛, 1𝑜⟩] ~Q <Q u}⟩ +P 1P), 1P⟩] ~R , 0R {x ∣ (1 x y x (y + 1) x)})

22-Apr-2020archpr 6613 For any positive real, there is an integer that is greater than it. This is also known as the "archimedean property". The integer x is embedded into the reals as described at nnprlu 6533. (Contributed by Jim Kingdon, 22-Apr-2020.)
(A Px N A<P ⟨{𝑙𝑙 <Q [⟨x, 1𝑜⟩] ~Q }, {u ∣ [⟨x, 1𝑜⟩] ~Q <Q u}⟩)

20-Apr-2020fzo0m 8777 A half-open integer range based at 0 is inhabited precisely if the upper bound is a positive integer. (Contributed by Jim Kingdon, 20-Apr-2020.)
(x x (0..^A) ↔ A ℕ)

20-Apr-2020fzom 8750 A half-open integer interval is inhabited iff it contains its left endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.)
(x x (𝑀..^𝑁) ↔ 𝑀 (𝑀..^𝑁))

18-Apr-2020eluzdc 8283 Membership of an integer in an upper set of integers is decidable. (Contributed by Jim Kingdon, 18-Apr-2020.)
((𝑀 𝑁 ℤ) → DECID 𝑁 (ℤ𝑀))

17-Apr-2020zlelttric 8026 Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
((A B ℤ) → (AB B < A))

16-Apr-2020fznlem 8635 A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.)
((𝑀 𝑁 ℤ) → (𝑁 < 𝑀 → (𝑀...𝑁) = ∅))

15-Apr-2020fzm 8632 Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.)
(x x (𝑀...𝑁) ↔ 𝑁 (ℤ𝑀))

15-Apr-2020xpdom3m 6244 A set is dominated by its Cartesian product with an inhabited set. Exercise 6 of [Suppes] p. 98. (Contributed by Jim Kingdon, 15-Apr-2020.)
((A 𝑉 B 𝑊 x x B) → A ≼ (A × B))

13-Apr-2020snfig 6227 A singleton is finite. (Contributed by Jim Kingdon, 13-Apr-2020.)
(A 𝑉 → {A} Fin)

13-Apr-2020en1bg 6216 A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Jim Kingdon, 13-Apr-2020.)
(A 𝑉 → (A ≈ 1𝑜A = { A}))

10-Apr-2020negm 8286 The image under negation of an inhabited set of reals is inhabited. (Contributed by Jim Kingdon, 10-Apr-2020.)
((A ⊆ ℝ x x A) → y y {z ℝ ∣ -z A})

8-Apr-2020zleloe 8028 Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
((A B ℤ) → (AB ↔ (A < B A = B)))

7-Apr-2020zdcle 8053 Integer is decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)
((A B ℤ) → DECID AB)

4-Apr-2020ioorebasg 8574 Open intervals are elements of the set of all open intervals. (Contributed by Jim Kingdon, 4-Apr-2020.)
((A * B *) → (A(,)B) ran (,))

30-Mar-2020icc0r 8525 An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.)
((A * B *) → (B < A → (A[,]B) = ∅))

30-Mar-2020ubioog 8513 An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
((A * B *) → ¬ B (A(,)B))

30-Mar-2020lbioog 8512 An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
((A * B *) → ¬ A (A(,)B))

29-Mar-2020iooidg 8508 An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.)
(A * → (A(,)A) = ∅)

27-Mar-2020zletric 8025 Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
((A B ℤ) → (AB BA))

26-Mar-20204z 8011 4 is an integer. (Contributed by BJ, 26-Mar-2020.)
4

25-Mar-2020elfzmlbm 8718 Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
(𝐾 (𝑀...𝑁) → (𝐾𝑀) (0...(𝑁𝑀)))

25-Mar-2020elfz0add 8709 An element of a finite set of sequential nonnegative integers is an element of an extended finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
((A 0 B 0) → (𝑁 (0...A) → 𝑁 (0...(A + B))))

25-Mar-20202eluzge0 8253 2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
2 (ℤ‘0)

23-Mar-2020rpnegap 8350 Either a real apart from zero or its negation is a positive real, but not both. (Contributed by Jim Kingdon, 23-Mar-2020.)
((A A # 0) → (A + ⊻ -A +))

23-Mar-2020reapltxor 7333 Real apartness in terms of less than (exclusive-or version). (Contributed by Jim Kingdon, 23-Mar-2020.)
((A B ℝ) → (A # B ↔ (A < BB < A)))

22-Mar-2020rpcnap0 8338 A positive real is a complex number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
(A + → (A A # 0))

22-Mar-2020rpreap0 8336 A positive real is a real number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
(A + → (A A # 0))

22-Mar-2020rpap0 8334 A positive real is apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
(A +A # 0)

20-Mar-2020qapne 8310 Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 20-Mar-2020.)
((A B ℚ) → (A # BAB))

20-Mar-2020divap1d 7518 If two complex numbers are apart, their quotient is apart from one. (Contributed by Jim Kingdon, 20-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)    &   (φA # B)       (φ → (A / B) # 1)

20-Mar-2020apmul1 7506 Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 20-Mar-2020.)
((A B (𝐶 𝐶 # 0)) → (A # B ↔ (A · 𝐶) # (B · 𝐶)))

19-Mar-2020divfnzn 8292 Division restricted to ℤ × ℕ is a function. Given excluded middle, it would be easy to prove this for ℂ × (ℂ ∖ {0}). The key difference is that an element of is apart from zero, whereas being an element of ℂ ∖ {0} implies being not equal to zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
( / ↾ (ℤ × ℕ)) Fn (ℤ × ℕ)

19-Mar-2020div2negapd 7522 Quotient of two negatives. (Contributed by Jim Kingdon, 19-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → (-A / -B) = (A / B))

19-Mar-2020divneg2apd 7521 Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → -(A / B) = (A / -B))

19-Mar-2020divnegapd 7520 Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → -(A / B) = (-A / B))

19-Mar-2020divap0bd 7519 A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → (A # 0 ↔ (A / B) # 0))

19-Mar-2020diveqap0ad 7517 A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 7403. (Contributed by Jim Kingdon, 19-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → ((A / B) = 0 ↔ A = 0))

19-Mar-2020diveqap1ad 7516 The quotient of two complex numbers is one iff they are equal. Deduction form of diveqap1 7424. Generalization of diveqap1d 7515. (Contributed by Jim Kingdon, 19-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → ((A / B) = 1 ↔ A = B))

19-Mar-2020diveqap1d 7515 Equality in terms of unit ratio. (Contributed by Jim Kingdon, 19-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)    &   (φ → (A / B) = 1)       (φA = B)

19-Mar-2020diveqap0d 7514 If a ratio is zero, the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)    &   (φ → (A / B) = 0)       (φA = 0)

15-Mar-2020nneoor 8076 A positive integer is even or odd. (Contributed by Jim Kingdon, 15-Mar-2020.)
(𝑁 ℕ → ((𝑁 / 2) ((𝑁 + 1) / 2) ℕ))

14-Mar-2020zltlen 8055 Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7373 which is a similar result for complex numbers. (Contributed by Jim Kingdon, 14-Mar-2020.)
((A B ℤ) → (A < B ↔ (AB BA)))

14-Mar-2020zdceq 8052 Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.)
((A B ℤ) → DECID A = B)

14-Mar-2020zapne 8051 Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝑀 𝑁 ℤ) → (𝑀 # 𝑁𝑀𝑁))

14-Mar-2020zltnle 8027 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.)
((A B ℤ) → (A < B ↔ ¬ BA))

14-Mar-2020ztri3or 8024 Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝑀 𝑁 ℤ) → (𝑀 < 𝑁 𝑀 = 𝑁 𝑁 < 𝑀))

14-Mar-2020ztri3or0 8023 Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.)
(𝑁 ℤ → (𝑁 < 0 𝑁 = 0 0 < 𝑁))

14-Mar-2020zaddcllemneg 8020 Lemma for zaddcl 8021. Special case in which -𝑁 is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝑀 𝑁 -𝑁 ℕ) → (𝑀 + 𝑁) ℤ)

14-Mar-2020zaddcllempos 8018 Lemma for zaddcl 8021. Special case in which 𝑁 is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝑀 𝑁 ℕ) → (𝑀 + 𝑁) ℤ)

14-Mar-2020dcne 2211 Decidable equality expressed in terms of . Basically the same as df-dc 742. (Contributed by Jim Kingdon, 14-Mar-2020.)
(DECID A = B ↔ (A = B AB))

9-Mar-20202muliap0 7886 2 · i is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
(2 · i) # 0

9-Mar-2020iap0 7885 The imaginary unit i is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
i # 0

9-Mar-20202ap0 7749 The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
2 # 0

9-Mar-20201ne0 7723 1 ≠ 0. See aso 1ap0 7334. (Contributed by Jim Kingdon, 9-Mar-2020.)
1 ≠ 0

9-Mar-2020redivclapi 7497 Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
A     &   B     &   B # 0       (A / B)

9-Mar-2020redivclapzi 7496 Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
A     &   B        (B # 0 → (A / B) ℝ)

9-Mar-2020rerecclapi 7495 Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
A     &   A # 0       (1 / A)

9-Mar-2020rerecclapzi 7494 Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
A        (A # 0 → (1 / A) ℝ)

9-Mar-2020divdivdivapi 7493 Division of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
A     &   B     &   𝐶     &   𝐷     &   B # 0    &   𝐷 # 0    &   𝐶 # 0       ((A / B) / (𝐶 / 𝐷)) = ((A · 𝐷) / (B · 𝐶))

A     &   B     &   𝐶     &   𝐷     &   B # 0    &   𝐷 # 0       ((A / B) + (𝐶 / 𝐷)) = (((A · 𝐷) + (𝐶 · B)) / (B · 𝐷))

9-Mar-2020divmul13api 7491 Swap denominators of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
A     &   B     &   𝐶     &   𝐷     &   B # 0    &   𝐷 # 0       ((A / B) · (𝐶 / 𝐷)) = ((𝐶 / B) · (A / 𝐷))

9-Mar-2020divmuldivapi 7490 Multiplication of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
A     &   B     &   𝐶     &   𝐷     &   B # 0    &   𝐷 # 0       ((A / B) · (𝐶 / 𝐷)) = ((A · 𝐶) / (B · 𝐷))

9-Mar-2020div11api 7489 One-to-one relationship for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
A     &   B     &   𝐶     &   𝐶 # 0       ((A / 𝐶) = (B / 𝐶) ↔ A = B)

9-Mar-2020div23api 7488 A commutative/associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
A     &   B     &   𝐶     &   𝐶 # 0       ((A · B) / 𝐶) = ((A / 𝐶) · B)

9-Mar-2020divdirapi 7487 Distribution of division over addition. (Contributed by Jim Kingdon, 9-Mar-2020.)
A     &   B     &   𝐶     &   𝐶 # 0       ((A + B) / 𝐶) = ((A / 𝐶) + (B / 𝐶))

9-Mar-2020divassapi 7486 An associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
A     &   B     &   𝐶     &   𝐶 # 0       ((A · B) / 𝐶) = (A · (B / 𝐶))

8-Mar-2020nnap0 7684 A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.)
(A ℕ → A # 0)

8-Mar-2020divdivap2d 7539 Division by a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φB # 0)    &   (φ𝐶 # 0)       (φ → (A / (B / 𝐶)) = ((A · 𝐶) / B))

8-Mar-2020divdivap1d 7538 Division into a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φB # 0)    &   (φ𝐶 # 0)       (φ → ((A / B) / 𝐶) = (A / (B · 𝐶)))

8-Mar-2020dmdcanap2d 7537 Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φB # 0)    &   (φ𝐶 # 0)       (φ → ((A / B) · (B / 𝐶)) = (A / 𝐶))

8-Mar-2020dmdcanapd 7536 Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φB # 0)    &   (φ𝐶 # 0)       (φ → ((B / 𝐶) · (A / B)) = (A / 𝐶))

8-Mar-2020divcanap7d 7535 Cancel equal divisors in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φB # 0)    &   (φ𝐶 # 0)       (φ → ((A / 𝐶) / (B / 𝐶)) = (A / B))

8-Mar-2020divcanap5rd 7534 Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φB # 0)    &   (φ𝐶 # 0)       (φ → ((A · 𝐶) / (B · 𝐶)) = (A / B))

8-Mar-2020divcanap5d 7533 Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φB # 0)    &   (φ𝐶 # 0)       (φ → ((𝐶 · A) / (𝐶 · B)) = (A / B))

8-Mar-2020divdiv32apd 7532 Swap denominators in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φB # 0)    &   (φ𝐶 # 0)       (φ → ((A / B) / 𝐶) = ((A / 𝐶) / B))

8-Mar-2020div13apd 7531 A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φB # 0)       (φ → ((A / B) · 𝐶) = ((𝐶 / B) · A))

8-Mar-2020div32apd 7530 A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φB # 0)       (φ → ((A / B) · 𝐶) = (A · (𝐶 / B)))

8-Mar-2020divmulapd 7529 Relationship between division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φB # 0)       (φ → ((A / B) = 𝐶 ↔ (B · 𝐶) = A))

7-Mar-2020nn1gt1 7688 A positive integer is either one or greater than one. This is for ; 0elnn 4283 is a similar theorem for 𝜔 (the natural numbers as ordinals). (Contributed by Jim Kingdon, 7-Mar-2020.)
(A ℕ → (A = 1 1 < A))

5-Mar-2020crap0 7651 The real representation of complex numbers is apart from zero iff one of its terms is apart from zero. (Contributed by Jim Kingdon, 5-Mar-2020.)
((A B ℝ) → ((A # 0 B # 0) ↔ (A + (i · B)) # 0))

3-Mar-2020rec11apd 7528 Reciprocal is one-to-one. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φA # 0)    &   (φB # 0)    &   (φ → (1 / A) = (1 / B))       (φA = B)

3-Mar-2020ddcanapd 7527 Cancellation in a double division. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φA # 0)    &   (φB # 0)       (φ → (A / (A / B)) = B)

3-Mar-2020divcanap6d 7526 Cancellation of inverted fractions. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φA # 0)    &   (φB # 0)       (φ → ((A / B) · (B / A)) = 1)

3-Mar-2020recdivap2d 7525 Division into a reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φA # 0)    &   (φB # 0)       (φ → ((1 / A) / B) = (1 / (A · B)))

3-Mar-2020recdivapd 7524 The reciprocal of a ratio. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φA # 0)    &   (φB # 0)       (φ → (1 / (A / B)) = (B / A))

3-Mar-2020divap0d 7523 The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φA # 0)    &   (φB # 0)       (φ → (A / B) # 0)

3-Mar-2020div0apd 7505 Division into zero is zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φA # 0)       (φ → (0 / A) = 0)

3-Mar-2020dividapd 7504 A number divided by itself is one. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φA # 0)       (φ → (A / A) = 1)

3-Mar-2020recrecapd 7503 A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φA # 0)       (φ → (1 / (1 / A)) = A)

3-Mar-2020recidap2d 7502 Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φA # 0)       (φ → ((1 / A) · A) = 1)

3-Mar-2020recidapd 7501 Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φA # 0)       (φ → (A · (1 / A)) = 1)

3-Mar-2020recap0d 7500 The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φA # 0)       (φ → (1 / A) # 0)

3-Mar-2020recclapd 7499 Closure law for reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
(φA ℂ)    &   (φA # 0)       (φ → (1 / A) ℂ)

2-Mar-2020div11apd 7547 One-to-one relationship for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φ𝐶 # 0)    &   (φ → (A / 𝐶) = (B / 𝐶))       (φA = B)

2-Mar-2020divsubdirapd 7546 Distribution of division over subtraction. (Contributed by Jim Kingdon, 2-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φ𝐶 # 0)       (φ → ((AB) / 𝐶) = ((A / 𝐶) − (B / 𝐶)))

2-Mar-2020divdirapd 7545 Distribution of division over addition. (Contributed by Jim Kingdon, 2-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φ𝐶 # 0)       (φ → ((A + B) / 𝐶) = ((A / 𝐶) + (B / 𝐶)))

2-Mar-2020div23apd 7544 A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φ𝐶 # 0)       (φ → ((A · B) / 𝐶) = ((A / 𝐶) · B))

2-Mar-2020div12apd 7543 A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φ𝐶 # 0)       (φ → (A · (B / 𝐶)) = (B · (A / 𝐶)))

2-Mar-2020divassapd 7542 An associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φ𝐶 # 0)       (φ → ((A · B) / 𝐶) = (A · (B / 𝐶)))

2-Mar-2020divmulap3d 7541 Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φ𝐶 # 0)       (φ → ((A / 𝐶) = BA = (B · 𝐶)))

2-Mar-2020divmulap2d 7540 Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φ𝐶 # 0)       (φ → ((A / 𝐶) = BA = (𝐶 · B)))

29-Feb-2020prodgt0gt0 7558 Infer that a multiplicand is positive from a positive multiplier and positive product. See prodgt0 7559 for the same theorem with 0 < A replaced by the weaker condition 0 ≤ A. (Contributed by Jim Kingdon, 29-Feb-2020.)
(((A B ℝ) (0 < A 0 < (A · B))) → 0 < B)

29-Feb-2020redivclapd 7549 Closure law for division of reals. (Contributed by Jim Kingdon, 29-Feb-2020.)
(φA ℝ)    &   (φB ℝ)    &   (φB # 0)       (φ → (A / B) ℝ)

29-Feb-2020rerecclapd 7548 Closure law for reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
(φA ℝ)    &   (φA # 0)       (φ → (1 / A) ℝ)

29-Feb-2020divcanap4d 7513 A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → ((A · B) / B) = A)

29-Feb-2020divcanap3d 7512 A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → ((B · A) / B) = A)

29-Feb-2020divrecap2d 7511 Relationship between division and reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → (A / B) = ((1 / B) · A))

29-Feb-2020divrecapd 7510 Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Jim Kingdon, 29-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → (A / B) = (A · (1 / B)))

29-Feb-2020divcanap2d 7509 A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → (B · (A / B)) = A)

29-Feb-2020divcanap1d 7508 A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → ((A / B) · B) = A)

29-Feb-2020divclapd 7507 Closure law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → (A / B) ℂ)

29-Feb-2020divdiv32api 7485 Swap denominators in a division. (Contributed by Jim Kingdon, 29-Feb-2020.)
A     &   B     &   𝐶     &   B # 0    &   𝐶 # 0       ((A / B) / 𝐶) = ((A / 𝐶) / B)

29-Feb-2020divmulapi 7484 Relationship between division and multiplication. (Contributed by Jim Kingdon, 29-Feb-2020.)
A     &   B     &   𝐶     &   B # 0       ((A / B) = 𝐶 ↔ (B · 𝐶) = A)

28-Feb-2020divdiv23apzi 7483 Swap denominators in a division. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B     &   𝐶        ((B # 0 𝐶 # 0) → ((A / B) / 𝐶) = ((A / 𝐶) / B))

28-Feb-2020divdirapzi 7482 Distribution of division over addition. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B     &   𝐶        (𝐶 # 0 → ((A + B) / 𝐶) = ((A / 𝐶) + (B / 𝐶)))

28-Feb-2020divmulapzi 7481 Relationship between division and multiplication. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B     &   𝐶        (B # 0 → ((A / B) = 𝐶 ↔ (B · 𝐶) = A))

28-Feb-2020divassapzi 7480 An associative law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B     &   𝐶        (𝐶 # 0 → ((A · B) / 𝐶) = (A · (B / 𝐶)))

28-Feb-2020rec11apii 7479 Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B     &   A # 0    &   B # 0       ((1 / A) = (1 / B) ↔ A = B)

28-Feb-2020divap0i 7478 The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B     &   A # 0    &   B # 0       (A / B) # 0

28-Feb-2020divcanap4i 7477 A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B     &   B # 0       ((A · B) / B) = A

28-Feb-2020divcanap3i 7476 A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B     &   B # 0       ((B · A) / B) = A

28-Feb-2020divrecapi 7475 Relationship between division and reciprocal. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B     &   B # 0       (A / B) = (A · (1 / B))

28-Feb-2020divcanap1i 7474 A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B     &   B # 0       ((A / B) · B) = A

28-Feb-2020divcanap2i 7473 A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B     &   B # 0       (B · (A / B)) = A

28-Feb-2020divclapi 7472 Closure law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B     &   B # 0       (A / B)

28-Feb-2020rec11api 7471 Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
A     &   B        ((A # 0 B # 0) → ((1 / A) = (1 / B) ↔ A = B))

28-Feb-2020ltleap 7373 Less than in terms of non-strict order and apartness. (Contributed by Jim Kingdon, 28-Feb-2020.)
((A B ℝ) → (A < B ↔ (AB A # B)))

27-Feb-2020divcanap4zi 7470 A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
A     &   B        (B # 0 → ((A · B) / B) = A)

27-Feb-2020divcanap3zi 7469 A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
A     &   B        (B # 0 → ((B · A) / B) = A)

27-Feb-2020divrecapzi 7468 Relationship between division and reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
A     &   B        (B # 0 → (A / B) = (A · (1 / B)))

27-Feb-2020divcanap2zi 7467 A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
A     &   B        (B # 0 → (B · (A / B)) = A)

27-Feb-2020divcanap1zi 7466 A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
A     &   B        (B # 0 → ((A / B) · B) = A)

27-Feb-2020divclapzi 7465 Closure law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
A     &   B        (B # 0 → (A / B) ℂ)

27-Feb-2020recidapzi 7457 Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
A        (A # 0 → (A · (1 / A)) = 1)

27-Feb-2020recap0apzi 7456 The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
A        (A # 0 → (1 / A) # 0)

27-Feb-2020recclapzi 7455 Closure law for reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
A        (A # 0 → (1 / A) ℂ)

27-Feb-2020divneg2ap 7454 Move negative sign inside of a division. (Contributed by Jim Kingdon, 27-Feb-2020.)
((A B B # 0) → -(A / B) = (A / -B))

27-Feb-2020div2negap 7453 Quotient of two negatives. (Contributed by Jim Kingdon, 27-Feb-2020.)
((A B B # 0) → (-A / -B) = (A / B))

27-Feb-2020negap0 7372 A number is apart from zero iff its negative is apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
(A ℂ → (A # 0 ↔ -A # 0))

27-Feb-2020gt0ap0d 7371 Positive implies apart from zero. Because of the way we define #, A must be an element of , not just *. (Contributed by Jim Kingdon, 27-Feb-2020.)
(φA ℝ)    &   (φ → 0 < A)       (φA # 0)

27-Feb-2020gt0ap0ii 7370 Positive implies apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
A     &   0 < A       A # 0

27-Feb-2020gt0ap0i 7369 Positive means apart from zero (useful for ordering theorems involving division). (Contributed by Jim Kingdon, 27-Feb-2020.)
A        (0 < AA # 0)

27-Feb-2020gt0ap0 7368 Positive implies apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
((A 0 < A) → A # 0)

26-Feb-20202times 7776 Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.)
(A ℂ → (2 · A) = (A + A))

26-Feb-2020redivclap 7449 Closure law for division of reals. (Contributed by Jim Kingdon, 26-Feb-2020.)
((A B B # 0) → (A / B) ℝ)

26-Feb-2020rerecclap 7448 Closure law for reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.)
((A A # 0) → (1 / A) ℝ)

26-Feb-2020conjmulap 7447 Two numbers whose reciprocals sum to 1 are called "conjugates" and satisfy this relationship. (Contributed by Jim Kingdon, 26-Feb-2020.)
(((𝑃 𝑃 # 0) (𝑄 𝑄 # 0)) → (((1 / 𝑃) + (1 / 𝑄)) = 1 ↔ ((𝑃 − 1) · (𝑄 − 1)) = 1))

26-Feb-2020divsubdivap 7446 Subtraction of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
(((A B ℂ) ((𝐶 𝐶 # 0) (𝐷 𝐷 # 0))) → ((A / 𝐶) − (B / 𝐷)) = (((A · 𝐷) − (B · 𝐶)) / (𝐶 · 𝐷)))

(((A B ℂ) ((𝐶 𝐶 # 0) (𝐷 𝐷 # 0))) → ((A / 𝐶) + (B / 𝐷)) = (((A · 𝐷) + (B · 𝐶)) / (𝐶 · 𝐷)))

26-Feb-2020ddcanap 7444 Cancellation in a double division. (Contributed by Jim Kingdon, 26-Feb-2020.)
(((A A # 0) (B B # 0)) → (A / (A / B)) = B)

26-Feb-2020recdivap2 7443 Division into a reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.)
(((A A # 0) (B B # 0)) → ((1 / A) / B) = (1 / (A · B)))

26-Feb-2020divdivap2 7442 Division by a fraction. (Contributed by Jim Kingdon, 26-Feb-2020.)
((A (B B # 0) (𝐶 𝐶 # 0)) → (A / (B / 𝐶)) = ((A · 𝐶) / B))

26-Feb-2020divdivap1 7441 Division into a fraction. (Contributed by Jim Kingdon, 26-Feb-2020.)
((A (B B # 0) (𝐶 𝐶 # 0)) → ((A / B) / 𝐶) = (A / (B · 𝐶)))

26-Feb-2020dmdcanap 7440 Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 26-Feb-2020.)
(((A A # 0) (B B # 0) 𝐶 ℂ) → ((A / B) · (𝐶 / A)) = (𝐶 / B))

26-Feb-2020divcanap7 7439 Cancel equal divisors in a division. (Contributed by Jim Kingdon, 26-Feb-2020.)
((A (B B # 0) (𝐶 𝐶 # 0)) → ((A / 𝐶) / (B / 𝐶)) = (A / B))

26-Feb-2020divdiv32ap 7438 Swap denominators in a division. (Contributed by Jim Kingdon, 26-Feb-2020.)
((A (B B # 0) (𝐶 𝐶 # 0)) → ((A / B) / 𝐶) = ((A / 𝐶) / B))

26-Feb-2020divcanap6 7437 Cancellation of inverted fractions. (Contributed by Jim Kingdon, 26-Feb-2020.)
(((A A # 0) (B B # 0)) → ((A / B) · (B / A)) = 1)

26-Feb-2020recdivap 7436 The reciprocal of a ratio. (Contributed by Jim Kingdon, 26-Feb-2020.)
(((A A # 0) (B B # 0)) → (1 / (A / B)) = (B / A))

26-Feb-2020divmuleqap 7435 Cross-multiply in an equality of ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
(((A B ℂ) ((𝐶 𝐶 # 0) (𝐷 𝐷 # 0))) → ((A / 𝐶) = (B / 𝐷) ↔ (A · 𝐷) = (B · 𝐶)))

26-Feb-2020divmul24ap 7434 Swap the numerators in the product of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
(((A B ℂ) ((𝐶 𝐶 # 0) (𝐷 𝐷 # 0))) → ((A / 𝐶) · (B / 𝐷)) = ((A / 𝐷) · (B / 𝐶)))

26-Feb-2020divmul13ap 7433 Swap the denominators in the product of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
(((A B ℂ) ((𝐶 𝐶 # 0) (𝐷 𝐷 # 0))) → ((A / 𝐶) · (B / 𝐷)) = ((B / 𝐶) · (A / 𝐷)))

25-Feb-2020divcanap5 7432 Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A (B B # 0) (𝐶 𝐶 # 0)) → ((𝐶 · A) / (𝐶 · B)) = (A / B))

25-Feb-2020divdivdivap 7431 Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by Jim Kingdon, 25-Feb-2020.)
(((A (B B # 0)) ((𝐶 𝐶 # 0) (𝐷 𝐷 # 0))) → ((A / B) / (𝐶 / 𝐷)) = ((A · 𝐷) / (B · 𝐶)))

25-Feb-2020divmuldivap 7430 Multiplication of two ratios. (Contributed by Jim Kingdon, 25-Feb-2020.)
(((A B ℂ) ((𝐶 𝐶 # 0) (𝐷 𝐷 # 0))) → ((A / 𝐶) · (B / 𝐷)) = ((A · B) / (𝐶 · 𝐷)))

25-Feb-2020rec11rap 7429 Mutual reciprocals. (Contributed by Jim Kingdon, 25-Feb-2020.)
(((A A # 0) (B B # 0)) → ((1 / A) = B ↔ (1 / B) = A))

25-Feb-2020rec11ap 7428 Reciprocal is one-to-one. (Contributed by Jim Kingdon, 25-Feb-2020.)
(((A A # 0) (B B # 0)) → ((1 / A) = (1 / B) ↔ A = B))

25-Feb-2020recrecap 7427 A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A A # 0) → (1 / (1 / A)) = A)

25-Feb-2020divnegap 7425 Move negative sign inside of a division. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A B B # 0) → -(A / B) = (-A / B))

25-Feb-2020diveqap1 7424 Equality in terms of unit ratio. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A B B # 0) → ((A / B) = 1 ↔ A = B))

25-Feb-2020div0ap 7421 Division into zero is zero. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A A # 0) → (0 / A) = 0)

25-Feb-2020dividap 7420 A number divided by itself is one. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A A # 0) → (A / A) = 1)

25-Feb-2020div11ap 7419 One-to-one relationship for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A B (𝐶 𝐶 # 0)) → ((A / 𝐶) = (B / 𝐶) ↔ A = B))

25-Feb-2020divcanap4 7418 A cancellation law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A B B # 0) → ((A · B) / B) = A)

25-Feb-2020divcanap3 7417 A cancellation law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A B B # 0) → ((B · A) / B) = A)

25-Feb-2020divdirap 7416 Distribution of division over addition. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A B (𝐶 𝐶 # 0)) → ((A + B) / 𝐶) = ((A / 𝐶) + (B / 𝐶)))

25-Feb-2020div12ap 7415 A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A B (𝐶 𝐶 # 0)) → (A · (B / 𝐶)) = (B · (A / 𝐶)))

25-Feb-2020div13ap 7414 A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A (B B # 0) 𝐶 ℂ) → ((A / B) · 𝐶) = ((𝐶 / B) · A))

25-Feb-2020div32ap 7413 A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A (B B # 0) 𝐶 ℂ) → ((A / B) · 𝐶) = (A · (𝐶 / B)))

25-Feb-2020div23ap 7412 A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A B (𝐶 𝐶 # 0)) → ((A · B) / 𝐶) = ((A / 𝐶) · B))

25-Feb-2020divassap 7411 An associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A B (𝐶 𝐶 # 0)) → ((A · B) / 𝐶) = (A · (B / 𝐶)))

25-Feb-2020divrecap2 7410 Relationship between division and reciprocal. (Contributed by Jim Kingdon, 25-Feb-2020.)
((A B B # 0) → (A / B) = ((1 / B) · A))

24-Feb-2020conventions 9165 Unless there is a reason to diverge, we follow the conventions of the Metamath Proof Explorer (aka "set.mm"). This list of conventions is intended to be read in conjunction with the corresponding conventions in the Metamath Proof Explorer, and only the differences are described below.

• Minimizing axioms and the axiom of choice. We prefer proofs that depend on fewer and/or weaker axioms, even if the proofs are longer. In particular, our choice of IZF (Intuitionistic Zermelo-Fraenkel) over CZF (Constructive Zermelo-Fraenkel, a weaker system) was just an expedient choice because IZF is easier to formalize in metamath. You can find some development using CZF in BJ's mathbox starting at ax-bd0 9202 (and the section header just above it). As for the axiom of choice, the full axiom of choice implies excluded middle as seen at acexmid 5454, although some authors will use countable choice or dependent choice. For example, countable choice or excluded middle is needed to show that the Cauchy reals coincide with the Dedekind reals - Corollary 11.4.3 of [HoTT], p. (varies).
• Junk/undefined results. Much of the discussion of this topic in the Metamath Proof Explorer applies except that certain techniques are not available to us. For example, the Metamath Proof Explorer will often say "if a function is evaluated within its domain, a certain result follows; if the function is evaluated outside its domain, the same result follows. Since the function must be evaluated within its domain or outside it, the result follows unconditionally" (the use of excluded middle in this argument is perhaps obvious when stated this way). For this reason, we generally need to prove we are evaluating functions within their domains and avoid the reverse closure theorems of the Metamath Proof Explorer.
• Bibliography references. The bibliography for the Intuitionistic Logic Explorer is separate from the one for the Metamath Proof Explorer but feel free to copy-paste a citation in either direction in order to cite it.

Label naming conventions

Here are a few of the label naming conventions:

• Suffixes. We follow the conventions of the Metamath Proof Explorer with a few additions. A biconditional in set.mm which is an implication in iset.mm should have a "r" (for the reverse direction), or "i"/"im" (for the forward direction) appended. A theorem in set.mm which has a decidability condition added should add "dc" to the theorem name. A theorem in set.mm where "nonempty class" is changed to "inhabited class" should add "m" (for member) to the theorem name.

The following table shows some commonly-used abbreviations in labels which are not found in the Metamath Proof Explorer, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME.

AbbreviationMnenomicSource ExpressionSyntax?Example(s)
apapart df-ap 7326 Yes apadd1 7352, apne 7367

• Community. The Metamath mailing list also covers the Intuitionistic Logic Explorer and is at: https://groups.google.com/forum/#!forum/metamath.
• (Contributed by Jim Kingdon, 24-Feb-2020.)

φ       φ

24-Feb-2020divrecap 7409 Relationship between division and reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
((A B B # 0) → (A / B) = (A · (1 / B)))

24-Feb-2020recidap2 7408 Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
((A A # 0) → ((1 / A) · A) = 1)

24-Feb-2020recidap 7407 Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
((A A # 0) → (A · (1 / A)) = 1)

24-Feb-2020recap0 7406 The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
((A A # 0) → (1 / A) # 0)

24-Feb-2020mulap0bbd 7383 A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 7381 and consequence of mulap0bd 7380. (Contributed by Jim Kingdon, 24-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ → (A · B) # 0)       (φB # 0)

24-Feb-2020mulap0bad 7382 A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 7381 and consequence of mulap0bd 7380. (Contributed by Jim Kingdon, 24-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ → (A · B) # 0)       (φA # 0)

24-Feb-2020mulap0bd 7380 The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
(φA ℂ)    &   (φB ℂ)       (φ → ((A # 0 B # 0) ↔ (A · B) # 0))

24-Feb-2020mulap0b 7378 The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
((A B ℂ) → ((A # 0 B # 0) ↔ (A · B) # 0))

24-Feb-2020mulap0r 7359 A product apart from zero. Lemma 2.13 of [Geuvers], p. 6. (Contributed by Jim Kingdon, 24-Feb-2020.)
((A B (A · B) # 0) → (A # 0 B # 0))

24-Feb-20201ap0 7334 One is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
1 # 0

23-Feb-2020mulap0d 7381 The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 23-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φA # 0)    &   (φB # 0)       (φ → (A · B) # 0)

23-Feb-2020mulap0i 7379 The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 23-Feb-2020.)
A     &   B     &   A # 0    &   B # 0       (A · B) # 0

23-Feb-2020mulext 7358 Strong extensionality for multiplication. Given excluded middle, apartness would be equivalent to negated equality and this would follow readily (for all operations) from oveq12 5464. For us, it is proved a different way. (Contributed by Jim Kingdon, 23-Feb-2020.)
(((A B ℂ) (𝐶 𝐷 ℂ)) → ((A · B) # (𝐶 · 𝐷) → (A # 𝐶 B # 𝐷)))

23-Feb-2020mulreim 7348 Complex multiplication in terms of real and imaginary parts. (Contributed by Jim Kingdon, 23-Feb-2020.)
(((A B ℝ) (𝐶 𝐷 ℝ)) → ((A + (i · B)) · (𝐶 + (i · 𝐷))) = (((A · 𝐶) + -(B · 𝐷)) + (i · ((𝐶 · B) + (𝐷 · A)))))

22-Feb-2020divap0 7405 The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
(((A A # 0) (B B # 0)) → (A / B) # 0)

22-Feb-2020divap0b 7404 The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
((A B B # 0) → (A # 0 ↔ (A / B) # 0))

22-Feb-2020diveqap0 7403 A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
((A B B # 0) → ((A / B) = 0 ↔ A = 0))

22-Feb-2020divcanap1 7402 A cancellation law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
((A B B # 0) → ((A / B) · B) = A)

22-Feb-2020divcanap2 7401 A cancellation law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
((A B B # 0) → (B · (A / B)) = A)

22-Feb-2020recclap 7400 Closure law for reciprocal. (Contributed by Jim Kingdon, 22-Feb-2020.)
((A A # 0) → (1 / A) ℂ)

22-Feb-2020divclap 7399 Closure law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
((A B B # 0) → (A / B) ℂ)

22-Feb-2020divmulap3 7398 Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
((A B (𝐶 𝐶 # 0)) → ((A / 𝐶) = BA = (B · 𝐶)))

22-Feb-2020divmulap2 7397 Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
((A B (𝐶 𝐶 # 0)) → ((A / 𝐶) = BA = (𝐶 · B)))

22-Feb-2020divmulap 7396 Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
((A B (𝐶 𝐶 # 0)) → ((A / 𝐶) = B ↔ (𝐶 · B) = A))

22-Feb-2020mulap0 7377 The product of two numbers apart from zero is apart from zero. Lemma 2.15 of [Geuvers], p. 6. (Contributed by Jim Kingdon, 22-Feb-2020.)
(((A A # 0) (B B # 0)) → (A · B) # 0)

22-Feb-2020mulext2 7357 Right extensionality for complex multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
((A B 𝐶 ℂ) → ((𝐶 · A) # (𝐶 · B) → A # B))

22-Feb-2020mulext1 7356 Left extensionality for complex multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
((A B 𝐶 ℂ) → ((A · 𝐶) # (B · 𝐶) → A # B))

22-Feb-2020remulext2 7344 Right extensionality for real multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
((A B 𝐶 ℝ) → ((𝐶 · A) # (𝐶 · B) → A # B))

21-Feb-2020divvalap 7395 Value of division: the (unique) element x such that (B · x) = A. This is meaningful only when B is apart from zero. (Contributed by Jim Kingdon, 21-Feb-2020.)
((A B B # 0) → (A / B) = (x ℂ (B · x) = A))

21-Feb-2020receuap 7392 Existential uniqueness of reciprocals. (Contributed by Jim Kingdon, 21-Feb-2020.)
((A B B # 0) → ∃!x ℂ (B · x) = A)

21-Feb-2020mulcanapi 7390 Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
A     &   B     &   𝐶     &   𝐶 # 0       ((𝐶 · A) = (𝐶 · B) ↔ A = B)

21-Feb-2020mulcanap2 7389 Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
((A B (𝐶 𝐶 # 0)) → ((A · 𝐶) = (B · 𝐶) ↔ A = B))

21-Feb-2020mulcanap 7388 Cancellation law for multiplication (full theorem form). (Contributed by Jim Kingdon, 21-Feb-2020.)
((A B (𝐶 𝐶 # 0)) → ((𝐶 · A) = (𝐶 · B) ↔ A = B))

21-Feb-2020mulcanap2ad 7387 Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcanap2d 7385. (Contributed by Jim Kingdon, 21-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φ𝐶 # 0)    &   (φ → (A · 𝐶) = (B · 𝐶))       (φA = B)

21-Feb-2020mulcanapad 7386 Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcanapd 7384. (Contributed by Jim Kingdon, 21-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φ𝐶 # 0)    &   (φ → (𝐶 · A) = (𝐶 · B))       (φA = B)

21-Feb-2020mulcanap2d 7385 Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φ𝐶 # 0)       (φ → ((A · 𝐶) = (B · 𝐶) ↔ A = B))

21-Feb-2020mulcanapd 7384 Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝐶 ℂ)    &   (φ𝐶 # 0)       (φ → ((𝐶 · A) = (𝐶 · B) ↔ A = B))

21-Feb-2020apne 7367 Apartness implies negated equality. We cannot in general prove the converse, which is the whole point of having separate notations for apartness and negated equality. (Contributed by Jim Kingdon, 21-Feb-2020.)
((A B ℂ) → (A # BAB))

21-Feb-2020apti 7366 Complex apartness is tight. (Contributed by Jim Kingdon, 21-Feb-2020.)
((A B ℂ) → (A = B ↔ ¬ A # B))

20-Feb-2020recexap 7376 Existence of reciprocal of nonzero complex number. (Contributed by Jim Kingdon, 20-Feb-2020.)
((A A # 0) → x ℂ (A · x) = 1)

20-Feb-2020recexaplem2 7375 Lemma for recexap 7376. (Contributed by Jim Kingdon, 20-Feb-2020.)
((A B (A + (i · B)) # 0) → ((A · A) + (B · B)) # 0)

19-Feb-2020remulext1 7343 Left extensionality for multiplication. (Contributed by Jim Kingdon, 19-Feb-2020.)
((A B 𝐶 ℝ) → ((A · 𝐶) # (B · 𝐶) → A # B))

18-Feb-2020ax-pre-mulext 6761 Strong extensionality of multiplication (expressed in terms of <). Axiom for real and complex numbers, justified by theorem axpre-mulext 6732

(Contributed by Jim Kingdon, 18-Feb-2020.)

((A B 𝐶 ℝ) → ((A · 𝐶) < (B · 𝐶) → (A < B B < A)))

18-Feb-2020axpre-mulext 6732 Strong extensionality of multiplication (expressed in terms of <). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulext 6761.

(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.)

((A B 𝐶 ℝ) → ((A · 𝐶) < (B · 𝐶) → (A < B B < A)))

18-Feb-2020mulextsr1 6667 Strong extensionality of multiplication of signed reals. (Contributed by Jim Kingdon, 18-Feb-2020.)
((A R B R 𝐶 R) → ((A ·R 𝐶) <R (B ·R 𝐶) → (A <R B B <R A)))

18-Feb-2020ltmprr 6612 Ordering property of multiplication. (Contributed by Jim Kingdon, 18-Feb-2020.)
((A P B P 𝐶 P) → ((𝐶 ·P A)<P (𝐶 ·P B) → A<P B))

17-Feb-2020mulextsr1lem 6666 Lemma for mulextsr1 6667. (Contributed by Jim Kingdon, 17-Feb-2020.)
(((𝑋 P 𝑌 P) (𝑍 P 𝑊 P) (𝑈 P 𝑉 P)) → ((((𝑋 ·P 𝑈) +P (𝑌 ·P 𝑉)) +P ((𝑍 ·P 𝑉) +P (𝑊 ·P 𝑈)))<P (((𝑋 ·P 𝑉) +P (𝑌 ·P 𝑈)) +P ((𝑍 ·P 𝑈) +P (𝑊 ·P 𝑉))) → ((𝑋 +P 𝑊)<P (𝑌 +P 𝑍) (𝑍 +P 𝑌)<P (𝑊 +P 𝑋))))

17-Feb-2020addextpr 6591 Strong extensionality of addition (ordering version). This is similar to addext 7354 but for positive reals and based on less-than rather than apartness. (Contributed by Jim Kingdon, 17-Feb-2020.)
(((A P B P) (𝐶 P 𝐷 P)) → ((A +P B)<P (𝐶 +P 𝐷) → (A<P 𝐶 B<P 𝐷)))

((A B 𝐶 ℂ) → (A # B ↔ (𝐶 + A) # (𝐶 + B)))

16-Feb-2020apcotr 7351 Apartness is cotransitive. (Contributed by Jim Kingdon, 16-Feb-2020.)
((A B 𝐶 ℂ) → (A # B → (A # 𝐶 B # 𝐶)))

16-Feb-2020apsym 7350 Apartness is symmetric. This theorem for real numbers is part of Definition 11.2.7(v) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Feb-2020.)
((A B ℂ) → (A # BB # A))

16-Feb-2020apirr 7349 Apartness is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2020.)
(A ℂ → ¬ A # A)

16-Feb-2020reapcotr 7342 Real apartness is cotransitive. Part of Definition 11.2.7(v) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Feb-2020.)
((A B 𝐶 ℝ) → (A # B → (A # 𝐶 B # 𝐶)))

15-Feb-2020addext 7354 Strong extensionality for addition. Given excluded middle, apartness would be equivalent to negated equality and this would follow readily (for all operations) from oveq12 5464. For us, it is proved a different way. (Contributed by Jim Kingdon, 15-Feb-2020.)
(((A B ℂ) (𝐶 𝐷 ℂ)) → ((A + B) # (𝐶 + 𝐷) → (A # 𝐶 B # 𝐷)))

14-Feb-2020apneg 7355 Negation respects apartness. (Contributed by Jim Kingdon, 14-Feb-2020.)
((A B ℂ) → (A # B ↔ -A # -B))

((A B 𝐶 ℂ) → (A # B ↔ (A + 𝐶) # (B + 𝐶)))

13-Feb-2020reapneg 7341 Real negation respects apartness. (Contributed by Jim Kingdon, 13-Feb-2020.)
((A B ℝ) → (A # B ↔ -A # -B))

((A B 𝐶 ℝ) → (A # B ↔ (A + 𝐶) # (B + 𝐶)))

12-Feb-2020apreim 7347 Complex apartness in terms of real and imaginary parts. (Contributed by Jim Kingdon, 12-Feb-2020.)
(((A B ℝ) (𝐶 𝐷 ℝ)) → ((A + (i · B)) # (𝐶 + (i · 𝐷)) ↔ (A # 𝐶 B # 𝐷)))

8-Feb-2020reapmul1 7339 Multiplication of both sides of real apartness by a real number apart from zero. Special case of apmul1 7506. (Contributed by Jim Kingdon, 8-Feb-2020.)
((A B (𝐶 𝐶 # 0)) → (A # B ↔ (A · 𝐶) # (B · 𝐶)))

8-Feb-2020reapmul1lem 7338 Lemma for reapmul1 7339. (Contributed by Jim Kingdon, 8-Feb-2020.)
((A B (𝐶 0 < 𝐶)) → (A # B ↔ (A · 𝐶) # (B · 𝐶)))

7-Feb-2020apsqgt0 7345 The square of a real number apart from zero is positive. (Contributed by Jim Kingdon, 7-Feb-2020.)
((A A # 0) → 0 < (A · A))

6-Feb-2020recexgt0 7324 Existence of reciprocal of positive real number. (Contributed by Jim Kingdon, 6-Feb-2020.)
((A 0 < A) → x ℝ (0 < x (A · x) = 1))

6-Feb-2020ax-precex 6753 Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 6724. (Contributed by Jim Kingdon, 6-Feb-2020.)
((A 0 < A) → x ℝ (0 < x (A · x) = 1))

6-Feb-2020axprecex 6724 Existence of positive reciprocal of positive real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-precex 6753.

In treatments which assume excluded middle, the 0 < A condition is generally replaced by A ≠ 0, and it may not be necessary to state that the reciproacal is positive. (Contributed by Jim Kingdon, 6-Feb-2020.) (New usage is discouraged.)

((A 0 < A) → x ℝ (0 < x (A · x) = 1))

6-Feb-2020recexgt0sr 6661 The reciprocal of a positive signed real exists and is positive. (Contributed by Jim Kingdon, 6-Feb-2020.)
(0R <R Ax R (0R <R x (A ·R x) = 1R))

1-Feb-2020reaplt 7332 Real apartness in terms of less than. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 1-Feb-2020.)
((A B ℝ) → (A # B ↔ (A < B B < A)))

31-Jan-2020apreap 7331 Complex apartness and real apartness agree on the real numbers. (Contributed by Jim Kingdon, 31-Jan-2020.)
((A B ℝ) → (A # BA # B))

30-Jan-2020rereim 7330 Decomposition of a real number into real part (itself) and imaginary part (zero). (Contributed by Jim Kingdon, 30-Jan-2020.)
(((A B ℝ) (𝐶 A = (B + (i · 𝐶)))) → (B = A 𝐶 = 0))

30-Jan-2020reapti 7323 Real apartness is tight. Beyond the development of apartness itself, proofs should use apti 7366. (Contributed by Jim Kingdon, 30-Jan-2020.) (New usage is discouraged.)
((A B ℝ) → (A = B ↔ ¬ A # B))

29-Jan-2020recexre 7322 Existence of reciprocal of real number. (Contributed by Jim Kingdon, 29-Jan-2020.)
((A A # 0) → x ℝ (A · x) = 1)

29-Jan-2020reapval 7320 Real apartness in terms of classes. Beyond the development of # itself, proofs should use reaplt 7332 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 29-Jan-2020.)
((A B ℝ) → (A # B ↔ (A < B B < A)))

29-Jan-2020axapti 6847 Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 6758 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.)
((A B ¬ (A < B B < A)) → A = B)

29-Jan-2020ax-pre-apti 6758 Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 6729. (Contributed by Jim Kingdon, 29-Jan-2020.)
((A B ¬ (A < B B < A)) → A = B)

29-Jan-2020axpre-apti 6729 Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-apti 6758.

(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.)

((A B ¬ (A < B B < A)) → A = B)

29-Jan-2020aptisr 6665 Apartness of signed reals is tight. (Contributed by Jim Kingdon, 29-Jan-2020.)
((A R B R ¬ (A <R B B <R A)) → A = B)

28-Jan-2020aptipr 6611 Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.)
((A P B P ¬ (A<P B B<P A)) → A = B)

28-Jan-2020aptiprlemu 6610 Lemma for aptipr 6611. (Contributed by Jim Kingdon, 28-Jan-2020.)
((A P B P ¬ B<P A) → (2ndB) ⊆ (2ndA))

28-Jan-2020aptiprleml 6609 Lemma for aptipr 6611. (Contributed by Jim Kingdon, 28-Jan-2020.)
((A P B P ¬ B<P A) → (1stA) ⊆ (1stB))

27-Jan-2020bj-dcbi 9313 Equivalence property for DECID. TODO: solve conflict with dcbi 843; minimize dcbii 746 and dcbid 747 with it, as well as theorems using those. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.)
((φψ) → (DECID φDECID ψ))

27-Jan-2020bj-notbid 9312 Deduction form of bj-notbi 9310. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.)
(φ → (ψχ))       (φ → (¬ ψ ↔ ¬ χ))

27-Jan-2020bj-notbii 9311 Inference associated with bj-notbi 9310. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.)
(φψ)       φ ↔ ¬ ψ)

27-Jan-2020bj-notbi 9310 Equivalence property for negation. TODO: minimize all theorems using notbid 591 and notbii 593. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.)
((φψ) → (¬ φ ↔ ¬ ψ))

26-Jan-2020df-ap 7326 Define complex apartness. Definition 6.1 of [Geuvers], p. 17.

Two numbers are considered apart if it is possible to separate them. One common usage is that we can divide by a number if it is apart from zero (see for example recclap 7400 which says that a number apart from zero has a reciprocal).

The defining characteristics of an apartness are irreflexivity (apirr 7349), symmetry (apsym 7350), and cotransitivity (apcotr 7351). Apartness implies negated equality, as seen at apne 7367, and the converse would also follow if we assumed excluded middle.

In addition, apartness of complex numbers is tight, which means that two numbers which are not apart are equal (apti 7366).

(Contributed by Jim Kingdon, 26-Jan-2020.)

# = {⟨x, y⟩ ∣ 𝑟 𝑠 𝑡 u ℝ ((x = (𝑟 + (i · 𝑠)) y = (𝑡 + (i · u))) (𝑟 # 𝑡 𝑠 # u))}

26-Jan-2020reapirr 7321 Real apartness is irreflexive. Part of Definition 11.2.7(v) of [HoTT], p. (varies). Beyond the development of # itself, proofs should use apirr 7349 instead. (Contributed by Jim Kingdon, 26-Jan-2020.)
(A ℝ → ¬ A # A)

26-Jan-2020df-reap 7319 Define real apartness. Definition in Section 11.2.1 of [HoTT], p. (varies). Although # is an apartness relation on the reals (see df-ap 7326 for more discussion of apartness relations), for our purposes it is just a stepping stone to defining # which is an apartness relation on complex numbers. On the reals, # and # agree (apreap 7331). (Contributed by Jim Kingdon, 26-Jan-2020.)
# = {⟨x, y⟩ ∣ ((x y ℝ) (x < y y < x))}

26-Jan-2020gt0add 7317 A positive sum must have a positive addend. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 26-Jan-2020.)
((A B 0 < (A + B)) → (0 < A 0 < B))

((A B ℂ) → (A + B) = (B + A))

17-Jan-2020ax-addcom 6743 Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 6714. Proofs should normally use addcom 6907 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
((A B ℂ) → (A + B) = (B + A))

17-Jan-2020axaddcom 6714 Addition commutes. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcom 6743 be used later. Instead, use addcom 6907.

In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.)

((A B ℂ) → (A + B) = (B + A))

16-Jan-2020addid1 6908 0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)
(A ℂ → (A + 0) = A)

16-Jan-2020ax-0id 6751 0 is an identity element for real addition. Axiom for real and complex numbers, justified by theorem ax0id 6722.

Proofs should normally use addid1 6908 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)

(A ℂ → (A + 0) = A)

16-Jan-2020ax0id 6722 0 is an identity element for real addition. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0id 6751.

In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.)

(A ℂ → (A + 0) = A)

15-Jan-2020axltwlin 6844 Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 6756 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.)
((A B 𝐶 ℝ) → (A < B → (A < 𝐶 𝐶 < B)))

15-Jan-2020axltirr 6843 Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 6755 with ordering on the extended reals. New proofs should use ltnr 6852 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
(A ℝ → ¬ A < A)

14-Jan-20202pwuninelg 5839 The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Jim Kingdon, 14-Jan-2020.)
(A 𝑉 → ¬ 𝒫 𝒫 A A)

13-Jan-20201re 6784 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
1

13-Jan-2020ax-1re 6737 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 6708. Proofs should use 1re 6784 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
1

13-Jan-2020ax1re 6708 1 is a real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1re 6737.

In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 6736 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)

1

12-Jan-2020ax-pre-ltwlin 6756 Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 6727. (Contributed by Jim Kingdon, 12-Jan-2020.)
((A B 𝐶 ℝ) → (A < B → (A < 𝐶 𝐶 < B)))

12-Jan-2020ax-pre-ltirr 6755 Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 6755. (Contributed by Jim Kingdon, 12-Jan-2020.)
(A ℝ → ¬ A < A)

12-Jan-2020ax-0lt1 6749 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 6720. Proofs should normally use 0lt1 6898 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
0 < 1

12-Jan-2020axpre-ltwlin 6727 Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 6756. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
((A B 𝐶 ℝ) → (A < B → (A < 𝐶 𝐶 < B)))

12-Jan-2020axpre-ltirr 6726 Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 6755. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
(A ℝ → ¬ A < A)

12-Jan-2020ax0lt1 6720 0 is less than 1. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0lt1 6749.

The version of this axiom in the Metamath Proof Explorer reads 1 ≠ 0; here we change it to 0 < 1. The proof of 0 < 1 from 1 ≠ 0 in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)

0 < 1

8-Jan-2020ecidg 6106 A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by Jim Kingdon, 8-Jan-2020.)
(A 𝑉 → [A] E = A)

5-Jan-2020elfzom1elp1fzo 8788 Membership of an integer incremented by one in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Proof shortened by AV, 5-Jan-2020.)
((𝑁 𝐼 (0..^(𝑁 − 1))) → (𝐼 + 1) (0..^𝑁))

5-Jan-20201idsr 6656 1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.)
(A R → (A ·R 1R) = A)

4-Jan-2020nn0ge2m1nn 7978 If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 4-Jan-2020.)
((𝑁 0 2 ≤ 𝑁) → (𝑁 − 1) ℕ)

4-Jan-2020distrsrg 6647 Multiplication of signed reals is distributive. (Contributed by Jim Kingdon, 4-Jan-2020.)
((A R B R 𝐶 R) → (A ·R (B +R 𝐶)) = ((A ·R B) +R (A ·R 𝐶)))

3-Jan-2020mulasssrg 6646 Multiplication of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
((A R B R 𝐶 R) → ((A ·R B) ·R 𝐶) = (A ·R (B ·R 𝐶)))

3-Jan-2020mulcomsrg 6645 Multiplication of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
((A R B R) → (A ·R B) = (B ·R A))

3-Jan-2020addasssrg 6644 Addition of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
((A R B R 𝐶 R) → ((A +R B) +R 𝐶) = (A +R (B +R 𝐶)))

3-Jan-2020addcomsrg 6643 Addition of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
((A R B R) → (A +R B) = (B +R A))

3-Jan-2020caovlem2d 5635 Rearrangement of expression involving multiplication (𝐺) and addition (𝐹). (Contributed by Jim Kingdon, 3-Jan-2020.)
((φ (x 𝑆 y 𝑆)) → (x𝐺y) = (y𝐺x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐺z) = ((x𝐺z)𝐹(y𝐺z)))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐺y)𝐺z) = (x𝐺(y𝐺z)))    &   ((φ (x 𝑆 y 𝑆)) → (x𝐺y) 𝑆)    &   (φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   (φ𝐷 𝑆)    &   (φ𝐻 𝑆)    &   (φ𝑅 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) 𝑆)       (φ → ((((A𝐺𝐶)𝐹(B𝐺𝐷))𝐺𝐻)𝐹(((A𝐺𝐷)𝐹(B𝐺𝐶))𝐺𝑅)) = ((A𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(B𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻)))))

2-Jan-2020bj-d0clsepcl 9314 Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
DECID φ

2-Jan-2020ax-bj-d0cl 9309 Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
BOUNDED φ       DECID φ

1-Jan-2020mulcmpblnrlemg 6628 Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.)
((((A P B P) (𝐶 P 𝐷 P)) ((𝐹 P 𝐺 P) (𝑅 P 𝑆 P))) → (((A +P 𝐷) = (B +P 𝐶) (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐷 ·P 𝐹) +P (((A ·P 𝐹) +P (B ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)))) = ((𝐷 ·P 𝐹) +P (((A ·P 𝐺) +P (B ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆))))))

31-Dec-2019eceq1d 6078 Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
(φA = B)       (φ → [A]𝐶 = [B]𝐶)

30-Dec-2019mulsrmo 6632 There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
((A ((P × P) / ~R ) B ((P × P) / ~R )) → ∃*zwvu𝑡((A = [⟨w, v⟩] ~R B = [⟨u, 𝑡⟩] ~R ) z = [⟨((w ·P u) +P (v ·P 𝑡)), ((w ·P 𝑡) +P (v ·P u))⟩] ~R ))

30-Dec-2019addsrmo 6631 There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
((A ((P × P) / ~R ) B ((P × P) / ~R )) → ∃*zwvu𝑡((A = [⟨w, v⟩] ~R B = [⟨u, 𝑡⟩] ~R ) z = [⟨(w +P u), (v +P 𝑡)⟩] ~R ))

30-Dec-2019prsrlem1 6630 Decomposing signed reals into positive reals. Lemma for addsrpr 6633 and mulsrpr 6634. (Contributed by Jim Kingdon, 30-Dec-2019.)
(((A ((P × P) / ~R ) B ((P × P) / ~R )) ((A = [⟨w, v⟩] ~R B = [⟨u, 𝑡⟩] ~R ) (A = [⟨𝑠, f⟩] ~R B = [⟨g, ⟩] ~R ))) → ((((w P v P) (𝑠 P f P)) ((u P 𝑡 P) (g P P))) ((w +P f) = (v +P 𝑠) (u +P ) = (𝑡 +P g))))

29-Dec-2019bj-omelon 9347 The set 𝜔 is an ordinal. Constructive proof of omelon 4274. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
𝜔 On

29-Dec-2019bj-omord 9346 The set 𝜔 is an ordinal. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
Ord 𝜔

29-Dec-2019bj-omtrans2 9345 The set 𝜔 is transitive. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
Tr 𝜔

29-Dec-2019bj-omtrans 9344 The set 𝜔 is transitive. A natural number is included in 𝜔.

The idea is to use bounded induction with the formula x ⊆ 𝜔. This formula, in a logic with terms, is bounded. So in our logic without terms, we need to temporarily replace it with x𝑎 and then deduce the original claim. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)

(A 𝜔 → A ⊆ 𝜔)

29-Dec-2019ltrnqg 6403 Ordering property of reciprocal for positive fractions. For a simplified version of the forward implication, see ltrnqi 6404. (Contributed by Jim Kingdon, 29-Dec-2019.)
((A Q B Q) → (A <Q B ↔ (*QB) <Q (*QA)))

29-Dec-2019rec1nq 6379 Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)
(*Q‘1Q) = 1Q

28-Dec-2019recexprlemupu 6598 The upper cut of B is upper. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 28-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       ((A P 𝑟 Q) → (𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)) → 𝑟 (2ndB)))

28-Dec-2019recexprlemopu 6597 The upper cut of B is open. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 28-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       ((A P 𝑟 Q 𝑟 (2ndB)) → 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)))

28-Dec-2019recexprlemlol 6596 The lower cut of B is lower. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 28-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       ((A P 𝑞 Q) → (𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB)) → 𝑞 (1stB)))

28-Dec-2019recexprlemopl 6595 The lower cut of B is open. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 28-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       ((A P 𝑞 Q 𝑞 (1stB)) → 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB)))

28-Dec-2019prmuloc2 6546 Positive reals are multiplicatively located. This is a variation of prmuloc 6545 which only constructs one (named) point and is therefore often easier to work with. It states that given a ratio B, there are elements of the lower and upper cut which have exactly that ratio between them. (Contributed by Jim Kingdon, 28-Dec-2019.)
((⟨𝐿, 𝑈 P 1Q <Q B) → x 𝐿 (x ·Q B) 𝑈)

28-Dec-20191pru 6536 The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
(2nd ‘1P) = {x ∣ 1Q <Q x}

28-Dec-20191prl 6535 The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
(1st ‘1P) = {xx <Q 1Q}

27-Dec-2019recexprlemex 6607 B is the reciprocal of A. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (A ·P B) = 1P)

27-Dec-2019recexprlemss1u 6606 The upper cut of A ·P B is a subset of the upper cut of one. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (2nd ‘(A ·P B)) ⊆ (2nd ‘1P))

27-Dec-2019recexprlemss1l 6605 The lower cut of A ·P B is a subset of the lower cut of one. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (1st ‘(A ·P B)) ⊆ (1st ‘1P))

27-Dec-2019recexprlem1ssu 6604 The upper cut of one is a subset of the upper cut of A ·P B. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (2nd ‘1P) ⊆ (2nd ‘(A ·P B)))

27-Dec-2019recexprlem1ssl 6603 The lower cut of one is a subset of the lower cut of A ·P B. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (1st ‘1P) ⊆ (1st ‘(A ·P B)))

27-Dec-2019recexprlempr 6602 B is a positive real. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A PB P)

27-Dec-2019recexprlemloc 6601 B is located. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1stB) 𝑟 (2ndB))))

27-Dec-2019recexprlemdisj 6600 B is disjoint. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P𝑞 Q ¬ (𝑞 (1stB) 𝑞 (2ndB)))

27-Dec-2019recexprlemrnd 6599 B is rounded. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (𝑞 Q (𝑞 (1stB) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB))) 𝑟 Q (𝑟 (2ndB) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)))))

27-Dec-2019recexprlemm 6594 B is inhabited. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (𝑞 Q 𝑞 (1stB) 𝑟 Q 𝑟 (2ndB)))

27-Dec-2019recexprlemelu 6593 Membership in the upper cut of B. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (𝐶 (2ndB) ↔ y(y <Q 𝐶 (*Qy) (1stA)))

27-Dec-2019recexprlemell 6592 Membership in the lower cut of B. Lemma for recexpr 6608. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (𝐶 (1stB) ↔ y(𝐶 <Q y (*Qy) (2ndA)))

26-Dec-2019ltaprg 6590 Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by Jim Kingdon, 26-Dec-2019.)
((A P B P 𝐶 P) → (A<P B ↔ (𝐶 +P A)<P (𝐶 +P B)))

26-Dec-2019prarloc2 6486 A Dedekind cut is arithmetically located. This is a variation of prarloc 6485 which only constructs one (named) point and is therefore often easier to work with. It states that given a tolerance 𝑃, there are elements of the lower and upper cut which are exactly that tolerance from each other. (Contributed by Jim Kingdon, 26-Dec-2019.)
((⟨𝐿, 𝑈 P 𝑃 Q) → 𝑎 𝐿 (𝑎 +Q 𝑃) 𝑈)

(((A P B P 𝐶 P) (A +P B) = (A +P 𝐶)) → (2ndB) ⊆ (2nd𝐶))

(((A P B P 𝐶 P) (A +P B) = (A +P 𝐶)) → (1stB) ⊆ (1st𝐶))

24-Dec-2019addcanprg 6588 Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.)
((A P B P 𝐶 P) → ((A +P B) = (A +P 𝐶) → B = 𝐶))

23-Dec-2019ltprordil 6563 If a positive real is less than a second positive real, its lower cut is a subset of the second's lower cut. (Contributed by Jim Kingdon, 23-Dec-2019.)
(A<P B → (1stA) ⊆ (1stB))

22-Dec-2019bj-findis 9363 Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 9335 for a bounded version not requiring ax-setind 4220. See finds 4266 for a proof in IZF. From this version, it is easy to prove of finds 4266, finds2 4267, finds1 4268. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.)
xψ    &   xχ    &   xθ    &   (x = ∅ → (ψφ))    &   (x = y → (φχ))    &   (x = suc y → (θφ))       ((ψ y 𝜔 (χθ)) → x 𝜔 φ)

21-Dec-2019ltexprlemupu 6576 The upper cut of our constructed difference is upper. Lemma for ltexpri 6585. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       ((A<P B 𝑟 Q) → (𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd𝐶)) → 𝑟 (2nd𝐶)))

21-Dec-2019ltexprlemopu 6575 The upper cut of our constructed difference is open. Lemma for ltexpri 6585. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       ((A<P B 𝑟 Q 𝑟 (2nd𝐶)) → 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd𝐶)))

21-Dec-2019ltexprlemlol 6574 The lower cut of our constructed difference is lower. Lemma for ltexpri 6585. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       ((A<P B 𝑞 Q) → (𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st𝐶)) → 𝑞 (1st𝐶)))

21-Dec-2019ltexprlemopl 6573 The lower cut of our constructed difference is open. Lemma for ltexpri 6585. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       ((A<P B 𝑞 Q 𝑞 (1st𝐶)) → 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st𝐶)))

21-Dec-2019ltexprlemelu 6571 Element in upper cut of the constructed difference. Lemma for ltexpri 6585. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (𝑟 (2nd𝐶) ↔ (𝑟 Q y(y (1stA) (y +Q 𝑟) (2ndB))))

21-Dec-2019ltexprlemell 6570 Element in lower cut of the constructed difference. Lemma for ltexpri 6585. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (𝑞 (1st𝐶) ↔ (𝑞 Q y(y (2ndA) (y +Q 𝑞) (1stB))))

17-Dec-2019ltexprlemru 6584 Lemma for ltexpri 6585. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (2ndB) ⊆ (2nd ‘(A +P 𝐶)))

17-Dec-2019ltexprlemfu 6583 Lemma for ltexpri 6585. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (2nd ‘(A +P 𝐶)) ⊆ (2ndB))

17-Dec-2019ltexprlemrl 6582 Lemma for ltexpri 6585. Reverse directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (1stB) ⊆ (1st ‘(A +P 𝐶)))

17-Dec-2019ltexprlemfl 6581 Lemma for ltexpri 6585. One directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (1st ‘(A +P 𝐶)) ⊆ (1stB))

17-Dec-2019ltexprlempr 6580 Our constructed difference is a positive real. Lemma for ltexpri 6585. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B𝐶 P)

17-Dec-2019ltexprlemloc 6579 Our constructed difference is located. Lemma for ltexpri 6585. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st𝐶) 𝑟 (2nd𝐶))))

17-Dec-2019ltexprlemdisj 6578 Our constructed difference is disjoint. Lemma for ltexpri 6585. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B𝑞 Q ¬ (𝑞 (1st𝐶) 𝑞 (2nd𝐶)))

17-Dec-2019ltexprlemrnd 6577 Our constructed difference is rounded. Lemma for ltexpri 6585. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (𝑞 Q (𝑞 (1st𝐶) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st𝐶))) 𝑟 Q (𝑟 (2nd𝐶) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd𝐶)))))

17-Dec-2019ltexprlemm 6572 Our constructed difference is inhabited. Lemma for ltexpri 6585. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (𝑞 Q 𝑞 (1st𝐶) 𝑟 Q 𝑟 (2nd𝐶)))

16-Dec-2019bj-sbime 9182 A strengthening of sbie 1671 (same proof). (Contributed by BJ, 16-Dec-2019.)
xψ    &   (x = y → (φψ))       ([y / x]φψ)

16-Dec-2019bj-sbimeh 9181 A strengthening of sbieh 1670 (same proof). (Contributed by BJ, 16-Dec-2019.)
(ψxψ)    &   (x = y → (φψ))       ([y / x]φψ)

16-Dec-2019bj-sbimedh 9180 A strengthening of sbiedh 1667 (same proof). (Contributed by BJ, 16-Dec-2019.)
(φxφ)    &   (φ → (χxχ))    &   (φ → (x = y → (ψχ)))       (φ → ([y / x]ψχ))

16-Dec-2019ltsopr 6568 Positive real 'less than' is a weak linear order (in the sense of df-iso 4025). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)
<P Or P

15-Dec-2019ltpopr 6567 Positive real 'less than' is a partial ordering. Remark ("< is transitive and irreflexive") preceding Proposition 11.2.3 of [HoTT], p. (varies). Lemma for ltsopr 6568. (Contributed by Jim Kingdon, 15-Dec-2019.)
<P Po P

15-Dec-2019ltdfpr 6488 More convenient form of df-iltp 6452. (Contributed by Jim Kingdon, 15-Dec-2019.)
((A P B P) → (A<P B𝑞 Q (𝑞 (2ndA) 𝑞 (1stB))))

15-Dec-2019prdisj 6474 A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.)
((⟨𝐿, 𝑈 P A Q) → ¬ (A 𝐿 A 𝑈))

13-Dec-20191idpru 6565 Lemma for 1idpr 6566. (Contributed by Jim Kingdon, 13-Dec-2019.)
(A P → (2nd ‘(A ·P 1P)) = (2ndA))

13-Dec-20191idprl 6564 Lemma for 1idpr 6566. (Contributed by Jim Kingdon, 13-Dec-2019.)
(A P → (1st ‘(A ·P 1P)) = (1stA))

13-Dec-2019gtnqex 6532 The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
{xA <Q x} V

13-Dec-2019ltnqex 6531 The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
{xx <Q A} V

13-Dec-2019sotritrieq 4053 A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.)
𝑅 Or A    &   ((B A 𝐶 A) → (B𝑅𝐶 B = 𝐶 𝐶𝑅B))       ((B A 𝐶 A) → (B = 𝐶 ↔ ¬ (B𝑅𝐶 𝐶𝑅B)))

12-Dec-2019distrprg 6562 Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A P B P 𝐶 P) → (A ·P (B +P 𝐶)) = ((A ·P B) +P (A ·P 𝐶)))

12-Dec-2019distrlem5pru 6561 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A P B P 𝐶 P) → (2nd ‘((A ·P B) +P (A ·P 𝐶))) ⊆ (2nd ‘(A ·P (B +P 𝐶))))

12-Dec-2019distrlem5prl 6560 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A P B P 𝐶 P) → (1st ‘((A ·P B) +P (A ·P 𝐶))) ⊆ (1st ‘(A ·P (B +P 𝐶))))

12-Dec-2019distrlem4pru 6559 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
(((A P B P 𝐶 P) ((x (2ndA) y (2ndB)) (f (2ndA) z (2nd𝐶)))) → ((x ·Q y) +Q (f ·Q z)) (2nd ‘(A ·P (B +P 𝐶))))

12-Dec-2019distrlem4prl 6558 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
(((A P B P 𝐶 P) ((x (1stA) y (1stB)) (f (1stA) z (1st𝐶)))) → ((x ·Q y) +Q (f ·Q z)) (1st ‘(A ·P (B +P 𝐶))))

12-Dec-2019distrlem1pru 6557 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A P B P 𝐶 P) → (2nd ‘(A ·P (B +P 𝐶))) ⊆ (2nd ‘((A ·P B) +P (A ·P 𝐶))))

12-Dec-2019distrlem1prl 6556 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A P B P 𝐶 P) → (1st ‘(A ·P (B +P 𝐶))) ⊆ (1st ‘((A ·P B) +P (A ·P 𝐶))))

12-Dec-2019ltdcnq 6381 Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A Q B Q) → DECID A <Q B)

12-Dec-2019ltdcpi 6307 Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A N B N) → DECID A <N B)

11-Dec-2019mulassprg 6555 Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
((A P B P 𝐶 P) → ((A ·P B) ·P 𝐶) = (A ·P (B ·P 𝐶)))

11-Dec-2019mulcomprg 6554 Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
((A P B P) → (A ·P B) = (B ·P A))

11-Dec-2019addassprg 6553 Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
((A P B P 𝐶 P) → ((A +P B) +P 𝐶) = (A +P (B +P 𝐶)))

11-Dec-2019addcomprg 6552 Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
((A P B P) → (A +P B) = (B +P A))

11-Dec-2019genpassg 6509 Associativity of an operation on reals. (Contributed by Jim Kingdon, 11-Dec-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)    &   dom 𝐹 = (P × P)    &   ((f P g P) → (f𝐹g) P)    &   ((f Q g Q Q) → ((f𝐺g)𝐺) = (f𝐺(g𝐺)))       ((A P B P 𝐶 P) → ((A𝐹B)𝐹𝐶) = (A𝐹(B𝐹𝐶)))

11-Dec-2019genpassu 6508 Associativity of upper cuts. Lemma for genpassg 6509. (Contributed by Jim Kingdon, 11-Dec-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)    &   dom 𝐹 = (P × P)    &   ((f P g P) → (f𝐹g) P)    &   ((f Q g Q Q) → ((f𝐺g)𝐺) = (f𝐺(g𝐺)))       ((A P B P 𝐶 P) → (2nd ‘((A𝐹B)𝐹𝐶)) = (2nd ‘(A𝐹(B𝐹𝐶))))

11-Dec-2019genpassl 6507 Associativity of lower cuts. Lemma for genpassg 6509. (Contributed by Jim Kingdon, 11-Dec-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)    &   dom 𝐹 = (P × P)    &   ((f P g P) → (f𝐹g) P)    &   ((f Q g Q Q) → ((f𝐺g)𝐺) = (f𝐺(g𝐺)))       ((A P B P 𝐶 P) → (1st ‘((A𝐹B)𝐹𝐶)) = (1st ‘(A𝐹(B𝐹𝐶))))

11-Dec-2019preqlu 6454 Two reals are equal if and only if their lower and upper cuts are. (Contributed by Jim Kingdon, 11-Dec-2019.)
((A P B P) → (A = B ↔ ((1stA) = (1stB) (2ndA) = (2ndB))))

11-Dec-2019fssd 4998 Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(φ𝐹:AB)    &   (φB𝐶)       (φ𝐹:A𝐶)

11-Dec-2019iffalsed 3335 Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(φ → ¬ χ)       (φ → if(χ, A, B) = B)

11-Dec-2019iftrued 3332 Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(φχ)       (φ → if(χ, A, B) = A)

10-Dec-2019mullocprlem 6549 Calculations for mullocpr 6550. (Contributed by Jim Kingdon, 10-Dec-2019.)
(φ → (A P B P))    &   (φ → (𝑈 ·Q 𝑄) <Q (𝐸 ·Q (𝐷 ·Q 𝑈)))    &   (φ → (𝐸 ·Q (𝐷 ·Q 𝑈)) <Q (𝑇 ·Q (𝐷 ·Q 𝑈)))    &   (φ → (𝑇 ·Q (𝐷 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅))    &   (φ → (𝑄 Q 𝑅 Q))    &   (φ → (𝐷 Q 𝑈 Q))    &   (φ → (𝐷 (1stA) 𝑈 (2ndA)))    &   (φ → (𝐸 Q 𝑇 Q))       (φ → (𝑄 (1st ‘(A ·P B)) 𝑅 (2nd ‘(A ·P B))))

10-Dec-2019mulnqpru 6548 Lemma to prove upward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
((((A P 𝐺 (2ndA)) (B P 𝐻 (2ndB))) 𝑋 Q) → ((𝐺 ·Q 𝐻) <Q 𝑋𝑋 (2nd ‘(A ·P B))))

10-Dec-2019mulnqprl 6547 Lemma to prove downward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 <Q (𝐺 ·Q 𝐻) → 𝑋 (1st ‘(A ·P B))))

9-Dec-2019prmuloclemcalc 6544 Calculations for prmuloc 6545. (Contributed by Jim Kingdon, 9-Dec-2019.)
(φ𝑅 <Q 𝑈)    &   (φ𝑈 <Q (𝐷 +Q 𝑃))    &   (φ → (A +Q 𝑋) = B)    &   (φ → (𝑃 ·Q B) <Q (𝑅 ·Q 𝑋))    &   (φA Q)    &   (φB Q)    &   (φ𝐷 Q)    &   (φ𝑃 Q)    &   (φ𝑋 Q)       (φ → (𝑈 ·Q A) <Q (𝐷 ·Q B))

9-Dec-2019appdiv0nq 6543 Approximate division for positive rationals. This can be thought of as a variation of appdivnq 6542 in which A is zero, although it can be stated and proved in terms of positive rationals alone, without zero as such. (Contributed by Jim Kingdon, 9-Dec-2019.)
((B Q 𝐶 Q) → 𝑚 Q (𝑚 ·Q 𝐶) <Q B)

9-Dec-2019ltmnqi 6387 Ordering property of multiplication for positive fractions. One direction of ltmnqg 6385. (Contributed by Jim Kingdon, 9-Dec-2019.)
((A <Q B 𝐶 Q) → (𝐶 ·Q A) <Q (𝐶 ·Q B))

9-Dec-2019ltanqi 6386 Ordering property of addition for positive fractions. One direction of ltanqg 6384. (Contributed by Jim Kingdon, 9-Dec-2019.)
((A <Q B 𝐶 Q) → (𝐶 +Q A) <Q (𝐶 +Q B))

8-Dec-2019bj-nn0sucALT 9362 Alternate proof of bj-nn0suc 9348, also constructive but from ax-inf2 9360, hence requiring ax-bdsetind 9352. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
(A 𝜔 ↔ (A = ∅ x 𝜔 A = suc x))

8-Dec-2019bj-omex2 9361 Using bounded set induction and the strong axiom of infinity, 𝜔 is a set, that is, we recover ax-infvn 9329 (see bj-2inf 9326 for the equivalence of the latter with bj-omex 9330). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
𝜔 V

8-Dec-2019bj-inf2vn2 9359 A sufficient condition for 𝜔 to be a set; unbounded version of bj-inf2vn 9358. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
(A 𝑉 → (x(x A ↔ (x = ∅ y A x = suc y)) → A = 𝜔))

8-Dec-2019bj-inf2vn 9358 A sufficient condition for 𝜔 to be a set. See bj-inf2vn2 9359 for the unbounded version from full set induction. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
BOUNDED A       (A 𝑉 → (x(x A ↔ (x = ∅ y A x = suc y)) → A = 𝜔))

8-Dec-2019bj-inf2vnlem4 9357 Lemma for bj-inf2vn2 9359. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
(x A (x = ∅ y A x = suc y) → (Ind 𝑍A𝑍))

8-Dec-2019bj-inf2vnlem3 9356 Lemma for bj-inf2vn 9358. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
BOUNDED A    &   BOUNDED 𝑍       (x A (x = ∅ y A x = suc y) → (Ind 𝑍A𝑍))

8-Dec-2019bj-inf2vnlem2 9355 Lemma for bj-inf2vnlem3 9356 and bj-inf2vnlem4 9357. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
(x A (x = ∅ y A x = suc y) → (Ind 𝑍u(𝑡 u (𝑡 A𝑡 𝑍) → (u Au 𝑍))))

8-Dec-2019bj-inf2vnlem1 9354 Lemma for bj-inf2vn 9358. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
(x(x A ↔ (x = ∅ y A x = suc y)) → Ind A)

8-Dec-2019bj-bdcel 9226 Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.)
BOUNDED y = A       BOUNDED A x

8-Dec-2019bj-ex 9171 Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1486 and 19.9ht 1529 or 19.23ht 1383). (Proof modification is discouraged.)
(xφφ)

8-Dec-2019mullocpr 6550 Locatedness of multiplication on positive reals. Lemma 12.9 in [BauerTaylor], p. 56 (but where both A and B are positive, not just A). (Contributed by Jim Kingdon, 8-Dec-2019.)
((A P B P) → 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B)))))

8-Dec-2019prmuloc 6545 Positive reals are multiplicatively located. Lemma 12.8 of [BauerTaylor], p. 56. (Contributed by Jim Kingdon, 8-Dec-2019.)
((⟨𝐿, 𝑈 P A <Q B) → 𝑑 Q u Q (𝑑 𝐿 u 𝑈 (u ·Q A) <Q (𝑑 ·Q B)))

8-Dec-2019appdivnq 6542 Approximate division for positive rationals. Proposition 12.7 of [BauerTaylor], p. 55 (a special case where A and B are positive, as well as 𝐶). Our proof is simpler than the one in BauerTaylor because we have reciprocals. (Contributed by Jim Kingdon, 8-Dec-2019.)
((A <Q B 𝐶 Q) → 𝑚 Q (A <Q (𝑚 ·Q 𝐶) (𝑚 ·Q 𝐶) <Q B))

8-Dec-2019nqprxx 6529 The canonical embedding of the rationals into the reals, expressed with the same variable for the lower and upper cuts. (Contributed by Jim Kingdon, 8-Dec-2019.)
(A Q → ⟨{xx <Q A}, {xA <Q x}⟩ P)

8-Dec-2019nqprloc 6528 A cut produced from a rational is located. Lemma for nqprlu 6530. (Contributed by Jim Kingdon, 8-Dec-2019.)
(A Q𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))

8-Dec-2019nqprdisj 6527 A cut produced from a rational is disjoint. Lemma for nqprlu 6530. (Contributed by Jim Kingdon, 8-Dec-2019.)
(A Q𝑞 Q ¬ (𝑞 {xx <Q A} 𝑞 {xA <Q x}))

8-Dec-2019nqprrnd 6526 A cut produced from a rational is rounded. Lemma for nqprlu 6530. (Contributed by Jim Kingdon, 8-Dec-2019.)
(A Q → (𝑞 Q (𝑞 {xx <Q A} ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 {xx <Q A})) 𝑟 Q (𝑟 {xA <Q x} ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 {xA <Q x}))))

8-Dec-2019nqprm 6525 A cut produced from a rational is inhabited. Lemma for nqprlu 6530. (Contributed by Jim Kingdon, 8-Dec-2019.)
(A Q → (𝑞 Q 𝑞 {xx <Q A} 𝑟 Q 𝑟 {xA <Q x}))

8-Dec-2019mpvlu 6522 Value of multiplication on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
((A P B P) → (A ·P B) = ⟨{x Qy (1stA)z (1stB)x = (y ·Q z)}, {x Qy (2ndA)z (2ndB)x = (y ·Q z)}⟩)

8-Dec-2019plpvlu 6521 Value of addition on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
((A P B P) → (A +P B) = ⟨{x Qy (1stA)z (1stB)x = (y +Q z)}, {x Qy (2ndA)z (2ndB)x = (y +Q z)}⟩)

7-Dec-2019addlocprlemeqgt 6515 Lemma for addlocpr 6519. This is a step used in both the 𝑄 = (𝐷 +Q 𝐸) and (𝐷 +Q 𝐸) <Q 𝑄 cases. (Contributed by Jim Kingdon, 7-Dec-2019.)
(φA P)    &   (φB P)    &   (φ𝑄 <Q 𝑅)    &   (φ𝑃 Q)    &   (φ → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   (φ𝐷 (1stA))    &   (φ𝑈 (2ndA))    &   (φ𝑈 <Q (𝐷 +Q 𝑃))    &   (φ𝐸 (1stB))    &   (φ𝑇 (2ndB))    &   (φ𝑇 <Q (𝐸 +Q 𝑃))       (φ → (𝑈 +Q 𝑇) <Q ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)))

7-Dec-2019addnqprulem 6511 Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
(((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) → (𝑆 <Q 𝑋 → ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) 𝑈))

7-Dec-2019addnqprllem 6510 Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
(((⟨𝐿, 𝑈 P 𝐺 𝐿) 𝑋 Q) → (𝑋 <Q 𝑆 → ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) 𝐿))

7-Dec-2019lt2addnq 6388 Ordering property of addition for positive fractions. (Contributed by Jim Kingdon, 7-Dec-2019.)
(((A Q B Q) (𝐶 Q 𝐷 Q)) → ((A <Q B 𝐶 <Q 𝐷) → (A +Q 𝐶) <Q (B +Q 𝐷)))

6-Dec-2019addlocprlem 6518 Lemma for addlocpr 6519. The result, in deduction form. (Contributed by Jim Kingdon, 6-Dec-2019.)
(φA P)    &   (φB P)    &   (φ𝑄 <Q 𝑅)    &   (φ𝑃 Q)    &   (φ → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   (φ𝐷 (1stA))    &   (φ𝑈 (2ndA))    &   (φ𝑈 <Q (𝐷 +Q 𝑃))    &   (φ𝐸 (1stB))    &   (φ𝑇 (2ndB))    &   (φ𝑇 <Q (𝐸 +Q 𝑃))       (φ → (𝑄 (1st ‘(A +P B)) 𝑅 (2nd ‘(A +P B))))

6-Dec-2019addlocprlemgt 6517 Lemma for addlocpr 6519. The (𝐷 +Q 𝐸) <Q 𝑄 case. (Contributed by Jim Kingdon, 6-Dec-2019.)
(φA P)    &   (φB P)    &   (φ𝑄 <Q 𝑅)    &   (φ𝑃 Q)    &   (φ → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   (φ𝐷 (1stA))    &   (φ𝑈 (2ndA))    &   (φ𝑈 <Q (𝐷 +Q 𝑃))    &   (φ𝐸 (1stB))    &   (φ𝑇 (2ndB))    &   (φ𝑇 <Q (𝐸 +Q 𝑃))       (φ → ((𝐷 +Q 𝐸) <Q 𝑄𝑅 (2nd ‘(A +P B))))

6-Dec-2019addlocprlemeq 6516 Lemma for addlocpr 6519. The 𝑄 = (𝐷 +Q 𝐸) case. (Contributed by Jim Kingdon, 6-Dec-2019.)
(φA P)    &   (φB P)    &   (φ𝑄 <Q 𝑅)    &   (φ𝑃 Q)    &   (φ → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   (φ𝐷 (1stA))    &   (φ𝑈 (2ndA))    &   (φ𝑈 <Q (𝐷 +Q 𝑃))    &   (φ𝐸 (1stB))    &   (φ𝑇 (2ndB))    &   (φ𝑇 <Q (𝐸 +Q 𝑃))       (φ → (𝑄 = (𝐷 +Q 𝐸) → 𝑅 (2nd ‘(A +P B))))

6-Dec-2019addlocprlemlt 6514 Lemma for addlocpr 6519. The 𝑄 <Q (𝐷 +Q 𝐸) case. (Contributed by Jim Kingdon, 6-Dec-2019.)
(φA P)    &   (φB P)    &   (φ𝑄 <Q 𝑅)    &   (φ𝑃 Q)    &   (φ → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   (φ𝐷 (1stA))    &   (φ𝑈 (2ndA))    &   (φ𝑈 <Q (𝐷 +Q 𝑃))    &   (φ𝐸 (1stB))    &   (φ𝑇 (2ndB))    &   (φ𝑇 <Q (𝐸 +Q 𝑃))       (φ → (𝑄 <Q (𝐷 +Q 𝐸) → 𝑄 (1st ‘(A +P B))))

5-Dec-2019addlocpr 6519 Locatedness of addition on positive reals. Lemma 11.16 in [BauerTaylor], p. 53. The proof in BauerTaylor relies on signed rationals, so we replace it with another proof which applies prarloc 6485 to both A and B, and uses nqtri3or 6380 rather than prloc 6473 to decide whether 𝑞 is too big to be in the lower cut of A +P B (and deduce that if it is, then 𝑟 must be in the upper cut). What the two proofs have in common is that they take the difference between 𝑞 and 𝑟 to determine how tight a range they need around the real numbers. (Contributed by Jim Kingdon, 5-Dec-2019.)
((A P B P) → 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A +P B)) 𝑟 (2nd ‘(A +P B)))))

5-Dec-2019addnqpru 6513 Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
((((A P 𝐺 (2ndA)) (B P 𝐻 (2ndB))) 𝑋 Q) → ((𝐺 +Q 𝐻) <Q 𝑋𝑋 (2nd ‘(A +P B))))

5-Dec-2019addnqprl 6512 Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 <Q (𝐺 +Q 𝐻) → 𝑋 (1st ‘(A +P B))))

5-Dec-2019genpmu 6501 The upper cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Dec-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)       ((A P B P) → 𝑞 Q 𝑞 (2nd ‘(A𝐹B)))

5-Dec-2019genpelxp 6493 Set containing the result of adding or multiplying positive reals. (Contributed by Jim Kingdon, 5-Dec-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)       ((A P B P) → (A𝐹B) (𝒫 Q × 𝒫 Q))

3-Dec-2019addassnq0lemcl 6443 A natural number closure law. Lemma for addassnq0 6444. (Contributed by Jim Kingdon, 3-Dec-2019.)
(((𝐼 𝜔 𝐽 N) (𝐾 𝜔 𝐿 N)) → (((𝐼 ·𝑜 𝐿) +𝑜 (𝐽 ·𝑜 𝐾)) 𝜔 (𝐽 ·𝑜 𝐿) N))

3-Dec-2019nndir 6008 Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.)
((A 𝜔 B 𝜔 𝐶 𝜔) → ((A +𝑜 B) ·𝑜 𝐶) = ((A ·𝑜 𝐶) +𝑜 (B ·𝑜 𝐶)))

1-Dec-2019nnanq0 6440 Addition of non-negative fractions with a common denominator. You can add two fractions with the same denominator by adding their numerators and keeping the same denominator. (Contributed by Jim Kingdon, 1-Dec-2019.)
((𝑁 𝜔 𝑀 𝜔 A N) → [⟨(𝑁 +𝑜 𝑀), A⟩] ~Q0 = ([⟨𝑁, A⟩] ~Q0 +Q0 [⟨𝑀, A⟩] ~Q0 ))

1-Dec-2019archnqq 6400 For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Jim Kingdon, 1-Dec-2019.)
(A Qx N A <Q [⟨x, 1𝑜⟩] ~Q )

30-Nov-2019bj-2inf 9326 Two formulations of the axiom of infinity (see ax-infvn 9329 and bj-omex 9330) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
(𝜔 V ↔ x(Ind x y(Ind yxy)))

30-Nov-2019bj-om 9325 A set is equal to 𝜔 if and only if it is the smallest inductive set. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
(A 𝑉 → (A = 𝜔 ↔ (Ind A x(Ind xAx))))

30-Nov-2019bj-ssom 9324 A characterization of subclasses of 𝜔. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
(x(Ind xAx) ↔ A ⊆ 𝜔)

30-Nov-2019bj-omssind 9323 𝜔 is included in all the inductive sets (but for the moment, we cannot prove that it is included in all the inductive classes). (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
(A 𝑉 → (Ind A → 𝜔 ⊆ A))

30-Nov-2019bj-omind 9322 𝜔 is an inductive class. (Contributed by BJ, 30-Nov-2019.)
Ind 𝜔

30-Nov-2019bj-dfom 9321 Alternate definition of 𝜔, as the intersection of all the inductive sets. Proposal: make this the definition. (Contributed by BJ, 30-Nov-2019.)
𝜔 = {x ∣ Ind x}

30-Nov-2019bj-indint 9320 The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.)
Ind {x A ∣ Ind x}

30-Nov-2019bj-bdind 9319 Boundedness of the formula "the setvar x is an inductive class". (Contributed by BJ, 30-Nov-2019.)
BOUNDED Ind x

30-Nov-2019bj-indeq 9318 Equality property for Ind. (Contributed by BJ, 30-Nov-2019.)
(A = B → (Ind A ↔ Ind B))

30-Nov-2019bj-indsuc 9317 A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.)
(Ind A → (B A → suc B A))

30-Nov-2019df-bj-ind 9316 Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.)
(Ind A ↔ (∅ A x A suc x A))

30-Nov-2019bj-bdsucel 9271 Boundedness of the formula "the successor of the setvar x belongs to the setvar y". (Contributed by BJ, 30-Nov-2019.)
BOUNDED suc x y

30-Nov-2019bj-bd0el 9257 Boundedness of the formula "the empty set belongs to the setvar x". (Contributed by BJ, 30-Nov-2019.)
BOUNDED x

30-Nov-2019bj-sseq 9200 If two converse inclusions are characterized each by a formula, then equality is characterized by the conjunction of these formulas. (Contributed by BJ, 30-Nov-2019.)
(φ → (ψAB))    &   (φ → (χBA))       (φ → ((ψ χ) ↔ A = B))

30-Nov-2019nqpnq0nq 6435 A positive fraction plus a non-negative fraction is a positive fraction. (Contributed by Jim Kingdon, 30-Nov-2019.)
((A Q B Q0) → (A +Q0 B) Q)

30-Nov-2019mulclnq0 6434 Closure of multiplication on non-negative fractions. (Contributed by Jim Kingdon, 30-Nov-2019.)
((A Q0 B Q0) → (A ·Q0 B) Q0)

30-Nov-2019prarloclemarch 6401 A version of the Archimedean property. This variation is "stronger" than archnqq 6400 in the sense that we provide an integer which is larger than a given rational A even after being multiplied by a second rational B. (Contributed by Jim Kingdon, 30-Nov-2019.)
((A Q B Q) → x N A <Q ([⟨x, 1𝑜⟩] ~Q ·Q B))

29-Nov-2019bj-elssuniab 9199 Version of elssuni 3599 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)
xA       (A 𝑉 → ([A / x]φA {xφ}))

29-Nov-2019bj-intabssel1 9198 Version of intss1 3621 using a class abstraction and implicit substitution. Closed form of intmin3 3633. (Contributed by BJ, 29-Nov-2019.)
xA    &   xψ    &   (x = A → (ψφ))       (A 𝑉 → (ψ {xφ} ⊆ A))

29-Nov-2019bj-intabssel 9197 Version of intss1 3621 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)
xA       (A 𝑉 → ([A / x]φ {xφ} ⊆ A))

29-Nov-2019nq02m 6447 Multiply a non-negative fraction by two. (Contributed by Jim Kingdon, 29-Nov-2019.)
(A Q0 → ([⟨2𝑜, 1𝑜⟩] ~Q0 ·Q0 A) = (A +Q0 A))

29-Nov-2019distnq0r 6445 Multiplication of non-negative fractions is distributive. Version of distrnq0 6441 with the multiplications commuted. (Contributed by Jim Kingdon, 29-Nov-2019.)
((A Q0 B Q0 𝐶 Q0) → ((B +Q0 𝐶) ·Q0 A) = ((B ·Q0 A) +Q0 (𝐶 ·Q0 A)))

29-Nov-2019addassnq0 6444 Addition of non-negaative fractions is associative. (Contributed by Jim Kingdon, 29-Nov-2019.)
((A Q0 B Q0 𝐶 Q0) → ((A +Q0 B) +Q0 𝐶) = (A +Q0 (B +Q0 𝐶)))

29-Nov-2019addclnq0 6433 Closure of addition on non-negative fractions. (Contributed by Jim Kingdon, 29-Nov-2019.)
((A Q0 B Q0) → (A +Q0 B) Q0)

29-Nov-2019mulcanenq0ec 6427 Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 29-Nov-2019.)
((A N B 𝜔 𝐶 N) → [⟨(A ·𝑜 B), (A ·𝑜 𝐶)⟩] ~Q0 = [⟨B, 𝐶⟩] ~Q0 )

28-Nov-2019ax-bdsetind 9352 Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.)
BOUNDED φ       (𝑎(y 𝑎 [y / 𝑎]φφ) → 𝑎φ)

28-Nov-2019bj-peano4 9343 Remove from peano4 4263 dependency on ax-setind 4220. Therefore, it only requires core constructive axioms (albeit more of them). (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.)
((A 𝜔 B 𝜔) → (suc A = suc BA = B))

28-Nov-2019bj-nnen2lp 9342 A version of en2lp 4232 for natural numbers, which does not require ax-setind 4220.

Note: using this theorem and bj-nnelirr 9341, one can remove dependency on ax-setind 4220 from nntri2 6012 and nndcel 6016; one can actually remove more dependencies from these. (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.)

((A 𝜔 B 𝜔) → ¬ (A B B A))

27-Nov-2019mulcomnq0 6442 Multiplication of non-negative fractions is commutative. (Contributed by Jim Kingdon, 27-Nov-2019.)
((A Q0 B Q0) → (A ·Q0 B) = (B ·Q0 A))

27-Nov-2019distrnq0 6441 Multiplication of non-negative fractions is distributive. (Contributed by Jim Kingdon, 27-Nov-2019.)
((A Q0 B Q0 𝐶 Q0) → (A ·Q0 (B +Q0 𝐶)) = ((A ·Q0 B) +Q0 (A ·Q0 𝐶)))

25-Nov-2019prcunqu 6467 An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.)
((⟨𝐿, 𝑈 P 𝐶 𝑈) → (𝐶 <Q BB 𝑈))

25-Nov-2019prarloclemarch2 6402 Like prarloclemarch 6401 but the integer must be at least two, and there is also B added to the right hand side. These details follow straightforwardly but are chosen to be helpful in the proof of prarloc 6485. (Contributed by Jim Kingdon, 25-Nov-2019.)
((A Q B Q 𝐶 Q) → x N (1𝑜 <N x A <Q (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶))))

25-Nov-2019subhalfnqq 6397 There is a number which is less than half of any positive fraction. The case where A is one is Lemma 11.4 of [BauerTaylor], p. 50, and they use the word "approximate half" for such a number (since there may be constructions, for some structures other than the rationals themselves, which rely on such an approximate half but do not require division by two as seen at halfnqq 6393). (Contributed by Jim Kingdon, 25-Nov-2019.)
(A Qx Q (x +Q x) <Q A)

24-Nov-2019bj-nnelirr 9341 A natural number does not belong to itself. Version of elirr 4224 for natural numbers, which does not require ax-setind 4220. (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.)
(A 𝜔 → ¬ A A)

24-Nov-2019bdcriota 9272 A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.)
BOUNDED φ    &   ∃!x y φ       BOUNDED (x y φ)

24-Nov-2019nq0nn 6424 Decomposition of a non-negative fraction into numerator and denominator. (Contributed by Jim Kingdon, 24-Nov-2019.)
(A Q0wv((w 𝜔 v N) A = [⟨w, v⟩] ~Q0 ))

24-Nov-2019enq0eceq 6419 Equivalence class equality of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 24-Nov-2019.)
(((A 𝜔 B N) (𝐶 𝜔 𝐷 N)) → ([⟨A, B⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ↔ (A ·𝑜 𝐷) = (B ·𝑜 𝐶)))

24-Nov-2019dfplq0qs 6412 Addition on non-negative fractions. This definition is similar to df-plq0 6409 but expands Q0 (Contributed by Jim Kingdon, 24-Nov-2019.)
+Q0 = {⟨⟨x, y⟩, z⟩ ∣ ((x ((𝜔 × N) / ~Q0 ) y ((𝜔 × N) / ~Q0 )) wvuf((x = [⟨w, v⟩] ~Q0 y = [⟨u, f⟩] ~Q0 ) z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 ))}

23-Nov-2019addnq0mo 6429 There is at most one result from adding non-negative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.)
((A ((𝜔 × N) / ~Q0 ) B ((𝜔 × N) / ~Q0 )) → ∃*zwvu𝑡((A = [⟨w, v⟩] ~Q0 B = [⟨u, 𝑡⟩] ~Q0 ) z = [⟨((w ·𝑜 𝑡) +𝑜 (v ·𝑜 u)), (v ·𝑜 𝑡)⟩] ~Q0 ))

23-Nov-2019nnnq0lem1 6428 Decomposing non-negative fractions into natural numbers. Lemma for addnnnq0 6431 and mulnnnq0 6432. (Contributed by Jim Kingdon, 23-Nov-2019.)
(((A ((𝜔 × N) / ~Q0 ) B ((𝜔 × N) / ~Q0 )) (((A = [⟨w, v⟩] ~Q0 B = [⟨u, 𝑡⟩] ~Q0 ) z = [𝐶] ~Q0 ) ((A = [⟨𝑠, f⟩] ~Q0 B = [⟨g, ⟩] ~Q0 ) 𝑞 = [𝐷] ~Q0 ))) → ((((w 𝜔 v N) (𝑠 𝜔 f N)) ((u 𝜔 𝑡 N) (g 𝜔 N))) ((w ·𝑜 f) = (v ·𝑜 𝑠) (u ·𝑜 ) = (𝑡 ·𝑜 g))))

23-Nov-2019addcmpblnq0 6425 Lemma showing compatibility of addition on non-negative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.)
((((A 𝜔 B N) (𝐶 𝜔 𝐷 N)) ((𝐹 𝜔 𝐺 N) (𝑅 𝜔 𝑆 N))) → (((A ·𝑜 𝐷) = (B ·𝑜 𝐶) (𝐹 ·𝑜 𝑆) = (𝐺 ·𝑜 𝑅)) → ⟨((A ·𝑜 𝐺) +𝑜 (B ·𝑜 𝐹)), (B ·𝑜 𝐺)⟩ ~Q0 ⟨((𝐶 ·𝑜 𝑆) +𝑜 (𝐷 ·𝑜 𝑅)), (𝐷 ·𝑜 𝑆)⟩))

23-Nov-2019ee8anv 1807 Rearrange existential quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
(xyzwvu𝑡𝑠(φ ψ) ↔ (xyzwφ vu𝑡𝑠ψ))

23-Nov-201919.42vvvv 1787 Theorem 19.42 of [Margaris] p. 90 with 4 quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
(wxyz(φ ψ) ↔ (φ wxyzψ))

22-Nov-2019bdsetindis 9353 Axiom of bounded set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
BOUNDED φ    &   xψ    &   xχ    &   yφ    &   yψ    &   (x = z → (φψ))    &   (x = y → (χφ))       (y(z y ψχ) → xφ)

22-Nov-2019setindis 9351 Axiom of set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.)
xψ    &   xχ    &   yφ    &   yψ    &   (x = z → (φψ))    &   (x = y → (χφ))       (y(z y ψχ) → xφ)

22-Nov-2019setindf 9350 Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.)
yφ       (x(y x [y / x]φφ) → xφ)

22-Nov-2019setindft 9349 Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.)
(xyφ → (x(y x [y / x]φφ) → xφ))

22-Nov-2019bj-nntrans2 9340 A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
(A 𝜔 → Tr A)

22-Nov-2019bj-nntrans 9339 A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
(A 𝜔 → (B ABA))

22-Nov-2019bdfind 9334 Bounded induction (principle of induction when A is assumed to be bounded), proved from basic constructive axioms. See find 4265 for a nonconstructive proof of the general case. See findset 9333 for a proof when A is assumed to be a set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
BOUNDED A       ((A ⊆ 𝜔 A x A suc x A) → A = 𝜔)

22-Nov-2019findset 9333 Bounded induction (principle of induction when A is assumed to be a set) allowing a proof from basic constructive axioms. See find 4265 for a nonconstructive proof of the general case. See bdfind 9334 for a proof when A is assumed to be bounded. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
(A 𝑉 → ((A ⊆ 𝜔 A x A suc x A) → A = 𝜔))

22-Nov-2019cbvrald 9196 Rule used to change bound variables, using implicit substitution. (Contributed by BJ, 22-Nov-2019.)
xφ    &   yφ    &   (φ → Ⅎyψ)    &   (φ → Ⅎxχ)    &   (φ → (x = y → (ψχ)))       (φ → (x A ψy A χ))

22-Nov-2019addnnnq0 6431 Addition of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 22-Nov-2019.)
(((A 𝜔 B N) (𝐶 𝜔 𝐷 N)) → ([⟨A, B⟩] ~Q0 +Q0 [⟨𝐶, 𝐷⟩] ~Q0 ) = [⟨((A ·𝑜 𝐷) +𝑜 (B ·𝑜 𝐶)), (B ·𝑜 𝐷)⟩] ~Q0 )

22-Nov-2019dfmq0qs 6411 Multiplication on non-negative fractions. This definition is similar to df-mq0 6410 but expands Q0 (Contributed by Jim Kingdon, 22-Nov-2019.)
·Q0 = {⟨⟨x, y⟩, z⟩ ∣ ((x ((𝜔 × N) / ~Q0 ) y ((𝜔 × N) / ~Q0 )) wvuf((x = [⟨w, v⟩] ~Q0 y = [⟨u, f⟩] ~Q0 ) z = [⟨(w ·𝑜 u), (v ·𝑜 f)⟩] ~Q0 ))}

21-Nov-2019bj-findes 9365 Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 9363 for explanations. From this version, it is easy to prove findes 4269. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
(([∅ / x]φ x 𝜔 (φ[suc x / x]φ)) → x 𝜔 φ)

21-Nov-2019bj-findisg 9364 Version of bj-findis 9363 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 9363 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
xψ    &   xχ    &   xθ    &   (x = ∅ → (ψφ))    &   (x = y → (φχ))    &   (x = suc y → (θφ))    &   xA    &   xτ    &   (x = A → (φτ))       ((ψ y 𝜔 (χθ)) → (A 𝜔 → τ))

21-Nov-2019bj-bdfindes 9337 Bounded induction (principle of induction for bounded formulas), using explicit substitutions. Constructive proof (from CZF). See the comment of bj-bdfindis 9335 for explanations. From this version, it is easy to prove the bounded version of findes 4269. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
BOUNDED φ       (([∅ / x]φ x 𝜔 (φ[suc x / x]φ)) → x 𝜔 φ)

21-Nov-2019bj-bdfindisg 9336 Version of bj-bdfindis 9335 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-bdfindis 9335 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
BOUNDED φ    &   xψ    &   xχ    &   xθ    &   (x = ∅ → (ψφ))    &   (x = y → (φχ))    &   (x = suc y → (θφ))    &   xA    &   xτ    &   (x = A → (φτ))       ((ψ y 𝜔 (χθ)) → (A 𝜔 → τ))

21-Nov-2019bj-bdfindis 9335 Bounded induction (principle of induction for bounded formulas), using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See finds 4266 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4266, finds2 4267, finds1 4268. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
BOUNDED φ    &   xψ    &   xχ    &   xθ    &   (x = ∅ → (ψφ))    &   (x = y → (φχ))    &   (x = suc y → (θφ))       ((ψ y 𝜔 (χθ)) → x 𝜔 φ)

21-Nov-2019bdeqsuc 9270 Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.)
BOUNDED x = suc y

21-Nov-2019bdop 9264 The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
BOUNDEDx, y

21-Nov-2019bdeq0 9256 Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.)
BOUNDED x = ∅

21-Nov-2019bj-rspg 9195 Restricted specialization, generalized. Weakens a hypothesis of rspccv 2647 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)
xA    &   xB    &   xψ    &   (x = A → (φψ))       (x B φ → (A Bψ))

21-Nov-2019bj-rspgt 9194 Restricted specialization, generalized. Weakens a hypothesis of rspccv 2647 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)
xA    &   xB    &   xψ       (x(x = A → (φψ)) → (x B φ → (A Bψ)))

21-Nov-2019elabg2 9193 One implication of elabg 2682. (Contributed by BJ, 21-Nov-2019.)
(x = A → (ψφ))       (A 𝑉 → (ψA {xφ}))

21-Nov-2019elab2a 9192 One implication of elab 2681. (Contributed by BJ, 21-Nov-2019.)
A V    &   (x = A → (ψφ))       (ψA {xφ})

21-Nov-2019elab1 9191 One implication of elab 2681. (Contributed by BJ, 21-Nov-2019.)
(x = A → (φψ))       (A {xφ} → ψ)

21-Nov-2019elabf2 9190 One implication of elabf 2680. (Contributed by BJ, 21-Nov-2019.)
xψ    &   A V    &   (x = A → (ψφ))       (ψA {xφ})

21-Nov-2019elabf1 9189 One implication of elabf 2680. (Contributed by BJ, 21-Nov-2019.)
xψ    &   (x = A → (φψ))       (A {xφ} → ψ)

21-Nov-2019elabgf2 9188 One implication of elabgf 2679. (Contributed by BJ, 21-Nov-2019.)
xA    &   xψ    &   (x = A → (ψφ))       (A B → (ψA {xφ}))

21-Nov-2019elabgf1 9187 One implication of elabgf 2679. (Contributed by BJ, 21-Nov-2019.)
xA    &   xψ    &   (x = A → (φψ))       (A {xφ} → ψ)

21-Nov-2019elabgft1 9186 One implication of elabgf 2679, in closed form. (Contributed by BJ, 21-Nov-2019.)
xA    &   xψ       (x(x = A → (φψ)) → (A {xφ} → ψ))

21-Nov-2019elabgf0 9185 Lemma for elabgf 2679. (Contributed by BJ, 21-Nov-2019.)
(x = A → (A {xφ} ↔ φ))

21-Nov-2019bj-vtoclgf 9184 Weakening two hypotheses of vtoclgf 2606. (Contributed by BJ, 21-Nov-2019.)
xA    &   xψ    &   (x = Aφ)    &   (x = A → (φψ))       (A 𝑉ψ)

21-Nov-2019bj-vtoclgft 9183 Weakening two hypotheses of vtoclgf 2606. (Contributed by BJ, 21-Nov-2019.)
xA    &   xψ    &   (x = Aφ)       (x(x = A → (φψ)) → (A 𝑉ψ))

21-Nov-2019bj-exlimmpi 9179 Lemma for bj-vtoclgf 9184. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
xψ    &   (χφ)    &   (χ → (φψ))       (xχψ)

21-Nov-2019bj-exlimmp 9178 Lemma for bj-vtoclgf 9184. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
xψ    &   (χφ)       (x(χ → (φψ)) → (xχψ))

21-Nov-20193anim2i 1090 Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019.)
(φψ)       ((χ φ θ) → (χ ψ θ))

20-Nov-2019mulnq0mo 6430 There is at most one result from multiplying non-negative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.)
((A ((𝜔 × N) / ~Q0 ) B ((𝜔 × N) / ~Q0 )) → ∃*zwvu𝑡((A = [⟨w, v⟩] ~Q0 B = [⟨u, 𝑡⟩] ~Q0 ) z = [⟨(w ·𝑜 u), (v ·𝑜 𝑡)⟩] ~Q0 ))

20-Nov-2019mulcmpblnq0 6426 Lemma showing compatibility of multiplication on non-negative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.)