Step | Hyp | Ref
| Expression |
1 | | elznn0nn 9280 |
. . 3
โข (๐ โ โค โ (๐ โ โ0 โจ
(๐ โ โ โง
-๐ โ
โ))) |
2 | | elznn0nn 9280 |
. . . 4
โข (๐ โ โค โ (๐ โ โ0 โจ
(๐ โ โ โง
-๐ โ
โ))) |
3 | | expadd 10575 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) |
4 | 3 | 3expia 1206 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ โ
โ0 โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
5 | 4 | adantlr 477 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด # 0) โง ๐ โ โ0) โ (๐ โ โ0
โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
6 | | expaddzaplem 10576 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) |
7 | 6 | 3expia 1206 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ)) โ (๐ โ โ0 โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
8 | 5, 7 | jaodan 798 |
. . . . 5
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ0 โจ (๐ โ โ โง -๐ โ โ))) โ (๐ โ โ0
โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
9 | | expaddzaplem 10576 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) |
10 | | simp3 1000 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ ๐ โ
โ0) |
11 | 10 | nn0cnd 9244 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ ๐ โ
โ) |
12 | | simp2l 1024 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ ๐ โ
โ) |
13 | 12 | recnd 7999 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ ๐ โ
โ) |
14 | 11, 13 | addcomd 8121 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ (๐ + ๐) = (๐ + ๐)) |
15 | 14 | oveq2d 5904 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ (๐ดโ(๐ + ๐)) = (๐ดโ(๐ + ๐))) |
16 | | simp1l 1022 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ ๐ด โ
โ) |
17 | | expcl 10551 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
18 | 16, 10, 17 | syl2anc 411 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ (๐ดโ๐) โ โ) |
19 | | simp1r 1023 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ ๐ด # 0) |
20 | 13 | negnegd 8272 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ --๐ = ๐) |
21 | | simp2r 1025 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ -๐ โ
โ) |
22 | 21 | nnnn0d 9242 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ -๐ โ
โ0) |
23 | | nn0negz 9300 |
. . . . . . . . . . . . 13
โข (-๐ โ โ0
โ --๐ โ
โค) |
24 | 22, 23 | syl 14 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ --๐ โ
โค) |
25 | 20, 24 | eqeltrrd 2265 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ ๐ โ
โค) |
26 | | expclzap 10558 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ โ โค) โ (๐ดโ๐) โ โ) |
27 | 16, 19, 25, 26 | syl3anc 1248 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ (๐ดโ๐) โ โ) |
28 | 18, 27 | mulcomd 7992 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ ((๐ดโ๐) ยท (๐ดโ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) |
29 | 9, 15, 28 | 3eqtr4d 2230 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง ๐ โ โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) |
30 | 29 | 3expia 1206 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ)) โ (๐ โ โ0 โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
31 | 30 | impancom 260 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด # 0) โง ๐ โ โ0) โ ((๐ โ โ โง -๐ โ โ) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
32 | | simp2l 1024 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ ๐ โ โ) |
33 | 32 | recnd 7999 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ ๐ โ โ) |
34 | | simp3l 1026 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ ๐ โ โ) |
35 | 34 | recnd 7999 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ ๐ โ โ) |
36 | 33, 35 | negdid 8294 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ -(๐ + ๐) = (-๐ + -๐)) |
37 | 36 | oveq2d 5904 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ-(๐ + ๐)) = (๐ดโ(-๐ + -๐))) |
38 | | simp1l 1022 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ ๐ด โ โ) |
39 | | simp2r 1025 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ -๐ โ โ) |
40 | 39 | nnnn0d 9242 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ -๐ โ
โ0) |
41 | | simp3r 1027 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ -๐ โ โ) |
42 | 41 | nnnn0d 9242 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ -๐ โ
โ0) |
43 | | expadd 10575 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง -๐ โ โ0
โง -๐ โ
โ0) โ (๐ดโ(-๐ + -๐)) = ((๐ดโ-๐) ยท (๐ดโ-๐))) |
44 | 38, 40, 42, 43 | syl3anc 1248 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ(-๐ + -๐)) = ((๐ดโ-๐) ยท (๐ดโ-๐))) |
45 | 37, 44 | eqtrd 2220 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ-(๐ + ๐)) = ((๐ดโ-๐) ยท (๐ดโ-๐))) |
46 | 45 | oveq2d 5904 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (1 / (๐ดโ-(๐ + ๐))) = (1 / ((๐ดโ-๐) ยท (๐ดโ-๐)))) |
47 | | 1t1e1 9084 |
. . . . . . . . . . 11
โข (1
ยท 1) = 1 |
48 | 47 | oveq1i 5898 |
. . . . . . . . . 10
โข ((1
ยท 1) / ((๐ดโ-๐) ยท (๐ดโ-๐))) = (1 / ((๐ดโ-๐) ยท (๐ดโ-๐))) |
49 | 46, 48 | eqtr4di 2238 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (1 / (๐ดโ-(๐ + ๐))) = ((1 ยท 1) / ((๐ดโ-๐) ยท (๐ดโ-๐)))) |
50 | | expcl 10551 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง -๐ โ โ0)
โ (๐ดโ-๐) โ
โ) |
51 | 38, 40, 50 | syl2anc 411 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ-๐) โ โ) |
52 | | simp1r 1023 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ ๐ด # 0) |
53 | 40 | nn0zd 9386 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ -๐ โ โค) |
54 | | expap0i 10565 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด # 0 โง -๐ โ โค) โ (๐ดโ-๐) # 0) |
55 | 38, 52, 53, 54 | syl3anc 1248 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ-๐) # 0) |
56 | | expcl 10551 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง -๐ โ โ0)
โ (๐ดโ-๐) โ
โ) |
57 | 38, 42, 56 | syl2anc 411 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ-๐) โ โ) |
58 | 42 | nn0zd 9386 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ -๐ โ โค) |
59 | | expap0i 10565 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด # 0 โง -๐ โ โค) โ (๐ดโ-๐) # 0) |
60 | 38, 52, 58, 59 | syl3anc 1248 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ-๐) # 0) |
61 | | ax-1cn 7917 |
. . . . . . . . . . 11
โข 1 โ
โ |
62 | | divmuldivap 8682 |
. . . . . . . . . . 11
โข (((1
โ โ โง 1 โ โ) โง (((๐ดโ-๐) โ โ โง (๐ดโ-๐) # 0) โง ((๐ดโ-๐) โ โ โง (๐ดโ-๐) # 0))) โ ((1 / (๐ดโ-๐)) ยท (1 / (๐ดโ-๐))) = ((1 ยท 1) / ((๐ดโ-๐) ยท (๐ดโ-๐)))) |
63 | 61, 61, 62 | mpanl12 436 |
. . . . . . . . . 10
โข ((((๐ดโ-๐) โ โ โง (๐ดโ-๐) # 0) โง ((๐ดโ-๐) โ โ โง (๐ดโ-๐) # 0)) โ ((1 / (๐ดโ-๐)) ยท (1 / (๐ดโ-๐))) = ((1 ยท 1) / ((๐ดโ-๐) ยท (๐ดโ-๐)))) |
64 | 51, 55, 57, 60, 63 | syl22anc 1249 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ ((1 / (๐ดโ-๐)) ยท (1 / (๐ดโ-๐))) = ((1 ยท 1) / ((๐ดโ-๐) ยท (๐ดโ-๐)))) |
65 | 49, 64 | eqtr4d 2223 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (1 / (๐ดโ-(๐ + ๐))) = ((1 / (๐ดโ-๐)) ยท (1 / (๐ดโ-๐)))) |
66 | 33, 35 | addcld 7990 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (๐ + ๐) โ โ) |
67 | 40, 42 | nn0addcld 9246 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (-๐ + -๐) โ
โ0) |
68 | 36, 67 | eqeltrd 2264 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ -(๐ + ๐) โ
โ0) |
69 | | expineg2 10542 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0) โง ((๐ + ๐) โ โ โง -(๐ + ๐) โ โ0)) โ (๐ดโ(๐ + ๐)) = (1 / (๐ดโ-(๐ + ๐)))) |
70 | 38, 52, 66, 68, 69 | syl22anc 1249 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ(๐ + ๐)) = (1 / (๐ดโ-(๐ + ๐)))) |
71 | | expineg2 10542 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ0)) โ (๐ดโ๐) = (1 / (๐ดโ-๐))) |
72 | 38, 52, 33, 40, 71 | syl22anc 1249 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ๐) = (1 / (๐ดโ-๐))) |
73 | | expineg2 10542 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ0)) โ (๐ดโ๐) = (1 / (๐ดโ-๐))) |
74 | 38, 52, 35, 42, 73 | syl22anc 1249 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ๐) = (1 / (๐ดโ-๐))) |
75 | 72, 74 | oveq12d 5906 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ ((๐ดโ๐) ยท (๐ดโ๐)) = ((1 / (๐ดโ-๐)) ยท (1 / (๐ดโ-๐)))) |
76 | 65, 70, 75 | 3eqtr4d 2230 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) |
77 | 76 | 3expia 1206 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โง -๐ โ โ)) โ ((๐ โ โ โง -๐ โ โ) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
78 | 31, 77 | jaodan 798 |
. . . . 5
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ0 โจ (๐ โ โ โง -๐ โ โ))) โ
((๐ โ โ โง
-๐ โ โ) โ
(๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
79 | 8, 78 | jaod 718 |
. . . 4
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ0 โจ (๐ โ โ โง -๐ โ โ))) โ
((๐ โ
โ0 โจ (๐
โ โ โง -๐
โ โ)) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
80 | 2, 79 | sylan2b 287 |
. . 3
โข (((๐ด โ โ โง ๐ด # 0) โง ๐ โ โค) โ ((๐ โ โ0 โจ (๐ โ โ โง -๐ โ โ)) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
81 | 1, 80 | biimtrid 152 |
. 2
โข (((๐ด โ โ โง ๐ด # 0) โง ๐ โ โค) โ (๐ โ โค โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
82 | 81 | impr 379 |
1
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โค โง ๐ โ โค)) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) |