zexex Show Code edit
## Rational and Integer Existence are the same
thm (zexex () () (<-> (z.E. x ph) (E. x ph))
x ph z.df-ex
(<-> (z.E. x ph) (-. (z.A. x (-. ph))))
x (-. ph) df-al bicomi
(<-> (z.A. x (-. ph)) (A. x (-. ph)))
BiReplaceBi1Not0
(<-> (z.E. x ph) (-. (A. x (-. ph))))
x ph df-ex bicomi
(<-> (-. (A. x (-. ph))) (E. x ph))
bitri
(<-> (z.E. x ph) (E. x ph))
)
edit