Step | Hyp | Ref
| Expression |
1 | | cvgratz.m |
. . . . 5
โข (๐ โ ๐ โ โค) |
2 | 1 | adantr 276 |
. . . 4
โข ((๐ โง 1 โค ๐) โ ๐ โ โค) |
3 | | fveq2 5515 |
. . . . . 6
โข (๐ = ๐ฅ โ (๐นโ๐) = (๐นโ๐ฅ)) |
4 | 3 | eleq1d 2246 |
. . . . 5
โข (๐ = ๐ฅ โ ((๐นโ๐) โ โ โ (๐นโ๐ฅ) โ โ)) |
5 | | cvgratz.6 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) |
6 | 5 | ralrimiva 2550 |
. . . . . 6
โข (๐ โ โ๐ โ ๐ (๐นโ๐) โ โ) |
7 | 6 | ad2antrr 488 |
. . . . 5
โข (((๐ โง 1 โค ๐) โง ๐ฅ โ (โคโฅโ๐)) โ โ๐ โ ๐ (๐นโ๐) โ โ) |
8 | | cvgratz.1 |
. . . . . . . 8
โข ๐ =
(โคโฅโ๐) |
9 | 8 | eleq2i 2244 |
. . . . . . 7
โข (๐ฅ โ ๐ โ ๐ฅ โ (โคโฅโ๐)) |
10 | 9 | biimpri 133 |
. . . . . 6
โข (๐ฅ โ
(โคโฅโ๐) โ ๐ฅ โ ๐) |
11 | 10 | adantl 277 |
. . . . 5
โข (((๐ โง 1 โค ๐) โง ๐ฅ โ (โคโฅโ๐)) โ ๐ฅ โ ๐) |
12 | 4, 7, 11 | rspcdva 2846 |
. . . 4
โข (((๐ โง 1 โค ๐) โง ๐ฅ โ (โคโฅโ๐)) โ (๐นโ๐ฅ) โ โ) |
13 | | eluzelz 9536 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
14 | 13 | adantl 277 |
. . . . . . 7
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โค) |
15 | | 1red 7971 |
. . . . . . . 8
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ 1 โ
โ) |
16 | 1 | zred 9374 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
17 | 16 | ad2antrr 488 |
. . . . . . . 8
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
18 | 14 | zred 9374 |
. . . . . . . 8
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
19 | | simplr 528 |
. . . . . . . 8
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ 1 โค ๐) |
20 | | eluzle 9539 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ๐) โ ๐ โค ๐) |
21 | 20 | adantl 277 |
. . . . . . . 8
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ ๐ โค ๐) |
22 | 15, 17, 18, 19, 21 | letrd 8080 |
. . . . . . 7
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ 1 โค ๐) |
23 | | elnnz1 9275 |
. . . . . . 7
โข (๐ โ โ โ (๐ โ โค โง 1 โค
๐)) |
24 | 14, 22, 23 | sylanbrc 417 |
. . . . . 6
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
25 | | elnnuz 9563 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
26 | | fveq2 5515 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐นโ๐) = (๐นโ๐)) |
27 | 26 | eleq1d 2246 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐นโ๐) โ โ โ (๐นโ๐) โ โ)) |
28 | | uzid 9541 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
29 | 1, 28 | syl 14 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ (โคโฅโ๐)) |
30 | 29, 8 | eleqtrrdi 2271 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ ๐) |
31 | 27, 6, 30 | rspcdva 2846 |
. . . . . . . . . . 11
โข (๐ โ (๐นโ๐) โ โ) |
32 | 31 | ad3antrrr 492 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ๐ < ๐) โ (๐นโ๐) โ โ) |
33 | | cvgratz.3 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ด โ โ) |
34 | | cvgratz.gt0 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 < ๐ด) |
35 | 33, 34 | elrpd 9692 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ด โ
โ+) |
36 | 35 | ad3antrrr 492 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ๐ < ๐) โ ๐ด โ
โ+) |
37 | 2 | adantr 276 |
. . . . . . . . . . . . . 14
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โ ๐ โ
โค) |
38 | 37 | adantr 276 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ๐ < ๐) โ ๐ โ โค) |
39 | 25 | biimpri 133 |
. . . . . . . . . . . . . . . 16
โข (๐ โ
(โคโฅโ1) โ ๐ โ โ) |
40 | 39 | adantl 277 |
. . . . . . . . . . . . . . 15
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โ ๐ โ
โ) |
41 | 40 | nnzd 9373 |
. . . . . . . . . . . . . 14
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โ ๐ โ
โค) |
42 | 41 | adantr 276 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ๐ < ๐) โ ๐ โ โค) |
43 | 38, 42 | zsubcld 9379 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ๐ < ๐) โ (๐ โ ๐) โ โค) |
44 | 36, 43 | rpexpcld 10677 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ๐ < ๐) โ (๐ดโ(๐ โ ๐)) โ
โ+) |
45 | 44 | rpcnd 9697 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ๐ < ๐) โ (๐ดโ(๐ โ ๐)) โ โ) |
46 | 44 | rpap0d 9701 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ๐ < ๐) โ (๐ดโ(๐ โ ๐)) # 0) |
47 | 32, 45, 46 | divclapd 8746 |
. . . . . . . . 9
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ๐ < ๐) โ ((๐นโ๐) / (๐ดโ(๐ โ ๐))) โ โ) |
48 | | simplll 533 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ยฌ ๐ < ๐) โ ๐) |
49 | 37 | adantr 276 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ยฌ ๐ < ๐) โ ๐ โ โค) |
50 | 41 | adantr 276 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ยฌ ๐ < ๐) โ ๐ โ โค) |
51 | 16 | ad3antrrr 492 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ยฌ ๐ < ๐) โ ๐ โ โ) |
52 | 50 | zred 9374 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ยฌ ๐ < ๐) โ ๐ โ โ) |
53 | | simpr 110 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ยฌ ๐ < ๐) โ ยฌ ๐ < ๐) |
54 | 51, 52, 53 | nltled 8077 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ยฌ ๐ < ๐) โ ๐ โค ๐) |
55 | | eluz2 9533 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ๐) โ (๐ โ โค โง ๐ โ โค โง ๐ โค ๐)) |
56 | 49, 50, 54, 55 | syl3anbrc 1181 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ยฌ ๐ < ๐) โ ๐ โ (โคโฅโ๐)) |
57 | 56, 8 | eleqtrrdi 2271 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ยฌ ๐ < ๐) โ ๐ โ ๐) |
58 | 48, 57, 5 | syl2anc 411 |
. . . . . . . . 9
โข ((((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โง ยฌ ๐ < ๐) โ (๐นโ๐) โ โ) |
59 | | zdclt 9329 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ
DECID ๐ <
๐) |
60 | 41, 37, 59 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โ DECID ๐ < ๐) |
61 | 47, 58, 60 | ifcldadc 3563 |
. . . . . . . 8
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) โ โ) |
62 | 25, 61 | sylan2b 287 |
. . . . . . 7
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) โ โ) |
63 | 24, 62 | syldan 282 |
. . . . . 6
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) โ โ) |
64 | | breq1 4006 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ < ๐ โ ๐ < ๐)) |
65 | | oveq2 5882 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ โ ๐) = (๐ โ ๐)) |
66 | 65 | oveq2d 5890 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ดโ(๐ โ ๐)) = (๐ดโ(๐ โ ๐))) |
67 | 66 | oveq2d 5890 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐นโ๐) / (๐ดโ(๐ โ ๐))) = ((๐นโ๐) / (๐ดโ(๐ โ ๐)))) |
68 | | fveq2 5515 |
. . . . . . . 8
โข (๐ = ๐ โ (๐นโ๐) = (๐นโ๐)) |
69 | 64, 67, 68 | ifbieq12d 3560 |
. . . . . . 7
โข (๐ = ๐ โ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) = if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))) |
70 | | eqid 2177 |
. . . . . . 7
โข (๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))) = (๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))) |
71 | 69, 70 | fvmptg 5592 |
. . . . . 6
โข ((๐ โ โ โง if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) โ โ) โ ((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ๐) = if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))) |
72 | 24, 63, 71 | syl2anc 411 |
. . . . 5
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ ((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ๐) = if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))) |
73 | 17, 18, 21 | lensymd 8078 |
. . . . . 6
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ ยฌ ๐ < ๐) |
74 | 73 | iffalsed 3544 |
. . . . 5
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) = (๐นโ๐)) |
75 | 72, 74 | eqtr2d 2211 |
. . . 4
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐) = ((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ๐)) |
76 | | addcl 7935 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ + ๐ฆ) โ โ) |
77 | 76 | adantl 277 |
. . . 4
โข (((๐ โง 1 โค ๐) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ + ๐ฆ) โ โ) |
78 | 2, 12, 75, 77 | seq3feq 10471 |
. . 3
โข ((๐ โง 1 โค ๐) โ seq๐( + , ๐น) = seq๐( + , (๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
79 | 33 | adantr 276 |
. . . . 5
โข ((๐ โง 1 โค ๐) โ ๐ด โ โ) |
80 | | cvgratz.4 |
. . . . . 6
โข (๐ โ ๐ด < 1) |
81 | 80 | adantr 276 |
. . . . 5
โข ((๐ โง 1 โค ๐) โ ๐ด < 1) |
82 | 34 | adantr 276 |
. . . . 5
โข ((๐ โง 1 โค ๐) โ 0 < ๐ด) |
83 | 71 | eleq1d 2246 |
. . . . . . . 8
โข ((๐ โ โ โง if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) โ โ) โ (((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ๐) โ โ โ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) โ โ)) |
84 | 40, 61, 83 | syl2anc 411 |
. . . . . . 7
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โ (((๐ โ โ
โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ๐) โ โ โ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) โ โ)) |
85 | 61, 84 | mpbird 167 |
. . . . . 6
โข (((๐ โง 1 โค ๐) โง ๐ โ (โคโฅโ1))
โ ((๐ โ โ
โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ๐) โ โ) |
86 | 25, 85 | sylan2b 287 |
. . . . 5
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ๐) โ โ) |
87 | 31 | ad3antrrr 492 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (๐นโ๐) โ โ) |
88 | 35 | ad3antrrr 492 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ ๐ด โ
โ+) |
89 | 2 | ad2antrr 488 |
. . . . . . . . . . . . . 14
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ ๐ โ โค) |
90 | 25, 41 | sylan2b 287 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ๐ โ โค) |
91 | 90 | adantr 276 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ ๐ โ โค) |
92 | 91 | peano2zd 9377 |
. . . . . . . . . . . . . 14
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (๐ + 1) โ โค) |
93 | 89, 92 | zsubcld 9379 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (๐ โ (๐ + 1)) โ โค) |
94 | 88, 93 | rpexpcld 10677 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (๐ดโ(๐ โ (๐ + 1))) โ
โ+) |
95 | 94 | rpcnd 9697 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (๐ดโ(๐ โ (๐ + 1))) โ โ) |
96 | 94 | rpap0d 9701 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (๐ดโ(๐ โ (๐ + 1))) # 0) |
97 | 87, 95, 96 | divclapd 8746 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))) โ โ) |
98 | | fveq2 5515 |
. . . . . . . . . . . 12
โข (๐ = (๐ + 1) โ (๐นโ๐) = (๐นโ(๐ + 1))) |
99 | 98 | eleq1d 2246 |
. . . . . . . . . . 11
โข (๐ = (๐ + 1) โ ((๐นโ๐) โ โ โ (๐นโ(๐ + 1)) โ โ)) |
100 | | fveq2 5515 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (๐นโ๐) = (๐นโ๐)) |
101 | 100 | eleq1d 2246 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((๐นโ๐) โ โ โ (๐นโ๐) โ โ)) |
102 | 101 | cbvralv 2703 |
. . . . . . . . . . . . 13
โข
(โ๐ โ
๐ (๐นโ๐) โ โ โ โ๐ โ ๐ (๐นโ๐) โ โ) |
103 | 6, 102 | sylib 122 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ โ ๐ (๐นโ๐) โ โ) |
104 | 103 | ad3antrrr 492 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ยฌ (๐ + 1) < ๐) โ โ๐ โ ๐ (๐นโ๐) โ โ) |
105 | 2 | ad2antrr 488 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ยฌ (๐ + 1) < ๐) โ ๐ โ โค) |
106 | | peano2nn 8930 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (๐ + 1) โ
โ) |
107 | 106 | adantl 277 |
. . . . . . . . . . . . . . 15
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (๐ + 1) โ โ) |
108 | 107 | nnzd 9373 |
. . . . . . . . . . . . . 14
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (๐ + 1) โ โค) |
109 | 108 | adantr 276 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ยฌ (๐ + 1) < ๐) โ (๐ + 1) โ โค) |
110 | 16 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ยฌ (๐ + 1) < ๐) โ ๐ โ โ) |
111 | 107 | nnred 8931 |
. . . . . . . . . . . . . . 15
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (๐ + 1) โ โ) |
112 | 111 | adantr 276 |
. . . . . . . . . . . . . 14
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ยฌ (๐ + 1) < ๐) โ (๐ + 1) โ โ) |
113 | | simpr 110 |
. . . . . . . . . . . . . 14
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ยฌ (๐ + 1) < ๐) โ ยฌ (๐ + 1) < ๐) |
114 | 110, 112,
113 | nltled 8077 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ยฌ (๐ + 1) < ๐) โ ๐ โค (๐ + 1)) |
115 | | eluz2 9533 |
. . . . . . . . . . . . 13
โข ((๐ + 1) โ
(โคโฅโ๐) โ (๐ โ โค โง (๐ + 1) โ โค โง ๐ โค (๐ + 1))) |
116 | 105, 109,
114, 115 | syl3anbrc 1181 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ยฌ (๐ + 1) < ๐) โ (๐ + 1) โ
(โคโฅโ๐)) |
117 | 116, 8 | eleqtrrdi 2271 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ยฌ (๐ + 1) < ๐) โ (๐ + 1) โ ๐) |
118 | 99, 104, 117 | rspcdva 2846 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ยฌ (๐ + 1) < ๐) โ (๐นโ(๐ + 1)) โ โ) |
119 | 2 | adantr 276 |
. . . . . . . . . . 11
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ๐ โ โค) |
120 | | zdclt 9329 |
. . . . . . . . . . 11
โข (((๐ + 1) โ โค โง ๐ โ โค) โ
DECID (๐ +
1) < ๐) |
121 | 108, 119,
120 | syl2anc 411 |
. . . . . . . . . 10
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ DECID
(๐ + 1) < ๐) |
122 | 97, 118, 121 | ifcldadc 3563 |
. . . . . . . . 9
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ if((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1))) โ โ) |
123 | 122 | abscld 11189 |
. . . . . . . 8
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (absโif((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) โ โ) |
124 | 16 | recnd 7985 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ โ) |
125 | 124 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ๐ โ โ) |
126 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ๐ โ โ) |
127 | 126 | nncnd 8932 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ๐ โ โ) |
128 | | 1cnd 7972 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ 1 โ
โ) |
129 | 125, 127,
128 | subsub4d 8298 |
. . . . . . . . . . . . . . 15
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ((๐ โ ๐) โ 1) = (๐ โ (๐ + 1))) |
130 | 129 | oveq2d 5890 |
. . . . . . . . . . . . . 14
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (๐ดโ((๐ โ ๐) โ 1)) = (๐ดโ(๐ โ (๐ + 1)))) |
131 | 33 | recnd 7985 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ด โ โ) |
132 | 131 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ๐ด โ โ) |
133 | 33, 34 | gt0ap0d 8585 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ด # 0) |
134 | 133 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ๐ด # 0) |
135 | 119, 90 | zsubcld 9379 |
. . . . . . . . . . . . . . 15
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (๐ โ ๐) โ โค) |
136 | 132, 134,
135 | expm1apd 10663 |
. . . . . . . . . . . . . 14
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (๐ดโ((๐ โ ๐) โ 1)) = ((๐ดโ(๐ โ ๐)) / ๐ด)) |
137 | 130, 136 | eqtr3d 2212 |
. . . . . . . . . . . . 13
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (๐ดโ(๐ โ (๐ + 1))) = ((๐ดโ(๐ โ ๐)) / ๐ด)) |
138 | 137 | oveq2d 5890 |
. . . . . . . . . . . 12
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))) = ((๐นโ๐) / ((๐ดโ(๐ โ ๐)) / ๐ด))) |
139 | 138 | adantr 276 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))) = ((๐นโ๐) / ((๐ดโ(๐ โ ๐)) / ๐ด))) |
140 | | simpr 110 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (๐ + 1) < ๐) |
141 | 140 | iftrued 3541 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ if((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1))) = ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1))))) |
142 | 126 | nnred 8931 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ๐ โ โ) |
143 | 142 | adantr 276 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ ๐ โ โ) |
144 | | peano2re 8092 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (๐ + 1) โ
โ) |
145 | 143, 144 | syl 14 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (๐ + 1) โ โ) |
146 | 16 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ ๐ โ โ) |
147 | 143 | ltp1d 8886 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ ๐ < (๐ + 1)) |
148 | 143, 145,
146, 147, 140 | lttrd 8082 |
. . . . . . . . . . . . . 14
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ ๐ < ๐) |
149 | 148 | iftrued 3541 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) = ((๐นโ๐) / (๐ดโ(๐ โ ๐)))) |
150 | 149 | oveq2d 5890 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (๐ด ยท if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))) = (๐ด ยท ((๐นโ๐) / (๐ดโ(๐ โ ๐))))) |
151 | 31 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (๐นโ๐) โ โ) |
152 | 132, 134,
135 | expclzapd 10658 |
. . . . . . . . . . . . . . 15
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (๐ดโ(๐ โ ๐)) โ โ) |
153 | 132, 134,
135 | expap0d 10659 |
. . . . . . . . . . . . . . 15
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (๐ดโ(๐ โ ๐)) # 0) |
154 | 151, 152,
132, 153, 134 | divdivap2d 8779 |
. . . . . . . . . . . . . 14
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ((๐นโ๐) / ((๐ดโ(๐ โ ๐)) / ๐ด)) = (((๐นโ๐) ยท ๐ด) / (๐ดโ(๐ โ ๐)))) |
155 | 151, 132 | mulcomd 7978 |
. . . . . . . . . . . . . . 15
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ((๐นโ๐) ยท ๐ด) = (๐ด ยท (๐นโ๐))) |
156 | 155 | oveq1d 5889 |
. . . . . . . . . . . . . 14
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (((๐นโ๐) ยท ๐ด) / (๐ดโ(๐ โ ๐))) = ((๐ด ยท (๐นโ๐)) / (๐ดโ(๐ โ ๐)))) |
157 | 132, 151,
152, 153 | divassapd 8782 |
. . . . . . . . . . . . . 14
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ((๐ด ยท (๐นโ๐)) / (๐ดโ(๐ โ ๐))) = (๐ด ยท ((๐นโ๐) / (๐ดโ(๐ โ ๐))))) |
158 | 154, 156,
157 | 3eqtrd 2214 |
. . . . . . . . . . . . 13
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ((๐นโ๐) / ((๐ดโ(๐ โ ๐)) / ๐ด)) = (๐ด ยท ((๐นโ๐) / (๐ดโ(๐ โ ๐))))) |
159 | 158 | adantr 276 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ ((๐นโ๐) / ((๐ดโ(๐ โ ๐)) / ๐ด)) = (๐ด ยท ((๐นโ๐) / (๐ดโ(๐ โ ๐))))) |
160 | 150, 159 | eqtr4d 2213 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (๐ด ยท if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))) = ((๐นโ๐) / ((๐ดโ(๐ โ ๐)) / ๐ด))) |
161 | 139, 141,
160 | 3eqtr4d 2220 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ if((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1))) = (๐ด ยท if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) |
162 | 161 | fveq2d 5519 |
. . . . . . . . 9
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (absโif((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) = (absโ(๐ด ยท if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
163 | 132, 62 | absmuld 11202 |
. . . . . . . . . 10
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (absโ(๐ด ยท if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) = ((absโ๐ด) ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
164 | 163 | adantr 276 |
. . . . . . . . 9
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (absโ(๐ด ยท if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) = ((absโ๐ด) ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
165 | 35 | rpge0d 9699 |
. . . . . . . . . . . 12
โข (๐ โ 0 โค ๐ด) |
166 | 33, 165 | absidd 11175 |
. . . . . . . . . . 11
โข (๐ โ (absโ๐ด) = ๐ด) |
167 | 166 | oveq1d 5889 |
. . . . . . . . . 10
โข (๐ โ ((absโ๐ด) ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) = (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
168 | 167 | ad3antrrr 492 |
. . . . . . . . 9
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ ((absโ๐ด) ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) = (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
169 | 162, 164,
168 | 3eqtrd 2214 |
. . . . . . . 8
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (absโif((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) = (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
170 | | eqle 8048 |
. . . . . . . 8
โข
(((absโif((๐ +
1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) โ โ โง
(absโif((๐ + 1) <
๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) = (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) โ (absโif((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) โค (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
171 | 123, 169,
170 | syl2an2r 595 |
. . . . . . 7
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) < ๐) โ (absโif((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) โค (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
172 | 16 | ad2antrr 488 |
. . . . . . . . . . . . . 14
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ๐ โ โ) |
173 | 111, 172 | lttri3d 8071 |
. . . . . . . . . . . . 13
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ((๐ + 1) = ๐ โ (ยฌ (๐ + 1) < ๐ โง ยฌ ๐ < (๐ + 1)))) |
174 | 173 | simprbda 383 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ ยฌ (๐ + 1) < ๐) |
175 | 174 | iffalsed 3544 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ if((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1))) = (๐นโ(๐ + 1))) |
176 | | simpr 110 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (๐ + 1) = ๐) |
177 | 176 | fveq2d 5519 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (๐นโ(๐ + 1)) = (๐นโ๐)) |
178 | 175, 177 | eqtrd 2210 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ if((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1))) = (๐นโ๐)) |
179 | 178 | fveq2d 5519 |
. . . . . . . . 9
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (absโif((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) = (absโ(๐นโ๐))) |
180 | 142 | adantr 276 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ ๐ โ โ) |
181 | 180 | ltp1d 8886 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ ๐ < (๐ + 1)) |
182 | | breq2 4007 |
. . . . . . . . . . . . . . . 16
โข ((๐ + 1) = ๐ โ (๐ < (๐ + 1) โ ๐ < ๐)) |
183 | 182 | adantl 277 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (๐ < (๐ + 1) โ ๐ < ๐)) |
184 | 181, 183 | mpbid 147 |
. . . . . . . . . . . . . 14
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ ๐ < ๐) |
185 | 184 | iftrued 3541 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) = ((๐นโ๐) / (๐ดโ(๐ โ ๐)))) |
186 | 176 | oveq1d 5889 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ ((๐ + 1) โ ๐) = (๐ โ ๐)) |
187 | 127 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ ๐ โ โ) |
188 | | 1cnd 7972 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ 1 โ โ) |
189 | 187, 188 | pncan2d 8269 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ ((๐ + 1) โ ๐) = 1) |
190 | 186, 189 | eqtr3d 2212 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (๐ โ ๐) = 1) |
191 | 190 | oveq2d 5890 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (๐ดโ(๐ โ ๐)) = (๐ดโ1)) |
192 | 132 | adantr 276 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ ๐ด โ โ) |
193 | 192 | exp1d 10648 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (๐ดโ1) = ๐ด) |
194 | 191, 193 | eqtrd 2210 |
. . . . . . . . . . . . . 14
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (๐ดโ(๐ โ ๐)) = ๐ด) |
195 | 194 | oveq2d 5890 |
. . . . . . . . . . . . 13
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ ((๐นโ๐) / (๐ดโ(๐ โ ๐))) = ((๐นโ๐) / ๐ด)) |
196 | 185, 195 | eqtrd 2210 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) = ((๐นโ๐) / ๐ด)) |
197 | 196 | oveq2d 5890 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (๐ด ยท if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))) = (๐ด ยท ((๐นโ๐) / ๐ด))) |
198 | 31, 131, 133 | divcanap2d 8748 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด ยท ((๐นโ๐) / ๐ด)) = (๐นโ๐)) |
199 | 198 | ad3antrrr 492 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (๐ด ยท ((๐นโ๐) / ๐ด)) = (๐นโ๐)) |
200 | 197, 199 | eqtrd 2210 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (๐ด ยท if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))) = (๐นโ๐)) |
201 | 200 | fveq2d 5519 |
. . . . . . . . 9
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (absโ(๐ด ยท if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) = (absโ(๐นโ๐))) |
202 | 167 | ad2antrr 488 |
. . . . . . . . . . 11
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ((absโ๐ด) ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) = (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
203 | 163, 202 | eqtrd 2210 |
. . . . . . . . . 10
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (absโ(๐ด ยท if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) = (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
204 | 203 | adantr 276 |
. . . . . . . . 9
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (absโ(๐ด ยท if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) = (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
205 | 179, 201,
204 | 3eqtr2d 2216 |
. . . . . . . 8
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (absโif((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) = (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
206 | 123, 205,
170 | syl2an2r 595 |
. . . . . . 7
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง (๐ + 1) = ๐) โ (absโif((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) โค (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
207 | | simplll 533 |
. . . . . . . . 9
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ ๐) |
208 | 119 | adantr 276 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ ๐ โ โค) |
209 | 90 | adantr 276 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ ๐ โ โค) |
210 | | simpr 110 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ ๐ < (๐ + 1)) |
211 | | zleltp1 9307 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โค ๐ โ ๐ < (๐ + 1))) |
212 | 119, 209,
211 | syl2an2r 595 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ (๐ โค ๐ โ ๐ < (๐ + 1))) |
213 | 210, 212 | mpbird 167 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ ๐ โค ๐) |
214 | 208, 209,
213, 55 | syl3anbrc 1181 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ ๐ โ (โคโฅโ๐)) |
215 | 214, 8 | eleqtrrdi 2271 |
. . . . . . . . 9
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ ๐ โ ๐) |
216 | | cvgratz.7 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ (absโ(๐นโ(๐ + 1))) โค (๐ด ยท (absโ(๐นโ๐)))) |
217 | 207, 215,
216 | syl2anc 411 |
. . . . . . . 8
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ (absโ(๐นโ(๐ + 1))) โค (๐ด ยท (absโ(๐นโ๐)))) |
218 | 172 | adantr 276 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ ๐ โ โ) |
219 | 111 | adantr 276 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ (๐ + 1) โ โ) |
220 | 218, 219,
210 | ltnsymd 8076 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ ยฌ (๐ + 1) < ๐) |
221 | 220 | iffalsed 3544 |
. . . . . . . . 9
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ if((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1))) = (๐นโ(๐ + 1))) |
222 | 221 | fveq2d 5519 |
. . . . . . . 8
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ (absโif((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) = (absโ(๐นโ(๐ + 1)))) |
223 | 142 | adantr 276 |
. . . . . . . . . . . 12
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ ๐ โ โ) |
224 | 218, 223,
213 | lensymd 8078 |
. . . . . . . . . . 11
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ ยฌ ๐ < ๐) |
225 | 224 | iffalsed 3544 |
. . . . . . . . . 10
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) = (๐นโ๐)) |
226 | 225 | fveq2d 5519 |
. . . . . . . . 9
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))) = (absโ(๐นโ๐))) |
227 | 226 | oveq2d 5890 |
. . . . . . . 8
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) = (๐ด ยท (absโ(๐นโ๐)))) |
228 | 217, 222,
227 | 3brtr4d 4035 |
. . . . . . 7
โข ((((๐ โง 1 โค ๐) โง ๐ โ โ) โง ๐ < (๐ + 1)) โ (absโif((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) โค (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
229 | | ztri3or 9295 |
. . . . . . . 8
โข (((๐ + 1) โ โค โง ๐ โ โค) โ ((๐ + 1) < ๐ โจ (๐ + 1) = ๐ โจ ๐ < (๐ + 1))) |
230 | 108, 119,
229 | syl2anc 411 |
. . . . . . 7
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ((๐ + 1) < ๐ โจ (๐ + 1) = ๐ โจ ๐ < (๐ + 1))) |
231 | 171, 206,
228, 230 | mpjao3dan 1307 |
. . . . . 6
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (absโif((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) โค (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
232 | | breq1 4006 |
. . . . . . . . . 10
โข (๐ = (๐ + 1) โ (๐ < ๐ โ (๐ + 1) < ๐)) |
233 | | oveq2 5882 |
. . . . . . . . . . . 12
โข (๐ = (๐ + 1) โ (๐ โ ๐) = (๐ โ (๐ + 1))) |
234 | 233 | oveq2d 5890 |
. . . . . . . . . . 11
โข (๐ = (๐ + 1) โ (๐ดโ(๐ โ ๐)) = (๐ดโ(๐ โ (๐ + 1)))) |
235 | 234 | oveq2d 5890 |
. . . . . . . . . 10
โข (๐ = (๐ + 1) โ ((๐นโ๐) / (๐ดโ(๐ โ ๐))) = ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1))))) |
236 | | fveq2 5515 |
. . . . . . . . . 10
โข (๐ = (๐ + 1) โ (๐นโ๐) = (๐นโ(๐ + 1))) |
237 | 232, 235,
236 | ifbieq12d 3560 |
. . . . . . . . 9
โข (๐ = (๐ + 1) โ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)) = if((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) |
238 | 237, 70 | fvmptg 5592 |
. . . . . . . 8
โข (((๐ + 1) โ โ โง
if((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1))) โ โ) โ ((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ(๐ + 1)) = if((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) |
239 | 107, 122,
238 | syl2anc 411 |
. . . . . . 7
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ(๐ + 1)) = if((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1)))) |
240 | 239 | fveq2d 5519 |
. . . . . 6
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (absโ((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ(๐ + 1))) = (absโif((๐ + 1) < ๐, ((๐นโ๐) / (๐ดโ(๐ โ (๐ + 1)))), (๐นโ(๐ + 1))))) |
241 | 126, 62, 71 | syl2anc 411 |
. . . . . . . 8
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ ((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ๐) = if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))) |
242 | 241 | fveq2d 5519 |
. . . . . . 7
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (absโ((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ๐)) = (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) |
243 | 242 | oveq2d 5890 |
. . . . . 6
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (๐ด ยท (absโ((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ๐))) = (๐ด ยท (absโif(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐))))) |
244 | 231, 240,
243 | 3brtr4d 4035 |
. . . . 5
โข (((๐ โง 1 โค ๐) โง ๐ โ โ) โ (absโ((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ(๐ + 1))) โค (๐ด ยท (absโ((๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))โ๐)))) |
245 | 79, 81, 82, 86, 244 | cvgratnn 11538 |
. . . 4
โข ((๐ โง 1 โค ๐) โ seq1( + , (๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) โ dom โ ) |
246 | | eqid 2177 |
. . . . 5
โข
(โคโฅโ1) =
(โคโฅโ1) |
247 | | 1zzd 9279 |
. . . . . 6
โข ((๐ โง 1 โค ๐) โ 1 โ โค) |
248 | | simpr 110 |
. . . . . 6
โข ((๐ โง 1 โค ๐) โ 1 โค ๐) |
249 | | eluz2 9533 |
. . . . . 6
โข (๐ โ
(โคโฅโ1) โ (1 โ โค โง ๐ โ โค โง 1 โค
๐)) |
250 | 247, 2, 248, 249 | syl3anbrc 1181 |
. . . . 5
โข ((๐ โง 1 โค ๐) โ ๐ โ
(โคโฅโ1)) |
251 | 246, 250,
85 | iserex 11346 |
. . . 4
โข ((๐ โง 1 โค ๐) โ (seq1( + , (๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) โ dom โ โ seq๐( + , (๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) โ dom โ )) |
252 | 245, 251 | mpbid 147 |
. . 3
โข ((๐ โง 1 โค ๐) โ seq๐( + , (๐ โ โ โฆ if(๐ < ๐, ((๐นโ๐) / (๐ดโ(๐ โ ๐))), (๐นโ๐)))) โ dom โ ) |
253 | 78, 252 | eqeltrd 2254 |
. 2
โข ((๐ โง 1 โค ๐) โ seq๐( + , ๐น) โ dom โ ) |
254 | 33 | adantr 276 |
. . . 4
โข ((๐ โง ๐ โค 1) โ ๐ด โ โ) |
255 | 80 | adantr 276 |
. . . 4
โข ((๐ โง ๐ โค 1) โ ๐ด < 1) |
256 | 34 | adantr 276 |
. . . 4
โข ((๐ โง ๐ โค 1) โ 0 < ๐ด) |
257 | 1 | adantr 276 |
. . . . . . 7
โข ((๐ โง ๐ โค 1) โ ๐ โ โค) |
258 | 257 | adantr 276 |
. . . . . 6
โข (((๐ โง ๐ โค 1) โง ๐ โ โ) โ ๐ โ โค) |
259 | | nnz 9271 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โค) |
260 | 259 | adantl 277 |
. . . . . 6
โข (((๐ โง ๐ โค 1) โง ๐ โ โ) โ ๐ โ โค) |
261 | 258 | zred 9374 |
. . . . . . 7
โข (((๐ โง ๐ โค 1) โง ๐ โ โ) โ ๐ โ โ) |
262 | | 1red 7971 |
. . . . . . 7
โข (((๐ โง ๐ โค 1) โง ๐ โ โ) โ 1 โ
โ) |
263 | 260 | zred 9374 |
. . . . . . 7
โข (((๐ โง ๐ โค 1) โง ๐ โ โ) โ ๐ โ โ) |
264 | | simplr 528 |
. . . . . . 7
โข (((๐ โง ๐ โค 1) โง ๐ โ โ) โ ๐ โค 1) |
265 | | nnge1 8941 |
. . . . . . . 8
โข (๐ โ โ โ 1 โค
๐) |
266 | 265 | adantl 277 |
. . . . . . 7
โข (((๐ โง ๐ โค 1) โง ๐ โ โ) โ 1 โค ๐) |
267 | 261, 262,
263, 264, 266 | letrd 8080 |
. . . . . 6
โข (((๐ โง ๐ โค 1) โง ๐ โ โ) โ ๐ โค ๐) |
268 | 258, 260,
267, 55 | syl3anbrc 1181 |
. . . . 5
โข (((๐ โง ๐ โค 1) โง ๐ โ โ) โ ๐ โ (โคโฅโ๐)) |
269 | 8 | eleq2i 2244 |
. . . . . . 7
โข (๐ โ ๐ โ ๐ โ (โคโฅโ๐)) |
270 | 269, 5 | sylan2br 288 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐) โ โ) |
271 | 270 | adantlr 477 |
. . . . 5
โข (((๐ โง ๐ โค 1) โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐) โ โ) |
272 | 268, 271 | syldan 282 |
. . . 4
โข (((๐ โง ๐ โค 1) โง ๐ โ โ) โ (๐นโ๐) โ โ) |
273 | 269, 216 | sylan2br 288 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (absโ(๐นโ(๐ + 1))) โค (๐ด ยท (absโ(๐นโ๐)))) |
274 | 273 | adantlr 477 |
. . . . 5
โข (((๐ โง ๐ โค 1) โง ๐ โ (โคโฅโ๐)) โ (absโ(๐นโ(๐ + 1))) โค (๐ด ยท (absโ(๐นโ๐)))) |
275 | 268, 274 | syldan 282 |
. . . 4
โข (((๐ โง ๐ โค 1) โง ๐ โ โ) โ (absโ(๐นโ(๐ + 1))) โค (๐ด ยท (absโ(๐นโ๐)))) |
276 | 254, 255,
256, 272, 275 | cvgratnn 11538 |
. . 3
โข ((๐ โง ๐ โค 1) โ seq1( + , ๐น) โ dom โ ) |
277 | | eqid 2177 |
. . . 4
โข
(โคโฅโ๐) = (โคโฅโ๐) |
278 | | 1zzd 9279 |
. . . . 5
โข ((๐ โง ๐ โค 1) โ 1 โ
โค) |
279 | | simpr 110 |
. . . . 5
โข ((๐ โง ๐ โค 1) โ ๐ โค 1) |
280 | | eluz2 9533 |
. . . . 5
โข (1 โ
(โคโฅโ๐) โ (๐ โ โค โง 1 โ โค โง
๐ โค 1)) |
281 | 257, 278,
279, 280 | syl3anbrc 1181 |
. . . 4
โข ((๐ โง ๐ โค 1) โ 1 โ
(โคโฅโ๐)) |
282 | 277, 281,
271 | iserex 11346 |
. . 3
โข ((๐ โง ๐ โค 1) โ (seq๐( + , ๐น) โ dom โ โ seq1( + , ๐น) โ dom โ
)) |
283 | 276, 282 | mpbird 167 |
. 2
โข ((๐ โง ๐ โค 1) โ seq๐( + , ๐น) โ dom โ ) |
284 | | 1z 9278 |
. . 3
โข 1 โ
โค |
285 | | zletric 9296 |
. . 3
โข ((1
โ โค โง ๐
โ โค) โ (1 โค ๐ โจ ๐ โค 1)) |
286 | 284, 1, 285 | sylancr 414 |
. 2
โข (๐ โ (1 โค ๐ โจ ๐ โค 1)) |
287 | 253, 283,
286 | mpjaodan 798 |
1
โข (๐ โ seq๐( + , ๐น) โ dom โ ) |