Step | Hyp | Ref
| Expression |
1 | | znq 9626 |
. . . 4
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) โ โ) |
2 | | intfracq.1 |
. . . . 5
โข ๐ = (โโ(๐ / ๐)) |
3 | | intfracq.2 |
. . . . 5
โข ๐น = ((๐ / ๐) โ ๐) |
4 | 2, 3 | intqfrac2 10321 |
. . . 4
โข ((๐ / ๐) โ โ โ (0 โค ๐น โง ๐น < 1 โง (๐ / ๐) = (๐ + ๐น))) |
5 | 1, 4 | syl 14 |
. . 3
โข ((๐ โ โค โง ๐ โ โ) โ (0 โค
๐น โง ๐น < 1 โง (๐ / ๐) = (๐ + ๐น))) |
6 | 5 | simp1d 1009 |
. 2
โข ((๐ โ โค โง ๐ โ โ) โ 0 โค
๐น) |
7 | | qfraclt1 10282 |
. . . . . . 7
โข ((๐ / ๐) โ โ โ ((๐ / ๐) โ (โโ(๐ / ๐))) < 1) |
8 | 1, 7 | syl 14 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / ๐) โ (โโ(๐ / ๐))) < 1) |
9 | 2 | oveq2i 5888 |
. . . . . . . 8
โข ((๐ / ๐) โ ๐) = ((๐ / ๐) โ (โโ(๐ / ๐))) |
10 | 3, 9 | eqtri 2198 |
. . . . . . 7
โข ๐น = ((๐ / ๐) โ (โโ(๐ / ๐))) |
11 | 10 | a1i 9 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ ๐น = ((๐ / ๐) โ (โโ(๐ / ๐)))) |
12 | | simpr 110 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
13 | 12 | nncnd 8935 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
14 | 12 | nnap0d 8967 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ ๐ # 0) |
15 | 13, 14 | dividapd 8745 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) = 1) |
16 | 8, 11, 15 | 3brtr4d 4037 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ) โ ๐น < (๐ / ๐)) |
17 | | qre 9627 |
. . . . . . . . 9
โข ((๐ / ๐) โ โ โ (๐ / ๐) โ โ) |
18 | 1, 17 | syl 14 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) โ โ) |
19 | 1 | flqcld 10279 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ
(โโ(๐ / ๐)) โ
โค) |
20 | 2, 19 | eqeltrid 2264 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โค) |
21 | 20 | zred 9377 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
22 | 18, 21 | resubcld 8340 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / ๐) โ ๐) โ โ) |
23 | 3, 22 | eqeltrid 2264 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ ๐น โ
โ) |
24 | | nnre 8928 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
25 | 24 | adantl 277 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
26 | | nngt0 8946 |
. . . . . . . 8
โข (๐ โ โ โ 0 <
๐) |
27 | 24, 26 | jca 306 |
. . . . . . 7
โข (๐ โ โ โ (๐ โ โ โง 0 <
๐)) |
28 | 27 | adantl 277 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โ โ โง 0 <
๐)) |
29 | | ltmuldiv2 8834 |
. . . . . 6
โข ((๐น โ โ โง ๐ โ โ โง (๐ โ โ โง 0 <
๐)) โ ((๐ ยท ๐น) < ๐ โ ๐น < (๐ / ๐))) |
30 | 23, 25, 28, 29 | syl3anc 1238 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ ยท ๐น) < ๐ โ ๐น < (๐ / ๐))) |
31 | 16, 30 | mpbird 167 |
. . . 4
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท ๐น) < ๐) |
32 | 3 | oveq2i 5888 |
. . . . . . 7
โข (๐ ยท ๐น) = (๐ ยท ((๐ / ๐) โ ๐)) |
33 | 18 | recnd 7988 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) โ โ) |
34 | 20 | zcnd 9378 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
35 | 13, 33, 34 | subdid 8373 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท ((๐ / ๐) โ ๐)) = ((๐ ยท (๐ / ๐)) โ (๐ ยท ๐))) |
36 | 32, 35 | eqtrid 2222 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท ๐น) = ((๐ ยท (๐ / ๐)) โ (๐ ยท ๐))) |
37 | | zcn 9260 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โ) |
38 | 37 | adantr 276 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
39 | 38, 13, 14 | divcanap2d 8751 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท (๐ / ๐)) = ๐) |
40 | | simpl 109 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โค) |
41 | 39, 40 | eqeltrd 2254 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท (๐ / ๐)) โ โค) |
42 | | nnz 9274 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โค) |
43 | 42 | adantl 277 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โค) |
44 | 43, 20 | zmulcld 9383 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท ๐) โ โค) |
45 | 41, 44 | zsubcld 9382 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ ยท (๐ / ๐)) โ (๐ ยท ๐)) โ โค) |
46 | 36, 45 | eqeltrd 2254 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท ๐น) โ โค) |
47 | | zltlem1 9312 |
. . . . 5
โข (((๐ ยท ๐น) โ โค โง ๐ โ โค) โ ((๐ ยท ๐น) < ๐ โ (๐ ยท ๐น) โค (๐ โ 1))) |
48 | 46, 43, 47 | syl2anc 411 |
. . . 4
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ ยท ๐น) < ๐ โ (๐ ยท ๐น) โค (๐ โ 1))) |
49 | 31, 48 | mpbid 147 |
. . 3
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท ๐น) โค (๐ โ 1)) |
50 | | peano2rem 8226 |
. . . . . 6
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
51 | 24, 50 | syl 14 |
. . . . 5
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
52 | 51 | adantl 277 |
. . . 4
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โ 1) โ
โ) |
53 | | lemuldiv2 8841 |
. . . 4
โข ((๐น โ โ โง (๐ โ 1) โ โ โง
(๐ โ โ โง 0
< ๐)) โ ((๐ ยท ๐น) โค (๐ โ 1) โ ๐น โค ((๐ โ 1) / ๐))) |
54 | 23, 52, 28, 53 | syl3anc 1238 |
. . 3
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ ยท ๐น) โค (๐ โ 1) โ ๐น โค ((๐ โ 1) / ๐))) |
55 | 49, 54 | mpbid 147 |
. 2
โข ((๐ โ โค โง ๐ โ โ) โ ๐น โค ((๐ โ 1) / ๐)) |
56 | 5 | simp3d 1011 |
. 2
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) = (๐ + ๐น)) |
57 | 6, 55, 56 | 3jca 1177 |
1
โข ((๐ โ โค โง ๐ โ โ) โ (0 โค
๐น โง ๐น โค ((๐ โ 1) / ๐) โง (๐ / ๐) = (๐ + ๐น))) |