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

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

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

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

Last updated on 21-Sep-2021 at 11:49 PM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
17-Sep-2021ontr2exmid 4222 An ordinal transitivity law which implies excluded middle. (Contributed by Jim Kingdon, 17-Sep-2021.)
𝑥 ∈ On ∀𝑦𝑧 ∈ On ((𝑥𝑦𝑦𝑧) → 𝑥𝑧)       (𝜑 ∨ ¬ 𝜑)
 
16-Sep-2021nnsseleq 6042 For natural numbers, inclusion is equivalent to membership or equality. (Contributed by Jim Kingdon, 16-Sep-2021.)
((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴𝐵 ↔ (𝐴𝐵𝐴 = 𝐵)))
 
15-Sep-2021fientri3 6315 Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon, 15-Sep-2021.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴𝐵𝐵𝐴))
 
15-Sep-2021nntri2or2 6039 A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-Sep-2021.)
((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴𝐵𝐵𝐴))
 
14-Sep-2021findcard2sd 6311 Deduction form of finite set induction . (Contributed by Jim Kingdon, 14-Sep-2021.)
(𝑥 = ∅ → (𝜓𝜒))    &   (𝑥 = 𝑦 → (𝜓𝜃))    &   (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓𝜏))    &   (𝑥 = 𝐴 → (𝜓𝜂))    &   (𝜑𝜒)    &   (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → (𝜃𝜏))    &   (𝜑𝐴 ∈ Fin)       (𝜑𝜂)
 
13-Sep-2021php5fin 6302 A finite set is not equinumerous to a set which adds one element. (Contributed by Jim Kingdon, 13-Sep-2021.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ (V ∖ 𝐴)) → ¬ 𝐴 ≈ (𝐴 ∪ {𝐵}))
 
13-Sep-2021fiunsnnn 6301 Adding one element to a finite set which is equinumerous to a natural number. (Contributed by Jim Kingdon, 13-Sep-2021.)
(((𝐴 ∈ Fin ∧ 𝐵 ∈ (V ∖ 𝐴)) ∧ (𝑁 ∈ ω ∧ 𝐴𝑁)) → (𝐴 ∪ {𝐵}) ≈ suc 𝑁)
 
12-Sep-2021fisbth 6303 Schroeder-Bernstein Theorem for finite sets. (Contributed by Jim Kingdon, 12-Sep-2021.)
(((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴𝐵𝐵𝐴)) → 𝐴𝐵)
 
11-Sep-2021diffisn 6312 Subtracting a singleton from a finite set produces a finite set. (Contributed by Jim Kingdon, 11-Sep-2021.)
((𝐴 ∈ Fin ∧ 𝐵𝐴) → (𝐴 ∖ {𝐵}) ∈ Fin)
 
10-Sep-2021fin0 6305 A nonempty finite set has at least one element. (Contributed by Jim Kingdon, 10-Sep-2021.)
(𝐴 ∈ Fin → (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴))
 
9-Sep-2021fidifsnid 6295 If we remove a single element from a finite set then put it back in, we end up with the original finite set. This strengthens difsnss 3507 from subset to equality when the set is finite. (Contributed by Jim Kingdon, 9-Sep-2021.)
((𝐴 ∈ Fin ∧ 𝐵𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
 
9-Sep-2021fidifsnen 6294 All decrements of a finite set are equinumerous. (Contributed by Jim Kingdon, 9-Sep-2021.)
((𝑋 ∈ Fin ∧ 𝐴𝑋𝐵𝑋) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵}))
 
8-Sep-2021diffifi 6313 Subtracting one finite set from another produces a finite set. (Contributed by Jim Kingdon, 8-Sep-2021.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐵𝐴) → (𝐴𝐵) ∈ Fin)
 
8-Sep-2021diffitest 6306 If subtracting any set from a finite set gives a finite set, any proposition of the form ¬ 𝜑 is decidable. This is not a proof of full excluded middle, but it is close enough to show we won't be able to prove 𝐴 ∈ Fin → (𝐴𝐵) ∈ Fin. (Contributed by Jim Kingdon, 8-Sep-2021.)
𝑎 ∈ Fin ∀𝑏(𝑎𝑏) ∈ Fin       𝜑 ∨ ¬ ¬ 𝜑)
 
6-Sep-2021phpelm 6291 Pigeonhole Principle. A natural number is not equinumerous to an element of itself. (Contributed by Jim Kingdon, 6-Sep-2021.)
((𝐴 ∈ ω ∧ 𝐵𝐴) → ¬ 𝐴𝐵)
 
5-Sep-2021fidceq 6293 Equality of members of a finite set is decidable. This may be counterintuitive: cannot any two sets be elements of a finite set? Well, to show, for example, that {𝐵, 𝐶} is finite would require showing it is equinumerous to 1𝑜 or to 2𝑜 but to show that you'd need to know 𝐵 = 𝐶 or ¬ 𝐵 = 𝐶, respectively. (Contributed by Jim Kingdon, 5-Sep-2021.)
((𝐴 ∈ Fin ∧ 𝐵𝐴𝐶𝐴) → DECID 𝐵 = 𝐶)
 
5-Sep-2021phplem4on 6292 Equinumerosity of successors of an ordinal and a natural number implies equinumerosity of the originals. (Contributed by Jim Kingdon, 5-Sep-2021.)
((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵𝐴𝐵))
 
3-Sep-20210elsucexmid 4259 If the successor of any ordinal class contains the empty set, excluded middle follows. (Contributed by Jim Kingdon, 3-Sep-2021.)
𝑥 ∈ On ∅ ∈ suc 𝑥       (𝜑 ∨ ¬ 𝜑)
 
1-Sep-2021php5dom 6288 A natural number does not dominate its successor. (Contributed by Jim Kingdon, 1-Sep-2021.)
(𝐴 ∈ ω → ¬ suc 𝐴𝐴)
 
1-Sep-2021phplem4dom 6287 Dominance of successors implies dominance of the original natural numbers. (Contributed by Jim Kingdon, 1-Sep-2021.)
((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≼ suc 𝐵𝐴𝐵))
 
1-Sep-2021snnen2oprc 6286 A singleton {𝐴} is never equinumerous with the ordinal number 2. If 𝐴 is a set, see snnen2og 6285. (Contributed by Jim Kingdon, 1-Sep-2021.)
𝐴 ∈ V → ¬ {𝐴} ≈ 2𝑜)
 
1-Sep-2021snnen2og 6285 A singleton {𝐴} is never equinumerous with the ordinal number 2. If 𝐴 is a proper class, see snnen2oprc 6286. (Contributed by Jim Kingdon, 1-Sep-2021.)
(𝐴𝑉 → ¬ {𝐴} ≈ 2𝑜)
 
1-Sep-2021phplem3g 6282 A natural number is equinumerous to its successor minus any element of the successor. Version of phplem3 6280 with unnecessary hypotheses removed. (Contributed by Jim Kingdon, 1-Sep-2021.)
((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵}))
 
31-Aug-2021nndifsnid 6043 If we remove a single element from a natural number then put it back in, we end up with the original natural number. This strengthens difsnss 3507 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
((𝐴 ∈ ω ∧ 𝐵𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
 
30-Aug-2021carden2bex 6326 If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.)
((𝐴𝐵 ∧ ∃𝑥 ∈ On 𝑥𝐴) → (card‘𝐴) = (card‘𝐵))
 
30-Aug-2021cardval3ex 6322 The value of (card‘𝐴). (Contributed by Jim Kingdon, 30-Aug-2021.)
(∃𝑥 ∈ On 𝑥𝐴 → (card‘𝐴) = {𝑦 ∈ On ∣ 𝑦𝐴})
 
30-Aug-2021cardcl 6318 The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.)
(∃𝑦 ∈ On 𝑦𝐴 → (card‘𝐴) ∈ On)
 
30-Aug-2021onintrab2im 4216 An existence condition which implies an intersection is an ordinal number. (Contributed by Jim Kingdon, 30-Aug-2021.)
(∃𝑥 ∈ On 𝜑 {𝑥 ∈ On ∣ 𝜑} ∈ On)
 
30-Aug-2021onintonm 4215 The intersection of an inhabited collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by Mario Carneiro and Jim Kingdon, 30-Aug-2021.)
((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → 𝐴 ∈ On)
 
29-Aug-2021onintexmid 4267 If the intersection (infimum) of an inhabited class of ordinal numbers belongs to the class, excluded middle follows. The hypothesis is an instance of ((𝐴 ⊆ On ∧ ∃𝑥𝑥𝐴) → 𝐴𝐴) which we would be able to prove given excluded middle. (Contributed by Mario Carneiro and Jim Kingdon, 29-Aug-2021.)
(({𝑦, 𝑧} ⊆ On ∧ ∃𝑥 𝑥 ∈ {𝑦, 𝑧}) → {𝑦, 𝑧} ∈ {𝑦, 𝑧})       (𝜑 ∨ ¬ 𝜑)
 
29-Aug-2021ordtri2or2exmid 4266 Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 29-Aug-2021.)
𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑦𝑥)       (𝜑 ∨ ¬ 𝜑)
 
29-Aug-2021ordtri2or2exmidlem 4223 A set which is 2𝑜 if 𝜑 or if ¬ 𝜑 is an ordinal. (Contributed by Jim Kingdon, 29-Aug-2021.)
{𝑥 ∈ {∅, {∅}} ∣ 𝜑} ∈ On
 
29-Aug-20212ordpr 4221 Version of 2on 5972 with the definition of 2𝑜 expanded and expressed in terms of Ord. (Contributed by Jim Kingdon, 29-Aug-2021.)
Ord {∅, {∅}}
 
25-Aug-2021nnap0d 7911 A positive integer is apart from zero. (Contributed by Jim Kingdon, 25-Aug-2021.)
(𝜑𝐴 ∈ ℕ)       (𝜑𝐴 # 0)
 
24-Aug-2021climcaucn 9723 A converging sequence of complex numbers is a Cauchy sequence. This is like climcau 9719 but adds the part that (𝐹𝑘) is complex. (Contributed by Jim Kingdon, 24-Aug-2021.)
𝑍 = (ℤ𝑀)       ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − (𝐹𝑗))) < 𝑥))
 
24-Aug-2021climcvg1nlem 9721 Lemma for climcvg1n 9722. We construct sequences of the real and imaginary parts of each term of 𝐹, show those converge, and use that to show that 𝐹 converges. (Contributed by Jim Kingdon, 24-Aug-2021.)
(𝜑𝐹:ℕ⟶ℂ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)(abs‘((𝐹𝑘) − (𝐹𝑛))) < (𝐶 / 𝑛))    &   𝐺 = (𝑥 ∈ ℕ ↦ (ℜ‘(𝐹𝑥)))    &   𝐻 = (𝑥 ∈ ℕ ↦ (ℑ‘(𝐹𝑥)))    &   𝐽 = (𝑥 ∈ ℕ ↦ (i · (𝐻𝑥)))       (𝜑𝐹 ∈ dom ⇝ )
 
23-Aug-2021climcvg1n 9722 A Cauchy sequence of complex numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within 𝐶 / 𝑛 of the nth term, where 𝐶 is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
(𝜑𝐹:ℕ⟶ℂ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)(abs‘((𝐹𝑘) − (𝐹𝑛))) < (𝐶 / 𝑛))       (𝜑𝐹 ∈ dom ⇝ )
 
23-Aug-2021climrecvg1n 9720 A Cauchy sequence of real numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within 𝐶 / 𝑛 of the nth term, where 𝐶 is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
(𝜑𝐹:ℕ⟶ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)(abs‘((𝐹𝑘) − (𝐹𝑛))) < (𝐶 / 𝑛))       (𝜑𝐹 ∈ dom ⇝ )
 
22-Aug-2021climserile 9718 The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by Jim Kingdon, 22-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑁𝑍)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → 0 ≤ (𝐹𝑘))       (𝜑 → (seq𝑀( + , 𝐹, ℂ)‘𝑁) ≤ 𝐴)
 
22-Aug-2021iserige0 9716 The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → 0 ≤ (𝐹𝑘))       (𝜑 → 0 ≤ 𝐴)
 
22-Aug-2021iserile 9715 Comparison of the limits of two infinite series. (Contributed by Jim Kingdon, 22-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)    &   (𝜑 → seq𝑀( + , 𝐺, ℂ) ⇝ 𝐵)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ≤ (𝐺𝑘))       (𝜑𝐴𝐵)
 
22-Aug-2021serile 9107 Comparison of partial sums of two infinite series of reals. (Contributed by Jim Kingdon, 22-Aug-2021.)
(𝜑𝑁 ∈ (ℤ𝑀))    &   ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) ∈ ℝ)    &   ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ≤ (𝐺𝑘))       (𝜑 → (seq𝑀( + , 𝐹, ℂ)‘𝑁) ≤ (seq𝑀( + , 𝐺, ℂ)‘𝑁))
 
22-Aug-2021serige0 9106 A finite sum of nonnegative terms is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.)
(𝜑𝑁 ∈ (ℤ𝑀))    &   ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℝ)    &   ((𝜑𝑘 ∈ (ℤ𝑀)) → 0 ≤ (𝐹𝑘))       (𝜑 → 0 ≤ (seq𝑀( + , 𝐹, ℂ)‘𝑁))
 
21-Aug-2021clim2iser2 9711 The limit of an infinite series with an initial segment added. (Contributed by Jim Kingdon, 21-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑁𝑍)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   (𝜑 → seq(𝑁 + 1)( + , 𝐹, ℂ) ⇝ 𝐴)       (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ (𝐴 + (seq𝑀( + , 𝐹, ℂ)‘𝑁)))
 
21-Aug-2021iseqdistr 9103 The distributive property for series. (Contributed by Jim Kingdon, 21-Aug-2021.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝐶𝑇(𝑥 + 𝑦)) = ((𝐶𝑇𝑥) + (𝐶𝑇𝑦)))    &   (𝜑𝑁 ∈ (ℤ𝑀))    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐺𝑥) ∈ 𝑆)    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) = (𝐶𝑇(𝐺𝑥)))    &   (𝜑𝑆𝑉)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝑇𝑦) ∈ 𝑆)    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)    &   (𝜑𝐶𝑆)       (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (𝐶𝑇(seq𝑀( + , 𝐺, 𝑆)‘𝑁)))
 
21-Aug-2021iseqhomo 9102 Apply a homomorphism to a sequence. (Contributed by Jim Kingdon, 21-Aug-2021.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)    &   (𝜑𝑆𝑉)    &   (𝜑𝑁 ∈ (ℤ𝑀))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻𝑥)𝑄(𝐻𝑦)))    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐻‘(𝐹𝑥)) = (𝐺𝑥))    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐺𝑥) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆)       (𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑁)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑁))
 
20-Aug-2021clim2iser 9710 The limit of an infinite series with an initial segment removed. (Contributed by Jim Kingdon, 20-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑁𝑍)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)    &   (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)       (𝜑 → seq(𝑁 + 1)( + , 𝐹, ℂ) ⇝ (𝐴 − (seq𝑀( + , 𝐹, ℂ)‘𝑁)))
 
20-Aug-2021iseqex 9067 Existence of the sequence builder operation. (Contributed by Jim Kingdon, 20-Aug-2021.)
seq𝑀( + , 𝐹, 𝑆) ∈ V
 
20-Aug-2021frecex 5944 Finite recursion produces a set. (Contributed by Jim Kingdon, 20-Aug-2021.)
frec(𝐹, 𝐴) ∈ V
 
20-Aug-2021tfrfun 5918 Transfinite recursion produces a function. (Contributed by Jim Kingdon, 20-Aug-2021.)
Fun recs(𝐹)
 
19-Aug-2021iserclim0 9679 The zero series converges to zero. (Contributed by Jim Kingdon, 19-Aug-2021.)
(𝑀 ∈ ℤ → seq𝑀( + , ((ℤ𝑀) × {0}), ℂ) ⇝ 0)
 
19-Aug-2021shftval4g 9292 Value of a sequence shifted by -𝐴. (Contributed by Jim Kingdon, 19-Aug-2021.)
((𝐹𝑉𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵)))
 
19-Aug-2021iser0f 9105 A zero-valued infinite series is equal to the constant zero function. (Contributed by Jim Kingdon, 19-Aug-2021.)
𝑍 = (ℤ𝑀)       (𝑀 ∈ ℤ → seq𝑀( + , (𝑍 × {0}), ℂ) = (𝑍 × {0}))
 
19-Aug-2021iser0 9104 The value of the partial sums in a zero-valued infinite series. (Contributed by Jim Kingdon, 19-Aug-2021.)
𝑍 = (ℤ𝑀)       (𝑁𝑍 → (seq𝑀( + , (𝑍 × {0}), ℂ)‘𝑁) = 0)
 
19-Aug-2021ovexg 5502 Evaluating a set operation at two sets gives a set. (Contributed by Jim Kingdon, 19-Aug-2021.)
((𝐴𝑉𝐹𝑊𝐵𝑋) → (𝐴𝐹𝐵) ∈ V)
 
18-Aug-2021iseqid3s 9100 A sequence that consists of zeroes up to 𝑁 sums to zero at 𝑁. In this case by "zero" we mean whatever the identity 𝑍 is for the operation +). (Contributed by Jim Kingdon, 18-Aug-2021.)
(𝜑 → (𝑍 + 𝑍) = 𝑍)    &   (𝜑𝑁 ∈ (ℤ𝑀))    &   ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) = 𝑍)    &   (𝜑𝑍𝑆)    &   (𝜑𝑆𝑉)    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)       (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = 𝑍)
 
18-Aug-2021iseqid3 9099 A sequence that consists entirely of zeroes (or whatever the identity 𝑍 is for operation +) sums to zero. (Contributed by Jim Kingdon, 18-Aug-2021.)
(𝜑 → (𝑍 + 𝑍) = 𝑍)    &   (𝜑𝑁 ∈ (ℤ𝑀))    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) = 𝑍)    &   (𝜑𝑍𝑉)       (𝜑 → (seq𝑀( + , 𝐹, {𝑍})‘𝑁) = 𝑍)
 
18-Aug-2021iseqss 9080 Specifying a larger universe for seq. As long as 𝐹 and + are closed over 𝑆, then any set which contains 𝑆 can be used as the last argument to seq. This theorem does not allow 𝑇 to be a proper class, however. It also currently requires that + be closed over 𝑇 (as well as 𝑆). (Contributed by Jim Kingdon, 18-Aug-2021.)
(𝜑𝑀 ∈ ℤ)    &   (𝜑𝑇𝑉)    &   (𝜑𝑆𝑇)    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥𝑇𝑦𝑇)) → (𝑥 + 𝑦) ∈ 𝑇)       (𝜑 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐹, 𝑇))
 
17-Aug-2021iseqcaopr 9096 The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Jim Kingdon, 17-Aug-2021.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   (𝜑𝑁 ∈ (ℤ𝑀))    &   ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ 𝑆)    &   ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) ∈ 𝑆)    &   ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐻𝑘) = ((𝐹𝑘) + (𝐺𝑘)))    &   (𝜑𝑆𝑉)       (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑁) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁) + (seq𝑀( + , 𝐺, 𝑆)‘𝑁)))
 
16-Aug-2021iseqcaopr3 9094 Lemma for iseqcaopr2 . (Contributed by Jim Kingdon, 16-Aug-2021.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆)    &   (𝜑𝑁 ∈ (ℤ𝑀))    &   ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ 𝑆)    &   ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) ∈ 𝑆)    &   ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐻𝑘) = ((𝐹𝑘)𝑄(𝐺𝑘)))    &   ((𝜑𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + (𝐺‘(𝑛 + 1)))))    &   (𝜑𝑆𝑉)       (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑁) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑁)))
 
16-Aug-2021iseq1p 9093 Removing the first term from a sequence. (Contributed by Jim Kingdon, 16-Aug-2021.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))    &   (𝜑𝑆𝑉)    &   (𝜑𝑀 ∈ ℤ)    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)       (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = ((𝐹𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁)))
 
16-Aug-2021iseqsplit 9092 Split a sequence into two sequences. (Contributed by Jim Kingdon, 16-Aug-2021.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))    &   (𝜑𝑆𝑉)    &   (𝜑𝑀 ∈ (ℤ𝐾))    &   ((𝜑𝑥 ∈ (ℤ𝐾)) → (𝐹𝑥) ∈ 𝑆)       (𝜑 → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁)))
 
15-Aug-2021shftfibg 9275 Value of a fiber of the relation 𝐹. (Contributed by Jim Kingdon, 15-Aug-2021.)
((𝐹𝑉𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵𝐴)}))
 
15-Aug-2021ovshftex 9274 Existence of the result of applying shift. (Contributed by Jim Kingdon, 15-Aug-2021.)
((𝐹𝑉𝐴 ∈ ℂ) → (𝐹 shift 𝐴) ∈ V)
 
15-Aug-2021isermono 9091 The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by Jim Kingdon, 15-Aug-2021.)
(𝜑𝐾 ∈ (ℤ𝑀))    &   (𝜑𝑁 ∈ (ℤ𝐾))    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ ℝ)    &   ((𝜑𝑥 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝐹𝑥))       (𝜑 → (seq𝑀( + , 𝐹, ℝ)‘𝐾) ≤ (seq𝑀( + , 𝐹, ℝ)‘𝑁))
 
15-Aug-2021iserf 9087 An infinite series of complex terms is a function from to . (Contributed by Jim Kingdon, 15-Aug-2021.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℤ)    &   ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)       (𝜑 → seq𝑀( + , 𝐹, ℂ):𝑍⟶ℂ)
 
15-Aug-2021iseqshft2 9086 Shifting the index set of a sequence. (Contributed by Jim Kingdon, 15-Aug-2021.)
(𝜑𝑁 ∈ (ℤ𝑀))    &   (𝜑𝐾 ∈ ℤ)    &   ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝐹𝑘) = (𝐺‘(𝑘 + 𝐾)))    &   (𝜑𝑆𝑉)    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)    &   ((𝜑𝑥 ∈ (ℤ‘(𝑀 + 𝐾))) → (𝐺𝑥) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)       (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑁 + 𝐾)))
 
15-Aug-2021iseqfeq 9085 Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.)
(𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆𝑉)    &   ((𝜑𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ 𝑆)    &   ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) = (𝐺𝑘))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)       (𝜑 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐺, 𝑆))
 
13-Aug-2021absdivapd 9645 Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐵 # 0)       (𝜑 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))
 
13-Aug-2021absrpclapd 9638 The absolute value of a complex number apart from zero is a positive real. (Contributed by Jim Kingdon, 13-Aug-2021.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 # 0)       (𝜑 → (abs‘𝐴) ∈ ℝ+)
 
13-Aug-2021absdivapzi 9604 Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (𝐵 # 0 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))
 
13-Aug-2021absgt0ap 9549 The absolute value of a number apart from zero is positive. (Contributed by Jim Kingdon, 13-Aug-2021.)
(𝐴 ∈ ℂ → (𝐴 # 0 ↔ 0 < (abs‘𝐴)))
 
13-Aug-2021recvalap 9547 Reciprocal expressed with a real denominator. (Contributed by Jim Kingdon, 13-Aug-2021.)
((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) = ((∗‘𝐴) / ((abs‘𝐴)↑2)))
 
13-Aug-2021sqap0 9174 A number is apart from zero iff its square is apart from zero. (Contributed by Jim Kingdon, 13-Aug-2021.)
(𝐴 ∈ ℂ → ((𝐴↑2) # 0 ↔ 𝐴 # 0))
 
13-Aug-2021leltapd 7580 '<_' implies 'less than' is 'apart'. (Contributed by Jim Kingdon, 13-Aug-2021.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴𝐵)       (𝜑 → (𝐴 < 𝐵𝐵 # 𝐴))
 
13-Aug-2021leltap 7567 '<_' implies 'less than' is 'apart'. (Contributed by Jim Kingdon, 13-Aug-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (𝐴 < 𝐵𝐵 # 𝐴))
 
12-Aug-2021abssubap0 9540 If the absolute value of a complex number is less than a real, its difference from the real is apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ (abs‘𝐴) < 𝐵) → (𝐵𝐴) # 0)
 
12-Aug-2021ltabs 9537 A number which is less than its absolute value is negative. (Contributed by Jim Kingdon, 12-Aug-2021.)
((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → 𝐴 < 0)
 
12-Aug-2021absext 9515 Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) # (abs‘𝐵) → 𝐴 # 𝐵))
 
12-Aug-2021sq11ap 9268 Analogue to sq11 9180 but for apartness. (Contributed by Jim Kingdon, 12-Aug-2021.)
(((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) # (𝐵↑2) ↔ 𝐴 # 𝐵))
 
12-Aug-2021subap0d 7583 Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐴 # 𝐵)       (𝜑 → (𝐴𝐵) # 0)
 
12-Aug-2021ltapd 7579 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)       (𝜑𝐴 # 𝐵)
 
12-Aug-2021gtapd 7578 'Greater than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)       (𝜑𝐵 # 𝐴)
 
12-Aug-2021ltapi 7577 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       (𝐴 < 𝐵𝐵 # 𝐴)
 
12-Aug-2021ltapii 7576 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ    &   𝐴 < 𝐵       𝐴 # 𝐵
 
12-Aug-2021gtapii 7575 'Greater than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ    &   𝐴 < 𝐵       𝐵 # 𝐴
 
12-Aug-2021ltap 7574 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 # 𝐴)
 
11-Aug-2021absexpzap 9530 Absolute value of integer exponentiation. (Contributed by Jim Kingdon, 11-Aug-2021.)
((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴𝑁)) = ((abs‘𝐴)↑𝑁))
 
11-Aug-2021absdivap 9522 Absolute value distributes over division. (Contributed by Jim Kingdon, 11-Aug-2021.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))
 
11-Aug-2021abs00ap 9514 The absolute value of a number is apart from zero iff the number is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
(𝐴 ∈ ℂ → ((abs‘𝐴) # 0 ↔ 𝐴 # 0))
 
11-Aug-2021absrpclap 9513 The absolute value of a number apart from zero is a positive real. (Contributed by Jim Kingdon, 11-Aug-2021.)
((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (abs‘𝐴) ∈ ℝ+)
 
11-Aug-2021sqrt11ap 9490 Analogue to sqrt11 9491 but for apartness. (Contributed by Jim Kingdon, 11-Aug-2021.)
(((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) # (√‘𝐵) ↔ 𝐴 # 𝐵))
 
11-Aug-2021cjap0d 9402 A number which is apart from zero has a complex conjugate which is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 # 0)       (𝜑 → (∗‘𝐴) # 0)
 
11-Aug-2021ap0gt0d 7582 A nonzero nonnegative number is positive. (Contributed by Jim Kingdon, 11-Aug-2021.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐴 # 0)       (𝜑 → 0 < 𝐴)
 
11-Aug-2021ap0gt0 7581 A nonnegative number is apart from zero if and only if it is positive. (Contributed by Jim Kingdon, 11-Aug-2021.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 # 0 ↔ 0 < 𝐴))
 
10-Aug-2021rersqrtthlem 9482 Lemma for resqrtth 9483. (Contributed by Jim Kingdon, 10-Aug-2021.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (√‘𝐴)))
 
10-Aug-2021rersqreu 9480 Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃!𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥))
 
10-Aug-2021rsqrmo 9479 Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃*𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥))
 
9-Aug-2021resqrexlemoverl 9473 Lemma for resqrex 9478. Every term in the sequence is an overestimate compared with the limit 𝐿. Although this theorem is stated in terms of a particular sequence the proof could be adapted for any decreasing convergent sequence. (Contributed by Jim Kingdon, 9-Aug-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐿 ∈ ℝ)    &   (𝜑 → ∀𝑒 ∈ ℝ+𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ𝑗)((𝐹𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹𝑖) + 𝑒)))    &   (𝜑𝐾 ∈ ℕ)       (𝜑𝐿 ≤ (𝐹𝐾))
 
8-Aug-2021resqrexlemga 9475 Lemma for resqrex 9478. The sequence formed by squaring each term of 𝐹 converges to 𝐴. (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐿 ∈ ℝ)    &   (𝜑 → ∀𝑒 ∈ ℝ+𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ𝑗)((𝐹𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹𝑖) + 𝑒)))    &   𝐺 = (𝑥 ∈ ℕ ↦ ((𝐹𝑥)↑2))       (𝜑 → ∀𝑒 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)((𝐺𝑘) < (𝐴 + 𝑒) ∧ 𝐴 < ((𝐺𝑘) + 𝑒)))

  Copyright terms: Public domain W3C HTML validation [external]