Step | Hyp | Ref
| Expression |
1 | | oveq2 7417 |
. . . . . 6
โข (๐ = 1 โ (๐ดโ๐) = (๐ดโ1)) |
2 | | oveq2 7417 |
. . . . . 6
โข (๐ = 1 โ (๐ตโ๐) = (๐ตโ1)) |
3 | 1, 2 | breq12d 5162 |
. . . . 5
โข (๐ = 1 โ ((๐ดโ๐) < (๐ตโ๐) โ (๐ดโ1) < (๐ตโ1))) |
4 | 3 | imbi2d 341 |
. . . 4
โข (๐ = 1 โ ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ดโ๐) < (๐ตโ๐)) โ (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ดโ1) < (๐ตโ1)))) |
5 | | oveq2 7417 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
6 | | oveq2 7417 |
. . . . . 6
โข (๐ = ๐ โ (๐ตโ๐) = (๐ตโ๐)) |
7 | 5, 6 | breq12d 5162 |
. . . . 5
โข (๐ = ๐ โ ((๐ดโ๐) < (๐ตโ๐) โ (๐ดโ๐) < (๐ตโ๐))) |
8 | 7 | imbi2d 341 |
. . . 4
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ดโ๐) < (๐ตโ๐)) โ (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ดโ๐) < (๐ตโ๐)))) |
9 | | oveq2 7417 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
10 | | oveq2 7417 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ตโ๐) = (๐ตโ(๐ + 1))) |
11 | 9, 10 | breq12d 5162 |
. . . . 5
โข (๐ = (๐ + 1) โ ((๐ดโ๐) < (๐ตโ๐) โ (๐ดโ(๐ + 1)) < (๐ตโ(๐ + 1)))) |
12 | 11 | imbi2d 341 |
. . . 4
โข (๐ = (๐ + 1) โ ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ดโ๐) < (๐ตโ๐)) โ (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ดโ(๐ + 1)) < (๐ตโ(๐ + 1))))) |
13 | | oveq2 7417 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
14 | | oveq2 7417 |
. . . . . 6
โข (๐ = ๐ โ (๐ตโ๐) = (๐ตโ๐)) |
15 | 13, 14 | breq12d 5162 |
. . . . 5
โข (๐ = ๐ โ ((๐ดโ๐) < (๐ตโ๐) โ (๐ดโ๐) < (๐ตโ๐))) |
16 | 15 | imbi2d 341 |
. . . 4
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ดโ๐) < (๐ตโ๐)) โ (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ดโ๐) < (๐ตโ๐)))) |
17 | | recn 11200 |
. . . . . . 7
โข (๐ด โ โ โ ๐ด โ
โ) |
18 | | recn 11200 |
. . . . . . 7
โข (๐ต โ โ โ ๐ต โ
โ) |
19 | | exp1 14033 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ดโ1) = ๐ด) |
20 | | exp1 14033 |
. . . . . . . 8
โข (๐ต โ โ โ (๐ตโ1) = ๐ต) |
21 | 19, 20 | breqan12d 5165 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ1) < (๐ตโ1) โ ๐ด < ๐ต)) |
22 | 17, 18, 21 | syl2an 597 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ1) < (๐ตโ1) โ ๐ด < ๐ต)) |
23 | 22 | biimpar 479 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด < ๐ต) โ (๐ดโ1) < (๐ตโ1)) |
24 | 23 | adantrl 715 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ดโ1) < (๐ตโ1)) |
25 | | simp2ll 1241 |
. . . . . . . . . 10
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ ๐ด โ โ) |
26 | | nnnn0 12479 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ0) |
27 | 26 | 3ad2ant1 1134 |
. . . . . . . . . 10
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ ๐ โ โ0) |
28 | 25, 27 | reexpcld 14128 |
. . . . . . . . 9
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ (๐ดโ๐) โ โ) |
29 | | simp2lr 1242 |
. . . . . . . . . 10
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ ๐ต โ โ) |
30 | 29, 27 | reexpcld 14128 |
. . . . . . . . 9
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ (๐ตโ๐) โ โ) |
31 | 28, 30 | jca 513 |
. . . . . . . 8
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ)) |
32 | | simp2rl 1243 |
. . . . . . . . . 10
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ 0 โค ๐ด) |
33 | 25, 27, 32 | expge0d 14129 |
. . . . . . . . 9
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ 0 โค (๐ดโ๐)) |
34 | | simp3 1139 |
. . . . . . . . 9
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ (๐ดโ๐) < (๐ตโ๐)) |
35 | 33, 34 | jca 513 |
. . . . . . . 8
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ (0 โค (๐ดโ๐) โง (๐ดโ๐) < (๐ตโ๐))) |
36 | | simp2l 1200 |
. . . . . . . 8
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ (๐ด โ โ โง ๐ต โ โ)) |
37 | | simp2r 1201 |
. . . . . . . 8
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ (0 โค ๐ด โง ๐ด < ๐ต)) |
38 | | ltmul12a 12070 |
. . . . . . . 8
โข
(((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ) โง (0 โค (๐ดโ๐) โง (๐ดโ๐) < (๐ตโ๐))) โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด < ๐ต))) โ ((๐ดโ๐) ยท ๐ด) < ((๐ตโ๐) ยท ๐ต)) |
39 | 31, 35, 36, 37, 38 | syl22anc 838 |
. . . . . . 7
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ ((๐ดโ๐) ยท ๐ด) < ((๐ตโ๐) ยท ๐ต)) |
40 | 25 | recnd 11242 |
. . . . . . . 8
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ ๐ด โ โ) |
41 | 40, 27 | expp1d 14112 |
. . . . . . 7
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
42 | 29 | recnd 11242 |
. . . . . . . 8
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ ๐ต โ โ) |
43 | 42, 27 | expp1d 14112 |
. . . . . . 7
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ (๐ตโ(๐ + 1)) = ((๐ตโ๐) ยท ๐ต)) |
44 | 39, 41, 43 | 3brtr4d 5181 |
. . . . . 6
โข ((๐ โ โ โง ((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง (๐ดโ๐) < (๐ตโ๐)) โ (๐ดโ(๐ + 1)) < (๐ตโ(๐ + 1))) |
45 | 44 | 3exp 1120 |
. . . . 5
โข (๐ โ โ โ (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ((๐ดโ๐) < (๐ตโ๐) โ (๐ดโ(๐ + 1)) < (๐ตโ(๐ + 1))))) |
46 | 45 | a2d 29 |
. . . 4
โข (๐ โ โ โ ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ดโ๐) < (๐ตโ๐)) โ (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ดโ(๐ + 1)) < (๐ตโ(๐ + 1))))) |
47 | 4, 8, 12, 16, 24, 46 | nnind 12230 |
. . 3
โข (๐ โ โ โ (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ดโ๐) < (๐ตโ๐))) |
48 | 47 | impcom 409 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง ๐ โ โ) โ (๐ดโ๐) < (๐ตโ๐)) |
49 | 48 | 3impa 1111 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต) โง ๐ โ โ) โ (๐ดโ๐) < (๐ตโ๐)) |