Step | Hyp | Ref
| Expression |
1 | | elprnq 10985 |
. . 3
โข ((๐ด โ P โง
๐ โ ๐ด) โ ๐ โ Q) |
2 | | ltrnq 10973 |
. . . . 5
โข (๐ฅ <Q
(๐
+Q โ) โ
(*Qโ(๐ +Q โ)) <Q
(*Qโ๐ฅ)) |
3 | | ltmnq 10966 |
. . . . . 6
โข (๐ฅ โ Q โ
((*Qโ(๐ +Q โ)) <Q
(*Qโ๐ฅ) โ (๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
<Q (๐ฅ ยทQ
(*Qโ๐ฅ)))) |
4 | | ovex 7441 |
. . . . . . 7
โข (๐ฅ
ยทQ (*Qโ(๐ +Q
โ))) โ
V |
5 | | ovex 7441 |
. . . . . . 7
โข (๐ฅ
ยทQ (*Qโ๐ฅ)) โ V |
6 | | ltmnq 10966 |
. . . . . . 7
โข (๐ค โ Q โ
(๐ฆ
<Q ๐ง โ (๐ค ยทQ ๐ฆ) <Q
(๐ค
ยทQ ๐ง))) |
7 | | vex 3478 |
. . . . . . 7
โข ๐ โ V |
8 | | mulcomnq 10947 |
. . . . . . 7
โข (๐ฆ
ยทQ ๐ง) = (๐ง ยทQ ๐ฆ) |
9 | 4, 5, 6, 7, 8 | caovord2 7618 |
. . . . . 6
โข (๐ โ Q โ
((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
<Q (๐ฅ ยทQ
(*Qโ๐ฅ)) โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) <Q ((๐ฅ
ยทQ (*Qโ๐ฅ))
ยทQ ๐))) |
10 | 3, 9 | sylan9bbr 511 |
. . . . 5
โข ((๐ โ Q โง
๐ฅ โ Q)
โ ((*Qโ(๐ +Q โ)) <Q
(*Qโ๐ฅ) โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) <Q ((๐ฅ
ยทQ (*Qโ๐ฅ))
ยทQ ๐))) |
11 | 2, 10 | bitrid 282 |
. . . 4
โข ((๐ โ Q โง
๐ฅ โ Q)
โ (๐ฅ
<Q (๐ +Q โ) โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) <Q ((๐ฅ
ยทQ (*Qโ๐ฅ))
ยทQ ๐))) |
12 | | recidnq 10959 |
. . . . . . 7
โข (๐ฅ โ Q โ
(๐ฅ
ยทQ (*Qโ๐ฅ)) =
1Q) |
13 | 12 | oveq1d 7423 |
. . . . . 6
โข (๐ฅ โ Q โ
((๐ฅ
ยทQ (*Qโ๐ฅ))
ยทQ ๐) = (1Q
ยทQ ๐)) |
14 | | mulcomnq 10947 |
. . . . . . 7
โข
(1Q ยทQ ๐) = (๐ ยทQ
1Q) |
15 | | mulidnq 10957 |
. . . . . . 7
โข (๐ โ Q โ
(๐
ยทQ 1Q) = ๐) |
16 | 14, 15 | eqtrid 2784 |
. . . . . 6
โข (๐ โ Q โ
(1Q ยทQ ๐) = ๐) |
17 | 13, 16 | sylan9eqr 2794 |
. . . . 5
โข ((๐ โ Q โง
๐ฅ โ Q)
โ ((๐ฅ
ยทQ (*Qโ๐ฅ))
ยทQ ๐) = ๐) |
18 | 17 | breq2d 5160 |
. . . 4
โข ((๐ โ Q โง
๐ฅ โ Q)
โ (((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ ๐) <Q ((๐ฅ
ยทQ (*Qโ๐ฅ))
ยทQ ๐) โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) <Q ๐)) |
19 | 11, 18 | bitrd 278 |
. . 3
โข ((๐ โ Q โง
๐ฅ โ Q)
โ (๐ฅ
<Q (๐ +Q โ) โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) <Q ๐)) |
20 | 1, 19 | sylan 580 |
. 2
โข (((๐ด โ P โง
๐ โ ๐ด) โง ๐ฅ โ Q) โ (๐ฅ <Q
(๐
+Q โ) โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) <Q ๐)) |
21 | | prcdnq 10987 |
. . 3
โข ((๐ด โ P โง
๐ โ ๐ด) โ (((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) <Q ๐ โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) โ ๐ด)) |
22 | 21 | adantr 481 |
. 2
โข (((๐ด โ P โง
๐ โ ๐ด) โง ๐ฅ โ Q) โ (((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ ๐) <Q ๐ โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) โ ๐ด)) |
23 | 20, 22 | sylbid 239 |
1
โข (((๐ด โ P โง
๐ โ ๐ด) โง ๐ฅ โ Q) โ (๐ฅ <Q
(๐
+Q โ) โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) โ ๐ด)) |