Expression of type Implies

from the theory of proveit.numbers.summation

import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import i, m, n, x
from proveit.logic import And, Equals, Forall, Implies, TRUE
from proveit.numbers import Add, Exp, Interval, Natural, Sum, frac, one, subtract, two, zero

# build up the expression from sub-expressions
sub_expr1 = [i]
sub_expr2 = Exp(x, i)
sub_expr3 = Add(m, one)
sub_expr4 = subtract(one, x)
expr = Implies(And(TRUE, Forall(instance_param_or_params = [m], instance_expr = Equals(Sum(index_or_indices = sub_expr1, summand = sub_expr2, domain = Interval(zero, sub_expr3)), frac(subtract(one, Exp(x, Add(m, two))), sub_expr4)), domain = Natural, condition = Equals(Sum(index_or_indices = sub_expr1, summand = sub_expr2, domain = Interval(zero, m)), frac(subtract(one, Exp(x, sub_expr3)), sub_expr4)))), Forall(instance_param_or_params = [n], instance_expr = Equals(Sum(index_or_indices = sub_expr1, summand = sub_expr2, domain = Interval(zero, n)), frac(subtract(one, Exp(x, Add(n, one))), sub_expr4)), domain = Natural))

expr:

# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")

Passed sanity check: expr matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left(\top \land \left[\forall_{m \in \mathbb{N}~|~\left(\sum_{i = 0}^{m} x^{i}\right) = \frac{1 - x^{m + 1}}{1 - x}}~\left(\left(\sum_{i = 0}^{m + 1} x^{i}\right) = \frac{1 - x^{m + 2}}{1 - x}\right)\right]\right) \Rightarrow \left[\forall_{n \in \mathbb{N}}~\left(\left(\sum_{i = 0}^{n} x^{i}\right) = \frac{1 - x^{n + 1}}{1 - x}\right)\right]

stored_expr.style_options()

name	description	default	current value	related methods
operation	'infix' or 'function' style formatting	infix	infix
wrap_positions	position(s) at which wrapping is to occur; '2 n - 1' is after the nth operand, '2 n' is after the nth operation.	()	()	('with_wrapping_at', 'with_wrap_before_operator', 'with_wrap_after_operator', 'without_wrapping', 'wrap_positions')
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	center	center	('with_justification',)
direction	Direction of the relation (normal or reversed)	normal	normal	('with_direction_reversed', 'is_reversed')

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	Operation	operator: 1 operands: 2
1	Literal
2	ExprTuple	3, 4
3	Operation	operator: 26 operands: 5
4	Operation	operator: 10 operand: 9
5	ExprTuple	7, 8
6	ExprTuple	9
7	Literal
8	Operation	operator: 10 operand: 14
9	Lambda	parameter: 93 body: 13
10	Literal
11	ExprTuple	14
12	ExprTuple	93
13	Conditional	value: 15 condition: 16
14	Lambda	parameter: 105 body: 18
15	Operation	operator: 39 operands: 19
16	Operation	operator: 83 operands: 20
17	ExprTuple	105
18	Conditional	value: 21 condition: 22
19	ExprTuple	23, 24
20	ExprTuple	93, 45
21	Operation	operator: 39 operands: 25
22	Operation	operator: 26 operands: 27
23	Operation	operator: 52 operand: 34
24	Operation	operator: 54 operands: 29
25	ExprTuple	30, 31
26	Literal
27	ExprTuple	32, 33
28	ExprTuple	34
29	ExprTuple	35, 62
30	Operation	operator: 52 operand: 43
31	Operation	operator: 54 operands: 37
32	Operation	operator: 83 operands: 38
33	Operation	operator: 39 operands: 40
34	Lambda	parameter: 90 body: 41
35	Operation	operator: 103 operands: 42
36	ExprTuple	43
37	ExprTuple	44, 62
38	ExprTuple	105, 45
39	Literal
40	ExprTuple	46, 47
41	Conditional	value: 75 condition: 48
42	ExprTuple	106, 49
43	Lambda	parameter: 90 body: 50
44	Operation	operator: 103 operands: 51
45	Literal
46	Operation	operator: 52 operand: 60
47	Operation	operator: 54 operands: 55
48	Operation	operator: 83 operands: 56
49	Operation	operator: 86 operand: 64
50	Conditional	value: 75 condition: 58
51	ExprTuple	106, 59
52	Literal
53	ExprTuple	60
54	Literal
55	ExprTuple	61, 62
56	ExprTuple	90, 63
57	ExprTuple	64
58	Operation	operator: 83 operands: 65
59	Operation	operator: 86 operand: 74
60	Lambda	parameter: 90 body: 68
61	Operation	operator: 103 operands: 69
62	Operation	operator: 103 operands: 70
63	Operation	operator: 95 operands: 71
64	Operation	operator: 97 operands: 72
65	ExprTuple	90, 73
66	ExprTuple	74
67	ExprTuple	90
68	Conditional	value: 75 condition: 76
69	ExprTuple	106, 77
70	ExprTuple	106, 78
71	ExprTuple	100, 93
72	ExprTuple	101, 79
73	Operation	operator: 95 operands: 80
74	Operation	operator: 97 operands: 81
75	Operation	operator: 97 operands: 82
76	Operation	operator: 83 operands: 84
77	Operation	operator: 86 operand: 92
78	Operation	operator: 86 operand: 101
79	Operation	operator: 103 operands: 88
80	ExprTuple	100, 102
81	ExprTuple	101, 89
82	ExprTuple	101, 90
83	Literal
84	ExprTuple	90, 91
85	ExprTuple	92
86	Literal
87	ExprTuple	101
88	ExprTuple	93, 106
89	Operation	operator: 103 operands: 94
90	Variable
91	Operation	operator: 95 operands: 96
92	Operation	operator: 97 operands: 98
93	Variable
94	ExprTuple	105, 99
95	Literal
96	ExprTuple	100, 105
97	Literal
98	ExprTuple	101, 102
99	Literal
100	Literal
101	Variable
102	Operation	operator: 103 operands: 104
103	Literal
104	ExprTuple	105, 106
105	Variable
106	Literal