Recent Additions to the Intuitionistic Logic
Explorer
| Date | Label | Description |
|---|
| Theorem |
|---|
| |
| 23-Sep-2021 | wepo 4092 |
A well-ordering is a partial ordering. (Contributed by Jim Kingdon,
23-Sep-2021.)
|
| ⊢ ((𝑅 We 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝑅 Po 𝐴) |
| |
| 23-Sep-2021 | df-wetr 4068 |
Define the well-ordering predicate. It is unusual to define
"well-ordering" in the absence of excluded middle, but we mean
an
ordering which is like the ordering which we have for ordinals (for
example, it does not entail trichotomy because ordinals don't have that
as seen at ordtriexmid 4243). Given excluded middle, well-ordering is
usually defined to require trichotomy (and the defintion of Fr is
typically also different). (Contributed by Mario Carneiro and Jim
Kingdon, 23-Sep-2021.)
|
| ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
| |
| 22-Sep-2021 | frforeq3 4081 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
| ⊢ (𝑆 = 𝑇 → ( FrFor 𝑅𝐴𝑆 ↔ FrFor 𝑅𝐴𝑇)) |
| |
| 22-Sep-2021 | frforeq2 4079 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
| ⊢ (𝐴 = 𝐵 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑅𝐵𝑇)) |
| |
| 22-Sep-2021 | frforeq1 4077 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
| ⊢ (𝑅 = 𝑆 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑆𝐴𝑇)) |
| |
| 22-Sep-2021 | df-frfor 4065 |
Define the well-founded relation predicate where 𝐴 might be a proper
class. By passing in 𝑆 we allow it potentially to be a
proper class
rather than a set. (Contributed by Jim Kingdon and Mario Carneiro,
22-Sep-2021.)
|
| ⊢ ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆)) |
| |
| 21-Sep-2021 | frirrg 4084 |
A well-founded relation is irreflexive. This is the case where 𝐴
exists. (Contributed by Jim Kingdon, 21-Sep-2021.)
|
| ⊢ ((𝑅 Fr 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
| |
| 21-Sep-2021 | df-frind 4066 |
Define the well-founded relation predicate. In the presence of excluded
middle, there are a variety of equivalent ways to define this. In our
case, this definition, in terms of an inductive principle, works better
than one along the lines of "there is an element which is minimal
when A
is ordered by R". Because 𝑠 is constrained to be a set (not a
proper class) here, sometimes it may be necessary to use FrFor
directly rather than via Fr. (Contributed by
Jim Kingdon and Mario
Carneiro, 21-Sep-2021.)
|
| ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠) |
| |
| 17-Sep-2021 | ontr2exmid 4246 |
An ordinal transitivity law which implies excluded middle. (Contributed
by Jim Kingdon, 17-Sep-2021.)
|
| ⊢ ∀𝑥 ∈ On ∀𝑦∀𝑧 ∈ On ((𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) |
| |
| 16-Sep-2021 | nnsseleq 6066 |
For natural numbers, inclusion is equivalent to membership or equality.
(Contributed by Jim Kingdon, 16-Sep-2021.)
|
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) |
| |
| 15-Sep-2021 | fientri3 6339 |
Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon,
15-Sep-2021.)
|
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
| |
| 15-Sep-2021 | nntri2or2 6063 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15-Sep-2021.)
|
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) |
| |
| 14-Sep-2021 | findcard2sd 6335 |
Deduction form of finite set induction . (Contributed by Jim Kingdon,
14-Sep-2021.)
|
| ⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒)
& ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝜃 → 𝜏)) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → 𝜂) |
| |
| 13-Sep-2021 | php5fin 6326 |
A finite set is not equinumerous to a set which adds one element.
(Contributed by Jim Kingdon, 13-Sep-2021.)
|
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ (V ∖ 𝐴)) → ¬ 𝐴 ≈ (𝐴 ∪ {𝐵})) |
| |
| 13-Sep-2021 | fiunsnnn 6325 |
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-2021 | fisbth 6327 |
Schroeder-Bernstein Theorem for finite sets. (Contributed by Jim
Kingdon, 12-Sep-2021.)
|
| ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≈ 𝐵) |
| |
| 11-Sep-2021 | diffisn 6336 |
Subtracting a singleton from a finite set produces a finite set.
(Contributed by Jim Kingdon, 11-Sep-2021.)
|
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → (𝐴 ∖ {𝐵}) ∈ Fin) |
| |
| 10-Sep-2021 | fin0 6329 |
A nonempty finite set has at least one element. (Contributed by Jim
Kingdon, 10-Sep-2021.)
|
| ⊢ (𝐴 ∈ Fin → (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)) |
| |
| 9-Sep-2021 | fidifsnid 6319 |
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-2021 | fidifsnen 6318 |
All decrements of a finite set are equinumerous. (Contributed by Jim
Kingdon, 9-Sep-2021.)
|
| ⊢ ((𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵})) |
| |
| 8-Sep-2021 | diffifi 6337 |
Subtracting one finite set from another produces a finite set.
(Contributed by Jim Kingdon, 8-Sep-2021.)
|
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (𝐴 ∖ 𝐵) ∈ Fin) |
| |
| 8-Sep-2021 | diffitest 6330 |
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-2021 | phpelm 6315 |
Pigeonhole Principle. A natural number is not equinumerous to an
element of itself. (Contributed by Jim Kingdon, 6-Sep-2021.)
|
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ¬ 𝐴 ≈ 𝐵) |
| |
| 5-Sep-2021 | fidceq 6317 |
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-2021 | phplem4on 6316 |
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-2021 | 0elsucexmid 4283 |
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-2021 | php5dom 6312 |
A natural number does not dominate its successor. (Contributed by Jim
Kingdon, 1-Sep-2021.)
|
| ⊢ (𝐴 ∈ ω → ¬ suc 𝐴 ≼ 𝐴) |
| |
| 1-Sep-2021 | phplem4dom 6311 |
Dominance of successors implies dominance of the original natural
numbers. (Contributed by Jim Kingdon, 1-Sep-2021.)
|
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≼ suc 𝐵 → 𝐴 ≼ 𝐵)) |
| |
| 1-Sep-2021 | snnen2oprc 6310 |
A singleton {𝐴} is never equinumerous with the
ordinal number 2. If
𝐴 is a set, see snnen2og 6309. (Contributed by Jim Kingdon,
1-Sep-2021.)
|
| ⊢ (¬ 𝐴 ∈ V → ¬ {𝐴} ≈
2𝑜) |
| |
| 1-Sep-2021 | snnen2og 6309 |
A singleton {𝐴} is never equinumerous with the
ordinal number 2. If
𝐴 is a proper class, see snnen2oprc 6310. (Contributed by Jim Kingdon,
1-Sep-2021.)
|
| ⊢ (𝐴 ∈ 𝑉 → ¬ {𝐴} ≈
2𝑜) |
| |
| 1-Sep-2021 | phplem3g 6306 |
A natural number is equinumerous to its successor minus any element of
the successor. Version of phplem3 6304 with unnecessary hypotheses
removed. (Contributed by Jim Kingdon, 1-Sep-2021.)
|
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) |
| |
| 31-Aug-2021 | nndifsnid 6067 |
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-2021 | carden2bex 6350 |
If two numerable sets are equinumerous, then they have equal
cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.)
|
| ⊢ ((𝐴 ≈ 𝐵 ∧ ∃𝑥 ∈ On 𝑥 ≈ 𝐴) → (card‘𝐴) = (card‘𝐵)) |
| |
| 30-Aug-2021 | cardval3ex 6346 |
The value of (card‘𝐴). (Contributed by Jim Kingdon,
30-Aug-2021.)
|
| ⊢ (∃𝑥 ∈ On 𝑥 ≈ 𝐴 → (card‘𝐴) = ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) |
| |
| 30-Aug-2021 | cardcl 6342 |
The cardinality of a well-orderable set is an ordinal. (Contributed by
Jim Kingdon, 30-Aug-2021.)
|
| ⊢ (∃𝑦 ∈ On 𝑦 ≈ 𝐴 → (card‘𝐴) ∈ On) |
| |
| 30-Aug-2021 | onintrab2im 4240 |
An existence condition which implies an intersection is an ordinal
number. (Contributed by Jim Kingdon, 30-Aug-2021.)
|
| ⊢ (∃𝑥 ∈ On 𝜑 → ∩ {𝑥 ∈ On ∣ 𝜑} ∈ On) |
| |
| 30-Aug-2021 | onintonm 4239 |
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-2021 | onintexmid 4291 |
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-2021 | ordtri2or2exmid 4290 |
Ordinal trichotomy implies excluded middle. (Contributed by Jim
Kingdon, 29-Aug-2021.)
|
| ⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) |
| |
| 29-Aug-2021 | ordtri2or2exmidlem 4247 |
A set which is 2𝑜 if 𝜑 or ∅ if ¬ 𝜑 is an ordinal.
(Contributed by Jim Kingdon, 29-Aug-2021.)
|
| ⊢ {𝑥 ∈ {∅, {∅}} ∣ 𝜑} ∈ On |
| |
| 29-Aug-2021 | 2ordpr 4245 |
Version of 2on 5996 with the definition of 2𝑜 expanded and expressed in
terms of Ord. (Contributed by Jim Kingdon,
29-Aug-2021.)
|
| ⊢ Ord {∅, {∅}} |
| |
| 25-Aug-2021 | nnap0d 7935 |
A positive integer is apart from zero. (Contributed by Jim Kingdon,
25-Aug-2021.)
|
| ⊢ (𝜑 → 𝐴 ∈ ℕ)
⇒ ⊢ (𝜑 → 𝐴 # 0) |
| |
| 24-Aug-2021 | climcaucn 9747 |
A converging sequence of complex numbers is a Cauchy sequence. This is
like climcau 9743 but adds the part that (𝐹‘𝑘) is complex.
(Contributed by Jim Kingdon, 24-Aug-2021.)
|
| ⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
| |
| 24-Aug-2021 | climcvg1nlem 9745 |
Lemma for climcvg1n 9746. 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-2021 | climcvg1n 9746 |
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-2021 | climrecvg1n 9744 |
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-2021 | climserile 9742 |
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-2021 | iserige0 9740 |
The limit of an infinite series of nonnegative reals is nonnegative.
(Contributed by Jim Kingdon, 22-Aug-2021.)
|
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) |
| |
| 22-Aug-2021 | iserile 9739 |
Comparison of the limits of two infinite series. (Contributed by Jim
Kingdon, 22-Aug-2021.)
|
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴)
& ⊢ (𝜑 → seq𝑀( + , 𝐺, ℂ) ⇝ 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| |
| 22-Aug-2021 | serile 9131 |
Comparison of partial sums of two infinite series of reals.
(Contributed by Jim Kingdon, 22-Aug-2021.)
|
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ≤ (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹, ℂ)‘𝑁) ≤ (seq𝑀( + , 𝐺, ℂ)‘𝑁)) |
| |
| 22-Aug-2021 | serige0 9130 |
A finite sum of nonnegative terms is nonnegative. (Contributed by Jim
Kingdon, 22-Aug-2021.)
|
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 0 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 0 ≤ (seq𝑀( + , 𝐹, ℂ)‘𝑁)) |
| |
| 21-Aug-2021 | clim2iser2 9735 |
The limit of an infinite series with an initial segment added.
(Contributed by Jim Kingdon, 21-Aug-2021.)
|
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq(𝑁 + 1)( + , 𝐹, ℂ) ⇝ 𝐴) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ (𝐴 + (seq𝑀( + , 𝐹, ℂ)‘𝑁))) |
| |
| 21-Aug-2021 | iseqdistr 9127 |
The distributive property for series. (Contributed by Jim Kingdon,
21-Aug-2021.)
|
| ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐶𝑇(𝑥 + 𝑦)) = ((𝐶𝑇𝑥) + (𝐶𝑇𝑦))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) = (𝐶𝑇(𝐺‘𝑥))) & ⊢ (𝜑 → 𝑆 ∈ 𝑉)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑇𝑦) ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (𝐶𝑇(seq𝑀( + , 𝐺, 𝑆)‘𝑁))) |
| |
| 21-Aug-2021 | iseqhomo 9126 |
Apply a homomorphism to a sequence. (Contributed by Jim Kingdon,
21-Aug-2021.)
|
| ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
& ⊢ (𝜑 → 𝑆 ∈ 𝑉)
& ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥))
& ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹, 𝑆)‘𝑁)) = (seq𝑀(𝑄, 𝐺, 𝑆)‘𝑁)) |
| |
| 20-Aug-2021 | clim2iser 9734 |
The limit of an infinite series with an initial segment removed.
(Contributed by Jim Kingdon, 20-Aug-2021.)
|
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹, ℂ) ⇝ 𝐴) ⇒ ⊢ (𝜑 → seq(𝑁 + 1)( + , 𝐹, ℂ) ⇝ (𝐴 − (seq𝑀( + , 𝐹, ℂ)‘𝑁))) |
| |
| 20-Aug-2021 | iseqex 9091 |
Existence of the sequence builder operation. (Contributed by Jim
Kingdon, 20-Aug-2021.)
|
| ⊢ seq𝑀( + , 𝐹, 𝑆) ∈ V |
| |
| 20-Aug-2021 | frecex 5968 |
Finite recursion produces a set. (Contributed by Jim Kingdon,
20-Aug-2021.)
|
| ⊢ frec(𝐹, 𝐴) ∈ V |
| |
| 20-Aug-2021 | tfrfun 5942 |
Transfinite recursion produces a function. (Contributed by Jim Kingdon,
20-Aug-2021.)
|
| ⊢ Fun recs(𝐹) |
| |
| 19-Aug-2021 | iserclim0 9703 |
The zero series converges to zero. (Contributed by Jim Kingdon,
19-Aug-2021.)
|
| ⊢ (𝑀 ∈ ℤ → seq𝑀( + , ((ℤ≥‘𝑀) × {0}), ℂ)
⇝ 0) |
| |
| 19-Aug-2021 | shftval4g 9316 |
Value of a sequence shifted by -𝐴. (Contributed by Jim Kingdon,
19-Aug-2021.)
|
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift -𝐴)‘𝐵) = (𝐹‘(𝐴 + 𝐵))) |
| |
| 19-Aug-2021 | iser0f 9129 |
A zero-valued infinite series is equal to the constant zero function.
(Contributed by Jim Kingdon, 19-Aug-2021.)
|
| ⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( + , (𝑍 × {0}), ℂ) = (𝑍 × {0})) |
| |
| 19-Aug-2021 | iser0 9128 |
The value of the partial sums in a zero-valued infinite series.
(Contributed by Jim Kingdon, 19-Aug-2021.)
|
| ⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑁 ∈ 𝑍 → (seq𝑀( + , (𝑍 × {0}), ℂ)‘𝑁) = 0) |
| |
| 19-Aug-2021 | ovexg 5526 |
Evaluating a set operation at two sets gives a set. (Contributed by Jim
Kingdon, 19-Aug-2021.)
|
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐹𝐵) ∈ V) |
| |
| 18-Aug-2021 | iseqid3s 9124 |
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-2021 | iseqid3 9123 |
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-2021 | iseqss 9104 |
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-2021 | iseqcaopr 9120 |
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-2021 | iseqcaopr3 9118 |
Lemma for iseqcaopr2 . (Contributed by Jim Kingdon, 16-Aug-2021.)
|
| ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆)
& ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘))) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + (𝐺‘(𝑛 + 1))))) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑁) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑁))) |
| |
| 16-Aug-2021 | iseq1p 9117 |
Removing the first term from a sequence. (Contributed by Jim Kingdon,
16-Aug-2021.)
|
| ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) & ⊢ (𝜑 → 𝑆 ∈ 𝑉)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = ((𝐹‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁))) |
| |
| 16-Aug-2021 | iseqsplit 9116 |
Split a sequence into two sequences. (Contributed by Jim Kingdon,
16-Aug-2021.)
|
| ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) & ⊢ (𝜑 → 𝑆 ∈ 𝑉)
& ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐾)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (𝐹‘𝑥) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁))) |
| |
| 15-Aug-2021 | shftfibg 9299 |
Value of a fiber of the relation 𝐹. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴) “ {𝐵}) = (𝐹 “ {(𝐵 − 𝐴)})) |
| |
| 15-Aug-2021 | ovshftex 9298 |
Existence of the result of applying shift. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ) → (𝐹 shift 𝐴) ∈ V) |
| |
| 15-Aug-2021 | isermono 9115 |
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-2021 | iserf 9111 |
An infinite series of complex terms is a function from ℕ to
ℂ. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹, ℂ):𝑍⟶ℂ) |
| |
| 15-Aug-2021 | iseqshft2 9110 |
Shifting the index set of a sequence. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾))) & ⊢ (𝜑 → 𝑆 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 𝐾))) → (𝐺‘𝑥) ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑁 + 𝐾))) |
| |
| 15-Aug-2021 | iseqfeq 9109 |
Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.)
|
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = (𝐺‘𝑘))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐺, 𝑆)) |
| |
| 13-Aug-2021 | absdivapd 9669 |
Absolute value distributes over division. (Contributed by Jim
Kingdon, 13-Aug-2021.)
|
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 # 0) ⇒ ⊢ (𝜑 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵))) |
| |
| 13-Aug-2021 | absrpclapd 9662 |
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-2021 | absdivapzi 9628 |
Absolute value distributes over division. (Contributed by Jim Kingdon,
13-Aug-2021.)
|
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐵 # 0 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵))) |
| |
| 13-Aug-2021 | absgt0ap 9573 |
The absolute value of a number apart from zero is positive. (Contributed
by Jim Kingdon, 13-Aug-2021.)
|
| ⊢ (𝐴 ∈ ℂ → (𝐴 # 0 ↔ 0 < (abs‘𝐴))) |
| |
| 13-Aug-2021 | recvalap 9571 |
Reciprocal expressed with a real denominator. (Contributed by Jim
Kingdon, 13-Aug-2021.)
|
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) = ((∗‘𝐴) / ((abs‘𝐴)↑2))) |
| |
| 13-Aug-2021 | sqap0 9198 |
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-2021 | leltapd 7604 |
'<_' implies 'less than' is 'apart'. (Contributed by Jim Kingdon,
13-Aug-2021.)
|
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 𝐵 # 𝐴)) |
| |
| 13-Aug-2021 | leltap 7591 |
'<_' implies 'less than' is 'apart'. (Contributed by Jim Kingdon,
13-Aug-2021.)
|
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (𝐴 < 𝐵 ↔ 𝐵 # 𝐴)) |
| |
| 12-Aug-2021 | abssubap0 9564 |
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-2021 | ltabs 9561 |
A number which is less than its absolute value is negative. (Contributed
by Jim Kingdon, 12-Aug-2021.)
|
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → 𝐴 < 0) |
| |
| 12-Aug-2021 | absext 9539 |
Strong extensionality for absolute value. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) # (abs‘𝐵) → 𝐴 # 𝐵)) |
| |
| 12-Aug-2021 | sq11ap 9292 |
Analogue to sq11 9204 but for apartness. (Contributed by Jim
Kingdon,
12-Aug-2021.)
|
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) # (𝐵↑2) ↔ 𝐴 # 𝐵)) |
| |
| 12-Aug-2021 | subap0d 7607 |
Two numbers apart from each other have difference apart from zero.
(Contributed by Jim Kingdon, 12-Aug-2021.)
|
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) # 0) |
| |
| 12-Aug-2021 | ltapd 7603 |
'Less than' implies apart. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 # 𝐵) |
| |
| 12-Aug-2021 | gtapd 7602 |
'Greater than' implies apart. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 # 𝐴) |
| |
| 12-Aug-2021 | ltapi 7601 |
'Less than' implies apart. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 → 𝐵 # 𝐴) |
| |
| 12-Aug-2021 | ltapii 7600 |
'Less than' implies apart. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐴 # 𝐵 |
| |
| 12-Aug-2021 | gtapii 7599 |
'Greater than' implies apart. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐵 # 𝐴 |
| |
| 12-Aug-2021 | ltap 7598 |
'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
|
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 # 𝐴) |
| |
| 11-Aug-2021 | absexpzap 9554 |
Absolute value of integer exponentiation. (Contributed by Jim Kingdon,
11-Aug-2021.)
|
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) |
| |
| 11-Aug-2021 | absdivap 9546 |
Absolute value distributes over division. (Contributed by Jim Kingdon,
11-Aug-2021.)
|
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵))) |
| |
| 11-Aug-2021 | abs00ap 9538 |
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-2021 | absrpclap 9537 |
The absolute value of a number apart from zero is a positive real.
(Contributed by Jim Kingdon, 11-Aug-2021.)
|
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (abs‘𝐴) ∈
ℝ+) |
| |
| 11-Aug-2021 | sqrt11ap 9514 |
Analogue to sqrt11 9515 but for apartness. (Contributed by Jim
Kingdon,
11-Aug-2021.)
|
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) # (√‘𝐵) ↔ 𝐴 # 𝐵)) |
User Mathboxes