Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . . . 7
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ = (๐ด Yrm ๐ต)) โ ๐ด โ
(โคโฅโ2)) |
2 | | simpl2 1193 |
. . . . . . 7
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ = (๐ด Yrm ๐ต)) โ ๐ต โ โ) |
3 | | simpl3 1194 |
. . . . . . 7
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ = (๐ด Yrm ๐ต)) โ ๐ถ โ โ) |
4 | | simpr 486 |
. . . . . . 7
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ = (๐ด Yrm ๐ต)) โ ๐ถ = (๐ด Yrm ๐ต)) |
5 | | eqid 2733 |
. . . . . . 7
โข (๐ด Xrm ๐ต) = (๐ด Xrm ๐ต) |
6 | | eqid 2733 |
. . . . . . 7
โข (๐ต ยท (๐ด Yrm ๐ต)) = (๐ต ยท (๐ด Yrm ๐ต)) |
7 | | eqid 2733 |
. . . . . . 7
โข (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) |
8 | | eqid 2733 |
. . . . . . 7
โข (๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) |
9 | | eqid 2733 |
. . . . . . 7
โข (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) |
10 | | eqid 2733 |
. . . . . . 7
โข ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) |
11 | | eqid 2733 |
. . . . . . 7
โข ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) |
12 | | eqid 2733 |
. . . . . . 7
โข (((๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) = (((๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ
1) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | jm2.27c 41374 |
. . . . . 6
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ = (๐ด Yrm ๐ต)) โ ((((๐ด Xrm ๐ต) โ โ0 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) โ โ0
โง (๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ โ0)
โง ((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ โ0
โง ((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ โ0
โง ((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) โ โ0))
โง ((((๐ด Yrm
(2 ยท (๐ต ยท
(๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) โ
โ0 โง ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = (((((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) + 1) ยท (2
ยท (๐ถโ2))) โง
(๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ)))))) |
14 | 13 | simpld 496 |
. . . . 5
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ = (๐ด Yrm ๐ต)) โ (((๐ด Xrm ๐ต) โ โ0 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) โ โ0
โง (๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ โ0)
โง ((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ โ0
โง ((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ โ0
โง ((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) โ
โ0))) |
15 | 14 | simpld 496 |
. . . 4
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ = (๐ด Yrm ๐ต)) โ ((๐ด Xrm ๐ต) โ โ0 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) โ โ0
โง (๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ
โ0)) |
16 | 14 | simprd 497 |
. . . . 5
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ = (๐ด Yrm ๐ต)) โ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ โ0 โง ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ โ0 โง ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) โ
โ0)) |
17 | 13 | simprd 497 |
. . . . . 6
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ = (๐ด Yrm ๐ต)) โ ((((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) โ
โ0 โง ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = (((((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) + 1) ยท (2
ยท (๐ถโ2))) โง
(๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ))))) |
18 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = (((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) โ (๐ + 1) = ((((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) + 1)) |
19 | 18 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ = (((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) โ ((๐ + 1) ยท (2 ยท
(๐ถโ2))) = (((((๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) + 1)
ยท (2 ยท (๐ถโ2)))) |
20 | 19 | eqeq2d 2744 |
. . . . . . . . . 10
โข (๐ = (((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) โ ((๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โ (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = (((((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) + 1) ยท (2
ยท (๐ถโ2))))) |
21 | 20 | 3anbi2d 1442 |
. . . . . . . . 9
โข (๐ = (((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) โ ((((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด)) โ (((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = (((((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) + 1) ยท (2
ยท (๐ถโ2))) โง
(๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด)))) |
22 | 21 | anbi2d 630 |
. . . . . . . 8
โข (๐ = (((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โ (((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = (((((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) + 1) ยท (2
ยท (๐ถโ2))) โง
(๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))))) |
23 | 22 | anbi1d 631 |
. . . . . . 7
โข (๐ = (((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) โ (((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ))) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = (((((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) + 1) ยท (2
ยท (๐ถโ2))) โง
(๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ))))) |
24 | 23 | rspcev 3580 |
. . . . . 6
โข
(((((๐ด
Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) โ
โ0 โง ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = (((((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) / (2 ยท (๐ถโ2))) โ 1) + 1) ยท (2
ยท (๐ถโ2))) โง
(๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ)))) โ โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ)))) |
25 | 17, 24 | syl 17 |
. . . . 5
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ = (๐ด Yrm ๐ต)) โ โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ)))) |
26 | | eleq1 2822 |
. . . . . . . . . 10
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (๐ โ (โคโฅโ2)
โ (๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ
(โคโฅโ2))) |
27 | 26 | 3anbi3d 1443 |
. . . . . . . . 9
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โ ((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ
(โคโฅโ2)))) |
28 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (๐โ2) = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2)) |
29 | 28 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ((๐โ2) โ 1) = (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1)) |
30 | 29 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (((๐โ2) โ 1) ยท (โโ2)) = ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (โโ2))) |
31 | 30 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = ((๐โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (โโ2)))) |
32 | 31 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โ ((๐โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (โโ2))) = 1)) |
33 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (๐ โ ๐ด) = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด)) |
34 | 33 | breq2d 5118 |
. . . . . . . . . 10
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด) โ (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) |
35 | 32, 34 | 3anbi13d 1439 |
. . . . . . . . 9
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ((((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด)) โ (((๐โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด)))) |
36 | 27, 35 | anbi12d 632 |
. . . . . . . 8
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด))) โ (((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((๐โ2) โ
((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท
(โโ2))) = 1 โง
(๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))))) |
37 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (๐ โ 1) = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1)) |
38 | 37 | breq2d 5118 |
. . . . . . . . . 10
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ((2 ยท ๐ถ) โฅ (๐ โ 1) โ (2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1))) |
39 | 38 | anbi1d 631 |
. . . . . . . . 9
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (((2 ยท ๐ถ) โฅ (๐ โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โ ((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)))) |
40 | 39 | anbi1d 631 |
. . . . . . . 8
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ((((2 ยท ๐ถ) โฅ (๐ โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)) โ (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) |
41 | 36, 40 | anbi12d 632 |
. . . . . . 7
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((๐โ2) โ
((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท
(โโ2))) = 1 โง
(๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |
42 | 41 | rexbidv 3172 |
. . . . . 6
โข (๐ = (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((๐โ2) โ
((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท
(โโ2))) = 1 โง
(๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |
43 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ (โโ2) = (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2)) |
44 | 43 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (โโ2)) = ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) |
45 | 44 | oveq2d 7374 |
. . . . . . . . . . 11
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ((๐โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (โโ2))) = ((๐โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2)))) |
46 | 45 | eqeq1d 2735 |
. . . . . . . . . 10
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ (((๐โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (โโ2))) = 1 โ ((๐โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1)) |
47 | 46 | 3anbi1d 1441 |
. . . . . . . . 9
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ((((๐โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด)) โ (((๐โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด)))) |
48 | 47 | anbi2d 630 |
. . . . . . . 8
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((๐โ2) โ
((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท
(โโ2))) = 1 โง
(๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โ (((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((๐โ2) โ
((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท
(((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))))) |
49 | | oveq1 7365 |
. . . . . . . . . . 11
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ (โ โ ๐ถ) = (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) |
50 | 49 | breq2d 5118 |
. . . . . . . . . 10
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ) โ (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ))) |
51 | 50 | anbi2d 630 |
. . . . . . . . 9
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โ ((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)))) |
52 | | oveq1 7365 |
. . . . . . . . . . 11
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ (โ โ ๐ต) = (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต)) |
53 | 52 | breq2d 5118 |
. . . . . . . . . 10
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โ (2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต))) |
54 | 53 | anbi1d 631 |
. . . . . . . . 9
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ (((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ) โ ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ))) |
55 | 51, 54 | anbi12d 632 |
. . . . . . . 8
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ((((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)) โ (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ)))) |
56 | 48, 55 | anbi12d 632 |
. . . . . . 7
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ (((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((๐โ2) โ
((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท
(โโ2))) = 1 โง
(๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((๐โ2) โ
((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท
(((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ))))) |
57 | 56 | rexbidv 3172 |
. . . . . 6
โข (โ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ (โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((๐โ2) โ
((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท
(โโ2))) = 1 โง
(๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((๐โ2) โ
((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท
(((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ))))) |
58 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) โ (๐โ2) = (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2)) |
59 | 58 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) โ ((๐โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2)))) |
60 | 59 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) โ (((๐โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1)) |
61 | 60 | 3anbi1d 1441 |
. . . . . . . . 9
โข (๐ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) โ ((((๐โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด)) โ (((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด)))) |
62 | 61 | anbi2d 630 |
. . . . . . . 8
โข (๐ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((๐โ2) โ
((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท
(((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โ (((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))))) |
63 | 62 | anbi1d 631 |
. . . . . . 7
โข (๐ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) โ (((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((๐โ2) โ
((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท
(((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ))) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ))))) |
64 | 63 | rexbidv 3172 |
. . . . . 6
โข (๐ = ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) โ (โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((๐โ2) โ
((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท
(((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ))) โ โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ))))) |
65 | 42, 57, 64 | rspc3ev 3593 |
. . . . 5
โข ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ โ0 โง ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ โ0 โง ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต) โ โ0) โง
โ๐ โ
โ0 ((((((๐ด
Xrm ๐ต)โ2)
โ (((๐ดโ2)
โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท ((๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง (๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ (โคโฅโ2))
โง (((((๐ด + (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Xrm ๐ต)โ2) โ ((((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด)))โ2) โ 1) ยท (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต)โ2))) = 1 โง (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ ๐ด))) โง (((2 ยท ๐ถ) โฅ ((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (((๐ด + (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) ยท (((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ ๐ด))) Yrm ๐ต) โ ๐ต) โง ๐ต โค ๐ถ)))) โ โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) |
66 | 16, 25, 65 | syl2anc 585 |
. . . 4
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ = (๐ด Yrm ๐ต)) โ โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) |
67 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = (๐ด Xrm ๐ต) โ (๐โ2) = ((๐ด Xrm ๐ต)โ2)) |
68 | 67 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ = (๐ด Xrm ๐ต) โ ((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = (((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2)))) |
69 | 68 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ = (๐ด Xrm ๐ต) โ (((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โ (((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) =
1)) |
70 | 69 | 3anbi1d 1441 |
. . . . . . . . 9
โข (๐ = (๐ด Xrm ๐ต) โ ((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โ ((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)))) |
71 | 70 | anbi1d 631 |
. . . . . . . 8
โข (๐ = (๐ด Xrm ๐ต) โ (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โ (((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))))) |
72 | 71 | anbi1d 631 |
. . . . . . 7
โข (๐ = (๐ด Xrm ๐ต) โ ((((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |
73 | 72 | 2rexbidv 3210 |
. . . . . 6
โข (๐ = (๐ด Xrm ๐ต) โ (โ๐ โ โ0 โ๐ โ โ0
(((((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐ถโ2))) = 1
โง ((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐โ2))) = 1
โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ โ๐ โ โ0 โ๐ โ โ0
((((((๐ด Xrm
๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐โ2))) = 1
โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |
74 | 73 | 2rexbidv 3210 |
. . . . 5
โข (๐ = (๐ด Xrm ๐ต) โ (โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 (((((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐โ2))) = 1
โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐โ2))) = 1
โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |
75 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ = (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (๐โ2) = ((๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2)) |
76 | 75 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ = (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (((๐ดโ2) โ 1) ยท (๐โ2)) = (((๐ดโ2) โ 1) ยท ((๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2))) |
77 | 76 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ = (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ ((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐โ2))) = ((๐โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2)))) |
78 | 77 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ = (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐โ2))) = 1 โ ((๐โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) =
1)) |
79 | 78 | 3anbi2d 1442 |
. . . . . . . . 9
โข (๐ = (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โ ((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)))) |
80 | | eqeq1 2737 |
. . . . . . . . . 10
โข (๐ = (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โ (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))))) |
81 | 80 | 3anbi2d 1442 |
. . . . . . . . 9
โข (๐ = (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ ((((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด)) โ (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด)))) |
82 | 79, 81 | anbi12d 632 |
. . . . . . . 8
โข (๐ = (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โ (((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))))) |
83 | 82 | anbi1d 631 |
. . . . . . 7
โข (๐ = (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |
84 | 83 | 2rexbidv 3210 |
. . . . . 6
โข (๐ = (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (โ๐ โ โ0 โ๐ โ โ0
((((((๐ด Xrm
๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐โ2))) = 1
โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ โ๐ โ โ0 โ๐ โ โ0
((((((๐ด Xrm
๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท ((๐ด Yrm
(2 ยท (๐ต ยท
(๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |
85 | 84 | 2rexbidv 3210 |
. . . . 5
โข (๐ = (๐ด Yrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐โ2))) = 1
โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท ((๐ด Yrm
(2 ยท (๐ต ยท
(๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |
86 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (๐โ2) = ((๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2)) |
87 | 86 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ ((๐โ2) โ (((๐ดโ2) โ 1) ยท ((๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2))) = (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2)))) |
88 | 87 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (((๐โ2) โ (((๐ดโ2) โ 1) ยท ((๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โ
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) =
1)) |
89 | 88 | 3anbi2d 1442 |
. . . . . . . . 9
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โ ((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)))) |
90 | | breq1 5109 |
. . . . . . . . . 10
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (๐ โฅ (๐ โ ๐ด) โ (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด))) |
91 | 90 | 3anbi3d 1443 |
. . . . . . . . 9
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ ((((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด)) โ (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด)))) |
92 | 89, 91 | anbi12d 632 |
. . . . . . . 8
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โ (((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด))))) |
93 | | breq1 5109 |
. . . . . . . . . 10
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (๐ โฅ (โ โ ๐ถ) โ (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ))) |
94 | 93 | anbi2d 630 |
. . . . . . . . 9
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โ ((2 ยท ๐ถ) โฅ (๐ โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)))) |
95 | 94 | anbi1d 631 |
. . . . . . . 8
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ ((((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)) โ (((2 ยท ๐ถ) โฅ (๐ โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) |
96 | 92, 95 | anbi12d 632 |
. . . . . . 7
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง (((๐ด Xrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |
97 | 96 | 2rexbidv 3210 |
. . . . . 6
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (โ๐ โ โ0 โ๐ โ โ0
((((((๐ด Xrm
๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท ((๐ด Yrm
(2 ยท (๐ต ยท
(๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ โ๐ โ โ0 โ๐ โ โ0
((((((๐ด Xrm
๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |
98 | 97 | 2rexbidv 3210 |
. . . . 5
โข (๐ = (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ (โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท ((๐ด Yrm
(2 ยท (๐ต ยท
(๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 ((((((๐ด Xrm ๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |
99 | 74, 85, 98 | rspc3ev 3593 |
. . . 4
โข ((((๐ด Xrm ๐ต) โ โ0
โง (๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ โ0
โง (๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต)))) โ โ0)
โง โ๐ โ
โ0 โโ
โ โ0 โ๐ โ โ0 โ๐ โ โ0
((((((๐ด Xrm
๐ต)โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
(((๐ด Xrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2) โ (((๐ดโ2) โ 1) ยท
((๐ด Yrm (2
ยท (๐ต ยท (๐ด Yrm ๐ต))))โ2))) = 1 โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง (๐ด Yrm (2 ยท
(๐ต ยท (๐ด Yrm ๐ต)))) = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง (๐ด Xrm (2 ยท (๐ต ยท (๐ด Yrm ๐ต)))) โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ โ๐ โ โ0 โ๐ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 (((((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐โ2))) = 1
โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) |
100 | 15, 66, 99 | syl2anc 585 |
. . 3
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ = (๐ด Yrm ๐ต)) โ โ๐ โ โ0 โ๐ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 (((((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐โ2))) = 1
โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) |
101 | 100 | ex 414 |
. 2
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ = (๐ด Yrm ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 (((((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐โ2))) = 1
โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |
102 | | simpll1 1213 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โ ๐ด โ
(โคโฅโ2)) |
103 | 102 | ad3antrrr 729 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ด โ
(โคโฅโ2)) |
104 | | simpll2 1214 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โ ๐ต โ โ) |
105 | 104 | ad3antrrr 729 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ต โ โ) |
106 | | simpll3 1215 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โ ๐ถ โ โ) |
107 | 106 | ad3antrrr 729 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ถ โ โ) |
108 | | simplrl 776 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โ ๐ โ โ0) |
109 | 108 | ad3antrrr 729 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ โ โ0) |
110 | | simplrr 777 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โ ๐ โ โ0) |
111 | 110 | ad3antrrr 729 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ โ โ0) |
112 | | simprl 770 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โ ๐ โ โ0) |
113 | 112 | ad3antrrr 729 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ โ โ0) |
114 | | simprr 772 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โ ๐ โ โ0) |
115 | 114 | ad3antrrr 729 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ โ โ0) |
116 | | simprl 770 |
. . . . . . . 8
โข
(((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โ โ โ
โ0) |
117 | 116 | ad2antrr 725 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ โ โ โ0) |
118 | | simprr 772 |
. . . . . . . 8
โข
(((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โ ๐ โ
โ0) |
119 | 118 | ad2antrr 725 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ โ โ0) |
120 | | simplr 768 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ โ โ0) |
121 | | simp2l1 1273 |
. . . . . . . 8
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง ((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1) |
122 | 121 | 3expb 1121 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1) |
123 | | simp2l2 1274 |
. . . . . . . 8
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง ((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐โ2))) = 1) |
124 | 123 | 3expb 1121 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐โ2))) = 1) |
125 | | simp2l3 1275 |
. . . . . . . 8
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง ((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ๐ โ
(โคโฅโ2)) |
126 | 125 | 3expb 1121 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ โ
(โคโฅโ2)) |
127 | | simp2r1 1276 |
. . . . . . . 8
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง ((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1) |
128 | 127 | 3expb 1121 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1) |
129 | | simp2r2 1277 |
. . . . . . . 8
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง ((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2)))) |
130 | 129 | 3expb 1121 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2)))) |
131 | | simp2r3 1278 |
. . . . . . . 8
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง ((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ๐ โฅ (๐ โ ๐ด)) |
132 | 131 | 3expb 1121 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ โฅ (๐ โ ๐ด)) |
133 | | simp3ll 1245 |
. . . . . . . 8
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง ((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ (2 ยท ๐ถ) โฅ (๐ โ 1)) |
134 | 133 | 3expb 1121 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ (2 ยท ๐ถ) โฅ (๐ โ 1)) |
135 | | simp3lr 1246 |
. . . . . . . 8
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง ((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ๐ โฅ (โ โ ๐ถ)) |
136 | 135 | 3expb 1121 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ โฅ (โ โ ๐ถ)) |
137 | | simp3rl 1247 |
. . . . . . . 8
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง ((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ (2 ยท ๐ถ) โฅ (โ โ ๐ต)) |
138 | 137 | 3expb 1121 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ (2 ยท ๐ถ) โฅ (โ โ ๐ต)) |
139 | | simp3rr 1248 |
. . . . . . . 8
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง ((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ๐ต โค ๐ถ) |
140 | 139 | 3expb 1121 |
. . . . . . 7
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ต โค ๐ถ) |
141 | 103, 105,
107, 109, 111, 113, 115, 117, 119, 120, 122, 124, 126, 128, 130, 132, 134, 136, 138, 140 | jm2.27b 41373 |
. . . . . 6
โข
(((((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โง ๐ โ
โ0) โง (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ)))) โ ๐ถ = (๐ด Yrm ๐ต)) |
142 | 141 | rexlimdva2 3151 |
. . . . 5
โข
(((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โง (โ โ โ0 โง ๐ โ โ0))
โ (โ๐ โ
โ0 (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ๐ถ = (๐ด Yrm ๐ต))) |
143 | 142 | rexlimdvva 3202 |
. . . 4
โข ((((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โง (๐ โ
โ0 โง ๐
โ โ0)) โ (โโ โ โ0 โ๐ โ โ0
โ๐ โ
โ0 (((((๐โ2) โ (((๐ดโ2) โ 1) ยท (๐ถโ2))) = 1 โง ((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐โ2))) = 1 โง
๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ๐ถ = (๐ด Yrm ๐ต))) |
144 | 143 | rexlimdvva 3202 |
. . 3
โข (((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ โ โ0 โง ๐ โ โ0))
โ (โ๐ โ
โ0 โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 (((((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐โ2))) = 1
โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ๐ถ = (๐ด Yrm ๐ต))) |
145 | 144 | rexlimdvva 3202 |
. 2
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โ (โ๐ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 โ๐ โ โ0
โโ โ
โ0 โ๐ โ โ0 โ๐ โ โ0
(((((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐ถโ2))) = 1
โง ((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐โ2))) = 1
โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))) โ ๐ถ = (๐ด Yrm ๐ต))) |
146 | 101, 145 | impbid 211 |
1
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ = (๐ด Yrm ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 โโ โ โ0
โ๐ โ
โ0 โ๐ โ โ0 (((((๐โ2) โ (((๐ดโ2) โ 1) ยท
(๐ถโ2))) = 1 โง
((๐โ2) โ
(((๐ดโ2) โ 1)
ยท (๐โ2))) = 1
โง ๐ โ
(โคโฅโ2)) โง (((๐โ2) โ (((๐โ2) โ 1) ยท (โโ2))) = 1 โง ๐ = ((๐ + 1) ยท (2 ยท (๐ถโ2))) โง ๐ โฅ (๐ โ ๐ด))) โง (((2 ยท ๐ถ) โฅ (๐ โ 1) โง ๐ โฅ (โ โ ๐ถ)) โง ((2 ยท ๐ถ) โฅ (โ โ ๐ต) โง ๐ต โค ๐ถ))))) |