Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . . . . 6
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โง ๐ฅ < 0) โ ๐ฅ โ โ) |
2 | | simpr 110 |
. . . . . . 7
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โง ๐ฅ < 0) โ ๐ฅ < 0) |
3 | 1, 2 | lt0ap0d 8609 |
. . . . . 6
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โง ๐ฅ < 0) โ ๐ฅ # 0) |
4 | | rerecclap 8690 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฅ # 0) โ (1 / ๐ฅ) โ
โ) |
5 | | recn 7947 |
. . . . . . . 8
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
6 | | recidap 8646 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฅ # 0) โ (๐ฅ ยท (1 / ๐ฅ)) = 1) |
7 | 5, 6 | sylan 283 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฅ # 0) โ (๐ฅ ยท (1 / ๐ฅ)) = 1) |
8 | | oveq2 5886 |
. . . . . . . . 9
โข (๐ง = (1 / ๐ฅ) โ (๐ฅ ยท ๐ง) = (๐ฅ ยท (1 / ๐ฅ))) |
9 | 8 | eqeq1d 2186 |
. . . . . . . 8
โข (๐ง = (1 / ๐ฅ) โ ((๐ฅ ยท ๐ง) = 1 โ (๐ฅ ยท (1 / ๐ฅ)) = 1)) |
10 | 9 | rspcev 2843 |
. . . . . . 7
โข (((1 /
๐ฅ) โ โ โง
(๐ฅ ยท (1 / ๐ฅ)) = 1) โ โ๐ง โ โ (๐ฅ ยท ๐ง) = 1) |
11 | 4, 7, 10 | syl2anc 411 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฅ # 0) โ โ๐ง โ โ (๐ฅ ยท ๐ง) = 1) |
12 | 1, 3, 11 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โง ๐ฅ < 0) โ โ๐ง โ โ (๐ฅ ยท ๐ง) = 1) |
13 | 12 | orcd 733 |
. . . 4
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โง ๐ฅ < 0) โ (โ๐ง โ โ (๐ฅ ยท ๐ง) = 1 โจ ๐ฅ = 0)) |
14 | | simpr 110 |
. . . . 5
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โง ๐ฅ = 0) โ ๐ฅ = 0) |
15 | 14 | olcd 734 |
. . . 4
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โง ๐ฅ = 0) โ (โ๐ง โ โ (๐ฅ ยท ๐ง) = 1 โจ ๐ฅ = 0)) |
16 | | simpll 527 |
. . . . . 6
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โง 0 < ๐ฅ) โ ๐ฅ โ โ) |
17 | | simpr 110 |
. . . . . . 7
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โง 0 < ๐ฅ) โ 0 < ๐ฅ) |
18 | 16, 17 | gt0ap0d 8589 |
. . . . . 6
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โง 0 < ๐ฅ) โ ๐ฅ # 0) |
19 | 16, 18, 11 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โง 0 < ๐ฅ) โ โ๐ง โ โ (๐ฅ ยท ๐ง) = 1) |
20 | 19 | orcd 733 |
. . . 4
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โง 0 < ๐ฅ) โ (โ๐ง โ โ (๐ฅ ยท ๐ง) = 1 โจ ๐ฅ = 0)) |
21 | | 0re 7960 |
. . . . . 6
โข 0 โ
โ |
22 | | breq2 4009 |
. . . . . . . 8
โข (๐ฆ = 0 โ (๐ฅ < ๐ฆ โ ๐ฅ < 0)) |
23 | | eqeq2 2187 |
. . . . . . . 8
โข (๐ฆ = 0 โ (๐ฅ = ๐ฆ โ ๐ฅ = 0)) |
24 | | breq1 4008 |
. . . . . . . 8
โข (๐ฆ = 0 โ (๐ฆ < ๐ฅ โ 0 < ๐ฅ)) |
25 | 22, 23, 24 | 3orbi123d 1311 |
. . . . . . 7
โข (๐ฆ = 0 โ ((๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ) โ (๐ฅ < 0 โจ ๐ฅ = 0 โจ 0 < ๐ฅ))) |
26 | 25 | rspcv 2839 |
. . . . . 6
โข (0 โ
โ โ (โ๐ฆ
โ โ (๐ฅ <
๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ) โ (๐ฅ < 0 โจ ๐ฅ = 0 โจ 0 < ๐ฅ))) |
27 | 21, 26 | ax-mp 5 |
. . . . 5
โข
(โ๐ฆ โ
โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ) โ (๐ฅ < 0 โจ ๐ฅ = 0 โจ 0 < ๐ฅ)) |
28 | 27 | adantl 277 |
. . . 4
โข ((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โ (๐ฅ < 0 โจ ๐ฅ = 0 โจ 0 < ๐ฅ)) |
29 | 13, 15, 20, 28 | mpjao3dan 1307 |
. . 3
โข ((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) โ (โ๐ง โ โ (๐ฅ ยท ๐ง) = 1 โจ ๐ฅ = 0)) |
30 | 29 | ralimiaa 2539 |
. 2
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ) โ โ๐ฅ โ โ (โ๐ง โ โ (๐ฅ ยท ๐ง) = 1 โจ ๐ฅ = 0)) |
31 | | oveq1 5885 |
. . . . . . 7
โข (๐ฅ = ๐ค โ (๐ฅ ยท ๐ง) = (๐ค ยท ๐ง)) |
32 | 31 | eqeq1d 2186 |
. . . . . 6
โข (๐ฅ = ๐ค โ ((๐ฅ ยท ๐ง) = 1 โ (๐ค ยท ๐ง) = 1)) |
33 | 32 | rexbidv 2478 |
. . . . 5
โข (๐ฅ = ๐ค โ (โ๐ง โ โ (๐ฅ ยท ๐ง) = 1 โ โ๐ง โ โ (๐ค ยท ๐ง) = 1)) |
34 | | eqeq1 2184 |
. . . . 5
โข (๐ฅ = ๐ค โ (๐ฅ = 0 โ ๐ค = 0)) |
35 | 33, 34 | orbi12d 793 |
. . . 4
โข (๐ฅ = ๐ค โ ((โ๐ง โ โ (๐ฅ ยท ๐ง) = 1 โจ ๐ฅ = 0) โ (โ๐ง โ โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0))) |
36 | 35 | cbvralv 2705 |
. . 3
โข
(โ๐ฅ โ
โ (โ๐ง โ
โ (๐ฅ ยท ๐ง) = 1 โจ ๐ฅ = 0) โ โ๐ค โ โ (โ๐ง โ โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0)) |
37 | | nfcv 2319 |
. . . . . . . . 9
โข
โฒ๐งโ |
38 | | nfre1 2520 |
. . . . . . . . . 10
โข
โฒ๐งโ๐ง โ โ (๐ค ยท ๐ง) = 1 |
39 | | nfv 1528 |
. . . . . . . . . 10
โข
โฒ๐ง ๐ค = 0 |
40 | 38, 39 | nfor 1574 |
. . . . . . . . 9
โข
โฒ๐ง(โ๐ง โ โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) |
41 | 37, 40 | nfralya 2517 |
. . . . . . . 8
โข
โฒ๐งโ๐ค โ โ (โ๐ง โ โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) |
42 | | nfv 1528 |
. . . . . . . 8
โข
โฒ๐ง(๐ฅ โ โ โง ๐ฆ โ
โ) |
43 | 41, 42 | nfan 1565 |
. . . . . . 7
โข
โฒ๐ง(โ๐ค โ โ (โ๐ง โ โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) |
44 | | nfv 1528 |
. . . . . . 7
โข
โฒ๐ง(๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ) |
45 | | simpr 110 |
. . . . . . . . . . 11
โข
(((((โ๐ค
โ โ (โ๐ง
โ โ (๐ค ยท
๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โง (๐ฆ โ ๐ฅ) < 0) โ (๐ฆ โ ๐ฅ) < 0) |
46 | | simprr 531 |
. . . . . . . . . . . . . 14
โข
((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ฆ โ โ) |
47 | 46 | ad2antrr 488 |
. . . . . . . . . . . . 13
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ ๐ฆ โ โ) |
48 | 47 | adantr 276 |
. . . . . . . . . . . 12
โข
(((((โ๐ค
โ โ (โ๐ง
โ โ (๐ค ยท
๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โง (๐ฆ โ ๐ฅ) < 0) โ ๐ฆ โ โ) |
49 | | simprl 529 |
. . . . . . . . . . . . . 14
โข
((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ฅ โ โ) |
50 | 49 | ad2antrr 488 |
. . . . . . . . . . . . 13
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ ๐ฅ โ โ) |
51 | 50 | adantr 276 |
. . . . . . . . . . . 12
โข
(((((โ๐ค
โ โ (โ๐ง
โ โ (๐ค ยท
๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โง (๐ฆ โ ๐ฅ) < 0) โ ๐ฅ โ โ) |
52 | 48, 51 | sublt0d 8530 |
. . . . . . . . . . 11
โข
(((((โ๐ค
โ โ (โ๐ง
โ โ (๐ค ยท
๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โง (๐ฆ โ ๐ฅ) < 0) โ ((๐ฆ โ ๐ฅ) < 0 โ ๐ฆ < ๐ฅ)) |
53 | 45, 52 | mpbid 147 |
. . . . . . . . . 10
โข
(((((โ๐ค
โ โ (โ๐ง
โ โ (๐ค ยท
๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โง (๐ฆ โ ๐ฅ) < 0) โ ๐ฆ < ๐ฅ) |
54 | 53 | 3mix3d 1174 |
. . . . . . . . 9
โข
(((((โ๐ค
โ โ (โ๐ง
โ โ (๐ค ยท
๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โง (๐ฆ โ ๐ฅ) < 0) โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) |
55 | | simpr 110 |
. . . . . . . . . . 11
โข
(((((โ๐ค
โ โ (โ๐ง
โ โ (๐ค ยท
๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โง 0 < (๐ฆ โ ๐ฅ)) โ 0 < (๐ฆ โ ๐ฅ)) |
56 | 50 | adantr 276 |
. . . . . . . . . . . 12
โข
(((((โ๐ค
โ โ (โ๐ง
โ โ (๐ค ยท
๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โง 0 < (๐ฆ โ ๐ฅ)) โ ๐ฅ โ โ) |
57 | 47 | adantr 276 |
. . . . . . . . . . . 12
โข
(((((โ๐ค
โ โ (โ๐ง
โ โ (๐ค ยท
๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โง 0 < (๐ฆ โ ๐ฅ)) โ ๐ฆ โ โ) |
58 | 56, 57 | posdifd 8492 |
. . . . . . . . . . 11
โข
(((((โ๐ค
โ โ (โ๐ง
โ โ (๐ค ยท
๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โง 0 < (๐ฆ โ ๐ฅ)) โ (๐ฅ < ๐ฆ โ 0 < (๐ฆ โ ๐ฅ))) |
59 | 55, 58 | mpbird 167 |
. . . . . . . . . 10
โข
(((((โ๐ค
โ โ (โ๐ง
โ โ (๐ค ยท
๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โง 0 < (๐ฆ โ ๐ฅ)) โ ๐ฅ < ๐ฆ) |
60 | 59 | 3mix1d 1172 |
. . . . . . . . 9
โข
(((((โ๐ค
โ โ (โ๐ง
โ โ (๐ค ยท
๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โง 0 < (๐ฆ โ ๐ฅ)) โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) |
61 | 47 | recnd 7989 |
. . . . . . . . . . . 12
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ ๐ฆ โ โ) |
62 | 50 | recnd 7989 |
. . . . . . . . . . . 12
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ ๐ฅ โ โ) |
63 | 61, 62 | subcld 8271 |
. . . . . . . . . . 11
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ (๐ฆ โ ๐ฅ) โ โ) |
64 | | simplr 528 |
. . . . . . . . . . . 12
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ ๐ง โ โ) |
65 | 64 | recnd 7989 |
. . . . . . . . . . 11
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ ๐ง โ โ) |
66 | | simpr 110 |
. . . . . . . . . . . 12
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) |
67 | | 1ap0 8550 |
. . . . . . . . . . . 12
โข 1 #
0 |
68 | 66, 67 | eqbrtrdi 4044 |
. . . . . . . . . . 11
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ ((๐ฆ โ ๐ฅ) ยท ๐ง) # 0) |
69 | 63, 65, 68 | mulap0bad 8619 |
. . . . . . . . . 10
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ (๐ฆ โ ๐ฅ) # 0) |
70 | 46, 49 | resubcld 8341 |
. . . . . . . . . . . 12
โข
((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฆ โ ๐ฅ) โ โ) |
71 | 70 | ad2antrr 488 |
. . . . . . . . . . 11
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ (๐ฆ โ ๐ฅ) โ โ) |
72 | | reaplt 8548 |
. . . . . . . . . . 11
โข (((๐ฆ โ ๐ฅ) โ โ โง 0 โ โ)
โ ((๐ฆ โ ๐ฅ) # 0 โ ((๐ฆ โ ๐ฅ) < 0 โจ 0 < (๐ฆ โ ๐ฅ)))) |
73 | 71, 21, 72 | sylancl 413 |
. . . . . . . . . 10
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ ((๐ฆ โ ๐ฅ) # 0 โ ((๐ฆ โ ๐ฅ) < 0 โจ 0 < (๐ฆ โ ๐ฅ)))) |
74 | 69, 73 | mpbid 147 |
. . . . . . . . 9
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ ((๐ฆ โ ๐ฅ) < 0 โจ 0 < (๐ฆ โ ๐ฅ))) |
75 | 54, 60, 74 | mpjaodan 798 |
. . . . . . . 8
โข
((((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) |
76 | 75 | exp31 364 |
. . . . . . 7
โข
((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ง โ โ โ (((๐ฆ โ ๐ฅ) ยท ๐ง) = 1 โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)))) |
77 | 43, 44, 76 | rexlimd 2591 |
. . . . . 6
โข
((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (โ๐ง โ โ ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1 โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ))) |
78 | 77 | imp 124 |
. . . . 5
โข
(((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง โ๐ง โ โ ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1) โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) |
79 | 46 | recnd 7989 |
. . . . . . . . 9
โข
((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ฆ โ โ) |
80 | 79 | adantr 276 |
. . . . . . . 8
โข
(((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง (๐ฆ โ ๐ฅ) = 0) โ ๐ฆ โ โ) |
81 | 49 | recnd 7989 |
. . . . . . . . 9
โข
((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ฅ โ โ) |
82 | 81 | adantr 276 |
. . . . . . . 8
โข
(((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง (๐ฆ โ ๐ฅ) = 0) โ ๐ฅ โ โ) |
83 | | simpr 110 |
. . . . . . . 8
โข
(((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง (๐ฆ โ ๐ฅ) = 0) โ (๐ฆ โ ๐ฅ) = 0) |
84 | 80, 82, 83 | subeq0d 8279 |
. . . . . . 7
โข
(((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง (๐ฆ โ ๐ฅ) = 0) โ ๐ฆ = ๐ฅ) |
85 | 84 | equcomd 1707 |
. . . . . 6
โข
(((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง (๐ฆ โ ๐ฅ) = 0) โ ๐ฅ = ๐ฆ) |
86 | 85 | 3mix2d 1173 |
. . . . 5
โข
(((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง (๐ฆ โ ๐ฅ) = 0) โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) |
87 | | oveq1 5885 |
. . . . . . . . 9
โข (๐ค = (๐ฆ โ ๐ฅ) โ (๐ค ยท ๐ง) = ((๐ฆ โ ๐ฅ) ยท ๐ง)) |
88 | 87 | eqeq1d 2186 |
. . . . . . . 8
โข (๐ค = (๐ฆ โ ๐ฅ) โ ((๐ค ยท ๐ง) = 1 โ ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1)) |
89 | 88 | rexbidv 2478 |
. . . . . . 7
โข (๐ค = (๐ฆ โ ๐ฅ) โ (โ๐ง โ โ (๐ค ยท ๐ง) = 1 โ โ๐ง โ โ ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1)) |
90 | | eqeq1 2184 |
. . . . . . 7
โข (๐ค = (๐ฆ โ ๐ฅ) โ (๐ค = 0 โ (๐ฆ โ ๐ฅ) = 0)) |
91 | 89, 90 | orbi12d 793 |
. . . . . 6
โข (๐ค = (๐ฆ โ ๐ฅ) โ ((โ๐ง โ โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โ (โ๐ง โ โ ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1 โจ (๐ฆ โ ๐ฅ) = 0))) |
92 | | simpl 109 |
. . . . . 6
โข
((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ โ๐ค โ โ (โ๐ง โ โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0)) |
93 | 91, 92, 70 | rspcdva 2848 |
. . . . 5
โข
((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (โ๐ง โ โ ((๐ฆ โ ๐ฅ) ยท ๐ง) = 1 โจ (๐ฆ โ ๐ฅ) = 0)) |
94 | 78, 86, 93 | mpjaodan 798 |
. . . 4
โข
((โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) |
95 | 94 | ralrimivva 2559 |
. . 3
โข
(โ๐ค โ
โ (โ๐ง โ
โ (๐ค ยท ๐ง) = 1 โจ ๐ค = 0) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) |
96 | 36, 95 | sylbi 121 |
. 2
โข
(โ๐ฅ โ
โ (โ๐ง โ
โ (๐ฅ ยท ๐ง) = 1 โจ ๐ฅ = 0) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) |
97 | 30, 96 | impbii 126 |
1
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ) โ โ๐ฅ โ โ (โ๐ง โ โ (๐ฅ ยท ๐ง) = 1 โจ ๐ฅ = 0)) |