proposition: Theorem zeta_3_irrational : ~ exists (r : rat), (z3 == r%:CR)%CR.
proof: Proof. case=> z3_rat z3_ratP; case: (denqP z3_rat) z3_ratP => d dP z3_ratP. have heps : 0 < 1 / 2%:Q by []. have [M MP] := sigma_goes_to_0 heps. pose sigma_Q (n : nat) := 2%:Q * (l n)%:Q ^ 3%N * (a n * z3_rat - b n). have sigma_QP (n : nat) : ((sigma_Q n)%:CR == sigma n)%CR. by rewrite /sigma z3_ratP -!cst_crealM -cst_crealB -cst_crealM. pose_big_enough n. have h_pos : 0 < sigma_Q n. apply/lt_creal_cst; rewrite sigma_QP; apply: lt_0_sigma; raise_big_enough. have h_lt1 : sigma_Q n < 1 / 2%:Q. apply/lt_creal_cst; rewrite sigma_QP; apply: MP; raise_big_enough. suff : 1 <= sigma_Q n by apply/negP; rewrite -ltNge; apply: lt_trans h_lt1 _. suff /QintP [z zP] : sigma_Q n \is a Qint. by move: h_pos; rewrite zP ler1z -gtz0_ge1 ltr0z; apply. rewrite /sigma_Q mulrDr mulrN; apply/rpredB/Qint_l3b. rewrite -mulrA; apply: rpredM (rpred_int _ _) _. rewrite /exprz exprSr mulrACA mulrC. apply/rpredM/rpredM/Qint_a/rpredX/rpred_int/iter_lcmn_mul_rat. rewrite normr_denq dP lez_nat; raise_big_enough. by close. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals) extra_mathcomp extra_cauchyreals tactics shift bigopz arithmetics seq_defs c_props s_props z3seq_props a_props b_props b_over_a_props