Step | Hyp | Ref
| Expression |
1 | | oveq2 5885 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
2 | 1 | breq1d 4015 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ๐) โค (๐ดโ๐))) |
3 | 2 | imbi2d 230 |
. . . . . 6
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)))) |
4 | | oveq2 5885 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
5 | 4 | breq1d 4015 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ๐) โค (๐ดโ๐))) |
6 | 5 | imbi2d 230 |
. . . . . 6
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)))) |
7 | | oveq2 5885 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
8 | 7 | breq1d 4015 |
. . . . . . 7
โข (๐ = (๐ + 1) โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐))) |
9 | 8 | imbi2d 230 |
. . . . . 6
โข (๐ = (๐ + 1) โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐)))) |
10 | | oveq2 5885 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
11 | 10 | breq1d 4015 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ๐) โค (๐ดโ๐))) |
12 | 11 | imbi2d 230 |
. . . . . 6
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)))) |
13 | | reexpcl 10539 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
14 | 13 | adantr 276 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ0)
โง (0 โค ๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โ โ) |
15 | 14 | leidd 8473 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ0)
โง (0 โค ๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) |
16 | 15 | a1i 9 |
. . . . . 6
โข (๐ โ โค โ (((๐ด โ โ โง ๐ โ โ0)
โง (0 โค ๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐))) |
17 | | simprll 537 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ด โ โ) |
18 | | 1red 7974 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ 1 โ
โ) |
19 | | simprlr 538 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ โ
โ0) |
20 | | simpl 109 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ โ (โคโฅโ๐)) |
21 | | eluznn0 9601 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ0) |
22 | 19, 20, 21 | syl2anc 411 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ โ โ0) |
23 | | reexpcl 10539 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
24 | 17, 22, 23 | syl2anc 411 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ๐) โ โ) |
25 | | simprrl 539 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ 0 โค ๐ด) |
26 | | expge0 10558 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ0
โง 0 โค ๐ด) โ 0
โค (๐ดโ๐)) |
27 | 17, 22, 25, 26 | syl3anc 1238 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ 0 โค (๐ดโ๐)) |
28 | | simprrr 540 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ด โค 1) |
29 | 17, 18, 24, 27, 28 | lemul2ad 8899 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ((๐ดโ๐) ยท ๐ด) โค ((๐ดโ๐) ยท 1)) |
30 | 17 | recnd 7988 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ด โ โ) |
31 | | expp1 10529 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
32 | 30, 22, 31 | syl2anc 411 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
33 | 24 | recnd 7988 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ๐) โ โ) |
34 | 33 | mulridd 7976 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ((๐ดโ๐) ยท 1) = (๐ดโ๐)) |
35 | 34 | eqcomd 2183 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ๐) = ((๐ดโ๐) ยท 1)) |
36 | 29, 32, 35 | 3brtr4d 4037 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐)) |
37 | | peano2nn0 9218 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
38 | 22, 37 | syl 14 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ + 1) โ
โ0) |
39 | | reexpcl 10539 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง (๐ + 1) โ
โ0) โ (๐ดโ(๐ + 1)) โ โ) |
40 | 17, 38, 39 | syl2anc 411 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ(๐ + 1)) โ โ) |
41 | 13 | ad2antrl 490 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ๐) โ โ) |
42 | | letr 8042 |
. . . . . . . . . 10
โข (((๐ดโ(๐ + 1)) โ โ โง (๐ดโ๐) โ โ โง (๐ดโ๐) โ โ) โ (((๐ดโ(๐ + 1)) โค (๐ดโ๐) โง (๐ดโ๐) โค (๐ดโ๐)) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐))) |
43 | 40, 24, 41, 42 | syl3anc 1238 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (((๐ดโ(๐ + 1)) โค (๐ดโ๐) โง (๐ดโ๐) โค (๐ดโ๐)) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐))) |
44 | 36, 43 | mpand 429 |
. . . . . . . 8
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐))) |
45 | 44 | ex 115 |
. . . . . . 7
โข (๐ โ
(โคโฅโ๐) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐)))) |
46 | 45 | a2d 26 |
. . . . . 6
โข (๐ โ
(โคโฅโ๐) โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐)))) |
47 | 3, 6, 9, 12, 16, 46 | uzind4 9590 |
. . . . 5
โข (๐ โ
(โคโฅโ๐) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐))) |
48 | 47 | expd 258 |
. . . 4
โข (๐ โ
(โคโฅโ๐) โ ((๐ด โ โ โง ๐ โ โ0) โ ((0 โค
๐ด โง ๐ด โค 1) โ (๐ดโ๐) โค (๐ดโ๐)))) |
49 | 48 | com12 30 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ โ
(โคโฅโ๐) โ ((0 โค ๐ด โง ๐ด โค 1) โ (๐ดโ๐) โค (๐ดโ๐)))) |
50 | 49 | 3impia 1200 |
. 2
โข ((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((0 โค ๐ด โง ๐ด โค 1) โ (๐ดโ๐) โค (๐ดโ๐))) |
51 | 50 | imp 124 |
1
โข (((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โง (0 โค ๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) |