proposition: Lemma z_exists : forall (b_0' : CC) (k : nat) (r eta : IR), let a_0 := AbsCC b_0' in [0] [<] a_0 -> [0] [<] a k -> 1 <= k -> k <= n -> [0] [<=] r -> [0] [<] eta -> AbsCC (b_0'[-]b_0) [<=] eta -> a k[*]r[^]k [<=] a_0 -> {z : CC | AbsCC z [=] r | AbsCC (b_0[+]b k[*]z[^]k) [<=] a_0[-]a k[*]r[^]k[+]eta}.
proof: Proof. intros b_0' k r eta a_0 H H0 H1 H2 H3 H4 H5 H6. cut (AbsCC b_0' [#] [0]). intro H7. 2: apply pos_ap_zero; auto. cut (cc_IR (AbsCC b_0') [#] [0]). intro H8. 2: astepr (cc_IR [0]); apply cc_IR_resp_ap; auto. cut (a k [#] [0]). intro H9. 2: apply pos_ap_zero; auto. cut (b k [#] [0]). intro H10. 2: apply AbsCC_ap_zero; apply ap_symmetric_unfolded; auto. cut (0 < k). intro H11. 2: auto with arith. cut ( [--] ((cc_IR (a k) [/] cc_IR (AbsCC b_0') [//]H8) [*] (b_0'[/] b k[//]H10)) [#] [0]). intro H12. elim (CnrootCC [--] ((cc_IR (a k) [/] cc_IR (AbsCC b_0') [//]H8) [*] (b_0'[/] b k[//]H10)) H12 k H11). intros w H13. cut (AbsCC w [=] [1]). intro H14. exists (cc_IR r[*]w). astepl (AbsCC (cc_IR r) [*]AbsCC w). astepl (r[*]AbsCC w). Step_final (r[*][1]). apply leEq_transitive with (AbsCC (b_0'[+]b k[*] (cc_IR r[*]w) [^]k) [+]AbsCC (b_0[-]b_0')). apply leEq_wdl with (AbsCC (b_0'[+]b k[*] (cc_IR r[*]w) [^]k[+] (b_0[-]b_0'))). apply triangle. apply AbsCC_wd; rational. apply leEq_wdl with (AbsCC b_0'[-]a k[*]r[^]k[+]AbsCC (b_0[-]b_0')). apply plus_resp_leEq_lft. astepl (AbsCC [--] (b_0[-]b_0')). apply leEq_wdl with (AbsCC (b_0'[-]b_0)); auto. apply AbsCC_wd; rational. apply bin_op_wd_unfolded. 2: algebra. apply eq_transitive_unfolded with (AbsCC ((b_0'[/] cc_IR (AbsCC b_0') [//]H8) [*] (cc_IR (AbsCC b_0') [-]cc_IR (a k) [*]cc_IR r[^]k))). astepl ([1][*] (AbsCC b_0'[-]a k[*]r[^]k)). astepr (AbsCC (b_0'[/] cc_IR (AbsCC b_0') [//]H8) [*] AbsCC (cc_IR (AbsCC b_0') [-]cc_IR (a k) [*]cc_IR r[^]k)). apply bin_op_wd_unfolded. astepl (AbsCC b_0'[/] AbsCC b_0'[//]H7). apply eq_symmetric_unfolded. apply cc_div_abs'. apply AbsCC_nonneg. apply eq_transitive_unfolded with (AbsCC (cc_IR (AbsCC b_0') [-]cc_IR (a k) [*]cc_IR (r[^]k))). 2: apply AbsCC_wd; algebra. astepr (AbsCC (cc_IR (AbsCC b_0') [-]cc_IR (a k[*]r[^]k))). astepr (AbsCC (cc_IR (AbsCC b_0'[-]a k[*]r[^]k))). cut ([0] [<=] AbsCC b_0'[-]a k[*]r[^]k). algebra. apply shift_leEq_lft; auto. apply AbsCC_wd. rstepl (b_0'[+] b k[*] (cc_IR r[^]k[*] [--] ((cc_IR (a k) [/] cc_IR (AbsCC b_0') [//]H8) [*] (b_0'[/] b k[//]H10)))). apply bin_op_wd_unfolded. algebra. apply bin_op_wd_unfolded. algebra. Step_final (cc_IR r[^]k[*]w[^]k). apply root_one with k; auto. apply AbsCC_nonneg. astepl (AbsCC (w[^]k)). astepl (AbsCC [--] ((cc_IR (a k) [/] cc_IR (AbsCC b_0') [//]H8) [*] (b_0'[/] b k[//]H10))). astepl (AbsCC ((cc_IR (a k) [/] cc_IR (AbsCC b_0') [//]H8) [*] (b_0'[/] b k[//]H10))). astepl (AbsCC (cc_IR (a k) [/] cc_IR (AbsCC b_0') [//]H8) [*] AbsCC (b_0'[/] b k[//]H10)). astepl (AbsCC (cc_IR (a k) [/] cc_IR (AbsCC b_0') [//]H8) [*] AbsCC (b_0'[/] b k[//]H10)). cut ([0] [<=] AbsCC b_0'). intro. 2: apply AbsCC_nonneg. astepl ((AbsCC (cc_IR (a k)) [/] AbsCC b_0'[//]H7) [*]AbsCC (b_0'[/] b k[//]H10)). astepl ((AbsCC (cc_IR (a k)) [/] AbsCC b_0'[//]H7) [*]AbsCC (b_0'[/] b k[//]H10)). cut ([0] [<=] a k). intro. 2: apply less_leEq; auto. astepl ((a k[/] AbsCC b_0'[//]H7) [*]AbsCC (b_0'[/] b k[//]H10)). astepl ((a k[/] AbsCC b_0'[//]H7) [*] (AbsCC b_0'[/] AbsCC (b k) [//]H9)). unfold a in |- *; rational. apply ap_wdl_unfolded with (cc_IR [--] (a k[/] AbsCC b_0'[//]H7) [*] (b_0'[/] b k[//]H10)). apply mult_resp_ap_zero. astepr (cc_IR [0]). apply cc_IR_resp_ap. apply inv_resp_ap_zero. apply div_resp_ap_zero_rev; auto. apply div_resp_ap_zero_rev. apply AbsCC_ap_zero. apply ap_symmetric_unfolded; auto. apply eq_transitive_unfolded with ( [--] (cc_IR (a k[/] AbsCC b_0'[//]H7)) [*] (b_0'[/] b k[//]H10)). apply mult_wdl. astepl (cc_IR ([0][-] (a k[/] AbsCC b_0'[//]H7))). astepr ([0][-]cc_IR (a k[/] AbsCC b_0'[//]H7)). Step_final (cc_IR [0][-]cc_IR (a k[/] AbsCC b_0'[//]H7)). astepl (([0][-]cc_IR (a k[/] AbsCC b_0'[//]H7)) [*] (b_0'[/] b k[//]H10)). astepl ((cc_IR [0][-]cc_IR (a k[/] AbsCC b_0'[//]H7)) [*] (b_0'[/] b k[//]H10)). astepl (cc_IR [0][*] (b_0'[/] b k[//]H10) [-] cc_IR (a k[/] AbsCC b_0'[//]H7) [*] (b_0'[/] b k[//]H10)). astepl ([0][*] (b_0'[/] b k[//]H10) [-] cc_IR (a k[/] AbsCC b_0'[//]H7) [*] (b_0'[/] b k[//]H10)). astepl ([0][-]cc_IR (a k[/] AbsCC b_0'[//]H7) [*] (b_0'[/] b k[//]H10)). astepl ( [--] (cc_IR (a k[/] AbsCC b_0'[//]H7) [*] (b_0'[/] b k[//]H10))). apply un_op_wd_unfolded. apply mult_wdl. unfold cc_IR in |- *; simpl in |- *; split; simpl in |- *; rational. Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma