environ
vocabularies HIDDEN, NUMBERS, NAT_1, XBOOLE_0, ARYTM_3, CARD_1, SUBSET_1, XXREAL_0, XCMPLX_0, COMPLEX1, ARYTM_1, RELAT_1, SQUARE_1, POWER, NEWTON, SIN_COS, XXREAL_1, FUNCT_1, ORDINAL2, REAL_1, FDIFF_1, RCOMP_1, VALUED_0, TARSKI, PARTFUN1, COMPTRIG;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, SQUARE_1, NAT_1, NEWTON, POWER, RELAT_1, FUNCT_1, RFUNCT_2, FCONT_1, FDIFF_1, PARTFUN1, PARTFUN2, RCOMP_1, SIN_COS, XXREAL_0;
definitions ;
theorems NAT_1, SQUARE_1, POWER, ABSVALUE, RELAT_1, FUNCT_1, RFUNCT_2, PARTFUN1, FCONT_2, RCOMP_1, FDIFF_1, ROLLE, COMPLEX1, SIN_COS, SIN_COS2, XBOOLE_0, XCMPLX_1, XREAL_1, XXREAL_0, NEWTON, XCMPLX_0, XXREAL_1, XBOOLE_1, XREAL_0;
schemes NAT_1;
registrations RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED, NEWTON, SIN_COS, VALUED_0, FCONT_1, FUNCT_1, SQUARE_1, ORDINAL1, CARD_1;
constructors HIDDEN, PARTFUN1, ARYTM_0, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_2, FCONT_1, FDIFF_1, COMSEQ_3, BINARITH, SIN_COS, BINOP_2, POWER, RVSUM_1, RELSET_1, ABIAN;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities SQUARE_1, COMPLEX1, XCMPLX_0;
expansions ;
scheme
Regrwithout0{
P1[
Nat] } :
provided
A1:
ex
k being non
zero Nat st
P1[
k]
and A2:
for
k being non
zero Nat st
k <> 1 &
P1[
k] holds
ex
n being non
zero Nat st
(
n < k &
P1[
n] )
PI in ].0,4.[
by SIN_COS:def 28;
then Lm1:
0 < PI
by XXREAL_1:4;
then Lm2:
0 + (PI / 2) < (PI / 2) + (PI / 2)
by XREAL_1:6;
Lm3:
0 + PI < PI + PI
by Lm1, XREAL_1:6;
Lm4:
0 + (PI / 2) < PI + (PI / 2)
by Lm1, XREAL_1:6;
Lm5:
(PI / 2) + (PI / 2) < PI + (PI / 2)
by Lm2, XREAL_1:6;
((3 / 2) * PI) + (PI / 2) = 2 * PI
;
then Lm6:
(3 / 2) * PI < 2 * PI
by Lm5, XREAL_1:6;
Lm7:
0 < (3 / 2) * PI
by Lm1;