Demonstrations for the theory of proveit.numbers.number_sets.complex_numbers

import proveit
from proveit import a, b, c, x
from proveit.logic import Boolean, Equals, NotEquals, InSet
from proveit.numbers import zero, Abs, RealNonZero, Complex, ComplexNonZero
%begin demonstrations

Complex Numbers $\mathbb{C}$

UNDER CONSTRUCTION

Introduction
Simple Expressions involving Complex number $\mathbb{C}$
Common Attributes of NumberSet classes
Axioms
Further Demonstrations

1. Demo 1
2. Demo 2
3. Demo 3

Introduction

UNDER CONSTRUCTION. Something here about the importance of having and using specifically pre-defined number sets such as the Complex numbers ($\mathbb{C}$), the axiomatic definition, and perhaps the distinctiveness from other predefined NumberSet classes.

InSet(InSet(x, Complex), Boolean).prove()

 ⊢  

InSet(InSet(x, ComplexNonZero), Boolean).prove()

 ⊢  

NotEquals(x, zero).prove(assumptions=[InSet(x, ComplexNonZero)], 
                         conclude_automation=False) # should be side-effect

 ⊢  

InSet(x, Complex).prove(assumptions=[InSet(x, ComplexNonZero)])

 ⊢  

InSet(x, ComplexNonZero).prove(assumptions=[InSet(x, Complex), NotEquals(x, zero)])

,  ⊢  

InSet(x, ComplexNonZero).prove(assumptions=[InSet(x, RealNonZero)])

 ⊢  

ComplexSet.abs_both_sides_of_equals()

Applying absolute value to both sides of an equality.

# some example products of exponentials
a_equals_b = Equals(a, b)

a_equals_b:

Complex.abs_both_sides_of_equals(
    a_equals_b, assumptions=[InSet(a, Complex), InSet(b, Complex), Equals(a, b)])

, ,  ⊢  

%end demonstrations