Step | Hyp | Ref
| Expression |
1 | | elq 9621 |
. . . 4
โข (๐ โ โ โ
โ๐ง โ โค
โ๐ค โ โ
๐ = (๐ง / ๐ค)) |
2 | 1 | biimpi 120 |
. . 3
โข (๐ โ โ โ
โ๐ง โ โค
โ๐ค โ โ
๐ = (๐ง / ๐ค)) |
3 | 2 | adantl 277 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ
โ๐ง โ โค
โ๐ค โ โ
๐ = (๐ง / ๐ค)) |
4 | | elq 9621 |
. . . . . . 7
โข (๐ โ โ โ
โ๐ฅ โ โค
โ๐ฆ โ โ
๐ = (๐ฅ / ๐ฆ)) |
5 | 4 | biimpi 120 |
. . . . . 6
โข (๐ โ โ โ
โ๐ฅ โ โค
โ๐ฆ โ โ
๐ = (๐ฅ / ๐ฆ)) |
6 | 5 | ad3antrrr 492 |
. . . . 5
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โง ๐ = (๐ง / ๐ค)) โ โ๐ฅ โ โค โ๐ฆ โ โ ๐ = (๐ฅ / ๐ฆ)) |
7 | | simplrl 535 |
. . . . . . . . . 10
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ฅ โ โค) |
8 | | simplrr 536 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โง ๐ = (๐ง / ๐ค)) โ ๐ค โ โ) |
9 | 8 | ad2antrr 488 |
. . . . . . . . . . 11
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ค โ โ) |
10 | 9 | nnzd 9373 |
. . . . . . . . . 10
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ค โ โค) |
11 | 7, 10 | zmulcld 9380 |
. . . . . . . . 9
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ (๐ฅ ยท ๐ค) โ โค) |
12 | | simplrl 535 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โง ๐ = (๐ง / ๐ค)) โ ๐ง โ โค) |
13 | 12 | ad2antrr 488 |
. . . . . . . . . 10
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ง โ โค) |
14 | | simplrr 536 |
. . . . . . . . . . 11
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ฆ โ โ) |
15 | 14 | nnzd 9373 |
. . . . . . . . . 10
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ฆ โ โค) |
16 | 13, 15 | zmulcld 9380 |
. . . . . . . . 9
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ (๐ง ยท ๐ฆ) โ โค) |
17 | | ztri3or 9295 |
. . . . . . . . 9
โข (((๐ฅ ยท ๐ค) โ โค โง (๐ง ยท ๐ฆ) โ โค) โ ((๐ฅ ยท ๐ค) < (๐ง ยท ๐ฆ) โจ (๐ฅ ยท ๐ค) = (๐ง ยท ๐ฆ) โจ (๐ง ยท ๐ฆ) < (๐ฅ ยท ๐ค))) |
18 | 11, 16, 17 | syl2anc 411 |
. . . . . . . 8
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ((๐ฅ ยท ๐ค) < (๐ง ยท ๐ฆ) โจ (๐ฅ ยท ๐ค) = (๐ง ยท ๐ฆ) โจ (๐ง ยท ๐ฆ) < (๐ฅ ยท ๐ค))) |
19 | | simpllr 534 |
. . . . . . . . . . 11
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ = (๐ง / ๐ค)) |
20 | 19 | breq2d 4015 |
. . . . . . . . . 10
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ((๐ฅ / ๐ฆ) < ๐ โ (๐ฅ / ๐ฆ) < (๐ง / ๐ค))) |
21 | | breq1 4006 |
. . . . . . . . . . 11
โข (๐ = (๐ฅ / ๐ฆ) โ (๐ < ๐ โ (๐ฅ / ๐ฆ) < ๐)) |
22 | 21 | adantl 277 |
. . . . . . . . . 10
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ (๐ < ๐ โ (๐ฅ / ๐ฆ) < ๐)) |
23 | 7 | zred 9374 |
. . . . . . . . . . 11
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ฅ โ โ) |
24 | 9 | nnrpd 9693 |
. . . . . . . . . . 11
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ค โ โ+) |
25 | 13 | zred 9374 |
. . . . . . . . . . 11
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ง โ โ) |
26 | 14 | nnrpd 9693 |
. . . . . . . . . . 11
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ฆ โ โ+) |
27 | 23, 24, 25, 26 | lt2mul2divd 9764 |
. . . . . . . . . 10
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ((๐ฅ ยท ๐ค) < (๐ง ยท ๐ฆ) โ (๐ฅ / ๐ฆ) < (๐ง / ๐ค))) |
28 | 20, 22, 27 | 3bitr4rd 221 |
. . . . . . . . 9
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ((๐ฅ ยท ๐ค) < (๐ง ยท ๐ฆ) โ ๐ < ๐)) |
29 | | simpr 110 |
. . . . . . . . . . 11
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ = (๐ฅ / ๐ฆ)) |
30 | 29, 19 | eqeq12d 2192 |
. . . . . . . . . 10
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ (๐ = ๐ โ (๐ฅ / ๐ฆ) = (๐ง / ๐ค))) |
31 | 7 | zcnd 9375 |
. . . . . . . . . . 11
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ฅ โ โ) |
32 | 13 | zcnd 9375 |
. . . . . . . . . . 11
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ง โ โ) |
33 | 14 | nncnd 8932 |
. . . . . . . . . . . 12
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ฆ โ โ) |
34 | 14 | nnap0d 8964 |
. . . . . . . . . . . 12
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ฆ # 0) |
35 | 33, 34 | jca 306 |
. . . . . . . . . . 11
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ (๐ฆ โ โ โง ๐ฆ # 0)) |
36 | 9 | nncnd 8932 |
. . . . . . . . . . . 12
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ค โ โ) |
37 | 9 | nnap0d 8964 |
. . . . . . . . . . . 12
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ๐ค # 0) |
38 | 36, 37 | jca 306 |
. . . . . . . . . . 11
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ (๐ค โ โ โง ๐ค # 0)) |
39 | | divmuleqap 8673 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ๐ง โ โ) โง ((๐ฆ โ โ โง ๐ฆ # 0) โง (๐ค โ โ โง ๐ค # 0))) โ ((๐ฅ / ๐ฆ) = (๐ง / ๐ค) โ (๐ฅ ยท ๐ค) = (๐ง ยท ๐ฆ))) |
40 | 31, 32, 35, 38, 39 | syl22anc 1239 |
. . . . . . . . . 10
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ((๐ฅ / ๐ฆ) = (๐ง / ๐ค) โ (๐ฅ ยท ๐ค) = (๐ง ยท ๐ฆ))) |
41 | 30, 40 | bitr2d 189 |
. . . . . . . . 9
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ((๐ฅ ยท ๐ค) = (๐ง ยท ๐ฆ) โ ๐ = ๐)) |
42 | 25, 26, 23, 24 | lt2mul2divd 9764 |
. . . . . . . . . 10
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ((๐ง ยท ๐ฆ) < (๐ฅ ยท ๐ค) โ (๐ง / ๐ค) < (๐ฅ / ๐ฆ))) |
43 | 19, 29 | breq12d 4016 |
. . . . . . . . . 10
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ (๐ < ๐ โ (๐ง / ๐ค) < (๐ฅ / ๐ฆ))) |
44 | 42, 43 | bitr4d 191 |
. . . . . . . . 9
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ ((๐ง ยท ๐ฆ) < (๐ฅ ยท ๐ค) โ ๐ < ๐)) |
45 | 28, 41, 44 | 3orbi123d 1311 |
. . . . . . . 8
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ (((๐ฅ ยท ๐ค) < (๐ง ยท ๐ฆ) โจ (๐ฅ ยท ๐ค) = (๐ง ยท ๐ฆ) โจ (๐ง ยท ๐ฆ) < (๐ฅ ยท ๐ค)) โ (๐ < ๐ โจ ๐ = ๐ โจ ๐ < ๐))) |
46 | 18, 45 | mpbid 147 |
. . . . . . 7
โข
((((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โง ๐ = (๐ฅ / ๐ฆ)) โ (๐ < ๐ โจ ๐ = ๐ โจ ๐ < ๐)) |
47 | 46 | ex 115 |
. . . . . 6
โข
(((((๐ โ
โ โง ๐ โ
โ) โง (๐ง โ
โค โง ๐ค โ
โ)) โง ๐ = (๐ง / ๐ค)) โง (๐ฅ โ โค โง ๐ฆ โ โ)) โ (๐ = (๐ฅ / ๐ฆ) โ (๐ < ๐ โจ ๐ = ๐ โจ ๐ < ๐))) |
48 | 47 | rexlimdvva 2602 |
. . . . 5
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โง ๐ = (๐ง / ๐ค)) โ (โ๐ฅ โ โค โ๐ฆ โ โ ๐ = (๐ฅ / ๐ฆ) โ (๐ < ๐ โจ ๐ = ๐ โจ ๐ < ๐))) |
49 | 6, 48 | mpd 13 |
. . . 4
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โง ๐ = (๐ง / ๐ค)) โ (๐ < ๐ โจ ๐ = ๐ โจ ๐ < ๐)) |
50 | 49 | ex 115 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โ (๐ = (๐ง / ๐ค) โ (๐ < ๐ โจ ๐ = ๐ โจ ๐ < ๐))) |
51 | 50 | rexlimdvva 2602 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ
(โ๐ง โ โค
โ๐ค โ โ
๐ = (๐ง / ๐ค) โ (๐ < ๐ โจ ๐ = ๐ โจ ๐ < ๐))) |
52 | 3, 51 | mpd 13 |
1
โข ((๐ โ โ โง ๐ โ โ) โ (๐ < ๐ โจ ๐ = ๐ โจ ๐ < ๐)) |