Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . 3
โข (((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โง ๐ด โ โ) โ ๐ด โ
โ) |
2 | | simpl2 1193 |
. . 3
โข (((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โง ๐ด โ โ) โ ๐ต โ
โ) |
3 | | simpl3 1194 |
. . 3
โข (((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โง ๐ด โ โ) โ 2 โค
๐ต) |
4 | | id 22 |
. . . . . . 7
โข (๐ = 1 โ ๐ = 1) |
5 | | oveq2 7417 |
. . . . . . 7
โข (๐ = 1 โ (๐ตโ๐) = (๐ตโ1)) |
6 | 4, 5 | breq12d 5162 |
. . . . . 6
โข (๐ = 1 โ (๐ โค (๐ตโ๐) โ 1 โค (๐ตโ1))) |
7 | 6 | imbi2d 341 |
. . . . 5
โข (๐ = 1 โ (((๐ต โ โ โง 2 โค ๐ต) โ ๐ โค (๐ตโ๐)) โ ((๐ต โ โ โง 2 โค ๐ต) โ 1 โค (๐ตโ1)))) |
8 | | id 22 |
. . . . . . 7
โข (๐ = ๐ โ ๐ = ๐) |
9 | | oveq2 7417 |
. . . . . . 7
โข (๐ = ๐ โ (๐ตโ๐) = (๐ตโ๐)) |
10 | 8, 9 | breq12d 5162 |
. . . . . 6
โข (๐ = ๐ โ (๐ โค (๐ตโ๐) โ ๐ โค (๐ตโ๐))) |
11 | 10 | imbi2d 341 |
. . . . 5
โข (๐ = ๐ โ (((๐ต โ โ โง 2 โค ๐ต) โ ๐ โค (๐ตโ๐)) โ ((๐ต โ โ โง 2 โค ๐ต) โ ๐ โค (๐ตโ๐)))) |
12 | | id 22 |
. . . . . . 7
โข (๐ = (๐ + 1) โ ๐ = (๐ + 1)) |
13 | | oveq2 7417 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐ตโ๐) = (๐ตโ(๐ + 1))) |
14 | 12, 13 | breq12d 5162 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ โค (๐ตโ๐) โ (๐ + 1) โค (๐ตโ(๐ + 1)))) |
15 | 14 | imbi2d 341 |
. . . . 5
โข (๐ = (๐ + 1) โ (((๐ต โ โ โง 2 โค ๐ต) โ ๐ โค (๐ตโ๐)) โ ((๐ต โ โ โง 2 โค ๐ต) โ (๐ + 1) โค (๐ตโ(๐ + 1))))) |
16 | | id 22 |
. . . . . . 7
โข (๐ = ๐ด โ ๐ = ๐ด) |
17 | | oveq2 7417 |
. . . . . . 7
โข (๐ = ๐ด โ (๐ตโ๐) = (๐ตโ๐ด)) |
18 | 16, 17 | breq12d 5162 |
. . . . . 6
โข (๐ = ๐ด โ (๐ โค (๐ตโ๐) โ ๐ด โค (๐ตโ๐ด))) |
19 | 18 | imbi2d 341 |
. . . . 5
โข (๐ = ๐ด โ (((๐ต โ โ โง 2 โค ๐ต) โ ๐ โค (๐ตโ๐)) โ ((๐ต โ โ โง 2 โค ๐ต) โ ๐ด โค (๐ตโ๐ด)))) |
20 | | simpl 484 |
. . . . . 6
โข ((๐ต โ โ โง 2 โค
๐ต) โ ๐ต โ โ) |
21 | | 1nn0 12488 |
. . . . . . 7
โข 1 โ
โ0 |
22 | 21 | a1i 11 |
. . . . . 6
โข ((๐ต โ โ โง 2 โค
๐ต) โ 1 โ
โ0) |
23 | | 1red 11215 |
. . . . . . 7
โข ((๐ต โ โ โง 2 โค
๐ต) โ 1 โ
โ) |
24 | | 2re 12286 |
. . . . . . . 8
โข 2 โ
โ |
25 | 24 | a1i 11 |
. . . . . . 7
โข ((๐ต โ โ โง 2 โค
๐ต) โ 2 โ
โ) |
26 | | 1le2 12421 |
. . . . . . . 8
โข 1 โค
2 |
27 | 26 | a1i 11 |
. . . . . . 7
โข ((๐ต โ โ โง 2 โค
๐ต) โ 1 โค
2) |
28 | | simpr 486 |
. . . . . . 7
โข ((๐ต โ โ โง 2 โค
๐ต) โ 2 โค ๐ต) |
29 | 23, 25, 20, 27, 28 | letrd 11371 |
. . . . . 6
โข ((๐ต โ โ โง 2 โค
๐ต) โ 1 โค ๐ต) |
30 | 20, 22, 29 | expge1d 14130 |
. . . . 5
โข ((๐ต โ โ โง 2 โค
๐ต) โ 1 โค (๐ตโ1)) |
31 | | simp1 1137 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ ๐ โ โ) |
32 | 31 | nnnn0d 12532 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ ๐ โ โ0) |
33 | 32 | nn0red 12533 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ ๐ โ โ) |
34 | | 1red 11215 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ 1 โ โ) |
35 | 33, 34 | readdcld 11243 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ + 1) โ โ) |
36 | 20 | 3ad2ant2 1135 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ ๐ต โ โ) |
37 | 33, 36 | remulcld 11244 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ ยท ๐ต) โ โ) |
38 | 36, 32 | reexpcld 14128 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ตโ๐) โ โ) |
39 | 38, 36 | remulcld 11244 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ ((๐ตโ๐) ยท ๐ต) โ โ) |
40 | 24 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ 2 โ โ) |
41 | 33, 40 | remulcld 11244 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ ยท 2) โ โ) |
42 | 31 | nnge1d 12260 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ 1 โค ๐) |
43 | 34, 33, 33, 42 | leadd2dd 11829 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ + 1) โค (๐ + ๐)) |
44 | 33 | recnd 11242 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ ๐ โ โ) |
45 | 44 | times2d 12456 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ ยท 2) = (๐ + ๐)) |
46 | 43, 45 | breqtrrd 5177 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ + 1) โค (๐ ยท 2)) |
47 | 32 | nn0ge0d 12535 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ 0 โค ๐) |
48 | | simp2r 1201 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ 2 โค ๐ต) |
49 | 40, 36, 33, 47, 48 | lemul2ad 12154 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ ยท 2) โค (๐ ยท ๐ต)) |
50 | 35, 41, 37, 46, 49 | letrd 11371 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ + 1) โค (๐ ยท ๐ต)) |
51 | | 0red 11217 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง 2 โค
๐ต) โ 0 โ
โ) |
52 | | 0le2 12314 |
. . . . . . . . . . . . 13
โข 0 โค
2 |
53 | 52 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง 2 โค
๐ต) โ 0 โค
2) |
54 | 51, 25, 20, 53, 28 | letrd 11371 |
. . . . . . . . . . 11
โข ((๐ต โ โ โง 2 โค
๐ต) โ 0 โค ๐ต) |
55 | 54 | 3ad2ant2 1135 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ 0 โค ๐ต) |
56 | | simp3 1139 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ ๐ โค (๐ตโ๐)) |
57 | 33, 38, 36, 55, 56 | lemul1ad 12153 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ ยท ๐ต) โค ((๐ตโ๐) ยท ๐ต)) |
58 | 35, 37, 39, 50, 57 | letrd 11371 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ + 1) โค ((๐ตโ๐) ยท ๐ต)) |
59 | 36 | recnd 11242 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ ๐ต โ โ) |
60 | 59, 32 | expp1d 14112 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ตโ(๐ + 1)) = ((๐ตโ๐) ยท ๐ต)) |
61 | 58, 60 | breqtrrd 5177 |
. . . . . . 7
โข ((๐ โ โ โง (๐ต โ โ โง 2 โค
๐ต) โง ๐ โค (๐ตโ๐)) โ (๐ + 1) โค (๐ตโ(๐ + 1))) |
62 | 61 | 3exp 1120 |
. . . . . 6
โข (๐ โ โ โ ((๐ต โ โ โง 2 โค
๐ต) โ (๐ โค (๐ตโ๐) โ (๐ + 1) โค (๐ตโ(๐ + 1))))) |
63 | 62 | a2d 29 |
. . . . 5
โข (๐ โ โ โ (((๐ต โ โ โง 2 โค
๐ต) โ ๐ โค (๐ตโ๐)) โ ((๐ต โ โ โง 2 โค ๐ต) โ (๐ + 1) โค (๐ตโ(๐ + 1))))) |
64 | 7, 11, 15, 19, 30, 63 | nnind 12230 |
. . . 4
โข (๐ด โ โ โ ((๐ต โ โ โง 2 โค
๐ต) โ ๐ด โค (๐ตโ๐ด))) |
65 | 64 | 3impib 1117 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง 2 โค
๐ต) โ ๐ด โค (๐ตโ๐ด)) |
66 | 1, 2, 3, 65 | syl3anc 1372 |
. 2
โข (((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โง ๐ด โ โ) โ ๐ด โค (๐ตโ๐ด)) |
67 | | 0le1 11737 |
. . . 4
โข 0 โค
1 |
68 | 67 | a1i 11 |
. . 3
โข (((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โง ๐ด = 0) โ 0 โค
1) |
69 | | simpr 486 |
. . 3
โข (((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โง ๐ด = 0) โ ๐ด = 0) |
70 | 69 | oveq2d 7425 |
. . . 4
โข (((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โง ๐ด = 0) โ (๐ตโ๐ด) = (๐ตโ0)) |
71 | | simpl2 1193 |
. . . . . 6
โข (((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โง ๐ด = 0) โ ๐ต โ โ) |
72 | 71 | recnd 11242 |
. . . . 5
โข (((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โง ๐ด = 0) โ ๐ต โ โ) |
73 | 72 | exp0d 14105 |
. . . 4
โข (((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โง ๐ด = 0) โ (๐ตโ0) = 1) |
74 | 70, 73 | eqtrd 2773 |
. . 3
โข (((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โง ๐ด = 0) โ (๐ตโ๐ด) = 1) |
75 | 68, 69, 74 | 3brtr4d 5181 |
. 2
โข (((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โง ๐ด = 0) โ ๐ด โค (๐ตโ๐ด)) |
76 | | elnn0 12474 |
. . . 4
โข (๐ด โ โ0
โ (๐ด โ โ
โจ ๐ด =
0)) |
77 | 76 | biimpi 215 |
. . 3
โข (๐ด โ โ0
โ (๐ด โ โ
โจ ๐ด =
0)) |
78 | 77 | 3ad2ant1 1134 |
. 2
โข ((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โ
(๐ด โ โ โจ
๐ด = 0)) |
79 | 66, 75, 78 | mpjaodan 958 |
1
โข ((๐ด โ โ0
โง ๐ต โ โ
โง 2 โค ๐ต) โ
๐ด โค (๐ตโ๐ด)) |