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] )
begin
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;
begin