Step | Hyp | Ref
| Expression |
1 | | simpll 765 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ
โ) |
2 | | simprl 769 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ๐ โ
โ) |
3 | | reccl 11915 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ 0) โ (1 / ๐) โ
โ) |
4 | 3 | adantr 479 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (1 / ๐) โ
โ) |
5 | 1, 2, 4 | mul32d 11460 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท ๐) ยท (1 / ๐)) = ((๐ ยท (1 / ๐)) ยท ๐)) |
6 | | recid 11922 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ 0) โ (๐ ยท (1 / ๐)) = 1) |
7 | 6 | oveq1d 7439 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ 0) โ ((๐ ยท (1 / ๐)) ยท ๐) = (1 ยท ๐)) |
8 | 7 | adantr 479 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท (1 / ๐)) ยท ๐) = (1 ยท ๐)) |
9 | | mullid 11249 |
. . . . . . 7
โข (๐ โ โ โ (1
ยท ๐) = ๐) |
10 | 9 | ad2antrl 726 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (1 ยท
๐) = ๐) |
11 | 5, 8, 10 | 3eqtrd 2771 |
. . . . 5
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท ๐) ยท (1 / ๐)) = ๐) |
12 | | reccl 11915 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ 0) โ (1 / ๐) โ
โ) |
13 | 12 | adantl 480 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (1 / ๐) โ
โ) |
14 | 1, 2, 13 | mulassd 11273 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท ๐) ยท (1 / ๐)) = (๐ ยท (๐ ยท (1 / ๐)))) |
15 | | recid 11922 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ 0) โ (๐ ยท (1 / ๐)) = 1) |
16 | 15 | oveq2d 7440 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ 0) โ (๐ ยท (๐ ยท (1 / ๐))) = (๐ ยท 1)) |
17 | 16 | adantl 480 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (๐ ยท (๐ ยท (1 / ๐))) = (๐ ยท 1)) |
18 | | mulrid 11248 |
. . . . . . 7
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
19 | 18 | ad2antrr 724 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (๐ ยท 1) = ๐) |
20 | 14, 17, 19 | 3eqtrd 2771 |
. . . . 5
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท ๐) ยท (1 / ๐)) = ๐) |
21 | 11, 20 | oveq12d 7442 |
. . . 4
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (((๐ ยท ๐) ยท (1 / ๐)) + ((๐ ยท ๐) ยท (1 / ๐))) = (๐ + ๐)) |
22 | | mulcl 11228 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
23 | 22 | ad2ant2r 745 |
. . . . 5
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (๐ ยท ๐) โ โ) |
24 | 23, 4, 13 | adddid 11274 |
. . . 4
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท ๐) ยท ((1 / ๐) + (1 / ๐))) = (((๐ ยท ๐) ยท (1 / ๐)) + ((๐ ยท ๐) ยท (1 / ๐)))) |
25 | | addcom 11436 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + ๐) = (๐ + ๐)) |
26 | 25 | ad2ant2r 745 |
. . . 4
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (๐ + ๐) = (๐ + ๐)) |
27 | 21, 24, 26 | 3eqtr4d 2777 |
. . 3
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท ๐) ยท ((1 / ๐) + (1 / ๐))) = (๐ + ๐)) |
28 | 22 | mulridd 11267 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) ยท 1) = (๐ ยท ๐)) |
29 | 28 | ad2ant2r 745 |
. . 3
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((๐ ยท ๐) ยท 1) = (๐ ยท ๐)) |
30 | 27, 29 | eqeq12d 2743 |
. 2
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (((๐ ยท ๐) ยท ((1 / ๐) + (1 / ๐))) = ((๐ ยท ๐) ยท 1) โ (๐ + ๐) = (๐ ยท ๐))) |
31 | | addcl 11226 |
. . . 4
โข (((1 /
๐) โ โ โง (1
/ ๐) โ โ) โ
((1 / ๐) + (1 / ๐)) โ
โ) |
32 | 3, 12, 31 | syl2an 594 |
. . 3
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((1 / ๐) + (1 / ๐)) โ โ) |
33 | | mulne0 11892 |
. . 3
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (๐ ยท ๐) โ 0) |
34 | | ax-1cn 11202 |
. . . 4
โข 1 โ
โ |
35 | | mulcan 11887 |
. . . 4
โข ((((1 /
๐) + (1 / ๐)) โ โ โง 1 โ โ
โง ((๐ ยท ๐) โ โ โง (๐ ยท ๐) โ 0)) โ (((๐ ยท ๐) ยท ((1 / ๐) + (1 / ๐))) = ((๐ ยท ๐) ยท 1) โ ((1 / ๐) + (1 / ๐)) = 1)) |
36 | 34, 35 | mp3an2 1445 |
. . 3
โข ((((1 /
๐) + (1 / ๐)) โ โ โง ((๐ ยท ๐) โ โ โง (๐ ยท ๐) โ 0)) โ (((๐ ยท ๐) ยท ((1 / ๐) + (1 / ๐))) = ((๐ ยท ๐) ยท 1) โ ((1 / ๐) + (1 / ๐)) = 1)) |
37 | 32, 23, 33, 36 | syl12anc 835 |
. 2
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (((๐ ยท ๐) ยท ((1 / ๐) + (1 / ๐))) = ((๐ ยท ๐) ยท 1) โ ((1 / ๐) + (1 / ๐)) = 1)) |
38 | | eqcom 2734 |
. . . 4
โข ((๐ + ๐) = (๐ ยท ๐) โ (๐ ยท ๐) = (๐ + ๐)) |
39 | | muleqadd 11894 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) = (๐ + ๐) โ ((๐ โ 1) ยท (๐ โ 1)) = 1)) |
40 | 38, 39 | bitrid 282 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ + ๐) = (๐ ยท ๐) โ ((๐ โ 1) ยท (๐ โ 1)) = 1)) |
41 | 40 | ad2ant2r 745 |
. 2
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((๐ + ๐) = (๐ ยท ๐) โ ((๐ โ 1) ยท (๐ โ 1)) = 1)) |
42 | 30, 37, 41 | 3bitr3d 308 |
1
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (((1 / ๐) + (1 / ๐)) = 1 โ ((๐ โ 1) ยท (๐ โ 1)) = 1)) |