Step
*
1
1
1
1
1
1
of Lemma
real-ball-slice_wf
1. n : ℕ+
2. t : ℝ
3. i : ℕn
4. p : ℝ^n - 1
5. λj.if j <z i then p j
if i <z j then p (j - 1)
else t
fi ∈ ℝ^n
6. ∀[x,y:ℝ^n]. (x⋅y = (x⋅y + λi@0.(x (i + i@0))⋅λi@0.(y (i + i@0))))
7. req-vec(i;λj.if j <z i then p j
if i <z j then p (j - 1)
else t
fi ;p)
8. λi@0.if i + i@0 <z i then p (i + i@0)
if i <z i + i@0 then p ((i + i@0) - 1)
else t
fi ∈ ℝ^n - i
9. req-vec(n - i;λi@0.if i + i@0 <z i then p (i + i@0)
if i <z i + i@0 then p ((i + i@0) - 1)
else t
fi ;λj.if (j =z 0) then t else p ((i + j) - 1) fi )
10. λj.if (j =z 0) then t else p ((i + j) - 1) fi ∈ ℝ^n - i
⊢ (p⋅p + λj.if (j =z 0) then t else p ((i + j) - 1) fi ⋅λj.if (j =z 0) then t else p ((i + j) - 1) fi ) = (p⋅p + t^2)
BY
{ (Decide ⌜i = (n - 1) ∈ ℤ⌝⋅ THENA Auto) }
1
1. n : ℕ+
2. t : ℝ
3. i : ℕn
4. p : ℝ^n - 1
5. λj.if j <z i then p j
if i <z j then p (j - 1)
else t
fi ∈ ℝ^n
6. ∀[x,y:ℝ^n]. (x⋅y = (x⋅y + λi@0.(x (i + i@0))⋅λi@0.(y (i + i@0))))
7. req-vec(i;λj.if j <z i then p j
if i <z j then p (j - 1)
else t
fi ;p)
8. λi@0.if i + i@0 <z i then p (i + i@0)
if i <z i + i@0 then p ((i + i@0) - 1)
else t
fi ∈ ℝ^n - i
9. req-vec(n - i;λi@0.if i + i@0 <z i then p (i + i@0)
if i <z i + i@0 then p ((i + i@0) - 1)
else t
fi ;λj.if (j =z 0) then t else p ((i + j) - 1) fi )
10. λj.if (j =z 0) then t else p ((i + j) - 1) fi ∈ ℝ^n - i
11. i = (n - 1) ∈ ℤ
⊢ (p⋅p + λj.if (j =z 0) then t else p ((i + j) - 1) fi ⋅λj.if (j =z 0) then t else p ((i + j) - 1) fi ) = (p⋅p + t^2)
2
1. n : ℕ+
2. t : ℝ
3. i : ℕn
4. p : ℝ^n - 1
5. λj.if j <z i then p j
if i <z j then p (j - 1)
else t
fi ∈ ℝ^n
6. ∀[x,y:ℝ^n]. (x⋅y = (x⋅y + λi@0.(x (i + i@0))⋅λi@0.(y (i + i@0))))
7. req-vec(i;λj.if j <z i then p j
if i <z j then p (j - 1)
else t
fi ;p)
8. λi@0.if i + i@0 <z i then p (i + i@0)
if i <z i + i@0 then p ((i + i@0) - 1)
else t
fi ∈ ℝ^n - i
9. req-vec(n - i;λi@0.if i + i@0 <z i then p (i + i@0)
if i <z i + i@0 then p ((i + i@0) - 1)
else t
fi ;λj.if (j =z 0) then t else p ((i + j) - 1) fi )
10. λj.if (j =z 0) then t else p ((i + j) - 1) fi ∈ ℝ^n - i
11. ¬(i = (n - 1) ∈ ℤ)
⊢ (p⋅p + λj.if (j =z 0) then t else p ((i + j) - 1) fi ⋅λj.if (j =z 0) then t else p ((i + j) - 1) fi ) = (p⋅p + t^2)
Latex:
Latex:
1. n : \mBbbN{}\msupplus{}
2. t : \mBbbR{}
3. i : \mBbbN{}n
4. p : \mBbbR{}\^{}n - 1
5. \mlambda{}j.if j <z i then p j
if i <z j then p (j - 1)
else t
fi \mmember{} \mBbbR{}\^{}n
6. \mforall{}[x,y:\mBbbR{}\^{}n]. (x\mcdot{}y = (x\mcdot{}y + \mlambda{}i@0.(x (i + i@0))\mcdot{}\mlambda{}i@0.(y (i + i@0))))
7. req-vec(i;\mlambda{}j.if j <z i then p j
if i <z j then p (j - 1)
else t
fi ;p)
8. \mlambda{}i@0.if i + i@0 <z i then p (i + i@0)
if i <z i + i@0 then p ((i + i@0) - 1)
else t
fi \mmember{} \mBbbR{}\^{}n - i
9. req-vec(n - i;\mlambda{}i@0.if i + i@0 <z i then p (i + i@0)
if i <z i + i@0 then p ((i + i@0) - 1)
else t
fi ;\mlambda{}j.if (j =\msubz{} 0) then t else p ((i + j) - 1) fi )
10. \mlambda{}j.if (j =\msubz{} 0) then t else p ((i + j) - 1) fi \mmember{} \mBbbR{}\^{}n - i
\mvdash{} (p\mcdot{}p
+ \mlambda{}j.if (j =\msubz{} 0) then t else p ((i + j) - 1) fi \mcdot{}\mlambda{}j.if (j =\msubz{} 0) then t else p ((i + j) - 1) fi )
= (p\mcdot{}p + t\^{}2)
By
Latex:
(Decide \mkleeneopen{}i = (n - 1)\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index