Step | Hyp | Ref
| Expression |
1 | | oveq2 7417 |
. . . . . . 7
โข (๐ = 0 โ (๐ดโ๐) = (๐ดโ0)) |
2 | | oveq2 7417 |
. . . . . . 7
โข (๐ = 0 โ (๐ตโ๐) = (๐ตโ0)) |
3 | 1, 2 | breq12d 5162 |
. . . . . 6
โข (๐ = 0 โ ((๐ดโ๐) โค (๐ตโ๐) โ (๐ดโ0) โค (๐ตโ0))) |
4 | 3 | imbi2d 341 |
. . . . 5
โข (๐ = 0 โ ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โ (๐ดโ๐) โค (๐ตโ๐)) โ (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ (๐ดโ0) โค (๐ตโ0)))) |
5 | | oveq2 7417 |
. . . . . . 7
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
6 | | oveq2 7417 |
. . . . . . 7
โข (๐ = ๐ โ (๐ตโ๐) = (๐ตโ๐)) |
7 | 5, 6 | breq12d 5162 |
. . . . . 6
โข (๐ = ๐ โ ((๐ดโ๐) โค (๐ตโ๐) โ (๐ดโ๐) โค (๐ตโ๐))) |
8 | 7 | imbi2d 341 |
. . . . 5
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ (๐ดโ๐) โค (๐ตโ๐)) โ (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ (๐ดโ๐) โค (๐ตโ๐)))) |
9 | | oveq2 7417 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
10 | | oveq2 7417 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐ตโ๐) = (๐ตโ(๐ + 1))) |
11 | 9, 10 | breq12d 5162 |
. . . . . 6
โข (๐ = (๐ + 1) โ ((๐ดโ๐) โค (๐ตโ๐) โ (๐ดโ(๐ + 1)) โค (๐ตโ(๐ + 1)))) |
12 | 11 | imbi2d 341 |
. . . . 5
โข (๐ = (๐ + 1) โ ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ (๐ดโ๐) โค (๐ตโ๐)) โ (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ (๐ดโ(๐ + 1)) โค (๐ตโ(๐ + 1))))) |
13 | | oveq2 7417 |
. . . . . . 7
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
14 | | oveq2 7417 |
. . . . . . 7
โข (๐ = ๐ โ (๐ตโ๐) = (๐ตโ๐)) |
15 | 13, 14 | breq12d 5162 |
. . . . . 6
โข (๐ = ๐ โ ((๐ดโ๐) โค (๐ตโ๐) โ (๐ดโ๐) โค (๐ตโ๐))) |
16 | 15 | imbi2d 341 |
. . . . 5
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ (๐ดโ๐) โค (๐ตโ๐)) โ (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ (๐ดโ๐) โค (๐ตโ๐)))) |
17 | | recn 11200 |
. . . . . . 7
โข (๐ด โ โ โ ๐ด โ
โ) |
18 | | recn 11200 |
. . . . . . 7
โข (๐ต โ โ โ ๐ต โ
โ) |
19 | | exp0 14031 |
. . . . . . . . . 10
โข (๐ด โ โ โ (๐ดโ0) = 1) |
20 | 19 | adantr 482 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ0) = 1) |
21 | | 1le1 11842 |
. . . . . . . . 9
โข 1 โค
1 |
22 | 20, 21 | eqbrtrdi 5188 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ0) โค
1) |
23 | | exp0 14031 |
. . . . . . . . 9
โข (๐ต โ โ โ (๐ตโ0) = 1) |
24 | 23 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ0) = 1) |
25 | 22, 24 | breqtrrd 5177 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ0) โค (๐ตโ0)) |
26 | 17, 18, 25 | syl2an 597 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ0) โค (๐ตโ0)) |
27 | 26 | adantr 482 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โ (๐ดโ0) โค (๐ตโ0)) |
28 | | reexpcl 14044 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
29 | 28 | ad4ant14 751 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ๐ โ โ0) โ (๐ดโ๐) โ โ) |
30 | | simplll 774 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ๐ โ โ0) โ ๐ด โ
โ) |
31 | | simpr 486 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ๐ โ โ0) โ ๐ โ
โ0) |
32 | | simplrl 776 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ๐ โ โ0) โ 0 โค
๐ด) |
33 | | expge0 14064 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ โ โ0
โง 0 โค ๐ด) โ 0
โค (๐ดโ๐)) |
34 | 30, 31, 32, 33 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ๐ โ โ0) โ 0 โค
(๐ดโ๐)) |
35 | | reexpcl 14044 |
. . . . . . . . . . . . . 14
โข ((๐ต โ โ โง ๐ โ โ0)
โ (๐ตโ๐) โ
โ) |
36 | 35 | ad4ant24 753 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ๐ โ โ0) โ (๐ตโ๐) โ โ) |
37 | 29, 34, 36 | jca31 516 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ๐ โ โ0) โ (((๐ดโ๐) โ โ โง 0 โค (๐ดโ๐)) โง (๐ตโ๐) โ โ)) |
38 | | simpl 484 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
39 | | simpl 484 |
. . . . . . . . . . . . . 14
โข ((0 โค
๐ด โง ๐ด โค ๐ต) โ 0 โค ๐ด) |
40 | 38, 39 | anim12i 614 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โ (๐ด โ โ โง 0 โค ๐ด)) |
41 | 40 | adantr 482 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ๐ โ โ0) โ (๐ด โ โ โง 0 โค
๐ด)) |
42 | | simpllr 775 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ๐ โ โ0) โ ๐ต โ
โ) |
43 | 37, 41, 42 | jca32 517 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ๐ โ โ0) โ ((((๐ดโ๐) โ โ โง 0 โค (๐ดโ๐)) โง (๐ตโ๐) โ โ) โง ((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ))) |
44 | 43 | adantr 482 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (0 โค ๐ด
โง ๐ด โค ๐ต)) โง ๐ โ โ0) โง (๐ดโ๐) โค (๐ตโ๐)) โ ((((๐ดโ๐) โ โ โง 0 โค (๐ดโ๐)) โง (๐ตโ๐) โ โ) โง ((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ))) |
45 | | simplrr 777 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ๐ โ โ0) โ ๐ด โค ๐ต) |
46 | 45 | anim1ci 617 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (0 โค ๐ด
โง ๐ด โค ๐ต)) โง ๐ โ โ0) โง (๐ดโ๐) โค (๐ตโ๐)) โ ((๐ดโ๐) โค (๐ตโ๐) โง ๐ด โค ๐ต)) |
47 | | lemul12a 12072 |
. . . . . . . . . 10
โข
(((((๐ดโ๐) โ โ โง 0 โค
(๐ดโ๐)) โง (๐ตโ๐) โ โ) โง ((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ)) โ (((๐ดโ๐) โค (๐ตโ๐) โง ๐ด โค ๐ต) โ ((๐ดโ๐) ยท ๐ด) โค ((๐ตโ๐) ยท ๐ต))) |
48 | 44, 46, 47 | sylc 65 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (0 โค ๐ด
โง ๐ด โค ๐ต)) โง ๐ โ โ0) โง (๐ดโ๐) โค (๐ตโ๐)) โ ((๐ดโ๐) ยท ๐ด) โค ((๐ตโ๐) ยท ๐ต)) |
49 | | expp1 14034 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
50 | 17, 49 | sylan 581 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
51 | 50 | ad5ant14 757 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (0 โค ๐ด
โง ๐ด โค ๐ต)) โง ๐ โ โ0) โง (๐ดโ๐) โค (๐ตโ๐)) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
52 | | expp1 14034 |
. . . . . . . . . . 11
โข ((๐ต โ โ โง ๐ โ โ0)
โ (๐ตโ(๐ + 1)) = ((๐ตโ๐) ยท ๐ต)) |
53 | 18, 52 | sylan 581 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ โ โ0)
โ (๐ตโ(๐ + 1)) = ((๐ตโ๐) ยท ๐ต)) |
54 | 53 | ad5ant24 760 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (0 โค ๐ด
โง ๐ด โค ๐ต)) โง ๐ โ โ0) โง (๐ดโ๐) โค (๐ตโ๐)) โ (๐ตโ(๐ + 1)) = ((๐ตโ๐) ยท ๐ต)) |
55 | 48, 51, 54 | 3brtr4d 5181 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (0 โค ๐ด
โง ๐ด โค ๐ต)) โง ๐ โ โ0) โง (๐ดโ๐) โค (๐ตโ๐)) โ (๐ดโ(๐ + 1)) โค (๐ตโ(๐ + 1))) |
56 | 55 | ex 414 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ๐ โ โ0) โ ((๐ดโ๐) โค (๐ตโ๐) โ (๐ดโ(๐ + 1)) โค (๐ตโ(๐ + 1)))) |
57 | 56 | expcom 415 |
. . . . . 6
โข (๐ โ โ0
โ (((๐ด โ โ
โง ๐ต โ โ)
โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ ((๐ดโ๐) โค (๐ตโ๐) โ (๐ดโ(๐ + 1)) โค (๐ตโ(๐ + 1))))) |
58 | 57 | a2d 29 |
. . . . 5
โข (๐ โ โ0
โ ((((๐ด โ โ
โง ๐ต โ โ)
โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ (๐ดโ๐) โค (๐ตโ๐)) โ (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ (๐ดโ(๐ + 1)) โค (๐ตโ(๐ + 1))))) |
59 | 4, 8, 12, 16, 27, 58 | nn0ind 12657 |
. . . 4
โข (๐ โ โ0
โ (((๐ด โ โ
โง ๐ต โ โ)
โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ (๐ดโ๐) โค (๐ตโ๐))) |
60 | 59 | exp4c 434 |
. . 3
โข (๐ โ โ0
โ (๐ด โ โ
โ (๐ต โ โ
โ ((0 โค ๐ด โง
๐ด โค ๐ต) โ (๐ดโ๐) โค (๐ตโ๐))))) |
61 | 60 | com3l 89 |
. 2
โข (๐ด โ โ โ (๐ต โ โ โ (๐ โ โ0
โ ((0 โค ๐ด โง
๐ด โค ๐ต) โ (๐ดโ๐) โค (๐ตโ๐))))) |
62 | 61 | 3imp1 1348 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ0)
โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ (๐ดโ๐) โค (๐ตโ๐)) |