Step | Hyp | Ref
| Expression |
1 | | fveq1 6845 |
. . . . 5
โข (๐ = ๐ โ (๐โ2) = (๐โ2)) |
2 | 1 | necon3i 2973 |
. . . 4
โข ((๐โ2) โ (๐โ2) โ ๐ โ ๐) |
3 | 2 | adantl 483 |
. . 3
โข (((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2)) โ ๐ โ ๐) |
4 | | rrx2line.i |
. . . 4
โข ๐ผ = {1, 2} |
5 | | rrx2line.e |
. . . 4
โข ๐ธ = (โ^โ๐ผ) |
6 | | rrx2line.b |
. . . 4
โข ๐ = (โ โm
๐ผ) |
7 | | rrx2line.l |
. . . 4
โข ๐ฟ = (LineMโ๐ธ) |
8 | 4, 5, 6, 7 | rrx2line 46916 |
. . 3
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐๐ฟ๐) = {๐ โ ๐ โฃ โ๐ก โ โ ((๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2))))}) |
9 | 3, 8 | syl3an3 1166 |
. 2
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ (๐๐ฟ๐) = {๐ โ ๐ โฃ โ๐ก โ โ ((๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2))))}) |
10 | | oveq2 7369 |
. . . . . . . . . . . . . 14
โข ((๐โ1) = (๐โ1) โ (๐ก ยท (๐โ1)) = (๐ก ยท (๐โ1))) |
11 | 10 | oveq2d 7377 |
. . . . . . . . . . . . 13
โข ((๐โ1) = (๐โ1) โ (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1)))) |
12 | 11 | eqcoms 2741 |
. . . . . . . . . . . 12
โข ((๐โ1) = (๐โ1) โ (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1)))) |
13 | 12 | adantr 482 |
. . . . . . . . . . 11
โข (((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2)) โ (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1)))) |
14 | 13 | 3ad2ant3 1136 |
. . . . . . . . . 10
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1)))) |
15 | 14 | adantr 482 |
. . . . . . . . 9
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1)))) |
16 | 15 | adantr 482 |
. . . . . . . 8
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง ๐ก โ โ) โ (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1)))) |
17 | 4, 6 | rrx2pxel 46887 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ (๐โ1) โ โ) |
18 | 17 | recnd 11191 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (๐โ1) โ โ) |
19 | 18 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ (๐โ1) โ โ) |
20 | 19 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (๐โ1) โ โ) |
21 | 20 | adantr 482 |
. . . . . . . . 9
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง ๐ก โ โ) โ (๐โ1) โ โ) |
22 | | recn 11149 |
. . . . . . . . . 10
โข (๐ก โ โ โ ๐ก โ
โ) |
23 | 22 | adantl 483 |
. . . . . . . . 9
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง ๐ก โ โ) โ ๐ก โ โ) |
24 | 21, 23 | affineid 46880 |
. . . . . . . 8
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง ๐ก โ โ) โ (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) = (๐โ1)) |
25 | 16, 24 | eqtrd 2773 |
. . . . . . 7
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง ๐ก โ โ) โ (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) = (๐โ1)) |
26 | 25 | eqeq2d 2744 |
. . . . . 6
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง ๐ก โ โ) โ ((๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) โ (๐โ1) = (๐โ1))) |
27 | 26 | anbi1d 631 |
. . . . 5
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง ๐ก โ โ) โ (((๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))) โ ((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))))) |
28 | 27 | rexbidva 3170 |
. . . 4
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (โ๐ก โ โ ((๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))) โ โ๐ก โ โ ((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))))) |
29 | | simpl 484 |
. . . . . . 7
โข (((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))) โ (๐โ1) = (๐โ1)) |
30 | 29 | a1i 11 |
. . . . . 6
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง ๐ก โ โ) โ (((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))) โ (๐โ1) = (๐โ1))) |
31 | 30 | rexlimdva 3149 |
. . . . 5
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (โ๐ก โ โ ((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))) โ (๐โ1) = (๐โ1))) |
32 | 4, 6 | rrx2pyel 46888 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (๐โ2) โ โ) |
33 | 32 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (๐โ2) โ โ) |
34 | 4, 6 | rrx2pyel 46888 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (๐โ2) โ โ) |
35 | 34 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ (๐โ2) โ โ) |
36 | 35 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (๐โ2) โ โ) |
37 | 33, 36 | resubcld 11591 |
. . . . . . . . 9
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ ((๐โ2) โ (๐โ2)) โ โ) |
38 | 4, 6 | rrx2pyel 46888 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (๐โ2) โ โ) |
39 | 38 | 3ad2ant2 1135 |
. . . . . . . . . . 11
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ (๐โ2) โ โ) |
40 | 39, 35 | resubcld 11591 |
. . . . . . . . . 10
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ ((๐โ2) โ (๐โ2)) โ โ) |
41 | 40 | adantr 482 |
. . . . . . . . 9
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ ((๐โ2) โ (๐โ2)) โ โ) |
42 | 38 | recnd 11191 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (๐โ2) โ โ) |
43 | 42 | 3ad2ant2 1135 |
. . . . . . . . . . 11
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ (๐โ2) โ โ) |
44 | 34 | recnd 11191 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (๐โ2) โ โ) |
45 | 44 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ (๐โ2) โ โ) |
46 | | simpr 486 |
. . . . . . . . . . . . 13
โข (((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2)) โ (๐โ2) โ (๐โ2)) |
47 | 46 | necomd 2996 |
. . . . . . . . . . . 12
โข (((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2)) โ (๐โ2) โ (๐โ2)) |
48 | 47 | 3ad2ant3 1136 |
. . . . . . . . . . 11
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ (๐โ2) โ (๐โ2)) |
49 | 43, 45, 48 | subne0d 11529 |
. . . . . . . . . 10
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ ((๐โ2) โ (๐โ2)) โ 0) |
50 | 49 | adantr 482 |
. . . . . . . . 9
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ ((๐โ2) โ (๐โ2)) โ 0) |
51 | 37, 41, 50 | redivcld 11991 |
. . . . . . . 8
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) โ โ) |
52 | 51 | adantr 482 |
. . . . . . 7
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง (๐โ1) = (๐โ1)) โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) โ โ) |
53 | | oveq2 7369 |
. . . . . . . . . . . 12
โข (๐ก = (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) โ (1 โ ๐ก) = (1 โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))))) |
54 | 53 | oveq1d 7376 |
. . . . . . . . . . 11
โข (๐ก = (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) โ ((1 โ ๐ก) ยท (๐โ2)) = ((1 โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2)))) ยท (๐โ2))) |
55 | | oveq1 7368 |
. . . . . . . . . . 11
โข (๐ก = (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) โ (๐ก ยท (๐โ2)) = ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท (๐โ2))) |
56 | 54, 55 | oveq12d 7379 |
. . . . . . . . . 10
โข (๐ก = (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) โ (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2))) = (((1 โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2)))) ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท (๐โ2)))) |
57 | 56 | eqeq2d 2744 |
. . . . . . . . 9
โข (๐ก = (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) โ ((๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2))) โ (๐โ2) = (((1 โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2)))) ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท (๐โ2))))) |
58 | 57 | anbi2d 630 |
. . . . . . . 8
โข (๐ก = (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) โ (((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))) โ ((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2)))) ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท (๐โ2)))))) |
59 | 58 | adantl 483 |
. . . . . . 7
โข
(((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง (๐โ1) = (๐โ1)) โง ๐ก = (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2)))) โ (((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))) โ ((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2)))) ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท (๐โ2)))))) |
60 | | simpr 486 |
. . . . . . . 8
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง (๐โ1) = (๐โ1)) โ (๐โ1) = (๐โ1)) |
61 | 44 | mullidd 11181 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ (1 ยท (๐โ2)) = (๐โ2)) |
62 | 61 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ (1 ยท (๐โ2)) = (๐โ2)) |
63 | 62 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (1 ยท (๐โ2)) = (๐โ2)) |
64 | 37 | recnd 11191 |
. . . . . . . . . . . . 13
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ ((๐โ2) โ (๐โ2)) โ โ) |
65 | 42 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ ๐ โง ๐ โ ๐) โ (๐โ2) โ โ) |
66 | 44 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ ๐ โง ๐ โ ๐) โ (๐โ2) โ โ) |
67 | 65, 66 | subcld 11520 |
. . . . . . . . . . . . . . 15
โข ((๐ โ ๐ โง ๐ โ ๐) โ ((๐โ2) โ (๐โ2)) โ โ) |
68 | 67 | 3adant3 1133 |
. . . . . . . . . . . . . 14
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ ((๐โ2) โ (๐โ2)) โ โ) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ ((๐โ2) โ (๐โ2)) โ โ) |
70 | 64, 69, 50 | divcan1d 11940 |
. . . . . . . . . . . 12
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท ((๐โ2) โ (๐โ2))) = ((๐โ2) โ (๐โ2))) |
71 | 63, 70 | oveq12d 7379 |
. . . . . . . . . . 11
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ ((1 ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท ((๐โ2) โ (๐โ2)))) = ((๐โ2) + ((๐โ2) โ (๐โ2)))) |
72 | 45 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (๐โ2) โ โ) |
73 | 32 | recnd 11191 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ (๐โ2) โ โ) |
74 | 73 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (๐โ2) โ โ) |
75 | 72, 74 | pncan3d 11523 |
. . . . . . . . . . 11
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ ((๐โ2) + ((๐โ2) โ (๐โ2))) = (๐โ2)) |
76 | 71, 75 | eqtr2d 2774 |
. . . . . . . . . 10
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (๐โ2) = ((1 ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท ((๐โ2) โ (๐โ2))))) |
77 | 76 | adantr 482 |
. . . . . . . . 9
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง (๐โ1) = (๐โ1)) โ (๐โ2) = ((1 ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท ((๐โ2) โ (๐โ2))))) |
78 | | 1cnd 11158 |
. . . . . . . . . . 11
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ 1 โ โ) |
79 | 51 | recnd 11191 |
. . . . . . . . . . 11
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) โ โ) |
80 | 43 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (๐โ2) โ โ) |
81 | 78, 79, 72, 80 | submuladdmuld 46877 |
. . . . . . . . . 10
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (((1 โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2)))) ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท (๐โ2))) = ((1 ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท ((๐โ2) โ (๐โ2))))) |
82 | 81 | adantr 482 |
. . . . . . . . 9
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง (๐โ1) = (๐โ1)) โ (((1 โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2)))) ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท (๐โ2))) = ((1 ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท ((๐โ2) โ (๐โ2))))) |
83 | 77, 82 | eqtr4d 2776 |
. . . . . . . 8
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง (๐โ1) = (๐โ1)) โ (๐โ2) = (((1 โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2)))) ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท (๐โ2)))) |
84 | 60, 83 | jca 513 |
. . . . . . 7
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง (๐โ1) = (๐โ1)) โ ((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ (((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2)))) ยท (๐โ2)) + ((((๐โ2) โ (๐โ2)) / ((๐โ2) โ (๐โ2))) ยท (๐โ2))))) |
85 | 52, 59, 84 | rspcedvd 3585 |
. . . . . 6
โข ((((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โง (๐โ1) = (๐โ1)) โ โ๐ก โ โ ((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2))))) |
86 | 85 | ex 414 |
. . . . 5
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ ((๐โ1) = (๐โ1) โ โ๐ก โ โ ((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))))) |
87 | 31, 86 | impbid 211 |
. . . 4
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (โ๐ก โ โ ((๐โ1) = (๐โ1) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))) โ (๐โ1) = (๐โ1))) |
88 | 28, 87 | bitrd 279 |
. . 3
โข (((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โง ๐ โ ๐) โ (โ๐ก โ โ ((๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2)))) โ (๐โ1) = (๐โ1))) |
89 | 88 | rabbidva 3413 |
. 2
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ {๐ โ ๐ โฃ โ๐ก โ โ ((๐โ1) = (((1 โ ๐ก) ยท (๐โ1)) + (๐ก ยท (๐โ1))) โง (๐โ2) = (((1 โ ๐ก) ยท (๐โ2)) + (๐ก ยท (๐โ2))))} = {๐ โ ๐ โฃ (๐โ1) = (๐โ1)}) |
90 | 9, 89 | eqtrd 2773 |
1
โข ((๐ โ ๐ โง ๐ โ ๐ โง ((๐โ1) = (๐โ1) โง (๐โ2) โ (๐โ2))) โ (๐๐ฟ๐) = {๐ โ ๐ โฃ (๐โ1) = (๐โ1)}) |