1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: Exp_prop.v,v 1.1.2.1 2004/07/16 19:31:32 herbelin Exp $ i*)
Require Rbase.
Require Rfunctions.
Require SeqSeries.
Require Rtrigo.
Require Ranalysis1.
Require PSeries_reg.
Require Div2.
Require Even.
Require Max.
V7only [Import R_scope.].
Open Local Scope nat_scope.
V7only [Import nat_scope.].
Open Local Scope R_scope.
Definition E1 [x:R] : nat->R := [N:nat](sum_f_R0 [k:nat]``/(INR (fact k))*(pow x k)`` N).
Lemma E1_cvg : (x:R) (Un_cv (E1 x) (exp x)).
Intro; Unfold exp; Unfold projT1.
Case (exist_exp x); Intro.
Unfold exp_in Un_cv; Unfold infinit_sum E1; Trivial.
Qed.
Definition Reste_E [x,y:R] : nat->R := [N:nat](sum_f_R0 [k:nat](sum_f_R0 [l:nat]``/(INR (fact (S (plus l k))))*(pow x (S (plus l k)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))`` (pred (minus N k))) (pred N)).
Lemma exp_form : (x,y:R;n:nat) (lt O n) -> ``(E1 x n)*(E1 y n)-(Reste_E x y n)==(E1 (x+y) n)``.
Intros; Unfold E1.
Rewrite cauchy_finite.
Unfold Reste_E; Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Or; Apply sum_eq; Intros.
Rewrite binomial.
Rewrite scal_sum; Apply sum_eq; Intros.
Unfold C; Unfold Rdiv; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym (INR (fact i))); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
Rewrite Rmult_1r; Rewrite Rinv_Rmult.
Ring.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Apply H.
Qed.
Definition maj_Reste_E [x,y:R] : nat->R := [N:nat]``4*(pow (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S O)) N))/(Rsqr (INR (fact (div2 (pred N)))))``.
Lemma Rle_Rinv : (x,y:R) ``0<x`` -> ``0<y`` -> ``x<=y`` -> ``/y<=/x``.
Intros; Apply Rle_monotony_contra with x.
Apply H.
Rewrite <- Rinv_r_sym.
Apply Rle_monotony_contra with y.
Apply H0.
Rewrite Rmult_1r; Rewrite Rmult_sym; Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
Rewrite Rmult_1r; Apply H1.
Red; Intro; Rewrite H2 in H0; Elim (Rlt_antirefl ? H0).
Red; Intro; Rewrite H2 in H; Elim (Rlt_antirefl ? H).
Qed.
(**********)
Lemma div2_double : (N:nat) (div2 (mult (2) N))=N.
Intro; Induction N.
Reflexivity.
Replace (mult (2) (S N)) with (S (S (mult (2) N))).
Simpl; Simpl in HrecN; Rewrite HrecN; Reflexivity.
Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
Qed.
Lemma div2_S_double : (N:nat) (div2 (S (mult (2) N)))=N.
Intro; Induction N.
Reflexivity.
Replace (mult (2) (S N)) with (S (S (mult (2) N))).
Simpl; Simpl in HrecN; Rewrite HrecN; Reflexivity.
Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
Qed.
Lemma div2_not_R0 : (N:nat) (lt (1) N) -> (lt O (div2 N)).
Intros; Induction N.
Elim (lt_n_O ? H).
Cut (lt (1) N)\/N=(1).
Intro; Elim H0; Intro.
Assert H2 := (even_odd_dec N).
Elim H2; Intro.
Rewrite <- (even_div2 ? a); Apply HrecN; Assumption.
Rewrite <- (odd_div2 ? b); Apply lt_O_Sn.
Rewrite H1; Simpl; Apply lt_O_Sn.
Inversion H.
Right; Reflexivity.
Left; Apply lt_le_trans with (2); [Apply lt_n_Sn | Apply H1].
Qed.
Lemma Reste_E_maj : (x,y:R;N:nat) (lt O N) -> ``(Rabsolu (Reste_E x y N))<=(maj_Reste_E x y N)``.
Intros; Pose M := (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))).
Apply Rle_trans with (Rmult (pow M (mult (2) N)) (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``/(Rsqr (INR (fact (div2 (S N)))))`` (pred (minus N k))) (pred N))).
Unfold Reste_E.
Apply Rle_trans with (sum_f_R0 [k:nat](Rabsolu (sum_f_R0 [l:nat]``/(INR (fact (S (plus l k))))*(pow x (S (plus l k)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))`` (pred (minus N k)))) (pred N)).
Apply (sum_Rabsolu [k:nat](sum_f_R0 [l:nat]``/(INR (fact (S (plus l k))))*(pow x (S (plus l k)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))`` (pred (minus N k))) (pred N)).
Apply Rle_trans with (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(Rabsolu (/(INR (fact (S (plus l k))))*(pow x (S (plus l k)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))))`` (pred (minus N k))) (pred N)).
Apply sum_Rle; Intros.
Apply (sum_Rabsolu [l:nat]``/(INR (fact (S (plus l n))))*(pow x (S (plus l n)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))``).
Apply Rle_trans with (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(pow M (mult (S (S O)) N))*/(INR (fact (S l)))*/(INR (fact (minus N l)))`` (pred (minus N k))) (pred N)).
Apply sum_Rle; Intros.
Apply sum_Rle; Intros.
Repeat Rewrite Rabsolu_mult.
Do 2 Rewrite <- Pow_Rabsolu.
Rewrite (Rabsolu_right ``/(INR (fact (S (plus n0 n))))``).
Rewrite (Rabsolu_right ``/(INR (fact (minus N n0)))``).
Replace ``/(INR (fact (S (plus n0 n))))*(pow (Rabsolu x) (S (plus n0 n)))*
(/(INR (fact (minus N n0)))*(pow (Rabsolu y) (minus N n0)))`` with ``/(INR (fact (minus N n0)))*/(INR (fact (S (plus n0 n))))*(pow (Rabsolu x) (S (plus n0 n)))*(pow (Rabsolu y) (minus N n0))``; [Idtac | Ring].
Rewrite <- (Rmult_sym ``/(INR (fact (minus N n0)))``).
Repeat Rewrite Rmult_assoc.
Apply Rle_monotony.
Left; Apply Rlt_Rinv; Apply INR_fact_lt_0.
Apply Rle_trans with ``/(INR (fact (S n0)))*(pow (Rabsolu x) (S (plus n0 n)))*(pow (Rabsolu y) (minus N n0))``.
Rewrite (Rmult_sym ``/(INR (fact (S (plus n0 n))))``); Rewrite (Rmult_sym ``/(INR (fact (S n0)))``); Repeat Rewrite Rmult_assoc; Apply Rle_monotony.
Apply pow_le; Apply Rabsolu_pos.
Rewrite (Rmult_sym ``/(INR (fact (S n0)))``); Apply Rle_monotony.
Apply pow_le; Apply Rabsolu_pos.
Apply Rle_Rinv.
Apply INR_fact_lt_0.
Apply INR_fact_lt_0.
Apply le_INR; Apply fact_growing; Apply le_n_S.
Apply le_plus_l.
Rewrite (Rmult_sym ``(pow M (mult (S (S O)) N))``); Rewrite Rmult_assoc; Apply Rle_monotony.
Left; Apply Rlt_Rinv; Apply INR_fact_lt_0.
Apply Rle_trans with ``(pow M (S (plus n0 n)))*(pow (Rabsolu y) (minus N n0))``.
Do 2 Rewrite <- (Rmult_sym ``(pow (Rabsolu y) (minus N n0))``).
Apply Rle_monotony.
Apply pow_le; Apply Rabsolu_pos.
Apply pow_incr; Split.
Apply Rabsolu_pos.
Apply Rle_trans with (Rmax (Rabsolu x) (Rabsolu y)).
Apply RmaxLess1.
Unfold M; Apply RmaxLess2.
Apply Rle_trans with ``(pow M (S (plus n0 n)))*(pow M (minus N n0))``.
Apply Rle_monotony.
Apply pow_le; Apply Rle_trans with R1.
Left; Apply Rlt_R0_R1.
Unfold M; Apply RmaxLess1.
Apply pow_incr; Split.
Apply Rabsolu_pos.
Apply Rle_trans with (Rmax (Rabsolu x) (Rabsolu y)).
Apply RmaxLess2.
Unfold M; Apply RmaxLess2.
Rewrite <- pow_add; Replace (plus (S (plus n0 n)) (minus N n0)) with (plus N (S n)).
Apply Rle_pow.
Unfold M; Apply RmaxLess1.
Replace (mult (2) N) with (plus N N); [Idtac | Ring].
Apply le_reg_l.
Replace N with (S (pred N)).
Apply le_n_S; Apply H0.
Symmetry; Apply S_pred with O; Apply H.
Apply INR_eq; Do 2 Rewrite plus_INR; Do 2 Rewrite S_INR; Rewrite plus_INR; Rewrite minus_INR.
Ring.
Apply le_trans with (pred (minus N n)).
Apply H1.
Apply le_S_n.
Replace (S (pred (minus N n))) with (minus N n).
Apply le_trans with N.
Apply simpl_le_plus_l with n.
Rewrite <- le_plus_minus.
Apply le_plus_r.
Apply le_trans with (pred N).
Apply H0.
Apply le_pred_n.
Apply le_n_Sn.
Apply S_pred with O.
Apply simpl_lt_plus_l with n.
Rewrite <- le_plus_minus.
Replace (plus n (0)) with n; [Idtac | Ring].
Apply le_lt_trans with (pred N).
Apply H0.
Apply lt_pred_n_n.
Apply H.
Apply le_trans with (pred N).
Apply H0.
Apply le_pred_n.
Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply INR_fact_lt_0.
Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply INR_fact_lt_0.
Rewrite scal_sum.
Apply sum_Rle; Intros.
Rewrite <- Rmult_sym.
Rewrite scal_sum.
Apply sum_Rle; Intros.
Rewrite (Rmult_sym ``/(Rsqr (INR (fact (div2 (S N)))))``).
Rewrite Rmult_assoc; Apply Rle_monotony.
Apply pow_le.
Apply Rle_trans with R1.
Left; Apply Rlt_R0_R1.
Unfold M; Apply RmaxLess1.
Assert H2 := (even_odd_cor N).
Elim H2; Intros N0 H3.
Elim H3; Intro.
Apply Rle_trans with ``/(INR (fact n0))*/(INR (fact (minus N n0)))``.
Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (minus N n0)))``).
Apply Rle_monotony.
Left; Apply Rlt_Rinv; Apply INR_fact_lt_0.
Apply Rle_Rinv.
Apply INR_fact_lt_0.
Apply INR_fact_lt_0.
Apply le_INR.
Apply fact_growing.
Apply le_n_Sn.
Replace ``/(INR (fact n0))*/(INR (fact (minus N n0)))`` with ``(C N n0)/(INR (fact N))``.
Pattern 1 N; Rewrite H4.
Apply Rle_trans with ``(C N N0)/(INR (fact N))``.
Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/(INR (fact N))``).
Apply Rle_monotony.
Left; Apply Rlt_Rinv; Apply INR_fact_lt_0.
Rewrite H4.
Apply C_maj.
Rewrite <- H4; Apply le_trans with (pred (minus N n)).
Apply H1.
Apply le_S_n.
Replace (S (pred (minus N n))) with (minus N n).
Apply le_trans with N.
Apply simpl_le_plus_l with n.
Rewrite <- le_plus_minus.
Apply le_plus_r.
Apply le_trans with (pred N).
Apply H0.
Apply le_pred_n.
Apply le_n_Sn.
Apply S_pred with O.
Apply simpl_lt_plus_l with n.
Rewrite <- le_plus_minus.
Replace (plus n (0)) with n; [Idtac | Ring].
Apply le_lt_trans with (pred N).
Apply H0.
Apply lt_pred_n_n.
Apply H.
Apply le_trans with (pred N).
Apply H0.
Apply le_pred_n.
Replace ``(C N N0)/(INR (fact N))`` with ``/(Rsqr (INR (fact N0)))``.
Rewrite H4; Rewrite div2_S_double; Right; Reflexivity.
Unfold Rsqr C Rdiv.
Repeat Rewrite Rinv_Rmult.
Rewrite (Rmult_sym (INR (fact N))).
Repeat Rewrite Rmult_assoc.
Rewrite <- Rinv_r_sym.
Rewrite Rmult_1r; Replace (minus N N0) with N0.
Ring.
Replace N with (plus N0 N0).
Symmetry; Apply minus_plus.
Rewrite H4.
Apply INR_eq; Rewrite plus_INR; Rewrite mult_INR; Do 2 Rewrite S_INR; Ring.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Unfold C Rdiv.
Rewrite (Rmult_sym (INR (fact N))).
Repeat Rewrite Rmult_assoc.
Rewrite <- Rinv_r_sym.
Rewrite Rinv_Rmult.
Rewrite Rmult_1r; Ring.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Replace ``/(INR (fact (S n0)))*/(INR (fact (minus N n0)))`` with ``(C (S N) (S n0))/(INR (fact (S N)))``.
Apply Rle_trans with ``(C (S N) (S N0))/(INR (fact (S N)))``.
Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (S N)))``).
Apply Rle_monotony.
Left; Apply Rlt_Rinv; Apply INR_fact_lt_0.
Cut (S N) = (mult (2) (S N0)).
Intro; Rewrite H5; Apply C_maj.
Rewrite <- H5; Apply le_n_S.
Apply le_trans with (pred (minus N n)).
Apply H1.
Apply le_S_n.
Replace (S (pred (minus N n))) with (minus N n).
Apply le_trans with N.
Apply simpl_le_plus_l with n.
Rewrite <- le_plus_minus.
Apply le_plus_r.
Apply le_trans with (pred N).
Apply H0.
Apply le_pred_n.
Apply le_n_Sn.
Apply S_pred with O.
Apply simpl_lt_plus_l with n.
Rewrite <- le_plus_minus.
Replace (plus n (0)) with n; [Idtac | Ring].
Apply le_lt_trans with (pred N).
Apply H0.
Apply lt_pred_n_n.
Apply H.
Apply le_trans with (pred N).
Apply H0.
Apply le_pred_n.
Apply INR_eq; Rewrite H4.
Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
Cut (S N) = (mult (2) (S N0)).
Intro.
Replace ``(C (S N) (S N0))/(INR (fact (S N)))`` with ``/(Rsqr (INR (fact (S N0))))``.
Rewrite H5; Rewrite div2_double.
Right; Reflexivity.
Unfold Rsqr C Rdiv.
Repeat Rewrite Rinv_Rmult.
Replace (minus (S N) (S N0)) with (S N0).
Rewrite (Rmult_sym (INR (fact (S N)))).
Repeat Rewrite Rmult_assoc.
Rewrite <- Rinv_r_sym.
Rewrite Rmult_1r; Reflexivity.
Apply INR_fact_neq_0.
Replace (S N) with (plus (S N0) (S N0)).
Symmetry; Apply minus_plus.
Rewrite H5; Ring.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Apply INR_eq; Rewrite H4; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
Unfold C Rdiv.
Rewrite (Rmult_sym (INR (fact (S N)))).
Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
Rewrite Rmult_1r; Rewrite Rinv_Rmult.
Reflexivity.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Unfold maj_Reste_E.
Unfold Rdiv; Rewrite (Rmult_sym ``4``).
Rewrite Rmult_assoc.
Apply Rle_monotony.
Apply pow_le.
Apply Rle_trans with R1.
Left; Apply Rlt_R0_R1.
Apply RmaxLess1.
Apply Rle_trans with (sum_f_R0 [k:nat]``(INR (minus N k))*/(Rsqr (INR (fact (div2 (S N)))))`` (pred N)).
Apply sum_Rle; Intros.
Rewrite sum_cte.
Replace (S (pred (minus N n))) with (minus N n).
Right; Apply Rmult_sym.
Apply S_pred with O.
Apply simpl_lt_plus_l with n.
Rewrite <- le_plus_minus.
Replace (plus n (0)) with n; [Idtac | Ring].
Apply le_lt_trans with (pred N).
Apply H0.
Apply lt_pred_n_n.
Apply H.
Apply le_trans with (pred N).
Apply H0.
Apply le_pred_n.
Apply Rle_trans with (sum_f_R0 [k:nat]``(INR N)*/(Rsqr (INR (fact (div2 (S N)))))`` (pred N)).
Apply sum_Rle; Intros.
Do 2 Rewrite <- (Rmult_sym ``/(Rsqr (INR (fact (div2 (S N)))))``).
Apply Rle_monotony.
Left; Apply Rlt_Rinv; Apply Rsqr_pos_lt.
Apply INR_fact_neq_0.
Apply le_INR.
Apply simpl_le_plus_l with n.
Rewrite <- le_plus_minus.
Apply le_plus_r.
Apply le_trans with (pred N).
Apply H0.
Apply le_pred_n.
Rewrite sum_cte; Replace (S (pred N)) with N.
Cut (div2 (S N)) = (S (div2 (pred N))).
Intro; Rewrite H0.
Rewrite fact_simpl; Rewrite mult_sym; Rewrite mult_INR; Rewrite Rsqr_times.
Rewrite Rinv_Rmult.
Rewrite (Rmult_sym (INR N)); Repeat Rewrite Rmult_assoc; Apply Rle_monotony.
Left; Apply Rlt_Rinv; Apply Rsqr_pos_lt; Apply INR_fact_neq_0.
Rewrite <- H0.
Cut ``(INR N)<=(INR (mult (S (S O)) (div2 (S N))))``.
Intro; Apply Rle_monotony_contra with ``(Rsqr (INR (div2 (S N))))``.
Apply Rsqr_pos_lt.
Apply not_O_INR; Red; Intro.
Cut (lt (1) (S N)).
Intro; Assert H4 := (div2_not_R0 ? H3).
Rewrite H2 in H4; Elim (lt_n_O ? H4).
Apply lt_n_S; Apply H.
Repeat Rewrite <- Rmult_assoc.
Rewrite <- Rinv_r_sym.
Rewrite Rmult_1l.
Replace ``(INR N)*(INR N)`` with (Rsqr (INR N)); [Idtac | Reflexivity].
Rewrite Rmult_assoc.
Rewrite Rmult_sym.
Replace ``4`` with (Rsqr ``2``); [Idtac | SqRing].
Rewrite <- Rsqr_times.
Apply Rsqr_incr_1.
Replace ``2`` with (INR (2)).
Rewrite <- mult_INR; Apply H1.
Reflexivity.
Left; Apply lt_INR_0; Apply H.
Left; Apply Rmult_lt_pos.
Sup0.
Apply lt_INR_0; Apply div2_not_R0.
Apply lt_n_S; Apply H.
Cut (lt (1) (S N)).
Intro; Unfold Rsqr; Apply prod_neq_R0; Apply not_O_INR; Intro; Assert H4 := (div2_not_R0 ? H2); Rewrite H3 in H4; Elim (lt_n_O ? H4).
Apply lt_n_S; Apply H.
Assert H1 := (even_odd_cor N).
Elim H1; Intros N0 H2.
Elim H2; Intro.
Pattern 2 N; Rewrite H3.
Rewrite div2_S_double.
Right; Rewrite H3; Reflexivity.
Pattern 2 N; Rewrite H3.
Replace (S (S (mult (2) N0))) with (mult (2) (S N0)).
Rewrite div2_double.
Rewrite H3.
Rewrite S_INR; Do 2 Rewrite mult_INR.
Rewrite (S_INR N0).
Rewrite Rmult_Rplus_distr.
Apply Rle_compatibility.
Rewrite Rmult_1r.
Simpl.
Pattern 1 R1; Rewrite <- Rplus_Or; Apply Rle_compatibility; Left; Apply Rlt_R0_R1.
Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
Unfold Rsqr; Apply prod_neq_R0; Apply INR_fact_neq_0.
Unfold Rsqr; Apply prod_neq_R0; Apply not_O_INR; Discriminate.
Assert H0 := (even_odd_cor N).
Elim H0; Intros N0 H1.
Elim H1; Intro.
Cut (lt O N0).
Intro; Rewrite H2.
Rewrite div2_S_double.
Replace (mult (2) N0) with (S (S (mult (2) (pred N0)))).
Replace (pred (S (S (mult (2) (pred N0))))) with (S (mult (2) (pred N0))).
Rewrite div2_S_double.
Apply S_pred with O; Apply H3.
Reflexivity.
Replace N0 with (S (pred N0)).
Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
Symmetry; Apply S_pred with O; Apply H3.
Rewrite H2 in H.
Apply neq_O_lt.
Red; Intro.
Rewrite <- H3 in H.
Simpl in H.
Elim (lt_n_O ? H).
Rewrite H2.
Replace (pred (S (mult (2) N0))) with (mult (2) N0); [Idtac | Reflexivity].
Replace (S (S (mult (2) N0))) with (mult (2) (S N0)).
Do 2 Rewrite div2_double.
Reflexivity.
Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
Apply S_pred with O; Apply H.
Qed.
Lemma maj_Reste_cv_R0 : (x,y:R) (Un_cv (maj_Reste_E x y) ``0``).
Intros; Assert H := (Majxy_cv_R0 x y).
Unfold Un_cv in H; Unfold Un_cv; Intros.
Cut ``0<eps/4``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]].
Elim (H ? H1); Intros N0 H2.
Exists (max (mult (2) (S N0)) (2)); Intros.
Unfold R_dist in H2; Unfold R_dist; Rewrite minus_R0; Unfold Majxy in H2; Unfold maj_Reste_E.
Rewrite Rabsolu_right.
Apply Rle_lt_trans with ``4*(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S (S (S O)))) (S (div2 (pred n)))))/(INR (fact (div2 (pred n))))``.
Apply Rle_monotony.
Left; Sup0.
Unfold Rdiv Rsqr; Rewrite Rinv_Rmult.
Rewrite (Rmult_sym ``(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S O)) n))``); Rewrite (Rmult_sym ``(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S (S (S O)))) (S (div2 (pred n)))))``); Rewrite Rmult_assoc; Apply Rle_monotony.
Left; Apply Rlt_Rinv; Apply INR_fact_lt_0.
Apply Rle_trans with ``(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S O)) n))``.
Rewrite Rmult_sym; Pattern 2 (pow (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (2) n)); Rewrite <- Rmult_1r; Apply Rle_monotony.
Apply pow_le; Apply Rle_trans with R1.
Left; Apply Rlt_R0_R1.
Apply RmaxLess1.
Apply Rle_monotony_contra with ``(INR (fact (div2 (pred n))))``.
Apply INR_fact_lt_0.
Rewrite Rmult_1r; Rewrite <- Rinv_r_sym.
Replace R1 with (INR (1)); [Apply le_INR | Reflexivity].
Apply lt_le_S.
Apply INR_lt.
Apply INR_fact_lt_0.
Apply INR_fact_neq_0.
Apply Rle_pow.
Apply RmaxLess1.
Assert H4 := (even_odd_cor n).
Elim H4; Intros N1 H5.
Elim H5; Intro.
Cut (lt O N1).
Intro.
Rewrite H6.
Replace (pred (mult (2) N1)) with (S (mult (2) (pred N1))).
Rewrite div2_S_double.
Replace (S (pred N1)) with N1.
Apply INR_le.
Right.
Do 3 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
Apply S_pred with O; Apply H7.
Replace (mult (2) N1) with (S (S (mult (2) (pred N1)))).
Reflexivity.
Pattern 2 N1; Replace N1 with (S (pred N1)).
Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
Symmetry ; Apply S_pred with O; Apply H7.
Apply INR_lt.
Apply Rlt_monotony_contra with (INR (2)).
Simpl; Sup0.
Rewrite Rmult_Or; Rewrite <- mult_INR.
Apply lt_INR_0.
Rewrite <- H6.
Apply lt_le_trans with (2).
Apply lt_O_Sn.
Apply le_trans with (max (mult (2) (S N0)) (2)).
Apply le_max_r.
Apply H3.
Rewrite H6.
Replace (pred (S (mult (2) N1))) with (mult (2) N1).
Rewrite div2_double.
Replace (mult (4) (S N1)) with (mult (2) (mult (2) (S N1))).
Apply mult_le.
Replace (mult (2) (S N1)) with (S (S (mult (2) N1))).
Apply le_n_Sn.
Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
Ring.
Reflexivity.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Apply Rlt_monotony_contra with ``/4``.
Apply Rlt_Rinv; Sup0.
Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
Rewrite Rmult_1l; Rewrite Rmult_sym.
Replace ``(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S (S (S O)))) (S (div2 (pred n)))))/(INR (fact (div2 (pred n))))`` with ``(Rabsolu ((pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S (S (S O)))) (S (div2 (pred n)))))/(INR (fact (div2 (pred n))))-0))``.
Apply H2; Unfold ge.
Cut (le (mult (2) (S N0)) n).
Intro; Apply le_S_n.
Apply INR_le; Apply Rle_monotony_contra with (INR (2)).
Simpl; Sup0.
Do 2 Rewrite <- mult_INR; Apply le_INR.
Apply le_trans with n.
Apply H4.
Assert H5 := (even_odd_cor n).
Elim H5; Intros N1 H6.
Elim H6; Intro.
Cut (lt O N1).
Intro.
Rewrite H7.
Apply mult_le.
Replace (pred (mult (2) N1)) with (S (mult (2) (pred N1))).
Rewrite div2_S_double.
Replace (S (pred N1)) with N1.
Apply le_n.
Apply S_pred with O; Apply H8.
Replace (mult (2) N1) with (S (S (mult (2) (pred N1)))).
Reflexivity.
Pattern 2 N1; Replace N1 with (S (pred N1)).
Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
Symmetry; Apply S_pred with O; Apply H8.
Apply INR_lt.
Apply Rlt_monotony_contra with (INR (2)).
Simpl; Sup0.
Rewrite Rmult_Or; Rewrite <- mult_INR.
Apply lt_INR_0.
Rewrite <- H7.
Apply lt_le_trans with (2).
Apply lt_O_Sn.
Apply le_trans with (max (mult (2) (S N0)) (2)).
Apply le_max_r.
Apply H3.
Rewrite H7.
Replace (pred (S (mult (2) N1))) with (mult (2) N1).
Rewrite div2_double.
Replace (mult (2) (S N1)) with (S (S (mult (2) N1))).
Apply le_n_Sn.
Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
Reflexivity.
Apply le_trans with (max (mult (2) (S N0)) (2)).
Apply le_max_l.
Apply H3.
Rewrite minus_R0; Apply Rabsolu_right.
Apply Rle_sym1.
Unfold Rdiv; Repeat Apply Rmult_le_pos.
Apply pow_le.
Apply Rle_trans with R1.
Left; Apply Rlt_R0_R1.
Apply RmaxLess1.
Left; Apply Rlt_Rinv; Apply INR_fact_lt_0.
DiscrR.
Apply Rle_sym1.
Unfold Rdiv; Apply Rmult_le_pos.
Left; Sup0.
Apply Rmult_le_pos.
Apply pow_le.
Apply Rle_trans with R1.
Left; Apply Rlt_R0_R1.
Apply RmaxLess1.
Left; Apply Rlt_Rinv; Apply Rsqr_pos_lt; Apply INR_fact_neq_0.
Qed.
(**********)
Lemma Reste_E_cv : (x,y:R) (Un_cv (Reste_E x y) R0).
Intros; Assert H := (maj_Reste_cv_R0 x y).
Unfold Un_cv in H; Unfold Un_cv; Intros; Elim (H ? H0); Intros.
Exists (max x0 (1)); Intros.
Unfold R_dist; Rewrite minus_R0.
Apply Rle_lt_trans with (maj_Reste_E x y n).
Apply Reste_E_maj.
Apply lt_le_trans with (1).
Apply lt_O_Sn.
Apply le_trans with (max x0 (1)).
Apply le_max_r.
Apply H2.
Replace (maj_Reste_E x y n) with (R_dist (maj_Reste_E x y n) R0).
Apply H1.
Unfold ge; Apply le_trans with (max x0 (1)).
Apply le_max_l.
Apply H2.
Unfold R_dist; Rewrite minus_R0; Apply Rabsolu_right.
Apply Rle_sym1; Apply Rle_trans with (Rabsolu (Reste_E x y n)).
Apply Rabsolu_pos.
Apply Reste_E_maj.
Apply lt_le_trans with (1).
Apply lt_O_Sn.
Apply le_trans with (max x0 (1)).
Apply le_max_r.
Apply H2.
Qed.
(**********)
Lemma exp_plus : (x,y:R) ``(exp (x+y))==(exp x)*(exp y)``.
Intros; Assert H0 := (E1_cvg x).
Assert H := (E1_cvg y).
Assert H1 := (E1_cvg ``x+y``).
EApply UL_sequence.
Apply H1.
Assert H2 := (CV_mult ? ? ? ? H0 H).
Assert H3 := (CV_minus ? ? ? ? H2 (Reste_E_cv x y)).
Unfold Un_cv; Unfold Un_cv in H3; Intros.
Elim (H3 ? H4); Intros.
Exists (S x0); Intros.
Rewrite <- (exp_form x y n).
Rewrite minus_R0 in H5.
Apply H5.
Unfold ge; Apply le_trans with (S x0).
Apply le_n_Sn.
Apply H6.
Apply lt_le_trans with (S x0).
Apply lt_O_Sn.
Apply H6.
Qed.
(**********)
Lemma exp_pos_pos : (x:R) ``0<x`` -> ``0<(exp x)``.
Intros; Pose An := [N:nat]``/(INR (fact N))*(pow x N)``.
Cut (Un_cv [n:nat](sum_f_R0 An n) (exp x)).
Intro; Apply Rlt_le_trans with (sum_f_R0 An O).
Unfold An; Simpl; Rewrite Rinv_R1; Rewrite Rmult_1r; Apply Rlt_R0_R1.
Apply sum_incr.
Assumption.
Intro; Unfold An; Left; Apply Rmult_lt_pos.
Apply Rlt_Rinv; Apply INR_fact_lt_0.
Apply (pow_lt ? n H).
Unfold exp; Unfold projT1; Case (exist_exp x); Intro.
Unfold exp_in; Unfold infinit_sum Un_cv; Trivial.
Qed.
(**********)
Lemma exp_pos : (x:R) ``0<(exp x)``.
Intro; Case (total_order_T R0 x); Intro.
Elim s; Intro.
Apply (exp_pos_pos ? a).
Rewrite <- b; Rewrite exp_0; Apply Rlt_R0_R1.
Replace (exp x) with ``1/(exp (-x))``.
Unfold Rdiv; Apply Rmult_lt_pos.
Apply Rlt_R0_R1.
Apply Rlt_Rinv; Apply exp_pos_pos.
Apply (Rgt_RO_Ropp ? r).
Cut ``(exp (-x))<>0``.
Intro; Unfold Rdiv; Apply r_Rmult_mult with ``(exp (-x))``.
Rewrite Rmult_1l; Rewrite <- Rinv_r_sym.
Rewrite <- exp_plus.
Rewrite Rplus_Ropp_l; Rewrite exp_0; Reflexivity.
Apply H.
Apply H.
Assert H := (exp_plus x ``-x``).
Rewrite Rplus_Ropp_r in H; Rewrite exp_0 in H.
Red; Intro; Rewrite H0 in H.
Rewrite Rmult_Or in H.
Elim R1_neq_R0; Assumption.
Qed.
(* ((exp h)-1)/h -> 0 quand h->0 *)
Lemma derivable_pt_lim_exp_0 : (derivable_pt_lim exp ``0`` ``1``).
Unfold derivable_pt_lim; Intros.
Pose fn := [N:nat][x:R]``(pow x N)/(INR (fact (S N)))``.
Cut (CVN_R fn).
Intro; Cut (x:R)(sigTT ? [l:R](Un_cv [N:nat](SP fn N x) l)).
Intro cv; Cut ((n:nat)(continuity (fn n))).
Intro; Cut (continuity (SFL fn cv)).
Intro; Unfold continuity in H1.
Assert H2 := (H1 R0).
Unfold continuity_pt in H2; Unfold continue_in in H2; Unfold limit1_in in H2; Unfold limit_in in H2; Simpl in H2; Unfold R_dist in H2.
Elim (H2 ? H); Intros alp H3.
Elim H3; Intros.
Exists (mkposreal ? H4); Intros.
Rewrite Rplus_Ol; Rewrite exp_0.
Replace ``((exp h)-1)/h`` with (SFL fn cv h).
Replace R1 with (SFL fn cv R0).
Apply H5.
Split.
Unfold D_x no_cond; Split.
Trivial.
Apply (not_sym ? ? H6).
Rewrite minus_R0; Apply H7.
Unfold SFL.
Case (cv ``0``); Intros.
EApply UL_sequence.
Apply u.
Unfold Un_cv SP.
Intros; Exists (1); Intros.
Unfold R_dist; Rewrite decomp_sum.
Rewrite (Rplus_sym (fn O R0)).
Replace (fn O R0) with R1.
Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Or.
Replace (sum_f_R0 [i:nat](fn (S i) ``0``) (pred n)) with R0.
Rewrite Rabsolu_R0; Apply H8.
Symmetry; Apply sum_eq_R0; Intros.
Unfold fn.
Simpl.
Unfold Rdiv; Do 2 Rewrite Rmult_Ol; Reflexivity.
Unfold fn; Simpl.
Unfold Rdiv; Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity.
Apply lt_le_trans with (1); [Apply lt_n_Sn | Apply H9].
Unfold SFL exp.
Unfold projT1.
Case (cv h); Case (exist_exp h); Intros.
EApply UL_sequence.
Apply u.
Unfold Un_cv; Intros.
Unfold exp_in in e.
Unfold infinit_sum in e.
Cut ``0<eps0*(Rabsolu h)``.
Intro; Elim (e ? H9); Intros N0 H10.
Exists N0; Intros.
Unfold R_dist.
Apply Rlt_monotony_contra with ``(Rabsolu h)``.
Apply Rabsolu_pos_lt; Assumption.
Rewrite <- Rabsolu_mult.
Rewrite Rminus_distr.
Replace ``h*(x-1)/h`` with ``(x-1)``.
Unfold R_dist in H10.
Replace ``h*(SP fn n h)-(x-1)`` with (Rminus (sum_f_R0 [i:nat]``/(INR (fact i))*(pow h i)`` (S n)) x).
Rewrite (Rmult_sym (Rabsolu h)).
Apply H10.
Unfold ge.
Apply le_trans with (S N0).
Apply le_n_Sn.
Apply le_n_S; Apply H11.
Rewrite decomp_sum.
Replace ``/(INR (fact O))*(pow h O)`` with R1.
Unfold Rminus.
Rewrite Ropp_distr1.
Rewrite Ropp_Ropp.
Rewrite <- (Rplus_sym ``-x``).
Rewrite <- (Rplus_sym ``-x+1``).
Rewrite Rplus_assoc; Repeat Apply Rplus_plus_r.
Replace (pred (S n)) with n; [Idtac | Reflexivity].
Unfold SP.
Rewrite scal_sum.
Apply sum_eq; Intros.
Unfold fn.
Replace (pow h (S i)) with ``h*(pow h i)``.
Unfold Rdiv; Ring.
Simpl; Ring.
Simpl; Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity.
Apply lt_O_Sn.
Unfold Rdiv.
Rewrite <- Rmult_assoc.
Symmetry; Apply Rinv_r_simpl_m.
Assumption.
Apply Rmult_lt_pos.
Apply H8.
Apply Rabsolu_pos_lt; Assumption.
Apply SFL_continuity; Assumption.
Intro; Unfold fn.
Replace [x:R]``(pow x n)/(INR (fact (S n)))`` with (div_fct (pow_fct n) (fct_cte (INR (fact (S n))))); [Idtac | Reflexivity].
Apply continuity_div.
Apply derivable_continuous; Apply (derivable_pow n).
Apply derivable_continuous; Apply derivable_const.
Intro; Unfold fct_cte; Apply INR_fact_neq_0.
Apply (CVN_R_CVS ? X).
Assert H0 := Alembert_exp.
Unfold CVN_R.
Intro; Unfold CVN_r.
Apply Specif.existT with [N:nat]``(pow r N)/(INR (fact (S N)))``.
Cut (SigT ? [l:R](Un_cv [n:nat](sum_f_R0 [k:nat](Rabsolu ``(pow r k)/(INR (fact (S k)))``) n) l)).
Intro.
Elim X; Intros.
Exists x; Intros.
Split.
Apply p.
Unfold Boule; Intros.
Rewrite minus_R0 in H1.
Unfold fn.
Unfold Rdiv; Rewrite Rabsolu_mult.
Cut ``0<(INR (fact (S n)))``.
Intro.
Rewrite (Rabsolu_right ``/(INR (fact (S n)))``).
Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (S n)))``).
Apply Rle_monotony.
Left; Apply Rlt_Rinv; Apply H2.
Rewrite <- Pow_Rabsolu.
Apply pow_maj_Rabs.
Rewrite Rabsolu_Rabsolu; Left; Apply H1.
Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply H2.
Apply INR_fact_lt_0.
Cut (r::R)<>``0``.
Intro; Apply Alembert_C2.
Intro; Apply Rabsolu_no_R0.
Unfold Rdiv; Apply prod_neq_R0.
Apply pow_nonzero; Assumption.
Apply Rinv_neq_R0; Apply INR_fact_neq_0.
Unfold Un_cv in H0.
Unfold Un_cv; Intros.
Cut ``0<eps0/r``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply (cond_pos r)]].
Elim (H0 ? H3); Intros N0 H4.
Exists N0; Intros.
Cut (ge (S n) N0).
Intro hyp_sn.
Assert H6 := (H4 ? hyp_sn).
Unfold R_dist in H6; Rewrite minus_R0 in H6.
Rewrite Rabsolu_Rabsolu in H6.
Unfold R_dist; Rewrite minus_R0.
Rewrite Rabsolu_Rabsolu.
Replace ``(Rabsolu ((pow r (S n))/(INR (fact (S (S n))))))/
(Rabsolu ((pow r n)/(INR (fact (S n)))))`` with ``r*/(INR (fact (S (S n))))*//(INR (fact (S n)))``.
Rewrite Rmult_assoc; Rewrite Rabsolu_mult.
Rewrite (Rabsolu_right r).
Apply Rlt_monotony_contra with ``/r``.
Apply Rlt_Rinv; Apply (cond_pos r).
Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
Rewrite Rmult_1l; Rewrite <- (Rmult_sym eps0).
Apply H6.
Assumption.
Apply Rle_sym1; Left; Apply (cond_pos r).
Unfold Rdiv.
Repeat Rewrite Rabsolu_mult.
Repeat Rewrite Rabsolu_Rinv.
Rewrite Rinv_Rmult.
Repeat Rewrite Rabsolu_right.
Rewrite Rinv_Rinv.
Rewrite (Rmult_sym r).
Rewrite (Rmult_sym (pow r (S n))).
Repeat Rewrite Rmult_assoc.
Apply Rmult_mult_r.
Rewrite (Rmult_sym r).
Rewrite <- Rmult_assoc; Rewrite <- (Rmult_sym (INR (fact (S n)))).
Apply Rmult_mult_r.
Simpl.
Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
Ring.
Apply pow_nonzero; Assumption.
Apply INR_fact_neq_0.
Apply Rle_sym1; Left; Apply INR_fact_lt_0.
Apply Rle_sym1; Left; Apply pow_lt; Apply (cond_pos r).
Apply Rle_sym1; Left; Apply INR_fact_lt_0.
Apply Rle_sym1; Left; Apply pow_lt; Apply (cond_pos r).
Apply Rabsolu_no_R0; Apply pow_nonzero; Assumption.
Apply Rinv_neq_R0; Apply Rabsolu_no_R0; Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Apply INR_fact_neq_0.
Unfold ge; Apply le_trans with n.
Apply H5.
Apply le_n_Sn.
Assert H1 := (cond_pos r); Red; Intro; Rewrite H2 in H1; Elim (Rlt_antirefl ? H1).
Qed.
(**********)
Lemma derivable_pt_lim_exp : (x:R) (derivable_pt_lim exp x (exp x)).
Intro; Assert H0 := derivable_pt_lim_exp_0.
Unfold derivable_pt_lim in H0; Unfold derivable_pt_lim; Intros.
Cut ``0<eps/(exp x)``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Apply H | Apply Rlt_Rinv; Apply exp_pos]].
Elim (H0 ? H1); Intros del H2.
Exists del; Intros.
Assert H5 := (H2 ? H3 H4).
Rewrite Rplus_Ol in H5; Rewrite exp_0 in H5.
Replace ``((exp (x+h))-(exp x))/h-(exp x)`` with ``(exp x)*(((exp h)-1)/h-1)``.
Rewrite Rabsolu_mult; Rewrite (Rabsolu_right (exp x)).
Apply Rlt_monotony_contra with ``/(exp x)``.
Apply Rlt_Rinv; Apply exp_pos.
Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
Rewrite Rmult_1l; Rewrite <- (Rmult_sym eps).
Apply H5.
Assert H6 := (exp_pos x); Red; Intro; Rewrite H7 in H6; Elim (Rlt_antirefl ? H6).
Apply Rle_sym1; Left; Apply exp_pos.
Rewrite Rminus_distr.
Rewrite Rmult_1r; Unfold Rdiv; Rewrite <- Rmult_assoc; Rewrite Rminus_distr.
Rewrite Rmult_1r; Rewrite exp_plus; Reflexivity.
Qed.
|
