Step | Hyp | Ref
| Expression |
1 | | oveq2 7419 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
2 | 1 | breq1d 5157 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ๐) โค (๐ดโ๐))) |
3 | 2 | imbi2d 339 |
. . . . . 6
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)))) |
4 | | oveq2 7419 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
5 | 4 | breq1d 5157 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ๐) โค (๐ดโ๐))) |
6 | 5 | imbi2d 339 |
. . . . . 6
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)))) |
7 | | oveq2 7419 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
8 | 7 | breq1d 5157 |
. . . . . . 7
โข (๐ = (๐ + 1) โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐))) |
9 | 8 | imbi2d 339 |
. . . . . 6
โข (๐ = (๐ + 1) โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐)))) |
10 | | oveq2 7419 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
11 | 10 | breq1d 5157 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ๐) โค (๐ดโ๐))) |
12 | 11 | imbi2d 339 |
. . . . . 6
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)))) |
13 | | reexpcl 14048 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
14 | 13 | adantr 479 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ0)
โง (0 โค ๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โ โ) |
15 | 14 | leidd 11784 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ0)
โง (0 โค ๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) |
16 | | simprll 775 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ด โ โ) |
17 | | 1red 11219 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ 1 โ
โ) |
18 | | simprlr 776 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ โ
โ0) |
19 | | simpl 481 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ โ (โคโฅโ๐)) |
20 | | eluznn0 12905 |
. . . . . . . . . . . . 13
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ0) |
21 | 18, 19, 20 | syl2anc 582 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ โ โ0) |
22 | | reexpcl 14048 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
23 | 16, 21, 22 | syl2anc 582 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ๐) โ โ) |
24 | | simprrl 777 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ 0 โค ๐ด) |
25 | | expge0 14068 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ0
โง 0 โค ๐ด) โ 0
โค (๐ดโ๐)) |
26 | 16, 21, 24, 25 | syl3anc 1369 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ 0 โค (๐ดโ๐)) |
27 | | simprrr 778 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ด โค 1) |
28 | 16, 17, 23, 26, 27 | lemul2ad 12158 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ((๐ดโ๐) ยท ๐ด) โค ((๐ดโ๐) ยท 1)) |
29 | 16 | recnd 11246 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ๐ด โ โ) |
30 | | expp1 14038 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
31 | 29, 21, 30 | syl2anc 582 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
32 | 23 | recnd 11246 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ๐) โ โ) |
33 | 32 | mulridd 11235 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ((๐ดโ๐) ยท 1) = (๐ดโ๐)) |
34 | 33 | eqcomd 2736 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ๐) = ((๐ดโ๐) ยท 1)) |
35 | 28, 31, 34 | 3brtr4d 5179 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐)) |
36 | | peano2nn0 12516 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
37 | 21, 36 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ + 1) โ
โ0) |
38 | | reexpcl 14048 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง (๐ + 1) โ
โ0) โ (๐ดโ(๐ + 1)) โ โ) |
39 | 16, 37, 38 | syl2anc 582 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ(๐ + 1)) โ โ) |
40 | 13 | ad2antrl 724 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (๐ดโ๐) โ โ) |
41 | | letr 11312 |
. . . . . . . . . 10
โข (((๐ดโ(๐ + 1)) โ โ โง (๐ดโ๐) โ โ โง (๐ดโ๐) โ โ) โ (((๐ดโ(๐ + 1)) โค (๐ดโ๐) โง (๐ดโ๐) โค (๐ดโ๐)) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐))) |
42 | 39, 23, 40, 41 | syl3anc 1369 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ (((๐ดโ(๐ + 1)) โค (๐ดโ๐) โง (๐ดโ๐) โค (๐ดโ๐)) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐))) |
43 | 35, 42 | mpand 691 |
. . . . . . . 8
โข ((๐ โ
(โคโฅโ๐) โง ((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1))) โ ((๐ดโ๐) โค (๐ดโ๐) โ (๐ดโ(๐ + 1)) โค (๐ดโ๐))) |
44 | 43 | ex 411 |
. . . . . . 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 12898 |
. . . . 5
โข (๐ โ
(โคโฅโ๐) โ (((๐ด โ โ โง ๐ โ โ0) โง (0 โค
๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐))) |
47 | 46 | expd 414 |
. . . 4
โข (๐ โ
(โคโฅโ๐) โ ((๐ด โ โ โง ๐ โ โ0) โ ((0 โค
๐ด โง ๐ด โค 1) โ (๐ดโ๐) โค (๐ดโ๐)))) |
48 | 47 | com12 32 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ โ
(โคโฅโ๐) โ ((0 โค ๐ด โง ๐ด โค 1) โ (๐ดโ๐) โค (๐ดโ๐)))) |
49 | 48 | 3impia 1115 |
. 2
โข ((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((0 โค ๐ด โง ๐ด โค 1) โ (๐ดโ๐) โค (๐ดโ๐))) |
50 | 49 | imp 405 |
1
โข (((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โง (0 โค ๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) |