begin
scheme
Regrwithout0{
P1[
Nat] } :
provided
A1:
ex
k being non
empty Nat st
P1[
k]
and A2:
for
k being non
empty Nat st
k <> 1 &
P1[
k] holds
ex
n being non
empty Nat st
(
n < k &
P1[
n] )
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem
theorem
canceled;
theorem
canceled;
theorem Th7:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th17:
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
PI in ].0 ,4.[
by SIN_COS:def 32;
then Lm1:
0 < PI
by XXREAL_1:4;
then Lm2:
0 + (PI / 2) < (PI / 2) + (PI / 2)
by XREAL_1:8;
Lm3:
0 + PI < PI + PI
by Lm1, XREAL_1:8;
Lm4:
0 + (PI / 2) < PI + (PI / 2)
by Lm1, XREAL_1:8;
Lm5:
(PI / 2) + (PI / 2) < PI + (PI / 2)
by Lm2, XREAL_1:8;
((3 / 2) * PI ) + (PI / 2) = 2 * PI
;
then Lm6:
(3 / 2) * PI < 2 * PI
by Lm5, XREAL_1:8;
Lm7:
0 < (3 / 2) * PI
by Lm1;
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem
theorem Th41:
theorem Th42:
theorem
canceled;
theorem
canceled;
theorem Th45:
theorem
theorem
theorem
theorem
theorem Th50:
theorem Th51:
begin
:: deftheorem Def1 defines Arg COMPTRIG:def 1 :
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem
theorem
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem
theorem
theorem Th67:
theorem Th68:
theorem
theorem
theorem Th71:
theorem
theorem Th73:
theorem Th74:
:: deftheorem Def2 defines CRoot COMPTRIG:def 2 :
theorem
theorem
theorem
theorem
theorem
theorem