Step | Hyp | Ref
| Expression |
1 | | prmuloc 7564 |
. 2
โข
((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โ โ๐ฅ โ Q
โ๐ฆ โ
Q (๐ฅ โ
๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต))) |
2 | | nfv 1528 |
. . 3
โข
โฒ๐ฅ(โจ๐ฟ, ๐โฉ โ P โง
1Q <Q ๐ต) |
3 | | nfre1 2520 |
. . 3
โข
โฒ๐ฅโ๐ฅ โ ๐ฟ (๐ฅ ยทQ ๐ต) โ ๐ |
4 | | simpr1 1003 |
. . . . . . . 8
โข
((((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง (๐ฅ โ Q โง ๐ฆ โ Q)) โง
(๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต))) โ ๐ฅ โ ๐ฟ) |
5 | | simpr3 1005 |
. . . . . . . . . 10
โข
((((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง (๐ฅ โ Q โง ๐ฆ โ Q)) โง
(๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต))) โ (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต)) |
6 | | simplrr 536 |
. . . . . . . . . . 11
โข
((((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง (๐ฅ โ Q โง ๐ฆ โ Q)) โง
(๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต))) โ ๐ฆ โ Q) |
7 | | mulidnq 7387 |
. . . . . . . . . . 11
โข (๐ฆ โ Q โ
(๐ฆ
ยทQ 1Q) = ๐ฆ) |
8 | | breq1 4006 |
. . . . . . . . . . 11
โข ((๐ฆ
ยทQ 1Q) = ๐ฆ โ ((๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต) โ ๐ฆ <Q (๐ฅ
ยทQ ๐ต))) |
9 | 6, 7, 8 | 3syl 17 |
. . . . . . . . . 10
โข
((((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง (๐ฅ โ Q โง ๐ฆ โ Q)) โง
(๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต))) โ ((๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต) โ ๐ฆ <Q (๐ฅ
ยทQ ๐ต))) |
10 | 5, 9 | mpbid 147 |
. . . . . . . . 9
โข
((((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง (๐ฅ โ Q โง ๐ฆ โ Q)) โง
(๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต))) โ ๐ฆ <Q (๐ฅ
ยทQ ๐ต)) |
11 | | simplll 533 |
. . . . . . . . . 10
โข
((((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง (๐ฅ โ Q โง ๐ฆ โ Q)) โง
(๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต))) โ โจ๐ฟ, ๐โฉ โ
P) |
12 | | simpr2 1004 |
. . . . . . . . . 10
โข
((((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง (๐ฅ โ Q โง ๐ฆ โ Q)) โง
(๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต))) โ ๐ฆ โ ๐) |
13 | | prcunqu 7483 |
. . . . . . . . . 10
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ฆ โ ๐) โ (๐ฆ <Q (๐ฅ
ยทQ ๐ต) โ (๐ฅ ยทQ ๐ต) โ ๐)) |
14 | 11, 12, 13 | syl2anc 411 |
. . . . . . . . 9
โข
((((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง (๐ฅ โ Q โง ๐ฆ โ Q)) โง
(๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต))) โ (๐ฆ <Q (๐ฅ
ยทQ ๐ต) โ (๐ฅ ยทQ ๐ต) โ ๐)) |
15 | 10, 14 | mpd 13 |
. . . . . . . 8
โข
((((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง (๐ฅ โ Q โง ๐ฆ โ Q)) โง
(๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต))) โ (๐ฅ ยทQ ๐ต) โ ๐) |
16 | | rspe 2526 |
. . . . . . . 8
โข ((๐ฅ โ ๐ฟ โง (๐ฅ ยทQ ๐ต) โ ๐) โ โ๐ฅ โ ๐ฟ (๐ฅ ยทQ ๐ต) โ ๐) |
17 | 4, 15, 16 | syl2anc 411 |
. . . . . . 7
โข
((((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง (๐ฅ โ Q โง ๐ฆ โ Q)) โง
(๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต))) โ โ๐ฅ โ ๐ฟ (๐ฅ ยทQ ๐ต) โ ๐) |
18 | 17 | ex 115 |
. . . . . 6
โข
(((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง (๐ฅ โ Q โง ๐ฆ โ Q)) โ
((๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต)) โ โ๐ฅ โ ๐ฟ (๐ฅ ยทQ ๐ต) โ ๐)) |
19 | 18 | anassrs 400 |
. . . . 5
โข
((((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง ๐ฅ โ Q) โง ๐ฆ โ Q) โ
((๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต)) โ โ๐ฅ โ ๐ฟ (๐ฅ ยทQ ๐ต) โ ๐)) |
20 | 19 | rexlimdva 2594 |
. . . 4
โข
(((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โง ๐ฅ โ Q) โ (โ๐ฆ โ Q (๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต)) โ โ๐ฅ โ ๐ฟ (๐ฅ ยทQ ๐ต) โ ๐)) |
21 | 20 | ex 115 |
. . 3
โข
((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โ (๐ฅ โ Q โ (โ๐ฆ โ Q (๐ฅ โ ๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต)) โ โ๐ฅ โ ๐ฟ (๐ฅ ยทQ ๐ต) โ ๐))) |
22 | 2, 3, 21 | rexlimd 2591 |
. 2
โข
((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โ (โ๐ฅ โ Q
โ๐ฆ โ
Q (๐ฅ โ
๐ฟ โง ๐ฆ โ ๐ โง (๐ฆ ยทQ
1Q) <Q (๐ฅ ยทQ ๐ต)) โ โ๐ฅ โ ๐ฟ (๐ฅ ยทQ ๐ต) โ ๐)) |
23 | 1, 22 | mpd 13 |
1
โข
((โจ๐ฟ, ๐โฉ โ P
โง 1Q <Q ๐ต) โ โ๐ฅ โ ๐ฟ (๐ฅ ยทQ ๐ต) โ ๐) |