Step | Hyp | Ref
| Expression |
1 | | elreal 7826 |
. . . 4
โข (๐ด โ โ โ
โ๐ฆ โ
R โจ๐ฆ,
0Rโฉ = ๐ด) |
2 | | df-rex 2461 |
. . . 4
โข
(โ๐ฆ โ
R โจ๐ฆ,
0Rโฉ = ๐ด โ โ๐ฆ(๐ฆ โ R โง โจ๐ฆ,
0Rโฉ = ๐ด)) |
3 | 1, 2 | bitri 184 |
. . 3
โข (๐ด โ โ โ
โ๐ฆ(๐ฆ โ R โง โจ๐ฆ,
0Rโฉ = ๐ด)) |
4 | | breq2 4007 |
. . . 4
โข
(โจ๐ฆ,
0Rโฉ = ๐ด โ (0 <โ
โจ๐ฆ,
0Rโฉ โ 0 <โ ๐ด)) |
5 | | oveq1 5881 |
. . . . . . 7
โข
(โจ๐ฆ,
0Rโฉ = ๐ด โ (โจ๐ฆ, 0Rโฉ ยท
๐ฅ) = (๐ด ยท ๐ฅ)) |
6 | 5 | eqeq1d 2186 |
. . . . . 6
โข
(โจ๐ฆ,
0Rโฉ = ๐ด โ ((โจ๐ฆ, 0Rโฉ ยท
๐ฅ) = 1 โ (๐ด ยท ๐ฅ) = 1)) |
7 | 6 | anbi2d 464 |
. . . . 5
โข
(โจ๐ฆ,
0Rโฉ = ๐ด โ ((0 <โ ๐ฅ โง (โจ๐ฆ, 0Rโฉ ยท
๐ฅ) = 1) โ (0
<โ ๐ฅ
โง (๐ด ยท ๐ฅ) = 1))) |
8 | 7 | rexbidv 2478 |
. . . 4
โข
(โจ๐ฆ,
0Rโฉ = ๐ด โ (โ๐ฅ โ โ (0 <โ
๐ฅ โง (โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = 1) โ โ๐ฅ โ โ (0 <โ
๐ฅ โง (๐ด ยท ๐ฅ) = 1))) |
9 | 4, 8 | imbi12d 234 |
. . 3
โข
(โจ๐ฆ,
0Rโฉ = ๐ด โ ((0 <โ
โจ๐ฆ,
0Rโฉ โ โ๐ฅ โ โ (0 <โ
๐ฅ โง (โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = 1)) โ (0 <โ
๐ด โ โ๐ฅ โ โ (0
<โ ๐ฅ
โง (๐ด ยท ๐ฅ) = 1)))) |
10 | | df-0 7817 |
. . . . . 6
โข 0 =
โจ0R,
0Rโฉ |
11 | 10 | breq1i 4010 |
. . . . 5
โข (0
<โ โจ๐ฆ, 0Rโฉ โ
โจ0R, 0Rโฉ
<โ โจ๐ฆ,
0Rโฉ) |
12 | | ltresr 7837 |
. . . . 5
โข
(โจ0R, 0Rโฉ
<โ โจ๐ฆ, 0Rโฉ โ
0R <R ๐ฆ) |
13 | 11, 12 | bitri 184 |
. . . 4
โข (0
<โ โจ๐ฆ, 0Rโฉ โ
0R <R ๐ฆ) |
14 | | recexgt0sr 7771 |
. . . . 5
โข
(0R <R ๐ฆ โ โ๐ง โ R
(0R <R ๐ง โง (๐ฆ ยทR ๐ง) =
1R)) |
15 | | opelreal 7825 |
. . . . . . . . . 10
โข
(โจ๐ง,
0Rโฉ โ โ โ ๐ง โ R) |
16 | 15 | anbi1i 458 |
. . . . . . . . 9
โข
((โจ๐ง,
0Rโฉ โ โ โง (0
<โ โจ๐ง, 0Rโฉ โง
(โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1))
โ (๐ง โ
R โง (0 <โ โจ๐ง, 0Rโฉ โง
(โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) =
1))) |
17 | 10 | breq1i 4010 |
. . . . . . . . . . . . 13
โข (0
<โ โจ๐ง, 0Rโฉ โ
โจ0R, 0Rโฉ
<โ โจ๐ง,
0Rโฉ) |
18 | | ltresr 7837 |
. . . . . . . . . . . . 13
โข
(โจ0R, 0Rโฉ
<โ โจ๐ง, 0Rโฉ โ
0R <R ๐ง) |
19 | 17, 18 | bitri 184 |
. . . . . . . . . . . 12
โข (0
<โ โจ๐ง, 0Rโฉ โ
0R <R ๐ง) |
20 | 19 | a1i 9 |
. . . . . . . . . . 11
โข ((๐ฆ โ R โง
๐ง โ R)
โ (0 <โ โจ๐ง, 0Rโฉ โ
0R <R ๐ง)) |
21 | | mulresr 7836 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ R โง
๐ง โ R)
โ (โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) =
โจ(๐ฆ
ยทR ๐ง),
0Rโฉ) |
22 | 21 | eqeq1d 2186 |
. . . . . . . . . . . 12
โข ((๐ฆ โ R โง
๐ง โ R)
โ ((โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1
โ โจ(๐ฆ
ยทR ๐ง), 0Rโฉ =
1)) |
23 | | df-1 7818 |
. . . . . . . . . . . . . 14
โข 1 =
โจ1R,
0Rโฉ |
24 | 23 | eqeq2i 2188 |
. . . . . . . . . . . . 13
โข
(โจ(๐ฆ
ยทR ๐ง), 0Rโฉ = 1
โ โจ(๐ฆ
ยทR ๐ง), 0Rโฉ =
โจ1R,
0Rโฉ) |
25 | | eqid 2177 |
. . . . . . . . . . . . . 14
โข
0R =
0R |
26 | | 1sr 7749 |
. . . . . . . . . . . . . . 15
โข
1R โ R |
27 | | 0r 7748 |
. . . . . . . . . . . . . . 15
โข
0R โ R |
28 | | opthg2 4239 |
. . . . . . . . . . . . . . 15
โข
((1R โ R โง
0R โ R) โ (โจ(๐ฆ
ยทR ๐ง), 0Rโฉ =
โจ1R, 0Rโฉ โ
((๐ฆ
ยทR ๐ง) = 1R โง
0R = 0R))) |
29 | 26, 27, 28 | mp2an 426 |
. . . . . . . . . . . . . 14
โข
(โจ(๐ฆ
ยทR ๐ง), 0Rโฉ =
โจ1R, 0Rโฉ โ
((๐ฆ
ยทR ๐ง) = 1R โง
0R = 0R)) |
30 | 25, 29 | mpbiran2 941 |
. . . . . . . . . . . . 13
โข
(โจ(๐ฆ
ยทR ๐ง), 0Rโฉ =
โจ1R, 0Rโฉ โ
(๐ฆ
ยทR ๐ง) =
1R) |
31 | 24, 30 | bitri 184 |
. . . . . . . . . . . 12
โข
(โจ(๐ฆ
ยทR ๐ง), 0Rโฉ = 1
โ (๐ฆ
ยทR ๐ง) =
1R) |
32 | 22, 31 | bitrdi 196 |
. . . . . . . . . . 11
โข ((๐ฆ โ R โง
๐ง โ R)
โ ((โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1
โ (๐ฆ
ยทR ๐ง) =
1R)) |
33 | 20, 32 | anbi12d 473 |
. . . . . . . . . 10
โข ((๐ฆ โ R โง
๐ง โ R)
โ ((0 <โ โจ๐ง, 0Rโฉ โง
(โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1)
โ (0R <R ๐ง โง (๐ฆ ยทR ๐ง) =
1R))) |
34 | 33 | pm5.32da 452 |
. . . . . . . . 9
โข (๐ฆ โ R โ
((๐ง โ R
โง (0 <โ โจ๐ง, 0Rโฉ โง
(โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1))
โ (๐ง โ
R โง (0R
<R ๐ง โง (๐ฆ ยทR ๐ง) =
1R)))) |
35 | 16, 34 | bitrid 192 |
. . . . . . . 8
โข (๐ฆ โ R โ
((โจ๐ง,
0Rโฉ โ โ โง (0
<โ โจ๐ง, 0Rโฉ โง
(โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1))
โ (๐ง โ
R โง (0R
<R ๐ง โง (๐ฆ ยทR ๐ง) =
1R)))) |
36 | | breq2 4007 |
. . . . . . . . . 10
โข (๐ฅ = โจ๐ง, 0Rโฉ โ (0
<โ ๐ฅ
โ 0 <โ โจ๐ง,
0Rโฉ)) |
37 | | oveq2 5882 |
. . . . . . . . . . 11
โข (๐ฅ = โจ๐ง, 0Rโฉ โ
(โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = (โจ๐ฆ, 0Rโฉ ยท
โจ๐ง,
0Rโฉ)) |
38 | 37 | eqeq1d 2186 |
. . . . . . . . . 10
โข (๐ฅ = โจ๐ง, 0Rโฉ โ
((โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = 1 โ (โจ๐ฆ, 0Rโฉ ยท
โจ๐ง,
0Rโฉ) = 1)) |
39 | 36, 38 | anbi12d 473 |
. . . . . . . . 9
โข (๐ฅ = โจ๐ง, 0Rโฉ โ
((0 <โ ๐ฅ โง (โจ๐ฆ, 0Rโฉ ยท
๐ฅ) = 1) โ (0
<โ โจ๐ง, 0Rโฉ โง
(โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) =
1))) |
40 | 39 | rspcev 2841 |
. . . . . . . 8
โข
((โจ๐ง,
0Rโฉ โ โ โง (0
<โ โจ๐ง, 0Rโฉ โง
(โจ๐ฆ,
0Rโฉ ยท โจ๐ง, 0Rโฉ) = 1))
โ โ๐ฅ โ
โ (0 <โ ๐ฅ โง (โจ๐ฆ, 0Rโฉ ยท
๐ฅ) = 1)) |
41 | 35, 40 | syl6bir 164 |
. . . . . . 7
โข (๐ฆ โ R โ
((๐ง โ R
โง (0R <R ๐ง โง (๐ฆ ยทR ๐ง) =
1R)) โ โ๐ฅ โ โ (0 <โ
๐ฅ โง (โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = 1))) |
42 | 41 | expd 258 |
. . . . . 6
โข (๐ฆ โ R โ
(๐ง โ R
โ ((0R <R ๐ง โง (๐ฆ ยทR ๐ง) = 1R)
โ โ๐ฅ โ
โ (0 <โ ๐ฅ โง (โจ๐ฆ, 0Rโฉ ยท
๐ฅ) = 1)))) |
43 | 42 | rexlimdv 2593 |
. . . . 5
โข (๐ฆ โ R โ
(โ๐ง โ
R (0R <R
๐ง โง (๐ฆ ยทR ๐ง) = 1R)
โ โ๐ฅ โ
โ (0 <โ ๐ฅ โง (โจ๐ฆ, 0Rโฉ ยท
๐ฅ) = 1))) |
44 | 14, 43 | syl5 32 |
. . . 4
โข (๐ฆ โ R โ
(0R <R ๐ฆ โ โ๐ฅ โ โ (0 <โ
๐ฅ โง (โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = 1))) |
45 | 13, 44 | biimtrid 152 |
. . 3
โข (๐ฆ โ R โ
(0 <โ โจ๐ฆ, 0Rโฉ โ
โ๐ฅ โ โ (0
<โ ๐ฅ
โง (โจ๐ฆ,
0Rโฉ ยท ๐ฅ) = 1))) |
46 | 3, 9, 45 | gencl 2769 |
. 2
โข (๐ด โ โ โ (0
<โ ๐ด
โ โ๐ฅ โ
โ (0 <โ ๐ฅ โง (๐ด ยท ๐ฅ) = 1))) |
47 | 46 | imp 124 |
1
โข ((๐ด โ โ โง 0
<โ ๐ด)
โ โ๐ฅ โ
โ (0 <โ ๐ฅ โง (๐ด ยท ๐ฅ) = 1)) |