Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Complexity theory
The Ackermann function
itcovalpclem1
Next ⟩
itcovalpclem2
Metamath Proof Explorer
Ascii
Unicode
Theorem
itcovalpclem1
Description:
Lemma 1 for
itcovalpc
: induction basis.
(Contributed by
AV
, 4-May-2024)
Ref
Expression
Hypothesis
itcovalpc.f
⊢
F
=
n
∈
ℕ
0
⟼
n
+
C
Assertion
itcovalpclem1
⊢
C
∈
ℕ
0
→
IterComp
⁡
F
⁡
0
=
n
∈
ℕ
0
⟼
n
+
C
⋅
0
Proof
Step
Hyp
Ref
Expression
1
itcovalpc.f
⊢
F
=
n
∈
ℕ
0
⟼
n
+
C
2
nn0ex
⊢
ℕ
0
∈
V
3
ovexd
⊢
n
∈
ℕ
0
→
n
+
C
∈
V
4
3
rgen
⊢
∀
n
∈
ℕ
0
n
+
C
∈
V
5
1
itcoval0mpt
⊢
ℕ
0
∈
V
∧
∀
n
∈
ℕ
0
n
+
C
∈
V
→
IterComp
⁡
F
⁡
0
=
n
∈
ℕ
0
⟼
n
6
2
4
5
mp2an
⊢
IterComp
⁡
F
⁡
0
=
n
∈
ℕ
0
⟼
n
7
nn0cn
⊢
C
∈
ℕ
0
→
C
∈
ℂ
8
7
mul01d
⊢
C
∈
ℕ
0
→
C
⋅
0
=
0
9
8
adantr
⊢
C
∈
ℕ
0
∧
n
∈
ℕ
0
→
C
⋅
0
=
0
10
9
oveq2d
⊢
C
∈
ℕ
0
∧
n
∈
ℕ
0
→
n
+
C
⋅
0
=
n
+
0
11
nn0cn
⊢
n
∈
ℕ
0
→
n
∈
ℂ
12
11
addridd
⊢
n
∈
ℕ
0
→
n
+
0
=
n
13
12
adantl
⊢
C
∈
ℕ
0
∧
n
∈
ℕ
0
→
n
+
0
=
n
14
10
13
eqtr2d
⊢
C
∈
ℕ
0
∧
n
∈
ℕ
0
→
n
=
n
+
C
⋅
0
15
14
mpteq2dva
⊢
C
∈
ℕ
0
→
n
∈
ℕ
0
⟼
n
=
n
∈
ℕ
0
⟼
n
+
C
⋅
0
16
6
15
eqtrid
⊢
C
∈
ℕ
0
→
IterComp
⁡
F
⁡
0
=
n
∈
ℕ
0
⟼
n
+
C
⋅
0