Step | Hyp | Ref
| Expression |
1 | | simpll1 1036 |
. . . 4
โข ((((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โง ๐ < ๐) โ ๐ด โ โ) |
2 | | simpll2 1037 |
. . . . 5
โข ((((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โง ๐ < ๐) โ ๐ โ
โ0) |
3 | 2 | nn0zd 9372 |
. . . 4
โข ((((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โง ๐ < ๐) โ ๐ โ โค) |
4 | | simpll3 1038 |
. . . . 5
โข ((((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โง ๐ < ๐) โ ๐ โ
โ0) |
5 | 4 | nn0zd 9372 |
. . . 4
โข ((((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โง ๐ < ๐) โ ๐ โ โค) |
6 | | simplr 528 |
. . . 4
โข ((((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โง ๐ < ๐) โ 1 < ๐ด) |
7 | | simpr 110 |
. . . 4
โข ((((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โง ๐ < ๐) โ ๐ < ๐) |
8 | | ltexp2a 10571 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โค โง ๐ โ โค) โง (1 <
๐ด โง ๐ < ๐)) โ (๐ดโ๐) < (๐ดโ๐)) |
9 | 1, 3, 5, 6, 7, 8 | syl32anc 1246 |
. . 3
โข ((((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โง ๐ < ๐) โ (๐ดโ๐) < (๐ดโ๐)) |
10 | 9 | ex 115 |
. 2
โข (((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โ (๐ < ๐ โ (๐ดโ๐) < (๐ดโ๐))) |
11 | | oveq2 5882 |
. . . . 5
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
12 | 11 | breq1d 4013 |
. . . 4
โข (๐ = ๐ โ ((๐ดโ๐) < (๐ดโ๐) โ (๐ดโ๐) < (๐ดโ๐))) |
13 | | breq1 4006 |
. . . 4
โข (๐ = ๐ โ (๐ < ๐ โ ๐ < ๐)) |
14 | 12, 13 | imbi12d 234 |
. . 3
โข (๐ = ๐ โ (((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐) โ ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐))) |
15 | | simpl3 1002 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โ ๐ โ
โ0) |
16 | | simpl1 1000 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โ ๐ด โ โ) |
17 | | simpr 110 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โ 1 < ๐ด) |
18 | | oveq2 5882 |
. . . . . . . . . 10
โข (๐ค = 0 โ (๐ดโ๐ค) = (๐ดโ0)) |
19 | 18 | breq2d 4015 |
. . . . . . . . 9
โข (๐ค = 0 โ ((๐ดโ๐) < (๐ดโ๐ค) โ (๐ดโ๐) < (๐ดโ0))) |
20 | | breq2 4007 |
. . . . . . . . 9
โข (๐ค = 0 โ (๐ < ๐ค โ ๐ < 0)) |
21 | 19, 20 | imbi12d 234 |
. . . . . . . 8
โข (๐ค = 0 โ (((๐ดโ๐) < (๐ดโ๐ค) โ ๐ < ๐ค) โ ((๐ดโ๐) < (๐ดโ0) โ ๐ < 0))) |
22 | 21 | ralbidv 2477 |
. . . . . . 7
โข (๐ค = 0 โ (โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐ค) โ ๐ < ๐ค) โ โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ0) โ ๐ < 0))) |
23 | 22 | imbi2d 230 |
. . . . . 6
โข (๐ค = 0 โ (((๐ด โ โ โง 1 < ๐ด) โ โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐ค) โ ๐ < ๐ค)) โ ((๐ด โ โ โง 1 < ๐ด) โ โ๐ โ โ0
((๐ดโ๐) < (๐ดโ0) โ ๐ < 0)))) |
24 | | oveq2 5882 |
. . . . . . . . . 10
โข (๐ค = ๐ โ (๐ดโ๐ค) = (๐ดโ๐)) |
25 | 24 | breq2d 4015 |
. . . . . . . . 9
โข (๐ค = ๐ โ ((๐ดโ๐) < (๐ดโ๐ค) โ (๐ดโ๐) < (๐ดโ๐))) |
26 | | breq2 4007 |
. . . . . . . . 9
โข (๐ค = ๐ โ (๐ < ๐ค โ ๐ < ๐)) |
27 | 25, 26 | imbi12d 234 |
. . . . . . . 8
โข (๐ค = ๐ โ (((๐ดโ๐) < (๐ดโ๐ค) โ ๐ < ๐ค) โ ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐))) |
28 | 27 | ralbidv 2477 |
. . . . . . 7
โข (๐ค = ๐ โ (โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ๐ค) โ ๐ < ๐ค) โ โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐))) |
29 | 28 | imbi2d 230 |
. . . . . 6
โข (๐ค = ๐ โ (((๐ด โ โ โง 1 < ๐ด) โ โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐ค) โ ๐ < ๐ค)) โ ((๐ด โ โ โง 1 < ๐ด) โ โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)))) |
30 | | oveq2 5882 |
. . . . . . . . . 10
โข (๐ค = (๐ + 1) โ (๐ดโ๐ค) = (๐ดโ(๐ + 1))) |
31 | 30 | breq2d 4015 |
. . . . . . . . 9
โข (๐ค = (๐ + 1) โ ((๐ดโ๐) < (๐ดโ๐ค) โ (๐ดโ๐) < (๐ดโ(๐ + 1)))) |
32 | | breq2 4007 |
. . . . . . . . 9
โข (๐ค = (๐ + 1) โ (๐ < ๐ค โ ๐ < (๐ + 1))) |
33 | 31, 32 | imbi12d 234 |
. . . . . . . 8
โข (๐ค = (๐ + 1) โ (((๐ดโ๐) < (๐ดโ๐ค) โ ๐ < ๐ค) โ ((๐ดโ๐) < (๐ดโ(๐ + 1)) โ ๐ < (๐ + 1)))) |
34 | 33 | ralbidv 2477 |
. . . . . . 7
โข (๐ค = (๐ + 1) โ (โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ๐ค) โ ๐ < ๐ค) โ โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ(๐ + 1)) โ ๐ < (๐ + 1)))) |
35 | 34 | imbi2d 230 |
. . . . . 6
โข (๐ค = (๐ + 1) โ (((๐ด โ โ โง 1 < ๐ด) โ โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐ค) โ ๐ < ๐ค)) โ ((๐ด โ โ โง 1 < ๐ด) โ โ๐ โ โ0
((๐ดโ๐) < (๐ดโ(๐ + 1)) โ ๐ < (๐ + 1))))) |
36 | | oveq2 5882 |
. . . . . . . . . 10
โข (๐ค = ๐ โ (๐ดโ๐ค) = (๐ดโ๐)) |
37 | 36 | breq2d 4015 |
. . . . . . . . 9
โข (๐ค = ๐ โ ((๐ดโ๐) < (๐ดโ๐ค) โ (๐ดโ๐) < (๐ดโ๐))) |
38 | | breq2 4007 |
. . . . . . . . 9
โข (๐ค = ๐ โ (๐ < ๐ค โ ๐ < ๐)) |
39 | 37, 38 | imbi12d 234 |
. . . . . . . 8
โข (๐ค = ๐ โ (((๐ดโ๐) < (๐ดโ๐ค) โ ๐ < ๐ค) โ ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐))) |
40 | 39 | ralbidv 2477 |
. . . . . . 7
โข (๐ค = ๐ โ (โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ๐ค) โ ๐ < ๐ค) โ โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐))) |
41 | 40 | imbi2d 230 |
. . . . . 6
โข (๐ค = ๐ โ (((๐ด โ โ โง 1 < ๐ด) โ โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐ค) โ ๐ < ๐ค)) โ ((๐ด โ โ โง 1 < ๐ด) โ โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)))) |
42 | | recn 7943 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ ๐ด โ
โ) |
43 | 42 | ad2antrr 488 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ ๐ด โ
โ) |
44 | 43 | exp0d 10647 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ (๐ดโ0) = 1) |
45 | | 1re 7955 |
. . . . . . . . . 10
โข 1 โ
โ |
46 | 44, 45 | eqeltrdi 2268 |
. . . . . . . . 9
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ (๐ดโ0) โ
โ) |
47 | | simpll 527 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ ๐ด โ
โ) |
48 | | simpr 110 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ ๐ โ
โ0) |
49 | 47, 48 | reexpcld 10670 |
. . . . . . . . 9
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ (๐ดโ๐) โ โ) |
50 | | 1red 7971 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ 1 โ
โ) |
51 | | simplr 528 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ 1 <
๐ด) |
52 | 50, 47, 51 | ltled 8075 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ 1 โค
๐ด) |
53 | 47, 48, 52 | expge1d 10672 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ 1 โค
(๐ดโ๐)) |
54 | 44, 53 | eqbrtrd 4025 |
. . . . . . . . 9
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ (๐ดโ0) โค (๐ดโ๐)) |
55 | 46, 49, 54 | lensymd 8078 |
. . . . . . . 8
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ ยฌ
(๐ดโ๐) < (๐ดโ0)) |
56 | 55 | pm2.21d 619 |
. . . . . . 7
โข (((๐ด โ โ โง 1 <
๐ด) โง ๐ โ โ0) โ ((๐ดโ๐) < (๐ดโ0) โ ๐ < 0)) |
57 | 56 | ralrimiva 2550 |
. . . . . 6
โข ((๐ด โ โ โง 1 <
๐ด) โ โ๐ โ โ0
((๐ดโ๐) < (๐ดโ0) โ ๐ < 0)) |
58 | | oveq2 5882 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
59 | 58 | breq1d 4013 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐ดโ๐) < (๐ดโ๐) โ (๐ดโ๐) < (๐ดโ๐))) |
60 | | breq1 4006 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ < ๐ โ ๐ < ๐)) |
61 | 59, 60 | imbi12d 234 |
. . . . . . . . . 10
โข (๐ = ๐ โ (((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐) โ ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐))) |
62 | 61 | cbvralv 2703 |
. . . . . . . . 9
โข
(โ๐ โ
โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐) โ โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) |
63 | | simplr 528 |
. . . . . . . . . . . . . . . . . 18
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ (๐ดโ๐) < (๐ดโ(๐ + 1))) |
64 | | simprl 529 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โ0
โง (๐ด โ โ
โง 1 < ๐ด)) โ
๐ด โ
โ) |
65 | 64 | ad4antr 494 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ ๐ด โ โ) |
66 | 65 | recnd 7985 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ ๐ด โ โ) |
67 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ ๐ โ โ) |
68 | | expm1t 10547 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ดโ๐) = ((๐ดโ(๐ โ 1)) ยท ๐ด)) |
69 | 66, 67, 68 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ (๐ดโ๐) = ((๐ดโ(๐ โ 1)) ยท ๐ด)) |
70 | | simp-5l 543 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ ๐ โ โ0) |
71 | 66, 70 | expp1d 10654 |
. . . . . . . . . . . . . . . . . 18
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
72 | 63, 69, 71 | 3brtr3d 4034 |
. . . . . . . . . . . . . . . . 17
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ ((๐ดโ(๐ โ 1)) ยท ๐ด) < ((๐ดโ๐) ยท ๐ด)) |
73 | | nnm1nn0 9216 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
74 | 73 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ (๐ โ 1) โ
โ0) |
75 | 65, 74 | reexpcld 10670 |
. . . . . . . . . . . . . . . . . 18
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ (๐ดโ(๐ โ 1)) โ โ) |
76 | 65, 70 | reexpcld 10670 |
. . . . . . . . . . . . . . . . . 18
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ (๐ดโ๐) โ โ) |
77 | | 0red 7957 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โ0
โง (๐ด โ โ
โง 1 < ๐ด)) โ 0
โ โ) |
78 | | 1red 7971 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โ0
โง (๐ด โ โ
โง 1 < ๐ด)) โ 1
โ โ) |
79 | | 0lt1 8083 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 0 <
1 |
80 | 79 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โ0
โง (๐ด โ โ
โง 1 < ๐ด)) โ 0
< 1) |
81 | | simprr 531 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โ0
โง (๐ด โ โ
โง 1 < ๐ด)) โ 1
< ๐ด) |
82 | 77, 78, 64, 80, 81 | lttrd 8082 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ0
โง (๐ด โ โ
โง 1 < ๐ด)) โ 0
< ๐ด) |
83 | 64, 82 | elrpd 9692 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ0
โง (๐ด โ โ
โง 1 < ๐ด)) โ
๐ด โ
โ+) |
84 | 83 | ad4antr 494 |
. . . . . . . . . . . . . . . . . 18
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ ๐ด โ
โ+) |
85 | 75, 76, 84 | ltmul1d 9737 |
. . . . . . . . . . . . . . . . 17
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ ((๐ดโ(๐ โ 1)) < (๐ดโ๐) โ ((๐ดโ(๐ โ 1)) ยท ๐ด) < ((๐ดโ๐) ยท ๐ด))) |
86 | 72, 85 | mpbird 167 |
. . . . . . . . . . . . . . . 16
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ (๐ดโ(๐ โ 1)) < (๐ดโ๐)) |
87 | | oveq2 5882 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = (๐ โ 1) โ (๐ดโ๐) = (๐ดโ(๐ โ 1))) |
88 | 87 | breq1d 4013 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (๐ โ 1) โ ((๐ดโ๐) < (๐ดโ๐) โ (๐ดโ(๐ โ 1)) < (๐ดโ๐))) |
89 | | breq1 4006 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (๐ โ 1) โ (๐ < ๐ โ (๐ โ 1) < ๐)) |
90 | 88, 89 | imbi12d 234 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ โ 1) โ (((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐) โ ((๐ดโ(๐ โ 1)) < (๐ดโ๐) โ (๐ โ 1) < ๐))) |
91 | | simp-4r 542 |
. . . . . . . . . . . . . . . . 17
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) |
92 | 90, 91, 74 | rspcdva 2846 |
. . . . . . . . . . . . . . . 16
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ ((๐ดโ(๐ โ 1)) < (๐ดโ๐) โ (๐ โ 1) < ๐)) |
93 | 86, 92 | mpd 13 |
. . . . . . . . . . . . . . 15
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ (๐ โ 1) < ๐) |
94 | | nnz 9271 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ๐ โ
โค) |
95 | 94 | adantl 277 |
. . . . . . . . . . . . . . . 16
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ ๐ โ โค) |
96 | 70 | nn0zd 9372 |
. . . . . . . . . . . . . . . 16
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ ๐ โ โค) |
97 | | zlem1lt 9308 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โค ๐ โ (๐ โ 1) < ๐)) |
98 | 95, 96, 97 | syl2anc 411 |
. . . . . . . . . . . . . . 15
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ (๐ โค ๐ โ (๐ โ 1) < ๐)) |
99 | 93, 98 | mpbird 167 |
. . . . . . . . . . . . . 14
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ ๐ โค ๐) |
100 | | zleltp1 9307 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โค ๐ โ ๐ < (๐ + 1))) |
101 | 95, 96, 100 | syl2anc 411 |
. . . . . . . . . . . . . 14
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ (๐ โค ๐ โ ๐ < (๐ + 1))) |
102 | 99, 101 | mpbid 147 |
. . . . . . . . . . . . 13
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ โ โ) โ ๐ < (๐ + 1)) |
103 | | simpr 110 |
. . . . . . . . . . . . . 14
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ = 0) โ ๐ = 0) |
104 | | nn0p1gt0 9204 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ 0 < (๐ +
1)) |
105 | 104 | ad5antr 496 |
. . . . . . . . . . . . . 14
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ = 0) โ 0 < (๐ + 1)) |
106 | 103, 105 | eqbrtrd 4025 |
. . . . . . . . . . . . 13
โข
((((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โง ๐ = 0) โ ๐ < (๐ + 1)) |
107 | | simplr 528 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โ ๐ โ โ0) |
108 | | elnn0 9177 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
109 | 107, 108 | sylib 122 |
. . . . . . . . . . . . 13
โข
(((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โ (๐ โ โ โจ ๐ = 0)) |
110 | 102, 106,
109 | mpjaodan 798 |
. . . . . . . . . . . 12
โข
(((((๐ โ
โ0 โง (๐ด โ โ โง 1 < ๐ด)) โง โ๐ โ โ0
((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โง (๐ดโ๐) < (๐ดโ(๐ + 1))) โ ๐ < (๐ + 1)) |
111 | 110 | ex 115 |
. . . . . . . . . . 11
โข ((((๐ โ โ0
โง (๐ด โ โ
โง 1 < ๐ด)) โง
โ๐ โ
โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โง ๐ โ โ0) โ ((๐ดโ๐) < (๐ดโ(๐ + 1)) โ ๐ < (๐ + 1))) |
112 | 111 | ralrimiva 2550 |
. . . . . . . . . 10
โข (((๐ โ โ0
โง (๐ด โ โ
โง 1 < ๐ด)) โง
โ๐ โ
โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โ โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ(๐ + 1)) โ ๐ < (๐ + 1))) |
113 | 112 | ex 115 |
. . . . . . . . 9
โข ((๐ โ โ0
โง (๐ด โ โ
โง 1 < ๐ด)) โ
(โ๐ โ
โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐) โ โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ(๐ + 1)) โ ๐ < (๐ + 1)))) |
114 | 62, 113 | biimtrrid 153 |
. . . . . . . 8
โข ((๐ โ โ0
โง (๐ด โ โ
โง 1 < ๐ด)) โ
(โ๐ โ
โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐) โ โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ(๐ + 1)) โ ๐ < (๐ + 1)))) |
115 | 114 | ex 115 |
. . . . . . 7
โข (๐ โ โ0
โ ((๐ด โ โ
โง 1 < ๐ด) โ
(โ๐ โ
โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐) โ โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ(๐ + 1)) โ ๐ < (๐ + 1))))) |
116 | 115 | a2d 26 |
. . . . . 6
โข (๐ โ โ0
โ (((๐ด โ โ
โง 1 < ๐ด) โ
โ๐ โ
โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) โ ((๐ด โ โ โง 1 < ๐ด) โ โ๐ โ โ0
((๐ดโ๐) < (๐ดโ(๐ + 1)) โ ๐ < (๐ + 1))))) |
117 | 23, 29, 35, 41, 57, 116 | nn0ind 9366 |
. . . . 5
โข (๐ โ โ0
โ ((๐ด โ โ
โง 1 < ๐ด) โ
โ๐ โ
โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐))) |
118 | 117 | imp 124 |
. . . 4
โข ((๐ โ โ0
โง (๐ด โ โ
โง 1 < ๐ด)) โ
โ๐ โ
โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) |
119 | 15, 16, 17, 118 | syl12anc 1236 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โ โ๐ โ โ0 ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) |
120 | | simpl2 1001 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โ ๐ โ
โ0) |
121 | 14, 119, 120 | rspcdva 2846 |
. 2
โข (((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โ ((๐ดโ๐) < (๐ดโ๐) โ ๐ < ๐)) |
122 | 10, 121 | impbid 129 |
1
โข (((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โง 1 < ๐ด) โ (๐ < ๐ โ (๐ดโ๐) < (๐ดโ๐))) |