Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . . . . . 7
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ ๐ โ โ) |
2 | | simprl 529 |
. . . . . . 7
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ ๐ โ โ) |
3 | | recclap 8649 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ # 0) โ (1 / ๐) โ
โ) |
4 | 3 | adantr 276 |
. . . . . . 7
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ (1 / ๐) โ โ) |
5 | 1, 2, 4 | mul32d 8123 |
. . . . . 6
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ ((๐ ยท ๐) ยท (1 / ๐)) = ((๐ ยท (1 / ๐)) ยท ๐)) |
6 | | recidap 8656 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ # 0) โ (๐ ยท (1 / ๐)) = 1) |
7 | 6 | oveq1d 5903 |
. . . . . . 7
โข ((๐ โ โ โง ๐ # 0) โ ((๐ ยท (1 / ๐)) ยท ๐) = (1 ยท ๐)) |
8 | 7 | adantr 276 |
. . . . . 6
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ ((๐ ยท (1 / ๐)) ยท ๐) = (1 ยท ๐)) |
9 | | mullid 7968 |
. . . . . . 7
โข (๐ โ โ โ (1
ยท ๐) = ๐) |
10 | 9 | ad2antrl 490 |
. . . . . 6
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ (1 ยท ๐) = ๐) |
11 | 5, 8, 10 | 3eqtrd 2224 |
. . . . 5
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ ((๐ ยท ๐) ยท (1 / ๐)) = ๐) |
12 | | recclap 8649 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ # 0) โ (1 / ๐) โ
โ) |
13 | 12 | adantl 277 |
. . . . . . 7
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ (1 / ๐) โ โ) |
14 | 1, 2, 13 | mulassd 7994 |
. . . . . 6
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ ((๐ ยท ๐) ยท (1 / ๐)) = (๐ ยท (๐ ยท (1 / ๐)))) |
15 | | recidap 8656 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ # 0) โ (๐ ยท (1 / ๐)) = 1) |
16 | 15 | oveq2d 5904 |
. . . . . . 7
โข ((๐ โ โ โง ๐ # 0) โ (๐ ยท (๐ ยท (1 / ๐))) = (๐ ยท 1)) |
17 | 16 | adantl 277 |
. . . . . 6
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ (๐ ยท (๐ ยท (1 / ๐))) = (๐ ยท 1)) |
18 | | mulrid 7967 |
. . . . . . 7
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
19 | 18 | ad2antrr 488 |
. . . . . 6
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ (๐ ยท 1) = ๐) |
20 | 14, 17, 19 | 3eqtrd 2224 |
. . . . 5
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ ((๐ ยท ๐) ยท (1 / ๐)) = ๐) |
21 | 11, 20 | oveq12d 5906 |
. . . 4
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ (((๐ ยท ๐) ยท (1 / ๐)) + ((๐ ยท ๐) ยท (1 / ๐))) = (๐ + ๐)) |
22 | | mulcl 7951 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
23 | 22 | ad2ant2r 509 |
. . . . 5
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ (๐ ยท ๐) โ โ) |
24 | 23, 4, 13 | adddid 7995 |
. . . 4
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ ((๐ ยท ๐) ยท ((1 / ๐) + (1 / ๐))) = (((๐ ยท ๐) ยท (1 / ๐)) + ((๐ ยท ๐) ยท (1 / ๐)))) |
25 | | addcom 8107 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + ๐) = (๐ + ๐)) |
26 | 25 | ad2ant2r 509 |
. . . 4
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ (๐ + ๐) = (๐ + ๐)) |
27 | 21, 24, 26 | 3eqtr4d 2230 |
. . 3
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ ((๐ ยท ๐) ยท ((1 / ๐) + (1 / ๐))) = (๐ + ๐)) |
28 | 22 | mulridd 7987 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) ยท 1) = (๐ ยท ๐)) |
29 | 28 | ad2ant2r 509 |
. . 3
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ ((๐ ยท ๐) ยท 1) = (๐ ยท ๐)) |
30 | 27, 29 | eqeq12d 2202 |
. 2
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ (((๐ ยท ๐) ยท ((1 / ๐) + (1 / ๐))) = ((๐ ยท ๐) ยท 1) โ (๐ + ๐) = (๐ ยท ๐))) |
31 | | addcl 7949 |
. . . 4
โข (((1 /
๐) โ โ โง (1
/ ๐) โ โ) โ
((1 / ๐) + (1 / ๐)) โ
โ) |
32 | 3, 12, 31 | syl2an 289 |
. . 3
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ ((1 / ๐) + (1 / ๐)) โ โ) |
33 | | mulap0 8624 |
. . 3
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ (๐ ยท ๐) # 0) |
34 | | ax-1cn 7917 |
. . . 4
โข 1 โ
โ |
35 | | mulcanap 8635 |
. . . 4
โข ((((1 /
๐) + (1 / ๐)) โ โ โง 1 โ โ
โง ((๐ ยท ๐) โ โ โง (๐ ยท ๐) # 0)) โ (((๐ ยท ๐) ยท ((1 / ๐) + (1 / ๐))) = ((๐ ยท ๐) ยท 1) โ ((1 / ๐) + (1 / ๐)) = 1)) |
36 | 34, 35 | mp3an2 1335 |
. . 3
โข ((((1 /
๐) + (1 / ๐)) โ โ โง ((๐ ยท ๐) โ โ โง (๐ ยท ๐) # 0)) โ (((๐ ยท ๐) ยท ((1 / ๐) + (1 / ๐))) = ((๐ ยท ๐) ยท 1) โ ((1 / ๐) + (1 / ๐)) = 1)) |
37 | 32, 23, 33, 36 | syl12anc 1246 |
. 2
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ (((๐ ยท ๐) ยท ((1 / ๐) + (1 / ๐))) = ((๐ ยท ๐) ยท 1) โ ((1 / ๐) + (1 / ๐)) = 1)) |
38 | | eqcom 2189 |
. . . 4
โข ((๐ + ๐) = (๐ ยท ๐) โ (๐ ยท ๐) = (๐ + ๐)) |
39 | | muleqadd 8638 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) = (๐ + ๐) โ ((๐ โ 1) ยท (๐ โ 1)) = 1)) |
40 | 38, 39 | bitrid 192 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ + ๐) = (๐ ยท ๐) โ ((๐ โ 1) ยท (๐ โ 1)) = 1)) |
41 | 40 | ad2ant2r 509 |
. 2
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ ((๐ + ๐) = (๐ ยท ๐) โ ((๐ โ 1) ยท (๐ โ 1)) = 1)) |
42 | 30, 37, 41 | 3bitr3d 218 |
1
โข (((๐ โ โ โง ๐ # 0) โง (๐ โ โ โง ๐ # 0)) โ (((1 / ๐) + (1 / ๐)) = 1 โ ((๐ โ 1) ยท (๐ โ 1)) = 1)) |