c_0_33
ord_less_eq_real @ zero_zero_real @ ( sin_real @ ( divide_divide_real @ pi @ ( semiri2110766477t_real @ n ) ) )
Proof
Proof Summary of Transcendental.thy:4159
Isabelle Statement
Lemma
lemma sin_pi_divide_n_ge_0 [simp]: assumes "n ≠ 0" shows "0 ≤ sin (pi/real n)"
Proof Excerpt
lemma sin_pi_divide_n_ge_0 [simp]:
assumes "n ≠ 0"
shows "0 ≤ sin (pi/real n)"
by (rule sin_ge_zero) (use assms in ‹simp_all add: field_split_simps›)Conjectures
Axioms
c_0_0
c_0_1
c_0_2
c_0_3
c_0_4
c_0_5
c_0_6
c_0_7
c_0_8
c_0_9
c_0_10
c_0_11
c_0_12
c_0_13
c_0_14
c_0_15
c_0_16
c_0_17
c_0_18
c_0_19
c_0_20
c_0_21
c_0_22
c_0_23
c_0_24
c_0_25
c_0_26
c_0_27
c_0_28
c_0_29
c_0_30
c_0_31
c_0_32
c_0_34
c_0_35
c_0_36
c_0_37
c_0_38
c_0_39
c_0_40
c_0_41
c_0_42
c_0_43
c_0_44
c_0_45
c_0_46
c_0_47
c_0_48
c_0_49
c_0_50
c_0_51
c_0_52
c_0_53
c_0_54
c_0_55