Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
2 | 1 | breq1d 5116 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ๐) โค (๐ดโ๐))) |
3 | 2 | imbi2d 341 |
. . . . . 6
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)))) |
4 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
5 | 4 | breq1d 5116 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ๐) โค (๐ดโ๐))) |
6 | 5 | imbi2d 341 |
. . . . . 6
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)))) |
7 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
8 | 7 | breq1d 5116 |
. . . . . . 7
โข (๐ = (๐ + 1) โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐))) |
9 | 8 | imbi2d 341 |
. . . . . 6
โข (๐ = (๐ + 1) โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐)))) |
10 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
11 | 10 | breq1d 5116 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ๐) โค (๐ดโ๐))) |
12 | 11 | imbi2d 341 |
. . . . . 6
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)))) |
13 | | reexpcl 13990 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
14 | 13 | adantr 482 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ0)
โง (0 โค ๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โ โ) |
15 | 14 | leidd 11726 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ0)
โง (0 โค ๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) |
16 | | simprll 778 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ด โ โ) |
17 | | 1red 11161 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ 1 โ
โ) |
18 | | simprlr 779 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ โ
โ0) |
19 | | simpl 484 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ โ (โคโฅโ๐)) |
20 | | eluznn0 12847 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ0) |
21 | 18, 19, 20 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ โ โ0) |
22 | | reexpcl 13990 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
23 | 16, 21, 22 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ๐) โ โ) |
24 | | simprrl 780 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ 0 โค ๐ด) |
25 | | expge0 14010 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ0
โง 0 โค ๐ด) โ 0
โค (๐ดโ๐)) |
26 | 16, 21, 24, 25 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ 0 โค (๐ดโ๐)) |
27 | | simprrr 781 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ด โค 1) |
28 | 16, 17, 23, 26, 27 | lemul2ad 12100 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ((๐ดโ๐) ยท ๐ด) โค ((๐ดโ๐) ยท 1)) |
29 | 16 | recnd 11188 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ด โ โ) |
30 | | expp1 13980 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
31 | 29, 21, 30 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
32 | 23 | recnd 11188 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ๐) โ โ) |
33 | 32 | mulid1d 11177 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ((๐ดโ๐) ยท 1) = (๐ดโ๐)) |
34 | 33 | eqcomd 2739 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ๐) = ((๐ดโ๐) ยท 1)) |
35 | 28, 31, 34 | 3brtr4d 5138 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐)) |
36 | | peano2nn0 12458 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
37 | 21, 36 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ + 1) โ
โ0) |
38 | | reexpcl 13990 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง (๐ + 1) โ
โ0) โ (๐ดโ(๐ + 1)) โ โ) |
39 | 16, 37, 38 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ(๐ + 1)) โ โ) |
40 | 13 | ad2antrl 727 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ๐) โ โ) |
41 | | letr 11254 |
. . . . . . . . . 10
โข (((๐ดโ(๐ + 1)) โ โ โง (๐ดโ๐) โ โ โง (๐ดโ๐) โ โ) โ (((๐ดโ(๐ + 1)) โค (๐ดโ๐) โง (๐ดโ๐) โค (๐ดโ๐)) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐))) |
42 | 39, 23, 40, 41 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (((๐ดโ(๐ + 1)) โค (๐ดโ๐) โง (๐ดโ๐) โค (๐ดโ๐)) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐))) |
43 | 35, 42 | mpand 694 |
. . . . . . . 8
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐))) |
44 | 43 | ex 414 |
. . . . . . 7
โข (๐ โ
(โคโฅโ๐) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐)))) |
45 | 44 | a2d 29 |
. . . . . 6
โข (๐ โ
(โคโฅโ๐) โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐)))) |
46 | 3, 6, 9, 12, 15, 45 | uzind4i 12840 |
. . . . 5
โข (๐ โ
(โคโฅโ๐) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐))) |
47 | 46 | expd 417 |
. . . 4
โข (๐ โ
(โคโฅโ๐) โ ((๐ด โ โ โง ๐ โ โ0) โ ((0 โค
๐ด โง ๐ด โค 1) โ (๐ดโ๐) โค (๐ดโ๐)))) |
48 | 47 | com12 32 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ โ
(โคโฅโ๐) โ ((0 โค ๐ด โง ๐ด โค 1) โ (๐ดโ๐) โค (๐ดโ๐)))) |
49 | 48 | 3impia 1118 |
. 2
โข ((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((0 โค ๐ด โง ๐ด โค 1) โ (๐ดโ๐) โค (๐ดโ๐))) |
50 | 49 | imp 408 |
1
โข (((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โง (0 โค ๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) |