Step | Hyp | Ref
| Expression |
1 | | tru 1546 |
. 2
โข
โค |
2 | | fveq2 6843 |
. . 3
โข (๐ฅ = ๐ฆ โ (expโ๐ฅ) = (expโ๐ฆ)) |
3 | | fveq2 6843 |
. . 3
โข (๐ฅ = ๐ด โ (expโ๐ฅ) = (expโ๐ด)) |
4 | | fveq2 6843 |
. . 3
โข (๐ฅ = ๐ต โ (expโ๐ฅ) = (expโ๐ต)) |
5 | | ssid 3967 |
. . 3
โข โ
โ โ |
6 | | reefcl 15974 |
. . . 4
โข (๐ฅ โ โ โ
(expโ๐ฅ) โ
โ) |
7 | 6 | adantl 483 |
. . 3
โข
((โค โง ๐ฅ
โ โ) โ (expโ๐ฅ) โ โ) |
8 | | simp2 1138 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ ๐ฆ โ โ) |
9 | | simp1 1137 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ ๐ฅ โ โ) |
10 | 8, 9 | resubcld 11588 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ (๐ฆ โ ๐ฅ) โ โ) |
11 | | posdif 11653 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ < ๐ฆ โ 0 < (๐ฆ โ ๐ฅ))) |
12 | 11 | biimp3a 1470 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ 0 < (๐ฆ โ ๐ฅ)) |
13 | 10, 12 | elrpd 12959 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ (๐ฆ โ ๐ฅ) โ
โ+) |
14 | | efgt1 16003 |
. . . . . . . 8
โข ((๐ฆ โ ๐ฅ) โ โ+ โ 1 <
(expโ(๐ฆ โ ๐ฅ))) |
15 | 13, 14 | syl 17 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ 1 < (expโ(๐ฆ โ ๐ฅ))) |
16 | 9 | reefcld 15975 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ (expโ๐ฅ) โ โ) |
17 | 10 | reefcld 15975 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ (expโ(๐ฆ โ ๐ฅ)) โ โ) |
18 | | efgt0 15990 |
. . . . . . . . 9
โข (๐ฅ โ โ โ 0 <
(expโ๐ฅ)) |
19 | 9, 18 | syl 17 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ 0 < (expโ๐ฅ)) |
20 | | ltmulgt11 12020 |
. . . . . . . 8
โข
(((expโ๐ฅ)
โ โ โง (expโ(๐ฆ โ ๐ฅ)) โ โ โง 0 <
(expโ๐ฅ)) โ (1
< (expโ(๐ฆ โ
๐ฅ)) โ (expโ๐ฅ) < ((expโ๐ฅ) ยท (expโ(๐ฆ โ ๐ฅ))))) |
21 | 16, 17, 19, 20 | syl3anc 1372 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ (1 < (expโ(๐ฆ โ ๐ฅ)) โ (expโ๐ฅ) < ((expโ๐ฅ) ยท (expโ(๐ฆ โ ๐ฅ))))) |
22 | 15, 21 | mpbid 231 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ (expโ๐ฅ) < ((expโ๐ฅ) ยท (expโ(๐ฆ โ ๐ฅ)))) |
23 | 9 | recnd 11188 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ ๐ฅ โ โ) |
24 | 10 | recnd 11188 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ (๐ฆ โ ๐ฅ) โ โ) |
25 | | efadd 15981 |
. . . . . . . 8
โข ((๐ฅ โ โ โง (๐ฆ โ ๐ฅ) โ โ) โ (expโ(๐ฅ + (๐ฆ โ ๐ฅ))) = ((expโ๐ฅ) ยท (expโ(๐ฆ โ ๐ฅ)))) |
26 | 23, 24, 25 | syl2anc 585 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ (expโ(๐ฅ + (๐ฆ โ ๐ฅ))) = ((expโ๐ฅ) ยท (expโ(๐ฆ โ ๐ฅ)))) |
27 | 8 | recnd 11188 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ ๐ฆ โ โ) |
28 | 23, 27 | pncan3d 11520 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ (๐ฅ + (๐ฆ โ ๐ฅ)) = ๐ฆ) |
29 | 28 | fveq2d 6847 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ (expโ(๐ฅ + (๐ฆ โ ๐ฅ))) = (expโ๐ฆ)) |
30 | 26, 29 | eqtr3d 2775 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ ((expโ๐ฅ) ยท (expโ(๐ฆ โ ๐ฅ))) = (expโ๐ฆ)) |
31 | 22, 30 | breqtrd 5132 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ < ๐ฆ) โ (expโ๐ฅ) < (expโ๐ฆ)) |
32 | 31 | 3expia 1122 |
. . . 4
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ < ๐ฆ โ (expโ๐ฅ) < (expโ๐ฆ))) |
33 | 32 | adantl 483 |
. . 3
โข
((โค โง (๐ฅ
โ โ โง ๐ฆ
โ โ)) โ (๐ฅ
< ๐ฆ โ
(expโ๐ฅ) <
(expโ๐ฆ))) |
34 | 2, 3, 4, 5, 7, 33 | ltord1 11686 |
. 2
โข
((โค โง (๐ด
โ โ โง ๐ต
โ โ)) โ (๐ด
< ๐ต โ
(expโ๐ด) <
(expโ๐ต))) |
35 | 1, 34 | mpan 689 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ (expโ๐ด) < (expโ๐ต))) |