a
⟺
a
∧
a
⟺
a
∨
a
⟺
¬
¬
a
⟺
a
∧
T
⟺
a
∨
F
{\displaystyle a\iff a\land a\iff a\lor a\iff \neg \neg a\iff a\land T\iff a\lor F}
a
∧
¬
a
⟺
F
⟺
a
∧
F
{\displaystyle a\land \neg a\iff F\iff a\land F}
a
∨
¬
a
⟺
T
⟺
a
∨
T
{\displaystyle a\lor \neg a\iff T\iff a\lor T}
a
∧
¬
b
∨
b
⟺
(
a
∨
b
)
∧
(
¬
b
∨
b
)
⟺
(
a
∨
b
)
∧
T
⟺
a
∨
b
{\displaystyle a\land \neg b\lor b\iff (a\lor b)\land (\neg b\lor b)\iff (a\lor b)\land T\iff a\lor b}
(
a
∨
¬
b
)
∧
b
⟺
a
∧
b
∨
¬
b
∧
b
⟺
a
∧
b
∨
F
⟺
a
∧
b
{\displaystyle (a\lor \neg b)\land b\iff a\land b\lor \neg b\land b\iff a\land b\lor F\iff a\land b}
(
a
∨
¬
b
)
∧
b
⟺
(
a
∨
¬
b
)
∧
(
b
∨
¬
(
a
∨
¬
b
)
)
⟺
(
a
∨
¬
b
)
∧
(
b
∨
¬
a
∧
b
)
⟺
(
a
∨
¬
b
)
∧
(
b
∨
¬
a
)
∧
(
b
∨
b
)
⟺
{\displaystyle (a\lor \neg b)\land b\iff (a\lor \neg b)\land (b\lor \neg (a\lor \neg b))\iff (a\lor \neg b)\land (b\lor \neg a\land b)\iff (a\lor \neg b)\land (b\lor \neg a)\land (b\lor b)\iff }
∃
.
.
.
⟺
∀
x
f
(
x
)
{\displaystyle \exists ...\iff \forall x\ f(x)}
[
a
⟹
a
∨
b
]
⟺
¬
a
∨
a
∨
b
⟺
T
∨
b
⟺
T
{\displaystyle [a\implies a\lor b]\iff \neg a\lor a\lor b\iff T\lor b\iff T}
[
a
∧
c
⟹
(
a
∨
b
)
∧
c
]
⟺
¬
(
a
∧
c
)
∨
(
a
∨
b
)
∧
c
⟺
¬
a
∨
¬
c
∨
(
a
∨
b
)
∧
c
⟺
¬
a
∨
¬
c
∨
a
∨
b
⟺
T
∨
¬
c
∨
b
⟺
T
{\displaystyle [a\land c\implies (a\lor b)\land c]\iff \neg (a\land c)\lor (a\lor b)\land c\iff \neg a\lor \neg c\lor (a\lor b)\land c\iff \neg a\lor \neg c\lor a\lor b\iff T\lor \neg c\lor b\iff T}
[
∀
x
f
(
x
)
⟹
∀
x
(
f
(
x
)
∨
g
(
x
)
)
]
⟺
¬
∀
x
f
(
x
)
∨
∀
x
(
f
(
x
)
∨
g
(
x
)
)
⟺
∃
x
¬
f
(
x
)
∨
{\displaystyle [\forall x\ f(x)\implies \forall x(f(x)\lor g(x))]\iff \neg \forall x\ f(x)\lor \forall x(f(x)\lor g(x))\iff \exists x\ \neg f(x)\lor }
T
⟺
[
¬
a
∧
¬
c
⟹
(
¬
a
∨
¬
b
)
∧
¬
c
]
⟺
[
¬
(
a
∨
c
)
⟹
¬
(
a
∧
b
∨
c
)
]
⟺
[
a
∧
b
∨
c
⟹
a
∨
c
]
{\displaystyle T\iff [\neg a\land \neg c\implies (\neg a\lor \neg b)\land \neg c]\iff [\neg (a\lor c)\implies \neg (a\land b\lor c)]\iff [a\land b\lor c\implies a\lor c]}
[
a
∧
b
⟹
a
]
⟺
¬
(
a
∧
b
)
∨
a
⟺
¬
a
∨
¬
b
∨
a
⟺
T
∨
¬
b
⟺
T
{\displaystyle [a\land b\implies a]\iff \neg (a\land b)\lor a\iff \neg a\lor \neg b\lor a\iff T\lor \neg b\iff T}
a
∧
b
⟹
a
⟹
a
∨
b
{\displaystyle a\land b\implies a\implies a\lor b}
[
a
⟹
b
]
⟹
[
a
∨
b
⟹
b
∨
b
⟺
b
]
∧
[
b
⟹
a
∨
b
]
⟺
[
b
⟺
a
∨
b
]
{\displaystyle [a\implies b]\implies [a\lor b\implies b\lor b\iff b]\land [b\implies a\lor b]\iff [b\iff a\lor b]}
[
a
⟹
b
]
⟹
[
a
⟺
a
∧
a
⟹
a
∧
b
]
∧
[
a
∧
b
⟹
a
]
⟺
[
a
⟺
a
∧
b
]
{\displaystyle [a\implies b]\implies [a\iff a\land a\implies a\land b]\land [a\land b\implies a]\iff [a\iff a\land b]}
[
a
⟹
b
]
⟹
[
f
(
a
)
⟺
f
(
a
∧
b
)
]
{\displaystyle [a\implies b]\implies [f(a)\iff f(a\land b)]}
f
(
a
∧
[
a
⟹
b
]
)
⟺
f
(
a
∧
[
¬
a
∨
b
]
)
⟺
f
(
a
∧
¬
a
∨
a
∧
b
)
⟺
f
(
F
∨
a
∧
b
)
⟺
f
(
a
∧
b
)
{\displaystyle f(a\land [a\implies b])\iff f(a\land [\neg a\lor b])\iff f(a\land \neg a\lor a\land b)\iff f(F\lor a\land b)\iff f(a\land b)}
[
(
a
⟹
b
)
⟹
(
a
∧
c
⟹
b
)
]
⟺
¬
(
¬
a
∨
b
)
∨
(
¬
(
a
∧
c
)
∨
b
)
⟺
a
∧
¬
b
∨
¬
a
∨
¬
c
∨
b
⟺
a
∨
b
∨
¬
a
∨
¬
c
⟺
T
∨
b
∨
¬
c
⟺
T
{\displaystyle [(a\implies b)\implies (a\land c\implies b)]\iff \neg (\neg a\lor b)\lor (\neg (a\land c)\lor b)\iff a\land \neg b\lor \neg a\lor \neg c\lor b\iff a\lor b\lor \neg a\lor \neg c\iff T\lor b\lor \neg c\iff T}
[
a
⟹
b
]
⟺
¬
a
∨
b
⟹
¬
a
∨
b
∨
¬
c
⟺
¬
(
a
∧
c
)
∨
b
⟺
[
a
∧
c
⟹
b
]
{\displaystyle [a\implies b]\iff \neg a\lor b\implies \neg a\lor b\lor \neg c\iff \neg (a\land c)\lor b\iff [a\land c\implies b]}
(
a
⟹
b
)
∧
(
c
⟹
d
)
⟺
(
¬
a
∨
b
)
∧
(
¬
c
∨
d
)
⟹
(
¬
a
∨
b
∨
¬
c
)
∧
(
¬
c
∨
d
∨
¬
a
)
⟺
(
¬
(
a
∧
c
)
∨
b
)
∧
(
¬
(
a
∧
c
)
∨
d
)
⟺
¬
(
a
∧
c
)
∨
b
∧
d
⟺
[
a
∧
c
⟹
b
∧
d
]
{\displaystyle (a\implies b)\land (c\implies d)\iff (\neg a\lor b)\land (\neg c\lor d)\implies (\neg a\lor b\lor \neg c)\land (\neg c\lor d\lor \neg a)\iff (\neg (a\land c)\lor b)\land (\neg (a\land c)\lor d)\iff \neg (a\land c)\lor b\land d\iff [a\land c\implies b\land d]}
(
a
∨
b
)
∧
(
b
⟹
c
)
⟺
(
a
∨
b
)
∧
(
¬
b
∨
c
)
⟺
a
∧
¬
b
∨
a
∧
c
∨
b
∧
¬
b
∨
b
∧
c
⟺
a
∧
¬
b
∨
a
∧
c
∨
b
∧
c
⟺
(
a
∨
a
)
∧
(
a
∨
c
)
∧
(
¬
b
∨
a
)
∧
(
¬
b
∨
c
)
∨
b
∧
c
{\displaystyle (a\lor b)\land (b\implies c)\iff (a\lor b)\land (\neg b\lor c)\iff a\land \neg b\lor a\land c\lor b\land \neg b\lor b\land c\iff a\land \neg b\lor a\land c\lor b\land c\iff (a\lor a)\land (a\lor c)\land (\neg b\lor a)\land (\neg b\lor c)\lor b\land c}
(
a
∨
b
)
∧
(
b
⟹
c
)
⟺
(
a
∨
b
)
∧
(
a
∨
c
∨
b
)
∧
(
¬
b
∨
a
∨
b
)
∧
(
¬
b
∨
c
∨
b
)
∧
(
a
∨
c
)
∧
(
a
∨
c
∨
c
)
∧
(
¬
b
∨
a
∨
c
)
∧
(
¬
b
∨
c
∨
c
)
⟹
a
∨
c
{\displaystyle (a\lor b)\land (b\implies c)\iff (a\lor b)\land (a\lor c\lor b)\land (\neg b\lor a\lor b)\land (\neg b\lor c\lor b)\land (a\lor c)\land (a\lor c\lor c)\land (\neg b\lor a\lor c)\land (\neg b\lor c\lor c)\implies a\lor c}
(
b
⟹
c
)
⟹
(
a
∨
b
⟹
a
∨
c
)
{\displaystyle (b\implies c)\implies (a\lor b\implies a\lor c)}
[
a
∧
b
⟹
c
]
⟺
¬
(
a
∧
b
)
∨
c
⟺
¬
a
∨
¬
b
∨
c
⟺
[
a
⟹
(
b
⟹
c
)
]
{\displaystyle [a\land b\implies c]\iff \neg (a\land b)\lor c\iff \neg a\lor \neg b\lor c\iff [a\implies (b\implies c)]}
(
a
∧
b
)
∧
(
b
⟹
c
)
⟺
a
∧
b
∧
(
¬
b
∨
c
)
⟺
a
∧
b
∧
¬
b
∨
a
∧
b
∧
c
⟺
F
∨
a
∧
b
∧
c
⟺
a
∧
b
∧
c
⟹
a
∧
c
{\displaystyle (a\land b)\land (b\implies c)\iff a\land b\land (\neg b\lor c)\iff a\land b\land \neg b\lor a\land b\land c\iff F\lor a\land b\land c\iff a\land b\land c\implies a\land c}
(
b
⟹
c
)
⟹
(
a
∧
b
⟹
a
∧
c
)
{\displaystyle (b\implies c)\implies (a\land b\implies a\land c)}
a
∧
(
a
⟹
b
)
⟺
a
∧
(
¬
a
∨
b
)
⟺
a
∧
¬
a
∨
a
∧
b
⟺
F
∨
a
∧
b
⟺
a
∧
b
⟹
b
{\displaystyle a\land (a\implies b)\iff a\land (\neg a\lor b)\iff a\land \neg a\lor a\land b\iff F\lor a\land b\iff a\land b\implies b}
f
(
a
)
⟺
a
∧
f
(
T
)
∨
¬
a
∧
f
(
F
)
{\displaystyle f(a)\iff a\land f(T)\lor \neg a\land f(F)}
a
∧
f
(
a
)
⟺
a
∧
f
(
T
)
{\displaystyle a\land f(a)\iff a\land f(T)}
a
∨
f
(
a
)
⟺
¬
(
¬
a
∧
¬
f
(
¬
¬
a
)
)
⟺
¬
(
¬
a
∧
¬
f
(
¬
T
)
)
⟺
a
∨
f
(
F
)
{\displaystyle a\lor f(a)\iff \neg (\neg a\land \neg f(\neg \neg a))\iff \neg (\neg a\land \neg f(\neg T))\iff a\lor f(F)}
[
a
⟹
f
(
a
)
]
⟺
¬
a
∨
f
(
¬
¬
a
)
⟺
¬
a
∨
f
(
¬
F
)
⟺
[
a
⟹
f
(
T
)
]
{\displaystyle [a\implies f(a)]\iff \neg a\lor f(\neg \neg a)\iff \neg a\lor f(\neg F)\iff [a\implies f(T)]}
∀
x
∈
A
f
(
x
)
{\displaystyle \forall x\in \mathbb {A} \ f(x)}
⟺
{\displaystyle \iff }
∀
x
[
x
∈
A
⟹
f
(
x
)
]
{\displaystyle \forall x\ [x\in \mathbb {A} \implies f(x)]}
⟺
{\displaystyle \iff }
∀
a
[
a
∈
A
⟹
f
(
a
)
]
{\displaystyle \forall a\ [a\in \mathbb {A} \implies f(a)]}
⟹
{\displaystyle \implies }
[
c
∈
A
⟹
f
(
c
)
]
{\displaystyle [c\in \mathbb {A} \implies f(c)]}
∀
x
∈
A
f
(
x
)
{\displaystyle \forall x\in \mathbb {A} \ f(x)}
⟺
{\displaystyle {\cancel {\iff }}}
[
x
∈
A
⟹
f
(
x
)
]
{\displaystyle [x\in \mathbb {A} \implies f(x)]}
x
{\displaystyle x}
counter example:
¬
∀
x
∈
A
f
(
x
)
⟺
¬
(
x
∈
A
⟹
f
(
x
)
)
⟺
¬
(
¬
x
∈
A
∨
f
(
x
)
)
⟺
x
∈
A
∧
¬
f
(
x
)
{\displaystyle \neg \forall x\in \mathbb {A} \ f(x){\cancel {\iff }}\neg (x\in \mathbb {A} \implies f(x))\iff \neg (\neg x\in \mathbb {A} \lor f(x))\iff x\in \mathbb {A} \land \neg f(x)}
∀
a
∈
A
f
(
a
)
∨
∀
b
∈
B
f
(
b
)
⟺
[
a
∈
A
⟹
f
(
a
)
∨
b
∈
B
⟹
f
(
b
)
]
⟺
¬
a
∈
A
∨
f
(
a
)
∨
¬
b
∈
B
∨
f
(
b
)
{\displaystyle \forall a\in \mathbb {A} \ f(a)\lor \forall b\in \mathbb {B} \ f(b){\cancel {\iff }}[a\in \mathbb {A} \implies f(a)\lor b\in \mathbb {B} \implies f(b)]\iff \neg a\in \mathbb {A} \lor f(a)\lor \neg b\in \mathbb {B} \lor f(b)}
∀
a
∈
A
f
(
a
)
∨
∀
b
∈
B
f
(
b
)
⟺
¬
(
a
∈
A
∧
b
∈
B
)
∨
f
(
a
)
∨
f
(
b
)
⟺
[
a
∈
A
∧
b
∈
B
⟹
f
(
a
)
∨
f
(
b
)
]
{\displaystyle \forall a\in \mathbb {A} \ f(a)\lor \forall b\in \mathbb {B} \ f(b){\cancel {\iff }}\neg (a\in \mathbb {A} \land b\in \mathbb {B} )\lor f(a)\lor f(b)\iff [a\in \mathbb {A} \land b\in \mathbb {B} \implies f(a)\lor f(b)]}
∀
x
∈
A
f
(
x
)
⟺
∀
a
∈
A
f
(
a
)
{\displaystyle \forall x\in \mathbb {A} \ f(x)\iff \forall a\in \mathbb {A} \ f(a)}
a
∈
A
∧
∀
x
∈
A
f
(
x
)
⟹
f
(
a
)
{\displaystyle a\in \mathbb {A} \land \forall x\in \mathbb {A} \ f(x)\implies f(a)}
∀
x
∈
A
f
(
x
∈
A
)
⟺
∀
x
[
x
∈
A
⟹
f
(
x
∈
A
)
]
⟺
∀
x
[
x
∈
A
⟹
f
(
T
)
]
⟺
∀
x
∈
A
f
(
T
)
{\displaystyle \forall x\in \mathbb {A} \ f(x\in \mathbb {A} )\iff \forall x\ [x\in \mathbb {A} \implies f(x\in \mathbb {A} )]\iff \forall x\ [x\in \mathbb {A} \implies f(T)]\iff \forall x\in \mathbb {A} \ f(T)}
∃
x
∈
A
f
(
x
∈
A
)
⟺
¬
∀
x
∈
A
¬
f
(
x
∈
A
)
⟺
¬
∀
x
∈
A
¬
f
(
T
)
⟺
∃
x
∈
A
f
(
T
)
{\displaystyle \exists x\in \mathbb {A} \ f(x\in \mathbb {A} )\iff \neg \forall x\in \mathbb {A} \ \neg f(x\in \mathbb {A} )\iff \neg \forall x\in \mathbb {A} \ \neg f(T)\iff \exists x\in \mathbb {A} \ f(T)}
a
∧
∀
x
∈
A
f
(
x
)
⟺
.
.
.
∀
x
∈
A
(
a
∧
f
(
x
)
)
{\displaystyle a\land \forall x\in \mathbb {A} \ f(x)\iff ...\forall x\in \mathbb {A} (a\land f(x))}
∀
x
∈
A
f
(
x
)
⟺
∀
x
∈
A
f
(
x
)
∧
∀
x
∈
A
f
(
x
)
⟺
∀
x
∈
A
f
(
x
)
∧
∀
a
∈
A
f
(
a
)
⟺
{\displaystyle \forall x\in \mathbb {A} \ f(x)\iff \forall x\in \mathbb {A} \ f(x)\land \forall x\in \mathbb {A} \ f(x)\iff \forall x\in \mathbb {A} \ f(x)\land \forall a\in \mathbb {A} \ f(a)\iff }
∀
x
[
f
(
x
)
∧
g
(
x
)
]
⟺
∀
x
f
(
x
)
∧
∀
x
g
(
x
)
{\displaystyle \forall x[f(x)\land g(x)]\iff \forall x\ f(x)\land \forall x\ g(x)}
∀
x
f
(
x
)
∨
∀
x
g
(
x
)
⟹
∀
x
[
f
(
x
)
∨
g
(
x
)
]
∨
∀
x
[
g
(
x
)
∨
f
(
x
)
]
⟺
∀
x
[
f
(
x
)
∨
g
(
x
)
]
{\displaystyle \forall x\ f(x)\lor \forall x\ g(x)\implies \forall x\ [f(x)\lor g(x)]\lor \forall x\ [g(x)\lor f(x)]\iff \forall x[f(x)\lor g(x)]}
¬
¬
(
∀
x
f
(
x
)
∨
∀
x
g
(
x
)
)
⟹
¬
¬
∀
x
[
f
(
x
)
∨
g
(
x
)
]
{\displaystyle \neg \neg (\forall x\ f(x)\lor \forall x\ g(x))\implies \neg \neg \forall x[f(x)\lor g(x)]}
¬
(
∃
x
¬
f
(
x
)
∧
∃
x
¬
g
(
x
)
)
⟹
¬
∃
x
[
¬
f
(
x
)
∧
¬
g
(
x
)
]
{\displaystyle \neg (\exists x\ \neg f(x)\land \exists x\ \neg g(x))\implies \neg \exists x[\neg f(x)\land \neg g(x)]}
¬
(
∃
x
f
(
x
)
∧
∃
x
g
(
x
)
)
⟹
¬
∃
x
[
f
(
x
)
∧
g
(
x
)
]
{\displaystyle \neg (\exists x\ f(x)\land \exists x\ g(x))\implies \neg \exists x[f(x)\land g(x)]}
∃
x
[
f
(
x
)
∧
g
(
x
)
]
⟺
∃
x
[
f
(
x
)
∧
g
(
x
)
]
∧
∃
x
[
f
(
x
)
∧
g
(
x
)
]
⟹
∃
x
f
(
x
)
∧
∃
x
g
(
x
)
{\displaystyle \exists x[f(x)\land g(x)]\iff \exists x[f(x)\land g(x)]\land \exists x[f(x)\land g(x)]\implies \exists x\ f(x)\land \exists x\ g(x)}
∃
x
[
f
(
x
)
∨
g
(
x
)
]
⟺
∃
x
f
(
x
)
∨
∃
x
g
(
x
)
{\displaystyle \exists x[f(x)\lor g(x)]\iff \exists x\ f(x)\lor \exists x\ g(x)}
∀
x
¬
f
(
x
)
⟺
¬
∃
x
f
(
x
)
{\displaystyle \forall x\ \neg f(x)\iff \neg \exists x\ f(x)}
∀
x
f
(
x
)
⟹
∃
x
f
(
x
)
{\displaystyle \forall x\ f(x)\implies \exists x\ f(x)}
∀
x
(
f
(
x
)
∧
g
(
x
)
)
⟺
∀
x
f
(
x
)
∧
∀
x
g
(
x
)
⟹
∀
x
f
(
x
)
{\displaystyle \forall x(f(x)\land g(x))\iff \forall x\ f(x)\land \forall x\ g(x)\implies \forall x\ f(x)}
∀
x
f
(
x
)
⟹
∀
x
(
f
(
x
)
∨
g
(
x
)
)
{\displaystyle \forall x\ f(x)\implies \forall x(f(x)\lor g(x))}
[
∀
x
(
f
(
x
)
⟹
g
(
x
)
)
⟹
(
∀
x
f
(
x
)
⟹
∀
x
g
(
x
)
)
]
⟺
¬
∀
x
(
¬
f
(
x
)
∨
g
(
x
)
)
∨
(
¬
∀
x
f
(
x
)
∨
∀
x
g
(
x
)
)
{\displaystyle [\forall x(f(x)\implies g(x))\implies (\forall x\ f(x)\implies \forall x\ g(x))]\iff \neg \forall x(\neg f(x)\lor g(x))\lor (\neg \forall x\ f(x)\lor \forall x\ g(x))}
[
∀
x
(
f
(
x
)
⟹
g
(
x
)
)
⟹
(
∀
x
f
(
x
)
⟹
∀
x
g
(
x
)
)
]
⟺
∃
x
(
f
(
x
)
∧
¬
g
(
x
)
)
∨
∃
x
¬
f
(
x
)
∨
∀
x
g
(
x
)
{\displaystyle [\forall x(f(x)\implies g(x))\implies (\forall x\ f(x)\implies \forall x\ g(x))]\iff \exists x(f(x)\land \neg g(x))\lor \exists x\ \neg f(x)\lor \forall x\ g(x)}
[
∀
x
(
f
(
x
)
⟹
g
(
x
)
)
⟹
(
∀
x
f
(
x
)
⟹
∀
x
g
(
x
)
)
]
⟺
∃
x
(
f
(
x
)
∧
¬
g
(
x
)
∨
¬
f
(
x
)
)
∨
∀
x
g
(
x
)
⟺
∃
x
(
¬
g
(
x
)
∨
¬
f
(
x
)
)
∨
∀
x
g
(
x
)
{\displaystyle [\forall x(f(x)\implies g(x))\implies (\forall x\ f(x)\implies \forall x\ g(x))]\iff \exists x(f(x)\land \neg g(x)\lor \neg f(x))\lor \forall x\ g(x)\iff \exists x(\neg g(x)\lor \neg f(x))\lor \forall x\ g(x)}
[
∀
x
(
f
(
x
)
⟹
g
(
x
)
)
⟹
(
∀
x
f
(
x
)
⟹
∀
x
g
(
x
)
)
]
⟺
∃
x
¬
g
(
x
)
∨
∃
x
¬
f
(
x
)
∨
¬
∃
x
¬
g
(
x
)
⟺
T
∨
∃
x
¬
f
(
x
)
⟺
T
{\displaystyle [\forall x(f(x)\implies g(x))\implies (\forall x\ f(x)\implies \forall x\ g(x))]\iff \exists x\ \neg g(x)\lor \exists x\ \neg f(x)\lor \neg \exists x\ \neg g(x)\iff T\lor \exists x\ \neg f(x)\iff T}
TODO: prove by "\implies"
∀
x
(
f
(
x
)
⟹
g
(
x
)
)
⟺
∀
x
(
¬
f
(
x
)
∨
g
(
x
)
)
⟹
∀
x
(
¬
f
(
x
)
∨
g
(
x
)
∨
¬
∀
x
f
(
x
)
)
?
?
?
{\displaystyle \forall x(f(x)\implies g(x))\iff \forall x(\neg f(x)\lor g(x))\implies \forall x(\neg f(x)\lor g(x)\lor \neg \forall x\ f(x))???}
∀
x
[
f
(
x
)
⟺
g
(
x
)
]
⟺
∀
x
[
f
(
x
)
∧
g
(
x
)
∨
¬
f
(
x
)
∧
¬
g
(
x
)
]
⟸
∀
x
[
f
(
x
)
∧
g
(
x
)
]
∨
∀
x
[
¬
f
(
x
)
∧
¬
g
(
x
)
]
⟺
∀
x
f
(
x
)
∧
∀
x
g
(
x
)
∨
∀
x
¬
f
(
x
)
∧
∀
x
¬
g
(
x
)
{\displaystyle \forall x[f(x)\iff g(x)]\iff \forall x[f(x)\land g(x)\lor \neg f(x)\land \neg g(x)]\Longleftarrow \forall x[f(x)\land g(x)]\lor \forall x[\neg f(x)\land \neg g(x)]\iff \forall x\ f(x)\land \forall x\ g(x)\lor \forall x\neg f(x)\land \forall x\neg g(x)}
∀
x
[
f
(
x
)
⟺
g
(
x
)
]
⟺
∀
x
[
f
(
x
)
∧
g
(
x
)
∨
¬
f
(
x
)
∧
¬
g
(
x
)
]
⟹
∃
x
[
f
(
x
)
∧
g
(
x
)
∨
¬
f
(
x
)
∧
¬
g
(
x
)
]
⟺
∃
x
[
f
(
x
)
∧
g
(
x
)
]
∨
∃
x
[
¬
f
(
x
)
∧
¬
g
(
x
)
]
⟹
∃
x
f
(
x
)
∧
∃
x
g
(
x
)
∨
∃
x
¬
f
(
x
)
∧
∃
x
¬
g
(
x
)
⟺
∃
x
f
(
x
)
∧
∃
x
g
(
x
)
∨
¬
∀
x
f
(
x
)
∧
¬
∀
x
g
(
x
)
{\displaystyle \forall x[f(x)\iff g(x)]\iff \forall x[f(x)\land g(x)\lor \neg f(x)\land \neg g(x)]\implies \exists x[f(x)\land g(x)\lor \neg f(x)\land \neg g(x)]\iff \exists x[f(x)\land g(x)]\lor \exists x[\neg f(x)\land \neg g(x)]\implies \exists x\ f(x)\land \exists x\ g(x)\lor \exists x\ \neg f(x)\land \exists x\ \neg g(x)\iff \exists x\ f(x)\land \exists x\ g(x)\lor \neg \forall x\ f(x)\land \neg \forall x\ g(x)}
¬
∀
x
[
f
(
x
)
⟺
g
(
x
)
]
⟺
∃
x
[
f
(
x
)
⟺
¬
g
(
x
)
]
⟺
∃
x
[
f
(
x
)
∧
¬
g
(
x
)
∨
¬
f
(
x
)
∧
g
(
x
)
]
⟺
∃
x
[
f
(
x
)
∧
¬
g
(
x
)
]
∨
∃
x
[
¬
f
(
x
)
∧
g
(
x
)
]
⟹
∃
x
f
(
x
)
∧
∃
x
¬
g
(
x
)
∨
∃
x
¬
f
(
x
)
∧
∃
x
g
(
x
)
⟺
∃
x
f
(
x
)
∧
¬
∀
x
g
(
x
)
∨
¬
∀
x
f
(
x
)
∧
∃
x
g
(
x
)
{\displaystyle \neg \forall x[f(x)\iff g(x)]\iff \exists x[f(x)\iff \neg g(x)]\iff \exists x[f(x)\land \neg g(x)\lor \neg f(x)\land g(x)]\iff \exists x[f(x)\land \neg g(x)]\lor \exists x[\neg f(x)\land g(x)]\implies \exists x\ f(x)\land \exists x\ \neg g(x)\lor \exists x\ \neg f(x)\land \exists x\ g(x)\iff \exists x\ f(x)\land \neg \forall x\ g(x)\lor \neg \forall x\ f(x)\land \exists x\ g(x)}
∀
x
[
f
(
x
)
⟺
g
(
x
)
]
⟺
∀
x
[
f
(
x
)
∧
g
(
x
)
∨
¬
f
(
x
)
∧
¬
g
(
x
)
]
⟺
∀
x
[
(
f
(
x
)
∨
¬
g
(
x
)
)
∧
(
¬
f
(
x
)
∨
g
(
x
)
)
]
⟺
∀
x
[
f
(
x
)
∨
¬
g
(
x
)
]
∧
∀
[
¬
f
(
x
)
∨
g
(
x
)
]
{\displaystyle \forall x[f(x)\iff g(x)]\iff \forall x[f(x)\land g(x)\lor \neg f(x)\land \neg g(x)]\iff \forall x[(f(x)\lor \neg g(x))\land (\neg f(x)\lor g(x))]\iff \forall x[f(x)\lor \neg g(x)]\land \forall [\neg f(x)\lor g(x)]}
(
x
−
ε
)
2
<<
x
2
+
a
<<
(
x
+
ε
)
2
;
x
>>
ε
>
0
{\displaystyle (x-\varepsilon )^{2}<<x^{2}+a<<(x+\varepsilon )^{2};\ x>>\varepsilon >0}
x
−
ε
<
x
2
+
a
<
x
+
ε
;
x
>>
ε
>
0
{\displaystyle x-\varepsilon <{\sqrt {x^{2}+a}}<x+\varepsilon ;\ x>>\varepsilon >0}
x
−
ε
−
x
<
x
2
+
a
−
x
<
x
+
ε
−
x
;
x
>>
ε
>
0
{\displaystyle x-\varepsilon -x<{\sqrt {x^{2}+a}}-x<x+\varepsilon -x;\ x>>\varepsilon >0}
−
ε
<
x
2
+
a
−
x
<
ε
;
x
>>
ε
>
0
{\displaystyle -\varepsilon <{\sqrt {x^{2}+a}}-x<\varepsilon ;\ x>>\varepsilon >0}
lim
x
→
∞
(
x
2
+
a
−
x
)
=
0
{\displaystyle \lim _{x\to \infty }({\sqrt {x^{2}+a}}-x)=0}
lim
x
→
∞
(
(
x
+
b
)
2
+
a
−
(
x
+
b
)
)
=
0
{\displaystyle \lim _{x\to \infty }({\sqrt {(x+b)^{2}+a}}-(x+b))=0}
lim
x
→
∞
(
(
x
+
b
)
2
+
a
−
x
)
=
b
{\displaystyle \lim _{x\to \infty }({\sqrt {(x+b)^{2}+a}}-x)=b}
lim
x
→
c
f
(
x
)
=
L
{\displaystyle \lim _{x\to c}f(x)=L}
∀
ε
>
0
∃
δ
>
0
∀
x
(
0
<
|
x
−
c
|
<
δ
⟹
|
f
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x(0<|x-c|<\delta \ \implies \ |f(x)-L|<\varepsilon )}
"0 < |x - c|" means that "x <> c"
lim
x
→
c
+
f
(
x
)
=
L
{\displaystyle \lim _{x\to c^{+}}f(x)=L}
∀
ε
>
0
∃
δ
>
0
∀
x
(
0
<
x
−
c
<
δ
⟹
|
f
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x(0<x-c<\delta \ \implies \ |f(x)-L|<\varepsilon )}
lim
x
→
0
+
f
(
x
)
=
L
=
lim
1
/
x
→
∞
f
(
1
/
(
1
/
x
)
)
=
lim
x
→
∞
f
(
1
/
x
)
{\displaystyle \lim _{x\to 0^{+}}f(x)=L=\lim _{1/x\to \infty }f(1/(1/x))=\lim _{x\to \infty }f(1/x)}
∀
ε
>
0
∃
δ
>
0
∀
x
(
0
<
x
<
δ
⟹
|
f
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x(0<x<\delta \ \implies \ |f(x)-L|<\varepsilon )}
∀
ε
>
0
∃
δ
>
0
∀
x
>
0
(
0
<
x
<
δ
⟹
|
f
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x>0(0<x<\delta \ \implies \ |f(x)-L|<\varepsilon )}
∀
ε
>
0
∃
δ
>
0
∀
x
>
0
(
∞
>
1
/
x
>
1
/
δ
⟹
|
f
(
1
/
(
1
/
x
)
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x>0(\infty >1/x>1/\delta \ \implies \ |f(1/(1/x))-L|<\varepsilon )}
∀
ε
>
0
∃
δ
>
0
∀
x
>
0
(
x
>
1
/
δ
⟹
|
f
(
1
/
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x>0(x>1/\delta \ \implies \ |f(1/x)-L|<\varepsilon )}
∀
ε
>
0
∃
δ
>
0
∀
x
>
0
(
x
>
δ
⟹
|
f
(
1
/
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x>0(x>\delta \ \implies \ |f(1/x)-L|<\varepsilon )}
∀
ε
>
0
∃
δ
>
0
∀
x
(
0
<
|
x
−
c
|
<
δ
⟹
|
f
(
x
)
−
L
|
<
ε
⟹
|
|
f
(
x
)
|
−
|
L
|
|
<
|
f
(
x
)
−
L
|
<
ε
)
.
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x(0<|x-c|<\delta \ \implies \ |f(x)-L|<\varepsilon \ \implies \ {\Big |}|f(x)|-|L|{\Big |}<|f(x)-L|<\varepsilon ).}
lim
x
→
c
f
(
x
)
=
L
⟹
lim
x
→
c
|
f
(
x
)
|
=
|
L
|
=
|
lim
x
→
c
f
(
x
)
|
{\displaystyle \lim _{x\to c}f(x)=L\implies \lim _{x\to c}\left|f(x)\right|=|L|=\left|\lim _{x\to c}f(x)\right|}
|
f
′
(
x
)
|
=
|
d
f
(
x
)
d
x
|
=
|
lim
d
x
→
0
f
(
x
+
d
x
)
−
f
(
x
)
d
x
|
=
lim
d
x
→
0
|
f
(
x
+
d
x
)
−
f
(
x
)
d
x
|
=
lim
d
x
→
0
|
f
(
x
+
d
x
)
−
f
(
x
)
|
|
d
x
|
=
lim
d
x
→
0
d
x
(
f
(
x
+
d
x
)
−
f
(
x
)
)
|
f
(
x
+
d
x
)
−
f
(
x
)
|
d
x
(
f
(
x
+
d
x
)
−
f
(
x
)
)
|
d
x
|
{\displaystyle \left|f'(x)\right|=\left|{\frac {df(x)}{dx}}\right|=\left|\lim _{dx\to 0}{\frac {f(x+dx)-f(x)}{dx}}\right|=\lim _{dx\to 0}\left|{\frac {f(x+dx)-f(x)}{dx}}\right|=\lim _{dx\to 0}{\frac {|f(x+dx)-f(x)|}{|dx|}}=\lim _{dx\to 0}{\frac {dx(f(x+dx)-f(x))|f(x+dx)-f(x)|}{dx(f(x+dx)-f(x))|dx|}}}
lim
d
x
→
0
d
x
(
f
(
x
+
d
x
)
−
f
(
x
)
)
|
f
(
x
+
d
x
)
−
f
(
x
)
|
d
x
(
f
(
x
+
d
x
)
−
f
(
x
)
)
|
d
x
|
=
lim
d
x
→
0
f
(
x
+
d
x
)
−
f
(
x
)
d
x
lim
d
x
→
0
d
x
|
f
(
x
+
d
x
)
−
f
(
x
)
|
|
d
x
|
(
f
(
x
+
d
x
)
−
f
(
x
)
)
=
lim
d
x
→
0
f
(
x
+
d
x
)
−
f
(
x
)
d
x
lim
d
x
→
0
|
d
x
(
f
(
x
+
d
x
)
−
f
(
x
)
)
|
d
x
(
f
(
x
+
d
x
)
−
f
(
x
)
)
=
f
′
(
x
)
.
.
.
?
?
?
{\displaystyle \lim _{dx\to 0}{\frac {dx(f(x+dx)-f(x))|f(x+dx)-f(x)|}{dx(f(x+dx)-f(x))|dx|}}=\lim _{dx\to 0}{\frac {f(x+dx)-f(x)}{dx}}\lim _{dx\to 0}{\frac {dx|f(x+dx)-f(x)|}{|dx|(f(x+dx)-f(x))}}=\lim _{dx\to 0}{\frac {f(x+dx)-f(x)}{dx}}\lim _{dx\to 0}{\frac {|dx(f(x+dx)-f(x))|}{dx(f(x+dx)-f(x))}}=f'(x)...???}
x
|
x
|
=
x
|
x
|
2
|
x
|
x
2
=
|
x
|
x
{\displaystyle {\frac {x}{|x|}}={\frac {x|x|^{2}}{|x|x^{2}}}={\frac {|x|}{x}}}
∃
δ
>
0
∀
x
(
0
<
|
x
−
c
|
<
δ
⟹
f
(
x
)
=
g
(
x
)
)
{\displaystyle \exists \delta >0\ \forall x(0<|x-c|<\delta \implies f(x)=g(x))}
∀
x
(
0
<
|
x
−
c
|
<
δ
g
⟹
f
(
x
)
=
g
(
x
)
)
;
δ
g
>
0
{\displaystyle \forall x(0<|x-c|<\delta _{g}\implies f(x)=g(x));\delta _{g}>0}
∀
ε
>
0
∃
δ
>
0
∀
x
(
0
<
|
x
−
c
|
<
δ
⟹
|
f
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x(0<|x-c|<\delta \ \implies \ |f(x)-L|<\varepsilon )}
∀
ε
>
0
∃
δ
>
0
∀
x
(
0
<
|
x
−
c
|
<
min
(
δ
,
δ
g
)
⟹
|
f
(
x
)
−
L
|
=
|
g
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x(0<|x-c|<\min(\delta ,\delta _{g})\ \implies \ |f(x)-L|=|g(x)-L|<\varepsilon )}
∀
ε
>
0
∃
min
(
δ
,
δ
g
)
>
0
∀
x
(
0
<
|
x
−
c
|
<
min
(
δ
,
δ
g
)
⟹
|
g
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \min(\delta ,\delta _{g})>0\ \ \forall x(0<|x-c|<\min(\delta ,\delta _{g})\ \implies \ |g(x)-L|<\varepsilon )}
lim
x
→
c
f
(
x
)
=
L
=
lim
x
→
c
g
(
x
)
{\displaystyle \lim _{x\to c}f(x)=L=\lim _{x\to c}g(x)}
∃
δ
>
0
∀
x
(
0
<
x
−
c
<
δ
⟹
f
(
x
)
=
g
(
x
)
)
{\displaystyle \exists \delta >0\ \forall x(0<x-c<\delta \implies f(x)=g(x))}
∀
x
(
0
<
x
−
c
<
δ
g
⟹
f
(
x
)
=
g
(
x
)
)
;
δ
g
>
0
{\displaystyle \forall x(0<x-c<\delta _{g}\implies f(x)=g(x));\delta _{g}>0}
∀
ε
>
0
∃
δ
>
0
∀
x
(
0
<
x
−
c
<
δ
⟹
|
f
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x(0<x-c<\delta \ \implies \ |f(x)-L|<\varepsilon )}
∀
ε
>
0
∃
δ
>
0
∀
x
(
0
<
x
−
c
<
min
(
δ
,
δ
g
)
⟹
|
f
(
x
)
−
L
|
=
|
g
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x(0<x-c<\min(\delta ,\delta _{g})\ \implies \ |f(x)-L|=|g(x)-L|<\varepsilon )}
∀
ε
>
0
∃
min
(
δ
,
δ
g
)
>
0
∀
x
(
0
<
x
−
c
<
min
(
δ
,
δ
g
)
⟹
|
g
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \min(\delta ,\delta _{g})>0\ \ \forall x(0<x-c<\min(\delta ,\delta _{g})\ \implies \ |g(x)-L|<\varepsilon )}
lim
x
→
c
+
f
(
x
)
=
L
=
lim
x
→
c
+
g
(
x
)
{\displaystyle \lim _{x\to c^{+}}f(x)=L=\lim _{x\to c^{+}}g(x)}
∃
δ
>
0
∀
x
(
0
<
x
−
c
<
δ
⟹
f
(
x
)
=
f
(
min
(
x
,
c
+
k
)
)
)
;
k
>
0
{\displaystyle \exists \delta >0\ \forall x(0<x-c<\delta \implies f(x)=f(\min(x,c+k)));k>0}
∀
x
(
0
<
x
−
c
<
k
⟺
c
<
x
<
c
+
k
⟹
x
=
min
(
x
,
c
+
k
)
⟹
f
(
x
)
=
f
(
min
(
x
,
c
+
k
)
)
)
;
k
>
0
{\displaystyle \forall x(0<x-c<k\iff c<x<c+k\implies x=\min(x,c+k)\implies f(x)=f(\min(x,c+k)));k>0}
∀
k
>
0
∀
x
(
0
<
x
−
c
<
k
⟹
f
(
x
)
=
f
(
min
(
x
,
c
+
k
)
)
)
{\displaystyle \forall k>0\ \forall x(0<x-c<k\implies f(x)=f(\min(x,c+k)))}
∀
δ
>
0
∀
x
(
0
<
x
−
c
<
δ
⟹
f
(
x
)
=
f
(
min
(
x
,
c
+
δ
)
)
)
{\displaystyle \forall \delta >0\ \forall x(0<x-c<\delta \implies f(x)=f(\min(x,c+\delta )))}
∃
δ
>
0
∀
x
(
0
<
x
−
c
<
δ
⟹
f
(
x
)
=
f
(
min
(
x
,
c
+
δ
)
)
)
{\displaystyle \exists \delta >0\ \forall x(0<x-c<\delta \implies f(x)=f(\min(x,c+\delta )))}
lim
x
→
c
+
f
(
x
)
=
L
=
lim
x
→
c
+
f
(
min
(
x
,
c
+
k
)
)
;
k
>
0
{\displaystyle \lim _{x\to c^{+}}f(x)=L=\lim _{x\to c^{+}}f(\min(x,c+k));k>0}
∀
x
(
0
<
x
−
c
<
k
⟹
x
=
min
(
x
,
c
+
k
)
⟹
f
(
x
,
x
)
=
f
(
min
(
x
,
c
+
k
)
,
x
)
)
;
k
>
0
{\displaystyle \forall x(0<x-c<k\implies x=\min(x,c+k)\implies f(x,x)=f(\min(x,c+k),x));k>0}
lim
x
→
c
+
f
(
x
,
x
)
=
L
=
lim
x
→
c
+
f
(
min
(
x
,
c
+
k
)
,
x
)
;
k
>
0
{\displaystyle \lim _{x\to c^{+}}f(x,x)=L=\lim _{x\to c^{+}}f(\min(x,c+k),x);k>0}
∀
x
(
0
<
x
−
c
<
k
⟹
x
=
max
(
x
,
c
)
⟹
f
(
x
,
x
)
=
f
(
max
(
x
,
c
)
,
x
)
)
;
k
>
0
{\displaystyle \forall x(0<x-c<k\implies x=\max(x,c)\implies f(x,x)=f(\max(x,c),x));k>0}
lim
x
→
c
+
f
(
x
,
x
)
=
L
=
lim
x
→
c
+
f
(
max
(
x
,
c
)
,
x
)
;
k
>
0
{\displaystyle \lim _{x\to c^{+}}f(x,x)=L=\lim _{x\to c^{+}}f(\max(x,c),x);k>0}
∃
δ
>
0
∀
x
(
0
<
c
−
x
<
δ
⟹
f
(
x
)
=
g
(
x
)
)
{\displaystyle \exists \delta >0\ \forall x(0<c-x<\delta \implies f(x)=g(x))}
∀
x
(
0
<
c
−
x
<
δ
g
⟹
f
(
x
)
=
g
(
x
)
)
;
δ
g
>
0
{\displaystyle \forall x(0<c-x<\delta _{g}\implies f(x)=g(x));\delta _{g}>0}
∀
ε
>
0
∃
δ
>
0
∀
x
(
0
<
c
−
x
<
δ
⟹
|
f
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x(0<c-x<\delta \ \implies \ |f(x)-L|<\varepsilon )}
∀
ε
>
0
∃
δ
>
0
∀
x
(
0
<
c
−
x
<
min
(
δ
,
δ
g
)
⟹
|
f
(
x
)
−
L
|
=
|
g
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \delta >0\ \ \forall x(0<c-x<\min(\delta ,\delta _{g})\ \implies \ |f(x)-L|=|g(x)-L|<\varepsilon )}
∀
ε
>
0
∃
min
(
δ
,
δ
g
)
>
0
∀
x
(
0
<
c
−
x
<
min
(
δ
,
δ
g
)
⟹
|
g
(
x
)
−
L
|
<
ε
)
{\displaystyle \forall \varepsilon >0\ \ \exists \min(\delta ,\delta _{g})>0\ \ \forall x(0<c-x<\min(\delta ,\delta _{g})\ \implies \ |g(x)-L|<\varepsilon )}
lim
x
→
c
−
f
(
x
)
=
L
=
lim
x
→
c
−
g
(
x
)
{\displaystyle \lim _{x\to c^{-}}f(x)=L=\lim _{x\to c^{-}}g(x)}
y
′
=
1
/
x
;
y
=
ln
x
+
c
{\displaystyle y'=1/x;y=\ln x+c}
y
=
ln
x
+
ln
1
=
ln
x
+
0
;
e
y
=
x
−
−
>
y
=
ln
x
+
2
n
π
j
{\displaystyle y=\ln x+\ln 1=\ln x+0;e^{y}=x-->y=\ln x+2n\pi j}
y
=
ln
−
x
=
ln
x
+
ln
−
1
=
ln
x
+
π
j
;
e
y
−
π
j
=
x
−
−
>
y
=
ln
x
+
(
2
n
+
1
)
π
j
{\displaystyle y=\ln -x=\ln x+\ln -1=\ln x+\pi j;e^{y-\pi j}=x-->y=\ln x+(2n+1)\pi j}
0
=
ln
(
1
)
=
ln
(
−
1
⋅
−
1
)
=
ln
(
−
1
)
+
ln
(
−
1
)
=
π
j
+
π
j
=
2
π
j
!
!
!
{\displaystyle 0=\ln(1)=\ln(-1\cdot -1)=\ln(-1)+\ln(-1)=\pi j+\pi j=2\pi j!!!}
1
=
1
=
−
1
⋅
−
1
=
−
1
−
1
=
j
⋅
j
=
−
1
!
!
!
{\displaystyle 1={\sqrt {1}}={\sqrt {-1\cdot -1}}={\sqrt {-1}}{\sqrt {-1}}=j\cdot j=-1!!!}
∫
a
a
+
t
f
(
x
)
d
x
=
lim
d
x
→
0
+
∑
i
=
1
⌊
t
/
d
x
⌋
−
1
f
(
a
+
i
d
x
)
d
x
=
F
(
t
)
;
t
>
0
{\displaystyle \int _{a}^{a+t}f(x)dx=\lim _{d_{x}\to 0^{+}}\sum _{i=1}^{\lfloor t/d_{x}\rfloor -1}f(a+id_{x})d_{x}=F(t);t>0}
∫
a
a
+
t
f
′
(
x
)
d
x
?
?
?
{\displaystyle \int _{a}^{a+t}f'(x)dx???}
∫
a
a
+
t
f
′
(
x
)
d
x
=
f
(
a
+
t
)
−
f
(
a
)
{\displaystyle \int _{a}^{a+t}f'(x)dx=f(a+t)-f(a)}
d
(
∫
a
a
+
t
f
(
x
)
d
x
)
d
t
=
d
(
F
(
a
+
t
)
−
F
(
a
)
)
d
t
=
d
F
(
a
+
t
)
d
t
−
d
F
(
a
)
d
t
=
f
(
a
+
t
)
−
0
{\displaystyle {\frac {d(\int _{a}^{a+t}f(x)dx)}{dt}}={\frac {d(F(a+t)-F(a))}{dt}}={\frac {dF(a+t)}{dt}}-{\frac {dF(a)}{dt}}=f(a+t)-0}
d
F
(
t
)
d
t
=
lim
d
t
→
0
F
(
t
+
d
t
)
−
F
(
t
)
d
t
=
lim
d
t
→
0
lim
d
x
→
0
+
∑
i
=
1
⌊
(
t
+
d
t
)
/
d
x
⌋
−
1
f
(
a
+
i
d
x
)
d
x
−
lim
d
x
→
0
+
∑
i
=
1
⌊
t
/
d
x
⌋
−
1
f
(
a
+
i
d
x
)
d
x
d
t
;
t
>
0
{\displaystyle {\frac {dF(t)}{dt}}=\lim _{d_{t}\to 0}{\frac {F(t+d_{t})-F(t)}{d_{t}}}=\lim _{d_{t}\to 0}{\frac {\lim _{d_{x}\to 0^{+}}\sum _{i=1}^{\lfloor (t+d_{t})/d_{x}\rfloor -1}f(a+id_{x})d_{x}-\lim _{d_{x}\to 0^{+}}\sum _{i=1}^{\lfloor t/d_{x}\rfloor -1}f(a+id_{x})d_{x}}{d_{t}}};t>0}
∀
d
t
(
0
<
|
d
t
−
0
|
<
t
⟹
t
+
d
t
>
0
)
;
t
>
0
{\displaystyle \forall d_{t}(0<|d_{t}-0|<t\implies t+d_{t}>0);t>0}
d
F
(
t
)
d
t
=
d
(
∫
a
a
+
t
f
(
x
)
d
x
)
d
t
{\displaystyle {\frac {dF(t)}{dt}}={\frac {d(\int _{a}^{a+t}f(x)dx)}{dt}}}
d
F
(
t
)
d
t
=
lim
d
t
→
0
lim
d
x
→
0
+
(
∑
i
=
1
⌊
(
t
+
d
t
)
/
d
x
⌋
−
1
f
(
a
+
i
d
x
)
d
x
−
∑
i
=
1
⌊
t
/
d
x
⌋
−
1
f
(
a
+
i
d
x
)
d
x
)
d
t
{\displaystyle {\frac {dF(t)}{dt}}=\lim _{d_{t}\to 0}{\frac {\lim _{d_{x}\to 0^{+}}\left(\sum _{i=1}^{\lfloor (t+d_{t})/d_{x}\rfloor -1}f(a+id_{x})d_{x}-\sum _{i=1}^{\lfloor t/d_{x}\rfloor -1}f(a+id_{x})d_{x}\right)}{d_{t}}}}
∑
i
=
1
n
+
m
f
(
i
)
=
∑
i
=
1
n
f
(
i
)
+
∑
i
=
n
+
1
n
+
m
f
(
i
)
{\displaystyle \sum _{i=1}^{n+m}f(i)=\sum _{i=1}^{n}f(i)+\sum _{i=n+1}^{n+m}f(i)}
F
(
t
)
=
lim
d
x
→
0
+
∑
i
=
1
⌊
t
/
d
x
⌋
−
1
f
(
a
+
i
d
x
)
d
x
=
lim
d
x
→
0
+
∑
i
=
1
⌊
t
/
min
(
d
x
,
0
+
t
/
2
)
⌋
−
1
f
(
a
+
i
d
x
)
d
x
;
t
/
2
>
0
{\displaystyle F(t)=\lim _{d_{x}\to 0^{+}}\sum _{i=1}^{\lfloor t/d_{x}\rfloor -1}f(a+id_{x})d_{x}=\lim _{d_{x}\to 0^{+}}\sum _{i=1}^{\lfloor t/\min(d_{x},0+t/2)\rfloor -1}f(a+id_{x})d_{x};t/2>0}
lim
x
→
c
+
f
(
x
,
x
)
=
L
=
lim
x
→
c
+
f
(
min
(
x
,
c
+
k
)
,
x
)
;
k
>
0
{\displaystyle \lim _{x\to c^{+}}f(x,x)=L=\lim _{x\to c^{+}}f(\min(x,c+k),x);k>0}
paradox
http://m.facebook.com/story.php?story_fbid=4357574176677&id=1207419880&comment_id=4544749&_rdr
"ประโยคที่ผมกำลังพูดอยู่นี้เป็นเท็จ"
"ประโยค a เป็นเท็จ" and ประโยค a == "ประโยค a เป็นเท็จ"
conclusion: [ประโยค a == "ประโยค a เป็นเท็จ"] เป็นเท็จ
"ประโยคที่ผมกำลังพูดอยู่นี้เป็นเท็จ" <==> "ประโยค a เป็นเท็จ" and ประโยค a == "ประโยค a เป็นเท็จ" ???
not "ประโยคที่ผมกำลังพูดอยู่นี้เป็นเท็จ" <==> not "ประโยค a เป็นเท็จ" or not ประโยค a == "ประโยค a เป็นเท็จ" ???
not "ประโยคที่ผมกำลังพูดอยู่นี้เป็นเท็จ" <==> "ประโยค a เป็นจริง" or ประโยค a != "ประโยค a เป็นเท็จ" ???
a
=
b
⟺
c
=
a
∧
c
=
b
{\displaystyle a=b\iff c=a\land c=b}
∃
c
c
=
a
∧
c
=
b
{\displaystyle \exists c\ c=a\land c=b}
Ans 13:42, 16 June 2017 (UTC))
c
=
a
∧
c
=
b
⟹
a
=
b
{\displaystyle c=a\land c=b\implies a=b}
a
=
b
⟹
[
c
=
a
⟺
c
=
b
]
{\displaystyle a=b\implies [c=a\iff c=b]}
[
c
=
a
⟺
c
=
b
]
⟹
a
=
b
{\displaystyle [c=a\iff c=b]\implies a=b}
"ประโยคที่ผมกำลังพูดอยู่นี้เป็นเท็จ" <== "ประโยค a เป็นเท็จ" and ประโยค a == "ประโยค a เป็นเท็จ"
not "ประโยคที่ผมกำลังพูดอยู่นี้เป็นเท็จ" ==> not "ประโยค a เป็นเท็จ" or not ประโยค a == "ประโยค a เป็นเท็จ"
not "ประโยคที่ผมกำลังพูดอยู่นี้เป็นเท็จ" ==> "ประโยค a เป็นจริง" or ประโยค a != "ประโยค a เป็นเท็จ" ???
all a ["ประโยคที่ผมกำลังพูดอยู่นี้เป็นเท็จ" <== "ประโยค a เป็นเท็จ" and ประโยค a == "ประโยค a เป็นเท็จ"]
all a [not "ประโยคที่ผมกำลังพูดอยู่นี้เป็นเท็จ" ==> not "ประโยค a เป็นเท็จ" or not ประโยค a == "ประโยค a เป็นเท็จ"]
all a [not "ประโยคที่ผมกำลังพูดอยู่นี้เป็นเท็จ" ==> "ประโยค a เป็นจริง" or ประโยค a != "ประโยค a เป็นเท็จ" ???]
a = !a, ถามว่า a เป็น T (true) หรือ F (false)?
ตอบ a ไม่สามารถเป็นได้ทั้ง T หรือ F
จึงสรุปว่า "a = !a" เป็นเท็จ, เมื่อมันเป็นเท็จ นั่นก็หมายความว่า "a != !a"?
ถ้ากำหนดให้, ประโยค a == "ประโยค a เป็นเท็จ", ถามว่า ประโยคที่ว่า "ประโยค a เป็นเท็จ" เป็นจริงหรือเท็จ?
"ประโยค a เป็นเท็จ" ไม่สามารถเป็นได้ทั้ง จริง หรือ เท็จ
ก็เหมือนกับคำถามว่า กำหนดให้ a == !a ถามว่า a เป็นจริงหรือเท็จหละ? คำตอบก็คือไม่สามารถเป็นได้ทั้งจริงและเท็จ นั่นก็คือไม่มีคำตอบ, หรือ ไม่มีค่า a ที่ทำให้ a == !a เป็นจริง, ซึ่งก็หมายความว่า a == !a ไม่มีทางเป็นจริง. เมื่อ a == !a ไม่มีทางเป็นจริง ก็ต้องกลับไปบอกว่า มันผิดตั้งแต่ตอนที่กำหนดให้ a == !a แล้ว, คือผิดตั้งแต่ตั้งคำถามแล้ว.
ด้วยตรรกะแบบเดียวกัน จึงไม่มีทางที่จะมี ประโยค a ที่ว่า ประโยค a == "ประโยค a เป็นเท็จ", นั่นก็หมายความว่า มันผิดตั้งแต่ตอนกำหนดให้ ประโยค a == "ประโยค a เป็นเท็จ" แล้ว.
"ประโยค a == ประโยคที่จะพูดถัดจากนี้". "ประโยค a เป็นเท็จ"
"ประโยคที่ผมกำลังพูดอยู่นี้เป็นเท็จ", ถามว่าประโยคข้างหน้านี้เป็นจริงหรือเท็จ?
สมมุติว่ามันเป็นจริง, ถ้ามันเป็นจริง ถ้างั้นก็หมายความว่ามันเป็นเท็จนะสิ, ก็ในเมื่อเชื่อว่ามันเป็นจริง ถ้าเชื่อมัน ก็มันบอกว่ามันเองเป็นเท็จก็ต้องเชื่อมัน ดังนั้นก็ต้องเชื่อตามมันว่ามันเป็นเท็จสิ. ซึ่งขัดแย้งกันจึงสรุปได้ว่าเป็นความเชื่อที่ผิดตั้งแต่ต้น เป็น assumption ที่ผิด จึงเป็นไปไม่ได้ที่มันจะเป็นจริง. (จริงๆ ตรงที่เชื่อตามมันว่ามันเป็นเท็จ ถ้าเชื่อว่ามันเป็นเท็จ ก็แสดงว่าจริงๆ แล้วไม่ได้เชื่อมันนะสิ, ขัดแย้งกันอีกละ ตกลงว่าจะเชื่อหรือไม่เชื่อมันกันแน่)
ถ้าเป็นไปไม่ได้ที่มันจะเป็นจริง ถ้างั้นก็หมายความว่ามันเป็นเท็จนะสิ. ถ้ามันเป็นเท็จ ก็ต้องไม่เชื่อมันใช่มั้ย, ในเมื่อไม่เชื่อมัน ดังนั้นที่มันบอกว่ามันเป็นเท็จก็ต้องไม่เชื่อมัน, เมื่อไม่เชื่อที่มันบอกว่ามันเป็นเท็จ ถ้างั้นมันก็ต้องเป็นจริงนะสิ. อ้าวขัดแย้งกับ assumption อีกละ ก็เป็นไปไม่ได้อีกเหมือนกันที่มันจะเป็นเท็จ.
อ้าว จริงก็ไม่ใช่ เท็จก็ไม่ใช่ แล้วตกลงค่าความจริงของมันเป็นอะไรหละ? ถ้างั้นสรุปได้ไหมว่า มันไม่ใช่ทั้งจริงและเท็จ? จะสรุปอย่างนั้นมันก็แปลกๆ อยู่นา ประโยคที่พูดมาถ้ามันไม่จริง มันก็ต้องเท็จ ถ้ามันไม่เท็จ มันก็ต้องจริง มันเป็นได้แค่สองอย่างนี้เท่านั้น, มันจะเป็นอย่างอื่นนอกเหนือจากนี้ได้ยังไง? ถ้ามันไม่ใช่ทั้งจริงและเท็จ แล้วมันจะหมายความว่ายังไงหละ มันเป็นสถานะที่แปลกๆ อยู่นา.
ยังบอกไม่ได้ว่าจริงหรือเท็จ เนื่องจากประโยคติดตัวแปร หรือเรียกตัวเอง (recursive) แบบไม่สิ้นสุด?
f
(
a
)
⟺
∀
x
∈
{
a
}
f
(
x
)
⟺
∀
x
(
x
=
a
⟹
f
(
x
)
)
⟺
∃
x
(
x
=
a
∧
f
(
x
)
)
{\displaystyle f(a)\iff \forall x\in \{a\}f(x)\iff \forall x(x=a\implies f(x))\iff \exists x(x=a\land f(x))}
f
(
a
(
x
)
)
⟺
∀
x
∈
{
x
|
x
=
a
(
x
)
}
f
(
x
)
⟺
∀
x
(
x
=
a
(
x
)
⟹
f
(
x
)
)
⟺
∃
x
(
x
=
a
(
x
)
∧
f
(
x
)
)
{\displaystyle f(a(x)){\cancel {\iff }}\forall x\in \{x|x=a(x)\}f(x)\iff \forall x(x=a(x)\implies f(x)){\cancel {\iff }}\exists x(x=a(x)\land f(x))}
Given that f(x) is a boolean function,
g
(
x
)
∈
R
⟹
f
(
g
(
x
)
)
{\displaystyle g(x)\in \mathbb {R} \implies f(g(x))}
x
∈
R
⟹
f
(
x
)
{\displaystyle x\in \mathbb {R} \implies f(x)}
Is #1 equivalent to #2?
∀
x
∈
A
f
(
x
)
{\displaystyle \forall x\in \mathbb {A} \ f(x)}
f
(
x
1
)
∧
f
(
x
2
)
∧
f
(
x
3
)
∧
⋯
∧
f
(
x
n
)
{\displaystyle f(x_{1})\land f(x_{2})\land f(x_{3})\land \dots \land f(x_{n})}
x
∈
A
⟹
f
(
x
)
{\displaystyle x\in \mathbb {A} \implies f(x)}
∀
x
∈
A
f
(
x
)
{\displaystyle \forall x\in \mathbb {A} \ f(x)}
⟺
{\displaystyle \iff }
x
∈
A
⟹
f
(
x
)
{\displaystyle x\in \mathbb {A} \implies f(x)}
∀
x
∈
A
f
(
x
)
{\displaystyle \forall x\in \mathbb {A} \ f(x)}
⟺
{\displaystyle \iff }
x
∈
A
⟹
f
(
x
)
{\displaystyle x\in \mathbb {A} \implies f(x)}
∃
x
∈
A
f
(
x
)
{\displaystyle \exists x\in \mathbb {A} \ f(x)}
¬
¬
(
∃
x
∈
A
f
(
x
)
)
{\displaystyle \neg \neg (\ \exists x\in \mathbb {A} \ f(x)\ )}
¬
(
∀
x
∈
A
¬
f
(
x
)
)
{\displaystyle \neg (\ \forall x\in \mathbb {A} \ \neg f(x)\ )}
¬
(
x
∈
A
⟹
¬
f
(
x
)
)
{\displaystyle \neg (\ x\in \mathbb {A} \implies \neg f(x)\ )}
¬
(
x
∉
A
∨
¬
f
(
x
)
)
{\displaystyle \neg (\ x\notin \mathbb {A} \lor \neg f(x)\ )}
x
∈
A
∧
f
(
x
)
{\displaystyle x\in \mathbb {A} \land f(x)}
x
∈
A
⟹
¬
f
(
x
)
{\displaystyle x\in \mathbb {A} \implies \neg f(x)}
x
∉
A
∨
¬
f
(
x
)
{\displaystyle x\notin \mathbb {A} \lor \neg f(x)}
¬
¬
(
x
∉
A
∨
¬
f
(
x
)
)
{\displaystyle \neg \neg (\ x\notin \mathbb {A} \lor \neg f(x)\ )}
¬
(
x
∈
A
∧
f
(
x
)
)
{\displaystyle \neg (\ x\in \mathbb {A} \land f(x)\ )}
x
∈
A
⟹
f
(
x
)
{\displaystyle x\in \mathbb {A} \implies f(x)}
x
∉
A
∨
f
(
x
)
{\displaystyle x\notin \mathbb {A} \lor f(x)}
¬
¬
(
x
∉
A
∨
f
(
x
)
)
{\displaystyle \neg \neg (\ x\notin \mathbb {A} \lor f(x)\ )}
¬
(
x
∈
A
∧
¬
f
(
x
)
)
{\displaystyle \neg (\ x\in \mathbb {A} \land \neg f(x)\ )}
¬
(
∃
x
∈
A
f
(
x
)
)
{\displaystyle \neg (\ \exists x\in \mathbb {A} \ f(x)\ )}
∀
x
∈
A
¬
f
(
x
)
{\displaystyle \forall x\in \mathbb {A} \ \neg f(x)}
x
∈
A
⟹
¬
f
(
x
)
{\displaystyle x\in \mathbb {A} \implies \neg f(x)}
x
∉
A
∨
¬
f
(
x
)
{\displaystyle x\notin \mathbb {A} \lor \neg f(x)}
¬
(
x
∈
A
∧
f
(
x
)
)
{\displaystyle \neg (\ x\in \mathbb {A} \land f(x)\ )}
∃
x
∈
A
f
(
x
)
{\displaystyle \exists x\in \mathbb {A} \ f(x)}
¬
¬
(
∃
x
∈
A
f
(
x
)
)
{\displaystyle \neg \neg (\ \exists x\in \mathbb {A} \ f(x)\ )}
¬
(
∀
x
∈
A
¬
f
(
x
)
)
{\displaystyle \neg (\ \forall x\in \mathbb {A} \ \neg f(x)\ )}
¬
(
x
∈
A
⟹
¬
f
(
x
)
;
f
o
r
a
n
y
x
)
{\displaystyle \neg (\ x\in \mathbb {A} \implies \neg f(x);\ for\ any\ x\ )}
¬
(
x
∉
A
∨
¬
f
(
x
)
;
f
o
r
a
n
y
x
)
{\displaystyle \neg (\ x\notin \mathbb {A} \lor \neg f(x);\ for\ any\ x\ )}
¬
(
x
∉
A
∨
¬
f
(
x
)
)
{\displaystyle \neg (\ x\notin \mathbb {A} \lor \neg f(x)\ )}
x
∈
A
∧
f
(
x
)
{\displaystyle x\in \mathbb {A} \land f(x)}
∀
x
∈
R
⟹
2
x
∈
R
{\displaystyle \forall x\in \mathbb {R} \implies 2x\in \mathbb {R} }
(
∀
x
∈
R
⟹
f
(
x
)
)
⟹
(
∀
x
∈
R
⟹
f
(
2
x
)
)
{\displaystyle (\ \forall x\in \mathbb {R} \implies f(x)\ )\implies (\ \forall x\in \mathbb {R} \implies f(2x)\ )}
^^^ need
∀
{\displaystyle \forall }
x
∈
R
⟹
2
x
∈
R
{\displaystyle x\in \mathbb {R} \implies 2x\in \mathbb {R} }
(
x
∈
R
⟹
f
(
x
)
)
⟹
(
x
∈
R
⟹
f
(
2
x
)
)
{\displaystyle (\ x\in \mathbb {R} \implies f(x)\ )\implies (\ x\in \mathbb {R} \implies f(2x)\ )}
[
[
a
]
b
]
[
(
a
)
b
]
[
(
(
a
)
)
b
]
(
f
)
(
f
′
)
(
f
2
)
(
f
′
2
)
{\displaystyle \left[\left[a\right]b\right]\left[(a)b\right]\left[\left((a)\right)b\right]\left(f\right)\left(f'\right)\left(f^{2}\right)\left(f'^{2}\right)}
s
→
(
t
)
=
[
a
cos
f
(
t
)
,
b
sin
f
(
t
)
]
{\displaystyle {\vec {s}}(t)=\left[a\cos f(t),b\sin f(t)\right]}
s
→
′
(
t
)
=
[
−
a
f
′
(
t
)
sin
f
(
t
)
,
b
f
′
(
t
)
cos
f
(
t
)
]
{\displaystyle {\vec {s}}\,'(t)=\left[-af'(t)\sin f(t),bf'(t)\cos f(t)\right]}
s
→
″
(
t
)
=
[
−
a
(
f
″
(
t
)
sin
f
(
t
)
+
f
′
2
(
t
)
cos
f
(
t
)
)
,
b
(
f
″
(
t
)
cos
f
(
t
)
−
f
′
2
(
t
)
sin
f
(
t
)
)
]
∝
s
→
(
t
)
+
[
k
,
0
]
{\displaystyle {\vec {s}}\,''(t)=\left[-a\left(f''(t)\sin f(t)+f'^{2}(t)\cos f(t)\right),b\left(f''(t)\cos f(t)-f'^{2}(t)\sin f(t)\right)\right]\propto {\vec {s}}(t)+[k,0]}
|
s
→
″
(
t
)
|
2
=
a
2
(
f
″
(
t
)
sin
f
(
t
)
+
f
′
2
(
t
)
cos
f
(
t
)
)
2
+
b
2
(
f
″
(
t
)
cos
f
(
t
)
−
f
′
2
(
t
)
sin
f
(
t
)
)
2
{\displaystyle \left|{\vec {s}}\,''(t)\right|^{2}=a^{2}\left(f''(t)\sin f(t)+f'^{2}(t)\cos f(t)\right)^{2}+b^{2}\left(f''(t)\cos f(t)-f'^{2}(t)\sin f(t)\right)^{2}}
|
s
→
″
(
t
)
|
2
=
f
″
2
(
t
)
(
a
2
sin
2
f
(
t
)
+
b
2
cos
2
f
(
t
)
)
+
f
′
4
(
t
)
(
a
2
cos
2
f
(
t
)
+
b
2
sin
2
f
(
t
)
)
+
2
f
″
(
t
)
f
′
2
(
t
)
sin
f
(
t
)
cos
f
(
t
)
(
a
2
−
b
2
)
{\displaystyle \left|{\vec {s}}\,''(t)\right|^{2}=f''^{2}(t)\left(a^{2}\sin ^{2}f(t)+b^{2}\cos ^{2}f(t)\right)+f'^{4}(t)\left(a^{2}\cos ^{2}f(t)+b^{2}\sin ^{2}f(t)\right)+2f''(t)f'^{2}(t)\sin f(t)\cos f(t)\left(a^{2}-b^{2}\right)}
|
s
→
″
(
t
)
|
2
=
f
″
2
(
t
)
(
a
2
+
(
b
2
−
a
2
)
cos
2
f
(
t
)
)
+
f
′
4
(
t
)
(
(
a
2
−
b
2
)
cos
2
f
(
t
)
+
b
2
)
+
f
″
(
t
)
f
′
2
(
t
)
sin
2
f
(
t
)
(
a
2
−
b
2
)
{\displaystyle \left|{\vec {s}}\,''(t)\right|^{2}=f''^{2}(t)\left(a^{2}+(b^{2}-a^{2})\cos ^{2}f(t)\right)+f'^{4}(t)\left((a^{2}-b^{2})\cos ^{2}f(t)+b^{2}\right)+f''(t)f'^{2}(t)\sin 2f(t)\left(a^{2}-b^{2}\right)}
a
cos
f
(
t
)
b
sin
f
(
t
)
=
−
a
(
f
″
(
t
)
sin
f
(
t
)
+
f
′
2
(
t
)
cos
f
(
t
)
)
b
(
f
″
(
t
)
cos
f
(
t
)
−
f
′
2
(
t
)
sin
f
(
t
)
)
{\displaystyle {\frac {a\cos f(t)}{b\sin f(t)}}={\frac {-a\left(f''(t)\sin f(t)+f'^{2}(t)\cos f(t)\right)}{b\left(f''(t)\cos f(t)-f'^{2}(t)\sin f(t)\right)}}}
a
cos
f
(
t
)
+
k
b
sin
f
(
t
)
=
−
a
(
f
″
(
t
)
sin
f
(
t
)
+
f
′
2
(
t
)
cos
f
(
t
)
)
b
(
f
″
(
t
)
cos
f
(
t
)
−
f
′
2
(
t
)
sin
f
(
t
)
)
{\displaystyle {\frac {a\cos f(t)+k}{b\sin f(t)}}={\frac {-a\left(f''(t)\sin f(t)+f'^{2}(t)\cos f(t)\right)}{b\left(f''(t)\cos f(t)-f'^{2}(t)\sin f(t)\right)}}}
a
cos
f
(
t
)
+
k
sin
f
(
t
)
=
−
a
(
f
″
(
t
)
sin
f
(
t
)
+
f
′
2
(
t
)
cos
f
(
t
)
)
(
f
″
(
t
)
cos
f
(
t
)
−
f
′
2
(
t
)
sin
f
(
t
)
)
{\displaystyle {\frac {a\cos f(t)+k}{\sin f(t)}}={\frac {-a\left(f''(t)\sin f(t)+f'^{2}(t)\cos f(t)\right)}{\left(f''(t)\cos f(t)-f'^{2}(t)\sin f(t)\right)}}}
a
(
f
″
(
t
)
cos
2
f
(
t
)
−
f
′
2
(
t
)
sin
f
(
t
)
cos
f
(
t
)
)
+
k
(
f
″
(
t
)
cos
f
(
t
)
−
f
′
2
(
t
)
sin
f
(
t
)
)
=
−
a
(
f
″
(
t
)
sin
2
f
(
t
)
+
f
′
2
(
t
)
sin
f
(
t
)
cos
f
(
t
)
)
{\displaystyle a\left(f''(t)\cos ^{2}f(t)-f'^{2}(t)\sin f(t)\cos f(t)\right)+k\left(f''(t)\cos f(t)-f'^{2}(t)\sin f(t)\right)=-a\left(f''(t)\sin ^{2}f(t)+f'^{2}(t)\sin f(t)\cos f(t)\right)}
a
f
″
(
t
)
(
cos
2
f
(
t
)
+
sin
2
f
(
t
)
)
+
k
(
f
″
(
t
)
cos
f
(
t
)
−
f
′
2
(
t
)
sin
f
(
t
)
)
=
0
{\displaystyle af''(t)\left(\cos ^{2}f(t)+\sin ^{2}f(t)\right)+k\left(f''(t)\cos f(t)-f'^{2}(t)\sin f(t)\right)=0}
a
f
″
(
t
)
+
k
f
″
(
t
)
cos
f
(
t
)
−
k
f
′
2
(
t
)
sin
f
(
t
)
=
0
{\displaystyle af''(t)+kf''(t)\cos f(t)-kf'^{2}(t)\sin f(t)=0}
(
a
+
k
cos
f
(
t
)
)
f
″
(
t
)
=
k
sin
f
(
t
)
f
′
2
(
t
)
{\displaystyle \left(a+k\cos f(t)\right)f''(t)=k\sin f(t)f'^{2}(t)}
f
″
(
t
)
=
k
sin
f
(
t
)
f
′
2
(
t
)
a
+
k
cos
f
(
t
)
{\displaystyle f''(t)={\frac {k\sin f(t)f'^{2}(t)}{a+k\cos f(t)}}}
f
″
(
t
)
f
′
2
(
t
)
=
d
f
′
(
t
)
f
′
2
(
t
)
d
t
=
k
sin
f
(
t
)
a
+
k
cos
f
(
t
)
{\displaystyle {\frac {f''(t)}{f'^{2}(t)}}={\frac {df'(t)}{f'^{2}(t)dt}}={\frac {k\sin f(t)}{a+k\cos f(t)}}}
−
d
1
/
f
′
(
t
)
d
t
=
k
sin
f
(
t
)
a
+
k
cos
f
(
t
)
{\displaystyle {\frac {-d1/f'(t)}{dt}}={\frac {k\sin f(t)}{a+k\cos f(t)}}}
f
″
(
t
)
=
k
sin
f
(
t
)
d
f
(
t
)
d
t
f
′
(
t
)
a
+
k
cos
f
(
t
)
=
−
k
d
cos
f
(
t
)
d
t
f
′
(
t
)
a
+
k
cos
f
(
t
)
=
−
d
(
a
+
k
cos
f
(
t
)
)
d
t
f
′
(
t
)
a
+
k
cos
f
(
t
)
{\displaystyle f''(t)={\frac {k\sin f(t){\frac {df(t)}{dt}}f'(t)}{a+k\cos f(t)}}={\frac {-k{\frac {d\cos f(t)}{dt}}f'(t)}{a+k\cos f(t)}}={\frac {-{\frac {d(a+k\cos f(t))}{dt}}f'(t)}{a+k\cos f(t)}}}
f
″
(
t
)
(
a
+
k
cos
f
(
t
)
)
=
k
sin
f
(
t
)
d
f
(
t
)
d
t
f
′
(
t
)
=
−
k
d
cos
f
(
t
)
d
t
f
′
(
t
)
=
−
d
(
a
+
k
cos
f
(
t
)
)
d
t
f
′
(
t
)
{\displaystyle f''(t)(a+k\cos f(t))=k\sin f(t){\frac {df(t)}{dt}}f'(t)=-k{\frac {d\cos f(t)}{dt}}f'(t)=-{\frac {d(a+k\cos f(t))}{dt}}f'(t)}
f
″
(
t
)
=
d
f
′
(
t
)
d
t
=
−
d
ln
|
a
+
k
cos
f
(
t
)
|
d
t
f
′
(
t
)
{\displaystyle f''(t)={\frac {df'(t)}{dt}}={\frac {-d\ln |a+k\cos f(t)|}{dt}}f'(t)}
d
ln
|
f
′
(
t
)
|
d
t
=
−
d
ln
|
a
+
k
cos
f
(
t
)
|
d
t
{\displaystyle {\frac {d\ln |f'(t)|}{dt}}={\frac {-d\ln |a+k\cos f(t)|}{dt}}}
d
ln
|
f
′
(
t
)
|
d
t
+
d
ln
|
a
+
k
cos
f
(
t
)
|
d
t
=
0
{\displaystyle {\frac {d\ln |f'(t)|}{dt}}+{\frac {d\ln |a+k\cos f(t)|}{dt}}=0}
d
(
ln
|
f
′
(
t
)
|
+
ln
|
a
+
k
cos
f
(
t
)
|
)
d
t
=
0
{\displaystyle {\frac {d\left(\ln |f'(t)|+\ln |a+k\cos f(t)|\right)}{dt}}=0}
ln
|
f
′
(
t
)
|
+
ln
|
a
+
k
cos
f
(
t
)
|
=
c
{\displaystyle \ln |f'(t)|+\ln |a+k\cos f(t)|=c}
e
ln
|
f
′
(
t
)
|
+
ln
|
a
+
k
cos
f
(
t
)
|
=
e
c
{\displaystyle e^{\ln |f'(t)|+\ln |a+k\cos f(t)|}=e^{c}}
|
f
′
(
t
)
|
⋅
|
a
+
k
cos
f
(
t
)
|
=
e
c
{\displaystyle |f'(t)|\cdot |a+k\cos f(t)|=e^{c}}
|
f
′
(
t
)
(
a
+
k
cos
f
(
t
)
)
|
=
e
c
{\displaystyle |f'(t)\left(a+k\cos f(t)\right)|=e^{c}}
|
d
f
(
t
)
d
t
(
a
+
k
cos
f
(
t
)
)
|
=
e
c
{\displaystyle \left|{\frac {df(t)}{dt}}\left(a+k\cos f(t)\right)\right|=e^{c}}
|
k
sin
f
(
t
)
d
f
(
t
)
d
t
(
a
+
k
cos
f
(
t
)
)
|
=
|
k
sin
f
(
t
)
|
e
c
{\displaystyle \left|k\sin f(t){\frac {df(t)}{dt}}\left(a+k\cos f(t)\right)\right|=|k\sin f(t)|e^{c}}
|
−
d
(
a
+
k
cos
f
(
t
)
)
d
t
(
a
+
k
cos
f
(
t
)
)
|
=
|
k
sin
f
(
t
)
|
e
c
{\displaystyle \left|-{\frac {d(a+k\cos f(t))}{dt}}\left(a+k\cos f(t)\right)\right|=|k\sin f(t)|e^{c}}
|
d
(
a
+
k
cos
f
(
t
)
)
2
d
t
|
=
2
|
k
sin
f
(
t
)
|
e
c
{\displaystyle \left|{\frac {d(a+k\cos f(t))^{2}}{dt}}\right|=2|k\sin f(t)|e^{c}}
|
d
(
a
f
(
t
)
+
k
sin
f
(
t
)
)
d
t
|
=
e
c
=
e
c
d
t
d
t
=
d
e
c
t
d
t
=
d
(
a
f
(
t
)
+
k
sin
f
(
t
)
)
d
t
abs
′
d
(
a
f
(
t
)
+
k
sin
f
(
t
)
)
d
t
{\displaystyle \left|{\frac {d\left(af(t)+k\sin f(t)\right)}{dt}}\right|=e^{c}=e^{c}{\frac {dt}{dt}}={\frac {de^{c}t}{dt}}={\frac {d\left(af(t)+k\sin f(t)\right)}{dt}}{\text{abs}}'{\frac {d\left(af(t)+k\sin f(t)\right)}{dt}}}
f
′
(
x
)
abs
′
f
(
x
)
=
g
′
(
x
)
abs
′
g
(
x
)
{\displaystyle f'(x){\text{abs}}'f(x)=g'(x){\text{abs}}'g(x)}
f
′
(
x
)
d
|
f
(
x
)
|
/
d
f
(
x
)
=
f
′
(
x
)
|
f
(
x
)
|
/
f
(
x
)
=
f
′
(
x
)
d
|
f
(
x
)
|
/
d
f
(
x
)
d
|
x
|
/
d
x
|
x
|
/
x
=
f
′
(
x
)
d
|
f
(
x
)
|
/
d
|
x
|
f
′
(
x
)
|
x
|
/
x
=
d
|
f
(
x
)
|
d
|
x
|
|
x
|
/
x
{\displaystyle f'(x)d|f(x)|/df(x)=f'(x)|f(x)|/f(x)=f'(x){\frac {d|f(x)|/df(x)}{d|x|/dx}}|x|/x=f'(x){\frac {d|f(x)|/d|x|}{f'(x)}}|x|/x={\frac {d|f(x)|}{d|x|}}|x|/x}
d
|
f
(
x
)
|
d
|
x
|
|
x
|
/
x
=
d
f
(
x
)
|
f
(
x
)
|
/
f
(
x
)
d
x
|
x
|
/
x
|
x
|
/
x
=
|
f
(
x
)
|
/
f
(
x
)
|
x
|
/
x
d
f
(
x
)
d
x
|
x
|
/
x
=
d
|
f
(
x
)
|
/
d
f
(
x
)
d
|
x
|
/
d
x
d
f
(
x
)
d
x
⋅
|
x
|
/
x
=
d
|
f
(
x
)
|
/
d
|
x
|
d
f
(
x
)
/
d
x
f
′
(
x
)
|
x
|
/
x
{\displaystyle {\frac {d|f(x)|}{d|x|}}|x|/x={\frac {df(x)|f(x)|/f(x)}{dx|x|/x}}|x|/x={\frac {|f(x)|/f(x)}{|x|/x}}{\frac {df(x)}{dx}}|x|/x={\frac {d|f(x)|/df(x)}{d|x|/dx}}{\frac {df(x)}{dx}}\cdot |x|/x={\frac {d|f(x)|/d|x|}{df(x)/dx}}f'(x)|x|/x}
abs
′
f
(
x
)
d
f
(
x
)
=
abs
′
g
(
x
)
d
g
(
x
)
{\displaystyle {\text{abs}}'f(x)df(x)={\text{abs}}'g(x)dg(x)}
d
|
f
(
x
)
|
=
d
|
g
(
x
)
|
{\displaystyle d|f(x)|=d|g(x)|}
d
x
|
x
|
/
d
x
=
|
x
|
d
x
/
d
x
+
x
d
|
x
|
/
d
x
=
|
x
|
+
|
x
|
=
2
|
x
|
{\displaystyle dx|x|/dx=|x|dx/dx+xd|x|/dx=|x|+|x|=2|x|}
(
0
+
d
x
)
|
0
+
d
x
|
−
0
|
0
|
d
x
=
d
x
|
d
x
|
/
d
x
=
|
d
x
|
=>
0
{\displaystyle {\frac {(0+dx)|0+dx|-0|0|}{dx}}=dx|dx|/dx=|dx|=>0}
d
|
x
|
/
d
x
=
|
x
|
/
x
;
d
|
x
|
/
d
x
⋅
d
x
/
d
|
x
|
=
d
|
x
|
/
d
x
⋅
x
/
|
x
|
=
1
=
|
d
x
/
d
x
|
{\displaystyle d|x|/dx=|x|/x;d|x|/dx\cdot dx/d|x|=d|x|/dx\cdot x/|x|=1=|dx/dx|}
d
|
f
(
x
)
|
/
d
x
=
d
|
f
(
x
)
|
/
d
|
x
|
⋅
d
|
x
|
/
d
x
{\displaystyle d|f(x)|/dx=d|f(x)|/d|x|\cdot d|x|/dx}
f
(
x
)
|
f
(
x
)
|
=
g
(
x
)
|
g
(
x
)
|
{\displaystyle f(x)|f(x)|=g(x)|g(x)|}
f
′
(
x
)
2
|
f
(
x
)
|
=
g
′
(
x
)
2
|
g
(
x
)
|
{\displaystyle f'(x)2|f(x)|=g'(x)2|g(x)|}
|
f
(
x
)
|
d
f
(
x
)
=
|
g
(
x
)
|
d
g
(
x
)
{\displaystyle |f(x)|df(x)=|g(x)|dg(x)}
|
f
′
(
x
)
|
=
|
g
′
(
x
)
|
=
f
′
(
x
)
|
f
′
(
x
)
|
/
f
′
(
x
)
?
?
?
=
f
′
(
x
)
d
|
f
′
(
x
)
|
/
d
f
′
(
x
)
=
f
′
(
x
)
|
d
f
(
x
)
/
d
x
|
d
f
(
x
)
/
d
x
{\displaystyle |f'(x)|=|g'(x)|=f'(x)|f'(x)|/f'(x)???=f'(x)d|f'(x)|/df'(x)={\frac {f'(x)|df(x)/dx|}{df(x)/dx}}}
|
d
f
(
x
)
/
d
t
|
=
|
d
g
(
x
)
/
d
t
|
{\displaystyle |df(x)/dt|=|dg(x)/dt|}
a
f
(
t
)
+
k
sin
f
(
t
)
=
±
e
c
t
+
c
2
=
c
1
t
+
c
2
{\displaystyle af(t)+k\sin f(t)=\pm e^{c}t+c_{2}=c_{1}t+c_{2}}
f
′
(
t
)
(
a
+
k
cos
f
(
t
)
)
=
±
e
c
=
c
1
{\displaystyle f'(t)(a+k\cos f(t))=\pm e^{c}=c_{1}}
f
″
(
t
)
(
a
+
k
cos
f
(
t
)
)
−
f
′
2
(
t
)
k
sin
f
(
t
)
=
0
{\displaystyle f''(t)(a+k\cos f(t))-f'^{2}(t)k\sin f(t)=0}
f
″
(
t
)
(
a
+
k
cos
f
(
t
)
)
=
f
′
2
(
t
)
k
sin
f
(
t
)
{\displaystyle f''(t)(a+k\cos f(t))=f'^{2}(t)k\sin f(t)}
f
″
(
t
)
(
a
+
k
cos
f
(
t
)
)
3
=
f
′
2
(
t
)
(
a
+
k
cos
f
(
t
)
)
2
k
sin
f
(
t
)
{\displaystyle f''(t)(a+k\cos f(t))^{3}=f'^{2}(t)(a+k\cos f(t))^{2}k\sin f(t)}
f
″
(
t
)
(
a
+
k
cos
f
(
t
)
)
3
=
c
1
2
k
sin
f
(
t
)
{\displaystyle f''(t)(a+k\cos f(t))^{3}=c_{1}^{2}k\sin f(t)}
s
→
′
(
t
)
(
a
+
k
cos
f
(
t
)
)
=
c
1
[
−
a
sin
f
(
t
)
,
b
cos
f
(
t
)
]
{\displaystyle {\vec {s}}\,'(t)(a+k\cos f(t))=c_{1}\left[-a\sin f(t),b\cos f(t)\right]}
s
→
″
(
t
)
(
a
+
k
cos
f
(
t
)
)
3
=
c
1
2
[
−
a
(
k
sin
2
f
(
t
)
+
(
a
+
k
cos
f
(
t
)
)
cos
f
(
t
)
)
,
b
(
k
sin
f
(
t
)
cos
f
(
t
)
−
(
a
+
k
cos
f
(
t
)
)
sin
f
(
t
)
)
]
{\displaystyle {\vec {s}}\,''(t)(a+k\cos f(t))^{3}=c_{1}^{2}\left[-a\left(k\sin ^{2}f(t)+(a+k\cos f(t))\cos f(t)\right),b\left(k\sin f(t)\cos f(t)-(a+k\cos f(t))\sin f(t)\right)\right]}
s
→
″
(
t
)
(
a
+
k
cos
f
(
t
)
)
3
=
c
1
2
[
−
a
(
k
+
a
cos
f
(
t
)
)
,
−
a
b
sin
f
(
t
)
]
{\displaystyle {\vec {s}}\,''(t)(a+k\cos f(t))^{3}=c_{1}^{2}\left[-a\left(k+a\cos f(t)\right),-ab\sin f(t)\right]}
s
→
″
(
t
)
(
a
+
k
cos
f
(
t
)
)
3
=
−
a
c
1
2
[
k
+
a
cos
f
(
t
)
,
b
sin
f
(
t
)
]
{\displaystyle {\vec {s}}\,''(t)(a+k\cos f(t))^{3}=-ac_{1}^{2}\left[k+a\cos f(t),b\sin f(t)\right]}
s
→
″
(
t
)
(
a
+
k
cos
f
(
t
)
)
3
=
−
a
c
1
2
(
s
→
(
t
)
+
[
k
,
0
]
)
{\displaystyle {\vec {s}}\,''(t)(a+k\cos f(t))^{3}=-ac_{1}^{2}({\vec {s}}(t)+[k,0])}
|
s
→
″
(
t
)
|
2
(
a
+
k
cos
f
(
t
)
)
6
=
(
a
c
1
2
)
2
|
s
→
(
t
)
+
[
k
,
0
]
|
2
=
a
2
c
1
4
R
2
{\displaystyle \left|{\vec {s}}\,''(t)\right|^{2}(a+k\cos f(t))^{6}=\left(ac_{1}^{2}\right)^{2}\left|{\vec {s}}(t)+[k,0]\right|^{2}=a^{2}c_{1}^{4}R^{2}}
s
→
(
t
)
+
[
k
,
0
]
=
[
a
cos
f
(
t
)
+
k
,
b
sin
f
(
t
)
]
{\displaystyle {\vec {s}}(t)+[k,0]=\left[a\cos f(t)+k,b\sin f(t)\right]}
R
2
=
|
s
→
(
t
)
+
[
k
,
0
]
|
2
=
(
a
cos
f
(
t
)
+
k
)
2
+
b
2
sin
2
f
(
t
)
=
k
2
+
2
a
k
cos
f
(
t
)
+
a
2
cos
2
f
(
t
)
+
b
2
sin
2
f
(
t
)
{\displaystyle R^{2}=\left|{\vec {s}}(t)+[k,0]\right|^{2}=(a\cos f(t)+k)^{2}+b^{2}\sin ^{2}f(t)=k^{2}+2ak\cos f(t)+a^{2}\cos ^{2}f(t)+b^{2}\sin ^{2}f(t)}
If k is focus point, then
k
2
=
a
2
−
b
2
{\displaystyle k^{2}=a^{2}-b^{2}}
R
2
=
k
2
+
2
a
k
cos
f
(
t
)
+
a
2
cos
2
f
(
t
)
+
(
a
2
−
k
2
)
sin
2
f
(
t
)
{\displaystyle R^{2}=k^{2}+2ak\cos f(t)+a^{2}\cos ^{2}f(t)+\left(a^{2}-k^{2}\right)\sin ^{2}f(t)}
R
2
=
k
2
(
1
−
sin
2
f
(
t
)
)
+
2
a
k
cos
f
(
t
)
+
a
2
=
k
2
cos
2
f
(
t
)
+
2
a
k
cos
f
(
t
)
+
a
2
=
(
a
+
k
cos
f
(
t
)
)
2
{\displaystyle R^{2}=k^{2}\left(1-\sin ^{2}f(t)\right)+2ak\cos f(t)+a^{2}=k^{2}\cos ^{2}f(t)+2ak\cos f(t)+a^{2}=\left(a+k\cos f(t)\right)^{2}}
|
s
→
″
(
t
)
|
2
R
6
=
a
2
c
1
4
R
2
{\displaystyle \left|{\vec {s}}\,''(t)\right|^{2}R^{6}=a^{2}c_{1}^{4}R^{2}}
|
s
→
″
(
t
)
|
=
a
c
1
2
R
2
{\displaystyle \left|{\vec {s}}\,''(t)\right|={\frac {ac_{1}^{2}}{R^{2}}}}
|
s
→
″
(
t
)
|
2
=
f
″
2
(
t
)
(
a
2
sin
2
f
(
t
)
+
(
a
2
−
k
2
)
cos
2
f
(
t
)
)
+
f
′
4
(
t
)
(
a
2
cos
2
f
(
t
)
+
(
a
2
−
k
2
)
sin
2
f
(
t
)
)
+
2
f
″
(
t
)
f
′
2
(
t
)
(
a
2
sin
f
(
t
)
cos
f
(
t
)
−
(
a
2
−
k
2
)
sin
f
(
t
)
cos
f
(
t
)
)
{\displaystyle \left|{\vec {s}}\,''(t)\right|^{2}=f''^{2}(t)\left(a^{2}\sin ^{2}f(t)+\left(a^{2}-k^{2}\right)\cos ^{2}f(t)\right)+f'^{4}(t)\left(a^{2}\cos ^{2}f(t)+\left(a^{2}-k^{2}\right)\sin ^{2}f(t)\right)+2f''(t)f'^{2}(t)\left(a^{2}\sin f(t)\cos f(t)-\left(a^{2}-k^{2}\right)\sin f(t)\cos f(t)\right)}
|
s
→
″
(
t
)
|
2
=
f
″
2
(
t
)
(
a
2
−
k
2
cos
2
f
(
t
)
)
+
f
′
4
(
t
)
(
a
2
−
k
2
sin
2
f
(
t
)
)
+
2
f
″
(
t
)
f
′
2
(
t
)
k
2
sin
f
(
t
)
cos
f
(
t
)
{\displaystyle \left|{\vec {s}}\,''(t)\right|^{2}=f''^{2}(t)\left(a^{2}-k^{2}\cos ^{2}f(t)\right)+f'^{4}(t)\left(a^{2}-k^{2}\sin ^{2}f(t)\right)+2f''(t)f'^{2}(t)k^{2}\sin f(t)\cos f(t)}
|
s
→
″
(
t
)
|
2
=
f
″
2
(
t
)
(
a
2
−
k
2
cos
2
f
(
t
)
)
+
f
′
4
(
t
)
(
k
2
cos
2
f
(
t
)
+
a
2
−
k
2
)
+
f
″
(
t
)
f
′
2
(
t
)
k
2
sin
2
f
(
t
)
{\displaystyle \left|{\vec {s}}\,''(t)\right|^{2}=f''^{2}(t)\left(a^{2}-k^{2}\cos ^{2}f(t)\right)+f'^{4}(t)\left(k^{2}\cos ^{2}f(t)+a^{2}-k^{2}\right)+f''(t)f'^{2}(t)k^{2}\sin 2f(t)}
R
4
=
a
4
+
4
a
3
k
cos
f
(
t
)
+
6
a
2
k
2
cos
2
f
(
t
)
+
4
a
k
3
cos
3
f
(
t
)
+
k
4
cos
4
f
(
t
)
{\displaystyle R^{4}=a^{4}+4a^{3}k\cos f(t)+6a^{2}k^{2}\cos ^{2}f(t)+4ak^{3}\cos ^{3}f(t)+k^{4}\cos ^{4}f(t)}
(
a
2
−
k
2
sin
2
f
(
t
)
)
R
4
=
a
6
+
4
a
5
k
cos
f
(
t
)
+
6
a
4
k
2
cos
2
f
(
t
)
+
4
a
3
k
3
cos
3
f
(
t
)
+
k
4
a
2
cos
4
f
(
t
)
−
(
a
4
k
2
sin
2
f
(
t
)
+
4
a
3
k
3
cos
f
(
t
)
sin
2
f
(
t
)
+
6
a
2
k
4
cos
2
f
(
t
)
sin
2
f
(
t
)
+
4
a
k
5
cos
3
f
(
t
)
sin
2
f
(
t
)
+
k
6
cos
4
f
(
t
)
sin
2
f
(
t
)
)
{\displaystyle \left(a^{2}-k^{2}\sin ^{2}f(t)\right)R^{4}=a^{6}+4a^{5}k\cos f(t)+6a^{4}k^{2}\cos ^{2}f(t)+4a^{3}k^{3}\cos ^{3}f(t)+k^{4}a^{2}\cos ^{4}f(t)-\left(a^{4}k^{2}\sin ^{2}f(t)+4a^{3}k^{3}\cos f(t)\sin ^{2}f(t)+6a^{2}k^{4}\cos ^{2}f(t)\sin ^{2}f(t)+4ak^{5}\cos ^{3}f(t)\sin ^{2}f(t)+k^{6}\cos ^{4}f(t)\sin ^{2}f(t)\right)}
a
2
R
4
=
a
6
+
4
a
5
k
cos
f
(
t
)
+
6
a
4
k
2
cos
2
f
(
t
)
+
4
a
3
k
3
cos
3
f
(
t
)
+
a
2
k
4
cos
4
f
(
t
)
{\displaystyle a^{2}R^{4}=a^{6}+4a^{5}k\cos f(t)+6a^{4}k^{2}\cos ^{2}f(t)+4a^{3}k^{3}\cos ^{3}f(t)+a^{2}k^{4}\cos ^{4}f(t)}
−
k
2
R
4
=
−
(
a
4
k
2
+
4
a
3
k
3
cos
f
(
t
)
+
6
a
2
k
4
cos
2
f
(
t
)
+
4
a
k
5
cos
3
f
(
t
)
+
k
6
cos
4
f
(
t
)
)
{\displaystyle -k^{2}R^{4}=-\left(a^{4}k^{2}+4a^{3}k^{3}\cos f(t)+6a^{2}k^{4}\cos ^{2}f(t)+4ak^{5}\cos ^{3}f(t)+k^{6}\cos ^{4}f(t)\right)}
k
2
cos
2
f
(
t
)
R
4
=
a
4
k
2
cos
2
f
(
t
)
+
4
a
3
k
3
cos
3
f
(
t
)
+
6
a
2
k
4
cos
4
f
(
t
)
+
4
a
k
5
cos
5
f
(
t
)
+
k
6
cos
6
f
(
t
)
{\displaystyle k^{2}\cos ^{2}f(t)R^{4}=a^{4}k^{2}\cos ^{2}f(t)+4a^{3}k^{3}\cos ^{3}f(t)+6a^{2}k^{4}\cos ^{4}f(t)+4ak^{5}\cos ^{5}f(t)+k^{6}\cos ^{6}f(t)}
(
a
6
−
a
4
k
2
)
+
(
4
a
5
k
−
4
a
3
k
3
)
cos
f
(
t
)
+
(
6
a
4
k
2
−
6
a
2
k
4
+
a
4
k
2
)
cos
2
f
(
t
)
+
(
4
a
3
k
3
−
4
a
k
5
+
4
a
3
k
3
)
cos
3
f
(
t
)
+
(
a
2
k
4
−
k
6
+
6
a
2
k
4
)
cos
4
f
(
t
)
+
4
a
k
5
cos
5
f
(
t
)
+
k
6
cos
6
f
(
t
)
{\displaystyle (a^{6}-a^{4}k^{2})+(4a^{5}k-4a^{3}k^{3})\cos f(t)+(6a^{4}k^{2}-6a^{2}k^{4}+a^{4}k^{2})\cos ^{2}f(t)+(4a^{3}k^{3}-4ak^{5}+4a^{3}k^{3})\cos ^{3}f(t)+(a^{2}k^{4}-k^{6}+6a^{2}k^{4})\cos ^{4}f(t)+4ak^{5}\cos ^{5}f(t)+k^{6}\cos ^{6}f(t)}
(
a
6
−
a
4
k
2
)
+
(
4
a
5
k
−
4
a
3
k
3
)
cos
f
(
t
)
+
(
7
a
4
k
2
−
6
a
2
k
4
)
cos
2
f
(
t
)
+
(
8
a
3
k
3
−
4
a
k
5
)
cos
3
f
(
t
)
+
(
7
a
2
k
4
−
k
6
)
cos
4
f
(
t
)
+
4
a
k
5
cos
5
f
(
t
)
+
k
6
cos
6
f
(
t
)
{\displaystyle (a^{6}-a^{4}k^{2})+(4a^{5}k-4a^{3}k^{3})\cos f(t)+(7a^{4}k^{2}-6a^{2}k^{4})\cos ^{2}f(t)+(8a^{3}k^{3}-4ak^{5})\cos ^{3}f(t)+(7a^{2}k^{4}-k^{6})\cos ^{4}f(t)+4ak^{5}\cos ^{5}f(t)+k^{6}\cos ^{6}f(t)}
f
′
(
t
)
f
(
t
)
=
c
⟺
d
f
2
(
t
)
d
t
=
2
c
⟺
f
2
(
t
)
=
2
c
t
+
c
2
{\displaystyle f'(t)f(t)=c\iff {\frac {df^{2}(t)}{dt}}=2c\iff f^{2}(t)=2ct+c_{2}}
f
′
(
t
)
f
(
t
)
=
0
⟺
d
f
2
(
t
)
d
t
=
0
⟺
f
2
(
t
)
=
c
2
{\displaystyle f'(t)f(t)=0\iff {\frac {df^{2}(t)}{dt}}=0\iff f^{2}(t)=c_{2}}
∀
t
f
′
(
t
)
f
(
t
)
=
0
⟺
?
?
?
∀
f
′
(
t
)
=
0
∨
∀
f
(
t
)
=
0
⟺
?
?
?
∀
f
(
t
)
=
c
∨
f
(
t
)
=
0
{\displaystyle \forall tf'(t)f(t)=0\iff ???\forall f'(t)=0\lor \forall f(t)=0\iff ???\forall f(t)=c\lor f(t)=0}
![{\displaystyle [a\implies a\lor b]\iff \neg a\lor a\lor b\iff T\lor b\iff T}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b740be08cdcf5f358aa9c9c4703f38358f43d585)
![{\displaystyle [a\land c\implies (a\lor b)\land c]\iff \neg (a\land c)\lor (a\lor b)\land c\iff \neg a\lor \neg c\lor (a\lor b)\land c\iff \neg a\lor \neg c\lor a\lor b\iff T\lor \neg c\lor b\iff T}](https://wikimedia.org/api/rest_v1/media/math/render/svg/16d2ca7d687c390b03e42a3570677bc0eb38c8e9)
![{\displaystyle [\forall x\ f(x)\implies \forall x(f(x)\lor g(x))]\iff \neg \forall x\ f(x)\lor \forall x(f(x)\lor g(x))\iff \exists x\ \neg f(x)\lor }](https://wikimedia.org/api/rest_v1/media/math/render/svg/60e5af8f1c23328c561f8c6c2a4a961788e42e2f)
![{\displaystyle T\iff [\neg a\land \neg c\implies (\neg a\lor \neg b)\land \neg c]\iff [\neg (a\lor c)\implies \neg (a\land b\lor c)]\iff [a\land b\lor c\implies a\lor c]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5b56035bd22849d5e7bfeaaa121c65339ac05d0a)
![{\displaystyle [a\land b\implies a]\iff \neg (a\land b)\lor a\iff \neg a\lor \neg b\lor a\iff T\lor \neg b\iff T}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f9e8c5f571ac4227229e554eb4f37258d80b0a0e)
![{\displaystyle [a\implies b]\implies [a\lor b\implies b\lor b\iff b]\land [b\implies a\lor b]\iff [b\iff a\lor b]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c38a39e94c37ef6a49da4ca300cc9733251c5adf)
![{\displaystyle [a\implies b]\implies [a\iff a\land a\implies a\land b]\land [a\land b\implies a]\iff [a\iff a\land b]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d7beaa4f25344edc03165b30884d01e2b693e7da)
![{\displaystyle [a\implies b]\implies [f(a)\iff f(a\land b)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/add293c191b7242ec88e239b609af781b1f8b02e)
![{\displaystyle f(a\land [a\implies b])\iff f(a\land [\neg a\lor b])\iff f(a\land \neg a\lor a\land b)\iff f(F\lor a\land b)\iff f(a\land b)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c9af1ff9c820b87e42d3bf498b873a996127343f)
![{\displaystyle [(a\implies b)\implies (a\land c\implies b)]\iff \neg (\neg a\lor b)\lor (\neg (a\land c)\lor b)\iff a\land \neg b\lor \neg a\lor \neg c\lor b\iff a\lor b\lor \neg a\lor \neg c\iff T\lor b\lor \neg c\iff T}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a1286cecb18fe466ece14f9f0c08a79b4cb97e07)
![{\displaystyle [a\implies b]\iff \neg a\lor b\implies \neg a\lor b\lor \neg c\iff \neg (a\land c)\lor b\iff [a\land c\implies b]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6ac1e48474369017f3e3457c45e3f8122341a4eb)
![{\displaystyle (a\implies b)\land (c\implies d)\iff (\neg a\lor b)\land (\neg c\lor d)\implies (\neg a\lor b\lor \neg c)\land (\neg c\lor d\lor \neg a)\iff (\neg (a\land c)\lor b)\land (\neg (a\land c)\lor d)\iff \neg (a\land c)\lor b\land d\iff [a\land c\implies b\land d]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f11f59d0ae9f4b2d230d7bbfc9a368d3f46cb6d0)
![{\displaystyle [a\land b\implies c]\iff \neg (a\land b)\lor c\iff \neg a\lor \neg b\lor c\iff [a\implies (b\implies c)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/98a782aff54ad55d6651c84b84a842c702f626e7)
![{\displaystyle [a\implies f(a)]\iff \neg a\lor f(\neg \neg a)\iff \neg a\lor f(\neg F)\iff [a\implies f(T)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dfe0b83d032ffe7dc8ca0c493524db393a6662be)
![{\displaystyle \forall x\ [x\in \mathbb {A} \implies f(x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8006f19af7dd3eac03cbeff2a3de206c11f80150)
![{\displaystyle \forall a\ [a\in \mathbb {A} \implies f(a)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/997224fb662af6de963f84e58bc1ef7c88834990)
![{\displaystyle [c\in \mathbb {A} \implies f(c)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8dbbb2ad0a13a255efef1bb4a9854458fa5b79c4)
![{\displaystyle [x\in \mathbb {A} \implies f(x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dca4af2b97fd6accc420505f2cc883214eb8d86d)
![{\displaystyle \forall a\in \mathbb {A} \ f(a)\lor \forall b\in \mathbb {B} \ f(b){\cancel {\iff }}[a\in \mathbb {A} \implies f(a)\lor b\in \mathbb {B} \implies f(b)]\iff \neg a\in \mathbb {A} \lor f(a)\lor \neg b\in \mathbb {B} \lor f(b)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8f88bd2fde45478d0676abc3c8e8b60189ed8a4d)
![{\displaystyle \forall a\in \mathbb {A} \ f(a)\lor \forall b\in \mathbb {B} \ f(b){\cancel {\iff }}\neg (a\in \mathbb {A} \land b\in \mathbb {B} )\lor f(a)\lor f(b)\iff [a\in \mathbb {A} \land b\in \mathbb {B} \implies f(a)\lor f(b)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/71bc72d0d57938f4a879f4ee818332078b34e037)
![{\displaystyle \forall x\in \mathbb {A} \ f(x\in \mathbb {A} )\iff \forall x\ [x\in \mathbb {A} \implies f(x\in \mathbb {A} )]\iff \forall x\ [x\in \mathbb {A} \implies f(T)]\iff \forall x\in \mathbb {A} \ f(T)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/71295139468dca35270682288d5f1e877abea7ef)
![{\displaystyle \forall x[f(x)\land g(x)]\iff \forall x\ f(x)\land \forall x\ g(x)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8fccac9bf25a2197a90d750bff101c2a62faa0d5)
![{\displaystyle \forall x\ f(x)\lor \forall x\ g(x)\implies \forall x\ [f(x)\lor g(x)]\lor \forall x\ [g(x)\lor f(x)]\iff \forall x[f(x)\lor g(x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a1ec6111b39be1375c674074fb63254ea725f383)
![{\displaystyle \neg \neg (\forall x\ f(x)\lor \forall x\ g(x))\implies \neg \neg \forall x[f(x)\lor g(x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0c9222861559e41d4026f92c0f280b73d4c06fc2)
![{\displaystyle \neg (\exists x\ \neg f(x)\land \exists x\ \neg g(x))\implies \neg \exists x[\neg f(x)\land \neg g(x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0cc6e65a81c0ce776ea86e7612c90b4e6cc34194)
![{\displaystyle \neg (\exists x\ f(x)\land \exists x\ g(x))\implies \neg \exists x[f(x)\land g(x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/17476d77621b1b06ccddf5d258d82d1ac8df8d21)
![{\displaystyle \exists x[f(x)\land g(x)]\iff \exists x[f(x)\land g(x)]\land \exists x[f(x)\land g(x)]\implies \exists x\ f(x)\land \exists x\ g(x)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cab56db1f83383f30a7f1f9d63eac3a2f50ca812)
![{\displaystyle \exists x[f(x)\lor g(x)]\iff \exists x\ f(x)\lor \exists x\ g(x)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8fa93ba38878632dc76d8e9ec564a9f88facec36)
![{\displaystyle [\forall x(f(x)\implies g(x))\implies (\forall x\ f(x)\implies \forall x\ g(x))]\iff \neg \forall x(\neg f(x)\lor g(x))\lor (\neg \forall x\ f(x)\lor \forall x\ g(x))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f8336c9200c1b3841e0f7ed4abac8c904ea34495)
![{\displaystyle [\forall x(f(x)\implies g(x))\implies (\forall x\ f(x)\implies \forall x\ g(x))]\iff \exists x(f(x)\land \neg g(x))\lor \exists x\ \neg f(x)\lor \forall x\ g(x)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bc9c66480e8b750f825362b69c16ffc5763e875a)
![{\displaystyle [\forall x(f(x)\implies g(x))\implies (\forall x\ f(x)\implies \forall x\ g(x))]\iff \exists x(f(x)\land \neg g(x)\lor \neg f(x))\lor \forall x\ g(x)\iff \exists x(\neg g(x)\lor \neg f(x))\lor \forall x\ g(x)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/13764217c4aed19a0be9343671faef882707a0f9)
![{\displaystyle [\forall x(f(x)\implies g(x))\implies (\forall x\ f(x)\implies \forall x\ g(x))]\iff \exists x\ \neg g(x)\lor \exists x\ \neg f(x)\lor \neg \exists x\ \neg g(x)\iff T\lor \exists x\ \neg f(x)\iff T}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dcb8e0b365c96d744107ad6a557e68e1a8664722)
![{\displaystyle \forall x[f(x)\iff g(x)]\iff \forall x[f(x)\land g(x)\lor \neg f(x)\land \neg g(x)]\Longleftarrow \forall x[f(x)\land g(x)]\lor \forall x[\neg f(x)\land \neg g(x)]\iff \forall x\ f(x)\land \forall x\ g(x)\lor \forall x\neg f(x)\land \forall x\neg g(x)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/540c11e7df5db276a2b29f73d5956f44f7f6185b)
![{\displaystyle \forall x[f(x)\iff g(x)]\iff \forall x[f(x)\land g(x)\lor \neg f(x)\land \neg g(x)]\implies \exists x[f(x)\land g(x)\lor \neg f(x)\land \neg g(x)]\iff \exists x[f(x)\land g(x)]\lor \exists x[\neg f(x)\land \neg g(x)]\implies \exists x\ f(x)\land \exists x\ g(x)\lor \exists x\ \neg f(x)\land \exists x\ \neg g(x)\iff \exists x\ f(x)\land \exists x\ g(x)\lor \neg \forall x\ f(x)\land \neg \forall x\ g(x)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5e85a652ce5415ec6de096baf0b43fbdc6757335)
![{\displaystyle \neg \forall x[f(x)\iff g(x)]\iff \exists x[f(x)\iff \neg g(x)]\iff \exists x[f(x)\land \neg g(x)\lor \neg f(x)\land g(x)]\iff \exists x[f(x)\land \neg g(x)]\lor \exists x[\neg f(x)\land g(x)]\implies \exists x\ f(x)\land \exists x\ \neg g(x)\lor \exists x\ \neg f(x)\land \exists x\ g(x)\iff \exists x\ f(x)\land \neg \forall x\ g(x)\lor \neg \forall x\ f(x)\land \exists x\ g(x)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f86e9564224a15dbc4b9a92f25a0da607f23d9a7)
![{\displaystyle \forall x[f(x)\iff g(x)]\iff \forall x[f(x)\land g(x)\lor \neg f(x)\land \neg g(x)]\iff \forall x[(f(x)\lor \neg g(x))\land (\neg f(x)\lor g(x))]\iff \forall x[f(x)\lor \neg g(x)]\land \forall [\neg f(x)\lor g(x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9f52c39a8d295ff38408ea52f9414111f449b78e)
![{\displaystyle a=b\implies [c=a\iff c=b]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/72f6ff5a39be5a9c9e95c9be3c4cda7665a7cab0)
![{\displaystyle [c=a\iff c=b]\implies a=b}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dd2553bededf341370be5455c559aae7c6cb6545)
![{\displaystyle \left[\left[a\right]b\right]\left[(a)b\right]\left[\left((a)\right)b\right]\left(f\right)\left(f'\right)\left(f^{2}\right)\left(f'^{2}\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6f900b29baaf49cf9d2a362f4b14f6779587ec81)
![{\displaystyle {\vec {s}}(t)=\left[a\cos f(t),b\sin f(t)\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/09ae62ab629c8421c8a9b52383179bdde7d00e32)
![{\displaystyle {\vec {s}}\,'(t)=\left[-af'(t)\sin f(t),bf'(t)\cos f(t)\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b39007d33caa1a3296f80a30e2a622856ff40f08)
![{\displaystyle {\vec {s}}\,''(t)=\left[-a\left(f''(t)\sin f(t)+f'^{2}(t)\cos f(t)\right),b\left(f''(t)\cos f(t)-f'^{2}(t)\sin f(t)\right)\right]\propto {\vec {s}}(t)+[k,0]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/165114cbdbf6053105845ea8158d89d8ebce9477)
![{\displaystyle {\vec {s}}\,'(t)(a+k\cos f(t))=c_{1}\left[-a\sin f(t),b\cos f(t)\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8c2b03ab7dc62bfe9cd6b4d4a1a1dfd32a5cf5cd)
![{\displaystyle {\vec {s}}\,''(t)(a+k\cos f(t))^{3}=c_{1}^{2}\left[-a\left(k\sin ^{2}f(t)+(a+k\cos f(t))\cos f(t)\right),b\left(k\sin f(t)\cos f(t)-(a+k\cos f(t))\sin f(t)\right)\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5b73bc51bcfc2916ee0e7309db9b329a9ac830c4)
![{\displaystyle {\vec {s}}\,''(t)(a+k\cos f(t))^{3}=c_{1}^{2}\left[-a\left(k+a\cos f(t)\right),-ab\sin f(t)\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/44e8d2f1d1f767cd8685b0b5a47bca5c7214c93c)
![{\displaystyle {\vec {s}}\,''(t)(a+k\cos f(t))^{3}=-ac_{1}^{2}\left[k+a\cos f(t),b\sin f(t)\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/87878675e745db2940047403a3b69246a37ad1e6)
![{\displaystyle {\vec {s}}\,''(t)(a+k\cos f(t))^{3}=-ac_{1}^{2}({\vec {s}}(t)+[k,0])}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3addb95fa8a0396dd891b6cbc7ee1a4333cb5c25)
![{\displaystyle \left|{\vec {s}}\,''(t)\right|^{2}(a+k\cos f(t))^{6}=\left(ac_{1}^{2}\right)^{2}\left|{\vec {s}}(t)+[k,0]\right|^{2}=a^{2}c_{1}^{4}R^{2}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0ea723c6a3a30252f606e97db9bf3e9c55a8f2d6)
![{\displaystyle {\vec {s}}(t)+[k,0]=\left[a\cos f(t)+k,b\sin f(t)\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9be916919c8d51da11cb116e5129af8126586f32)
![{\displaystyle R^{2}=\left|{\vec {s}}(t)+[k,0]\right|^{2}=(a\cos f(t)+k)^{2}+b^{2}\sin ^{2}f(t)=k^{2}+2ak\cos f(t)+a^{2}\cos ^{2}f(t)+b^{2}\sin ^{2}f(t)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/71e4ade2ece01302e2ac3d21ee02832746df8652)
