Step | Hyp | Ref
| Expression |
1 | | cnre 7952 |
. . 3
โข (๐ด โ โ โ
โ๐ โ โ
โ๐ โ โ
๐ด = (๐ + (i ยท ๐))) |
2 | | recexaplem2 8608 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ โง (๐ + (i ยท ๐)) # 0) โ ((๐ ยท ๐) + (๐ ยท ๐)) # 0) |
3 | 2 | 3expia 1205 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ + (i ยท ๐)) # 0 โ ((๐ ยท ๐) + (๐ ยท ๐)) # 0)) |
4 | | remulcl 7938 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
5 | 4 | anidms 397 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ ยท ๐) โ โ) |
6 | | remulcl 7938 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
7 | 6 | anidms 397 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ ยท ๐) โ โ) |
8 | | readdcl 7936 |
. . . . . . . . . . 11
โข (((๐ ยท ๐) โ โ โง (๐ ยท ๐) โ โ) โ ((๐ ยท ๐) + (๐ ยท ๐)) โ โ) |
9 | 5, 7, 8 | syl2an 289 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) + (๐ ยท ๐)) โ โ) |
10 | | 0re 7956 |
. . . . . . . . . 10
โข 0 โ
โ |
11 | | apreap 8543 |
. . . . . . . . . 10
โข ((((๐ ยท ๐) + (๐ ยท ๐)) โ โ โง 0 โ โ)
โ (((๐ ยท ๐) + (๐ ยท ๐)) # 0 โ ((๐ ยท ๐) + (๐ ยท ๐)) #โ 0)) |
12 | 9, 10, 11 | sylancl 413 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ ยท ๐) + (๐ ยท ๐)) # 0 โ ((๐ ยท ๐) + (๐ ยท ๐)) #โ 0)) |
13 | | recexre 8534 |
. . . . . . . . . . . 12
โข ((((๐ ยท ๐) + (๐ ยท ๐)) โ โ โง ((๐ ยท ๐) + (๐ ยท ๐)) #โ 0) โ โ๐ฆ โ โ (((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ) = 1) |
14 | 9, 13 | sylan 283 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ((๐ ยท ๐) + (๐ ยท ๐)) #โ 0) โ โ๐ฆ โ โ (((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ) = 1) |
15 | | recn 7943 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
16 | | recn 7943 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
17 | | recn 7943 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
18 | | ax-icn 7905 |
. . . . . . . . . . . . . . . . . . . . 21
โข i โ
โ |
19 | | mulcl 7937 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((i
โ โ โง ๐
โ โ) โ (i ยท ๐) โ โ) |
20 | 18, 19 | mpan 424 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ (i
ยท ๐) โ
โ) |
21 | | subcl 8155 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง (i
ยท ๐) โ โ)
โ (๐ โ (i
ยท ๐)) โ
โ) |
22 | 20, 21 | sylan2 286 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โ (i ยท ๐)) โ
โ) |
23 | | mulcl 7937 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ (i ยท ๐)) โ โ โง ๐ฆ โ โ) โ ((๐ โ (i ยท ๐)) ยท ๐ฆ) โ โ) |
24 | 22, 23 | sylan 283 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง ๐ โ โ) โง ๐ฆ โ โ) โ ((๐ โ (i ยท ๐)) ยท ๐ฆ) โ โ) |
25 | 24 | adantr 276 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ฆ โ โ) โง (((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ) = 1) โ ((๐ โ (i ยท ๐)) ยท ๐ฆ) โ โ) |
26 | | addcl 7935 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ โ โง (i
ยท ๐) โ โ)
โ (๐ + (i ยท
๐)) โ
โ) |
27 | 20, 26 | sylan2 286 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + (i ยท ๐)) โ
โ) |
28 | 27 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ โง ๐ โ โ) โง ๐ฆ โ โ) โ (๐ + (i ยท ๐)) โ
โ) |
29 | 22 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ โง ๐ โ โ) โง ๐ฆ โ โ) โ (๐ โ (i ยท ๐)) โ
โ) |
30 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ โง ๐ โ โ) โง ๐ฆ โ โ) โ ๐ฆ โ
โ) |
31 | 28, 29, 30 | mulassd 7980 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ โง ๐ โ โ) โง ๐ฆ โ โ) โ (((๐ + (i ยท ๐)) ยท (๐ โ (i ยท ๐))) ยท ๐ฆ) = ((๐ + (i ยท ๐)) ยท ((๐ โ (i ยท ๐)) ยท ๐ฆ))) |
32 | | recextlem1 8607 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ + (i ยท ๐)) ยท (๐ โ (i ยท ๐))) = ((๐ ยท ๐) + (๐ ยท ๐))) |
33 | 32 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ โง ๐ โ โ) โง ๐ฆ โ โ) โ ((๐ + (i ยท ๐)) ยท (๐ โ (i ยท ๐))) = ((๐ ยท ๐) + (๐ ยท ๐))) |
34 | 33 | oveq1d 5889 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ โง ๐ โ โ) โง ๐ฆ โ โ) โ (((๐ + (i ยท ๐)) ยท (๐ โ (i ยท ๐))) ยท ๐ฆ) = (((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ)) |
35 | 31, 34 | eqtr3d 2212 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง ๐ โ โ) โง ๐ฆ โ โ) โ ((๐ + (i ยท ๐)) ยท ((๐ โ (i ยท ๐)) ยท ๐ฆ)) = (((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ)) |
36 | | id 19 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ) = 1 โ (((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ) = 1) |
37 | 35, 36 | sylan9eq 2230 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ฆ โ โ) โง (((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ) = 1) โ ((๐ + (i ยท ๐)) ยท ((๐ โ (i ยท ๐)) ยท ๐ฆ)) = 1) |
38 | | oveq2 5882 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ = ((๐ โ (i ยท ๐)) ยท ๐ฆ) โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = ((๐ + (i ยท ๐)) ยท ((๐ โ (i ยท ๐)) ยท ๐ฆ))) |
39 | 38 | eqeq1d 2186 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ = ((๐ โ (i ยท ๐)) ยท ๐ฆ) โ (((๐ + (i ยท ๐)) ยท ๐ฅ) = 1 โ ((๐ + (i ยท ๐)) ยท ((๐ โ (i ยท ๐)) ยท ๐ฆ)) = 1)) |
40 | 39 | rspcev 2841 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ (i ยท ๐)) ยท ๐ฆ) โ โ โง ((๐ + (i ยท ๐)) ยท ((๐ โ (i ยท ๐)) ยท ๐ฆ)) = 1) โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1) |
41 | 25, 37, 40 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ฆ โ โ) โง (((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ) = 1) โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1) |
42 | 41 | exp31 364 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ โ) โ (๐ฆ โ โ โ ((((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ) = 1 โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1))) |
43 | 17, 42 | syl5 32 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ (๐ฆ โ โ โ ((((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ) = 1 โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1))) |
44 | 43 | rexlimdv 2593 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ
(โ๐ฆ โ โ
(((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ) = 1 โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1)) |
45 | 15, 16, 44 | syl2an 289 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ
(โ๐ฆ โ โ
(((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ) = 1 โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1)) |
46 | 45 | adantr 276 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ((๐ ยท ๐) + (๐ ยท ๐)) #โ 0) โ
(โ๐ฆ โ โ
(((๐ ยท ๐) + (๐ ยท ๐)) ยท ๐ฆ) = 1 โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1)) |
47 | 14, 46 | mpd 13 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ((๐ ยท ๐) + (๐ ยท ๐)) #โ 0) โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1) |
48 | 47 | ex 115 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ ยท ๐) + (๐ ยท ๐)) #โ 0 โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1)) |
49 | 12, 48 | sylbid 150 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ ยท ๐) + (๐ ยท ๐)) # 0 โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1)) |
50 | 3, 49 | syld 45 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ + (i ยท ๐)) # 0 โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1)) |
51 | 50 | adantr 276 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ด = (๐ + (i ยท ๐))) โ ((๐ + (i ยท ๐)) # 0 โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1)) |
52 | | breq1 4006 |
. . . . . . 7
โข (๐ด = (๐ + (i ยท ๐)) โ (๐ด # 0 โ (๐ + (i ยท ๐)) # 0)) |
53 | 52 | adantl 277 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ด = (๐ + (i ยท ๐))) โ (๐ด # 0 โ (๐ + (i ยท ๐)) # 0)) |
54 | | oveq1 5881 |
. . . . . . . . 9
โข (๐ด = (๐ + (i ยท ๐)) โ (๐ด ยท ๐ฅ) = ((๐ + (i ยท ๐)) ยท ๐ฅ)) |
55 | 54 | eqeq1d 2186 |
. . . . . . . 8
โข (๐ด = (๐ + (i ยท ๐)) โ ((๐ด ยท ๐ฅ) = 1 โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1)) |
56 | 55 | rexbidv 2478 |
. . . . . . 7
โข (๐ด = (๐ + (i ยท ๐)) โ (โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1 โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1)) |
57 | 56 | adantl 277 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ด = (๐ + (i ยท ๐))) โ (โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1 โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) ยท ๐ฅ) = 1)) |
58 | 51, 53, 57 | 3imtr4d 203 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ด = (๐ + (i ยท ๐))) โ (๐ด # 0 โ โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1)) |
59 | 58 | ex 115 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (๐ด = (๐ + (i ยท ๐)) โ (๐ด # 0 โ โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1))) |
60 | 59 | rexlimivv 2600 |
. . 3
โข
(โ๐ โ
โ โ๐ โ
โ ๐ด = (๐ + (i ยท ๐)) โ (๐ด # 0 โ โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1)) |
61 | 1, 60 | syl 14 |
. 2
โข (๐ด โ โ โ (๐ด # 0 โ โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1)) |
62 | 61 | imp 124 |
1
โข ((๐ด โ โ โง ๐ด # 0) โ โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1) |