Step | Hyp | Ref
| Expression |
1 | | zre 12508 |
. . . . . 6
โข (๐ โ โค โ ๐ โ
โ) |
2 | 1 | adantr 482 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
3 | | nnre 12165 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
4 | 3 | adantl 483 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
5 | | nnne0 12192 |
. . . . . 6
โข (๐ โ โ โ ๐ โ 0) |
6 | 5 | adantl 483 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ 0) |
7 | 2, 4, 6 | redivcld 11988 |
. . . 4
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) โ โ) |
8 | | intfracq.1 |
. . . . 5
โข ๐ = (โโ(๐ / ๐)) |
9 | | intfracq.2 |
. . . . 5
โข ๐น = ((๐ / ๐) โ ๐) |
10 | 8, 9 | intfrac2 13769 |
. . . 4
โข ((๐ / ๐) โ โ โ (0 โค ๐น โง ๐น < 1 โง (๐ / ๐) = (๐ + ๐น))) |
11 | 7, 10 | syl 17 |
. . 3
โข ((๐ โ โค โง ๐ โ โ) โ (0 โค
๐น โง ๐น < 1 โง (๐ / ๐) = (๐ + ๐น))) |
12 | 11 | simp1d 1143 |
. 2
โข ((๐ โ โค โง ๐ โ โ) โ 0 โค
๐น) |
13 | | fraclt1 13713 |
. . . . . . 7
โข ((๐ / ๐) โ โ โ ((๐ / ๐) โ (โโ(๐ / ๐))) < 1) |
14 | 7, 13 | syl 17 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / ๐) โ (โโ(๐ / ๐))) < 1) |
15 | 8 | oveq2i 7369 |
. . . . . . . 8
โข ((๐ / ๐) โ ๐) = ((๐ / ๐) โ (โโ(๐ / ๐))) |
16 | 9, 15 | eqtri 2761 |
. . . . . . 7
โข ๐น = ((๐ / ๐) โ (โโ(๐ / ๐))) |
17 | 16 | a1i 11 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ ๐น = ((๐ / ๐) โ (โโ(๐ / ๐)))) |
18 | | nncn 12166 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
19 | 18, 5 | dividd 11934 |
. . . . . . 7
โข (๐ โ โ โ (๐ / ๐) = 1) |
20 | 19 | adantl 483 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) = 1) |
21 | 14, 17, 20 | 3brtr4d 5138 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ) โ ๐น < (๐ / ๐)) |
22 | | reflcl 13707 |
. . . . . . . . . 10
โข ((๐ / ๐) โ โ โ
(โโ(๐ / ๐)) โ
โ) |
23 | 7, 22 | syl 17 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ
(โโ(๐ / ๐)) โ
โ) |
24 | 8, 23 | eqeltrid 2838 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
25 | 7, 24 | resubcld 11588 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / ๐) โ ๐) โ โ) |
26 | 9, 25 | eqeltrid 2838 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ ๐น โ
โ) |
27 | | nngt0 12189 |
. . . . . . . 8
โข (๐ โ โ โ 0 <
๐) |
28 | 3, 27 | jca 513 |
. . . . . . 7
โข (๐ โ โ โ (๐ โ โ โง 0 <
๐)) |
29 | 28 | adantl 483 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โ โ โง 0 <
๐)) |
30 | | ltmuldiv2 12034 |
. . . . . 6
โข ((๐น โ โ โง ๐ โ โ โง (๐ โ โ โง 0 <
๐)) โ ((๐ ยท ๐น) < ๐ โ ๐น < (๐ / ๐))) |
31 | 26, 4, 29, 30 | syl3anc 1372 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ ยท ๐น) < ๐ โ ๐น < (๐ / ๐))) |
32 | 21, 31 | mpbird 257 |
. . . 4
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท ๐น) < ๐) |
33 | 9 | oveq2i 7369 |
. . . . . . 7
โข (๐ ยท ๐น) = (๐ ยท ((๐ / ๐) โ ๐)) |
34 | 18 | adantl 483 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
35 | 7 | recnd 11188 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) โ โ) |
36 | 7 | flcld 13709 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ
(โโ(๐ / ๐)) โ
โค) |
37 | 8, 36 | eqeltrid 2838 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โค) |
38 | 37 | zcnd 12613 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
39 | 34, 35, 38 | subdid 11616 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท ((๐ / ๐) โ ๐)) = ((๐ ยท (๐ / ๐)) โ (๐ ยท ๐))) |
40 | 33, 39 | eqtrid 2785 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท ๐น) = ((๐ ยท (๐ / ๐)) โ (๐ ยท ๐))) |
41 | | zcn 12509 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โ) |
42 | 41 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
43 | 42, 34, 6 | divcan2d 11938 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท (๐ / ๐)) = ๐) |
44 | | simpl 484 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โค) |
45 | 43, 44 | eqeltrd 2834 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท (๐ / ๐)) โ โค) |
46 | | nnz 12525 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โค) |
47 | 46 | adantl 483 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โค) |
48 | 47, 37 | zmulcld 12618 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท ๐) โ โค) |
49 | 45, 48 | zsubcld 12617 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ ยท (๐ / ๐)) โ (๐ ยท ๐)) โ โค) |
50 | 40, 49 | eqeltrd 2834 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท ๐น) โ โค) |
51 | | zltlem1 12561 |
. . . . 5
โข (((๐ ยท ๐น) โ โค โง ๐ โ โค) โ ((๐ ยท ๐น) < ๐ โ (๐ ยท ๐น) โค (๐ โ 1))) |
52 | 50, 47, 51 | syl2anc 585 |
. . . 4
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ ยท ๐น) < ๐ โ (๐ ยท ๐น) โค (๐ โ 1))) |
53 | 32, 52 | mpbid 231 |
. . 3
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท ๐น) โค (๐ โ 1)) |
54 | | peano2rem 11473 |
. . . . . 6
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
55 | 3, 54 | syl 17 |
. . . . 5
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
56 | 55 | adantl 483 |
. . . 4
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โ 1) โ
โ) |
57 | | lemuldiv2 12041 |
. . . 4
โข ((๐น โ โ โง (๐ โ 1) โ โ โง
(๐ โ โ โง 0
< ๐)) โ ((๐ ยท ๐น) โค (๐ โ 1) โ ๐น โค ((๐ โ 1) / ๐))) |
58 | 26, 56, 29, 57 | syl3anc 1372 |
. . 3
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ ยท ๐น) โค (๐ โ 1) โ ๐น โค ((๐ โ 1) / ๐))) |
59 | 53, 58 | mpbid 231 |
. 2
โข ((๐ โ โค โง ๐ โ โ) โ ๐น โค ((๐ โ 1) / ๐)) |
60 | 11 | simp3d 1145 |
. 2
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) = (๐ + ๐น)) |
61 | 12, 59, 60 | 3jca 1129 |
1
โข ((๐ โ โค โง ๐ โ โ) โ (0 โค
๐น โง ๐น โค ((๐ โ 1) / ๐) โง (๐ / ๐) = (๐ + ๐น))) |