Step | Hyp | Ref
| Expression |
1 | | eluzelcn 12783 |
. . . . 5
โข (๐ด โ
(โคโฅโ2) โ ๐ด โ โ) |
2 | 1 | sqcld 14058 |
. . . 4
โข (๐ด โ
(โคโฅโ2) โ (๐ดโ2) โ โ) |
3 | | ax-1cn 11117 |
. . . 4
โข 1 โ
โ |
4 | | subcl 11408 |
. . . 4
โข (((๐ดโ2) โ โ โง 1
โ โ) โ ((๐ดโ2) โ 1) โ
โ) |
5 | 2, 3, 4 | sylancl 587 |
. . 3
โข (๐ด โ
(โคโฅโ2) โ ((๐ดโ2) โ 1) โ
โ) |
6 | 5 | sqrtcld 15331 |
. 2
โข (๐ด โ
(โคโฅโ2) โ (โโ((๐ดโ2) โ 1)) โ
โ) |
7 | | eluz2nn 12817 |
. . . . 5
โข (๐ด โ
(โคโฅโ2) โ ๐ด โ โ) |
8 | 7 | nnsqcld 14156 |
. . . 4
โข (๐ด โ
(โคโฅโ2) โ (๐ดโ2) โ โ) |
9 | | nnm1nn0 12462 |
. . . 4
โข ((๐ดโ2) โ โ โ
((๐ดโ2) โ 1)
โ โ0) |
10 | 8, 9 | syl 17 |
. . 3
โข (๐ด โ
(โคโฅโ2) โ ((๐ดโ2) โ 1) โ
โ0) |
11 | | nnm1nn0 12462 |
. . . 4
โข (๐ด โ โ โ (๐ด โ 1) โ
โ0) |
12 | 7, 11 | syl 17 |
. . 3
โข (๐ด โ
(โคโฅโ2) โ (๐ด โ 1) โ
โ0) |
13 | | binom2sub1 14133 |
. . . . . 6
โข (๐ด โ โ โ ((๐ด โ 1)โ2) = (((๐ดโ2) โ (2 ยท
๐ด)) + 1)) |
14 | 1, 13 | syl 17 |
. . . . 5
โข (๐ด โ
(โคโฅโ2) โ ((๐ด โ 1)โ2) = (((๐ดโ2) โ (2 ยท ๐ด)) + 1)) |
15 | | 2cnd 12239 |
. . . . . . 7
โข (๐ด โ
(โคโฅโ2) โ 2 โ โ) |
16 | 15, 1 | mulcld 11183 |
. . . . . 6
โข (๐ด โ
(โคโฅโ2) โ (2 ยท ๐ด) โ โ) |
17 | 3 | a1i 11 |
. . . . . 6
โข (๐ด โ
(โคโฅโ2) โ 1 โ โ) |
18 | 2, 16, 17 | subsubd 11548 |
. . . . 5
โข (๐ด โ
(โคโฅโ2) โ ((๐ดโ2) โ ((2 ยท ๐ด) โ 1)) = (((๐ดโ2) โ (2 ยท
๐ด)) + 1)) |
19 | 14, 18 | eqtr4d 2776 |
. . . 4
โข (๐ด โ
(โคโฅโ2) โ ((๐ด โ 1)โ2) = ((๐ดโ2) โ ((2 ยท ๐ด) โ 1))) |
20 | | 1red 11164 |
. . . . 5
โข (๐ด โ
(โคโฅโ2) โ 1 โ โ) |
21 | | 2re 12235 |
. . . . . . . 8
โข 2 โ
โ |
22 | 21 | a1i 11 |
. . . . . . 7
โข (๐ด โ
(โคโฅโ2) โ 2 โ โ) |
23 | | eluzelre 12782 |
. . . . . . 7
โข (๐ด โ
(โคโฅโ2) โ ๐ด โ โ) |
24 | 22, 23 | remulcld 11193 |
. . . . . 6
โข (๐ด โ
(โคโฅโ2) โ (2 ยท ๐ด) โ โ) |
25 | 24, 20 | resubcld 11591 |
. . . . 5
โข (๐ด โ
(โคโฅโ2) โ ((2 ยท ๐ด) โ 1) โ
โ) |
26 | 8 | nnred 12176 |
. . . . 5
โข (๐ด โ
(โคโฅโ2) โ (๐ดโ2) โ โ) |
27 | | eluz2gt1 12853 |
. . . . . . 7
โข (๐ด โ
(โคโฅโ2) โ 1 < ๐ด) |
28 | 20, 20, 23, 27, 27 | lt2addmuld 12411 |
. . . . . 6
โข (๐ด โ
(โคโฅโ2) โ (1 + 1) < (2 ยท ๐ด)) |
29 | | remulcl 11144 |
. . . . . . . 8
โข ((2
โ โ โง ๐ด
โ โ) โ (2 ยท ๐ด) โ โ) |
30 | 21, 23, 29 | sylancr 588 |
. . . . . . 7
โข (๐ด โ
(โคโฅโ2) โ (2 ยท ๐ด) โ โ) |
31 | 20, 20, 30 | ltaddsubd 11763 |
. . . . . 6
โข (๐ด โ
(โคโฅโ2) โ ((1 + 1) < (2 ยท ๐ด) โ 1 < ((2 ยท
๐ด) โ
1))) |
32 | 28, 31 | mpbid 231 |
. . . . 5
โข (๐ด โ
(โคโฅโ2) โ 1 < ((2 ยท ๐ด) โ 1)) |
33 | 20, 25, 26, 32 | ltsub2dd 11776 |
. . . 4
โข (๐ด โ
(โคโฅโ2) โ ((๐ดโ2) โ ((2 ยท ๐ด) โ 1)) < ((๐ดโ2) โ
1)) |
34 | 19, 33 | eqbrtrd 5131 |
. . 3
โข (๐ด โ
(โคโฅโ2) โ ((๐ด โ 1)โ2) < ((๐ดโ2) โ 1)) |
35 | 26 | ltm1d 12095 |
. . . 4
โข (๐ด โ
(โคโฅโ2) โ ((๐ดโ2) โ 1) < (๐ดโ2)) |
36 | | npcan 11418 |
. . . . . 6
โข ((๐ด โ โ โง 1 โ
โ) โ ((๐ด โ
1) + 1) = ๐ด) |
37 | 1, 3, 36 | sylancl 587 |
. . . . 5
โข (๐ด โ
(โคโฅโ2) โ ((๐ด โ 1) + 1) = ๐ด) |
38 | 37 | oveq1d 7376 |
. . . 4
โข (๐ด โ
(โคโฅโ2) โ (((๐ด โ 1) + 1)โ2) = (๐ดโ2)) |
39 | 35, 38 | breqtrrd 5137 |
. . 3
โข (๐ด โ
(โคโฅโ2) โ ((๐ดโ2) โ 1) < (((๐ด โ 1) +
1)โ2)) |
40 | | nonsq 16642 |
. . 3
โข
(((((๐ดโ2)
โ 1) โ โ0 โง (๐ด โ 1) โ โ0)
โง (((๐ด โ
1)โ2) < ((๐ดโ2)
โ 1) โง ((๐ดโ2) โ 1) < (((๐ด โ 1) + 1)โ2)))
โ ยฌ (โโ((๐ดโ2) โ 1)) โ
โ) |
41 | 10, 12, 34, 39, 40 | syl22anc 838 |
. 2
โข (๐ด โ
(โคโฅโ2) โ ยฌ (โโ((๐ดโ2) โ 1)) โ
โ) |
42 | 6, 41 | eldifd 3925 |
1
โข (๐ด โ
(โคโฅโ2) โ (โโ((๐ดโ2) โ 1)) โ (โ โ
โ)) |