Step | Hyp | Ref
| Expression |
1 | | axprecex 7878 |
. . 3
โข ((๐ด โ โ โง 0
<โ ๐ด)
โ โ๐ฅ โ
โ (0 <โ ๐ฅ โง (๐ด ยท ๐ฅ) = 1)) |
2 | | simpr 110 |
. . . 4
โข ((0
<โ ๐ฅ
โง (๐ด ยท ๐ฅ) = 1) โ (๐ด ยท ๐ฅ) = 1) |
3 | 2 | reximi 2574 |
. . 3
โข
(โ๐ฅ โ
โ (0 <โ ๐ฅ โง (๐ด ยท ๐ฅ) = 1) โ โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1) |
4 | 1, 3 | syl 14 |
. 2
โข ((๐ด โ โ โง 0
<โ ๐ด)
โ โ๐ฅ โ
โ (๐ด ยท ๐ฅ) = 1) |
5 | | eqtr3 2197 |
. . . . 5
โข (((๐ด ยท ๐ฅ) = 1 โง (๐ด ยท ๐ฆ) = 1) โ (๐ด ยท ๐ฅ) = (๐ด ยท ๐ฆ)) |
6 | | axprecex 7878 |
. . . . . . 7
โข ((๐ด โ โ โง 0
<โ ๐ด)
โ โ๐ง โ
โ (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1)) |
7 | 6 | adantr 276 |
. . . . . 6
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ โ๐ง โ
โ (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1)) |
8 | | axresscn 7858 |
. . . . . . . . . . . . 13
โข โ
โ โ |
9 | | simpll 527 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ ๐ด โ
โ) |
10 | 8, 9 | sselid 3153 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ ๐ด โ
โ) |
11 | | simprl 529 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ ๐ฅ โ
โ) |
12 | 8, 11 | sselid 3153 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ ๐ฅ โ
โ) |
13 | | axmulcom 7869 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ฅ โ โ) โ (๐ด ยท ๐ฅ) = (๐ฅ ยท ๐ด)) |
14 | 10, 12, 13 | syl2anc 411 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ (๐ด ยท ๐ฅ) = (๐ฅ ยท ๐ด)) |
15 | | simprr 531 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ ๐ฆ โ
โ) |
16 | 8, 15 | sselid 3153 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ ๐ฆ โ
โ) |
17 | | axmulcom 7869 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ฆ โ โ) โ (๐ด ยท ๐ฆ) = (๐ฆ ยท ๐ด)) |
18 | 10, 16, 17 | syl2anc 411 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ (๐ด ยท ๐ฆ) = (๐ฆ ยท ๐ด)) |
19 | 14, 18 | eqeq12d 2192 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ ((๐ด ยท ๐ฅ) = (๐ด ยท ๐ฆ) โ (๐ฅ ยท ๐ด) = (๐ฆ ยท ๐ด))) |
20 | 19 | adantr 276 |
. . . . . . . . 9
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ ((๐ด ยท ๐ฅ) = (๐ด ยท ๐ฆ) โ (๐ฅ ยท ๐ด) = (๐ฆ ยท ๐ด))) |
21 | | oveq1 5881 |
. . . . . . . . 9
โข ((๐ฅ ยท ๐ด) = (๐ฆ ยท ๐ด) โ ((๐ฅ ยท ๐ด) ยท ๐ง) = ((๐ฆ ยท ๐ด) ยท ๐ง)) |
22 | 20, 21 | syl6bi 163 |
. . . . . . . 8
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ ((๐ด ยท ๐ฅ) = (๐ด ยท ๐ฆ) โ ((๐ฅ ยท ๐ด) ยท ๐ง) = ((๐ฆ ยท ๐ด) ยท ๐ง))) |
23 | 12 | adantr 276 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ ๐ฅ โ โ) |
24 | 10 | adantr 276 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ ๐ด โ โ) |
25 | | simprl 529 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ ๐ง โ โ) |
26 | 8, 25 | sselid 3153 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ ๐ง โ โ) |
27 | | axmulass 7871 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ด โ โ โง ๐ง โ โ) โ ((๐ฅ ยท ๐ด) ยท ๐ง) = (๐ฅ ยท (๐ด ยท ๐ง))) |
28 | 23, 24, 26, 27 | syl3anc 1238 |
. . . . . . . . 9
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ ((๐ฅ ยท ๐ด) ยท ๐ง) = (๐ฅ ยท (๐ด ยท ๐ง))) |
29 | 16 | adantr 276 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ ๐ฆ โ โ) |
30 | | axmulass 7871 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ๐ด โ โ โง ๐ง โ โ) โ ((๐ฆ ยท ๐ด) ยท ๐ง) = (๐ฆ ยท (๐ด ยท ๐ง))) |
31 | 29, 24, 26, 30 | syl3anc 1238 |
. . . . . . . . 9
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ ((๐ฆ ยท ๐ด) ยท ๐ง) = (๐ฆ ยท (๐ด ยท ๐ง))) |
32 | 28, 31 | eqeq12d 2192 |
. . . . . . . 8
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ (((๐ฅ ยท ๐ด) ยท ๐ง) = ((๐ฆ ยท ๐ด) ยท ๐ง) โ (๐ฅ ยท (๐ด ยท ๐ง)) = (๐ฆ ยท (๐ด ยท ๐ง)))) |
33 | 22, 32 | sylibd 149 |
. . . . . . 7
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ ((๐ด ยท ๐ฅ) = (๐ด ยท ๐ฆ) โ (๐ฅ ยท (๐ด ยท ๐ง)) = (๐ฆ ยท (๐ด ยท ๐ง)))) |
34 | | oveq2 5882 |
. . . . . . . . . 10
โข ((๐ด ยท ๐ง) = 1 โ (๐ฅ ยท (๐ด ยท ๐ง)) = (๐ฅ ยท 1)) |
35 | 34 | ad2antll 491 |
. . . . . . . . 9
โข ((๐ง โ โ โง (0
<โ ๐ง
โง (๐ด ยท ๐ง) = 1)) โ (๐ฅ ยท (๐ด ยท ๐ง)) = (๐ฅ ยท 1)) |
36 | | ax1rid 7875 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ (๐ฅ ยท 1) = ๐ฅ) |
37 | 11, 36 | syl 14 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ (๐ฅ ยท 1) =
๐ฅ) |
38 | 35, 37 | sylan9eqr 2232 |
. . . . . . . 8
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ (๐ฅ ยท (๐ด ยท ๐ง)) = ๐ฅ) |
39 | | oveq2 5882 |
. . . . . . . . . 10
โข ((๐ด ยท ๐ง) = 1 โ (๐ฆ ยท (๐ด ยท ๐ง)) = (๐ฆ ยท 1)) |
40 | 39 | ad2antll 491 |
. . . . . . . . 9
โข ((๐ง โ โ โง (0
<โ ๐ง
โง (๐ด ยท ๐ง) = 1)) โ (๐ฆ ยท (๐ด ยท ๐ง)) = (๐ฆ ยท 1)) |
41 | | ax1rid 7875 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (๐ฆ ยท 1) = ๐ฆ) |
42 | 41 | ad2antll 491 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ (๐ฆ ยท 1) =
๐ฆ) |
43 | 40, 42 | sylan9eqr 2232 |
. . . . . . . 8
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ (๐ฆ ยท (๐ด ยท ๐ง)) = ๐ฆ) |
44 | 38, 43 | eqeq12d 2192 |
. . . . . . 7
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ ((๐ฅ ยท (๐ด ยท ๐ง)) = (๐ฆ ยท (๐ด ยท ๐ง)) โ ๐ฅ = ๐ฆ)) |
45 | 33, 44 | sylibd 149 |
. . . . . 6
โข ((((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โง (๐ง โ โ
โง (0 <โ ๐ง โง (๐ด ยท ๐ง) = 1))) โ ((๐ด ยท ๐ฅ) = (๐ด ยท ๐ฆ) โ ๐ฅ = ๐ฆ)) |
46 | 7, 45 | rexlimddv 2599 |
. . . . 5
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ ((๐ด ยท ๐ฅ) = (๐ด ยท ๐ฆ) โ ๐ฅ = ๐ฆ)) |
47 | 5, 46 | syl5 32 |
. . . 4
โข (((๐ด โ โ โง 0
<โ ๐ด)
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ (((๐ด ยท ๐ฅ) = 1 โง (๐ด ยท ๐ฆ) = 1) โ ๐ฅ = ๐ฆ)) |
48 | 47 | ralrimivva 2559 |
. . 3
โข ((๐ด โ โ โง 0
<โ ๐ด)
โ โ๐ฅ โ
โ โ๐ฆ โ
โ (((๐ด ยท ๐ฅ) = 1 โง (๐ด ยท ๐ฆ) = 1) โ ๐ฅ = ๐ฆ)) |
49 | | oveq2 5882 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ด ยท ๐ฅ) = (๐ด ยท ๐ฆ)) |
50 | 49 | eqeq1d 2186 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((๐ด ยท ๐ฅ) = 1 โ (๐ด ยท ๐ฆ) = 1)) |
51 | 50 | rmo4 2930 |
. . 3
โข
(โ*๐ฅ โ
โ (๐ด ยท ๐ฅ) = 1 โ โ๐ฅ โ โ โ๐ฆ โ โ (((๐ด ยท ๐ฅ) = 1 โง (๐ด ยท ๐ฆ) = 1) โ ๐ฅ = ๐ฆ)) |
52 | 48, 51 | sylibr 134 |
. 2
โข ((๐ด โ โ โง 0
<โ ๐ด)
โ โ*๐ฅ โ
โ (๐ด ยท ๐ฅ) = 1) |
53 | | reu5 2689 |
. 2
โข
(โ!๐ฅ โ
โ (๐ด ยท ๐ฅ) = 1 โ (โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1 โง โ*๐ฅ โ โ (๐ด ยท ๐ฅ) = 1)) |
54 | 4, 52, 53 | sylanbrc 417 |
1
โข ((๐ด โ โ โง 0
<โ ๐ด)
โ โ!๐ฅ โ
โ (๐ด ยท ๐ฅ) = 1) |