Step | Hyp | Ref
| Expression |
1 | | jm3.1.b |
. . . 4
โข (๐ โ ๐พ โ
(โคโฅโ2)) |
2 | | eluzelre 12779 |
. . . 4
โข (๐พ โ
(โคโฅโ2) โ ๐พ โ โ) |
3 | 1, 2 | syl 17 |
. . 3
โข (๐ โ ๐พ โ โ) |
4 | | jm3.1.c |
. . . 4
โข (๐ โ ๐ โ โ) |
5 | 4 | nnnn0d 12478 |
. . 3
โข (๐ โ ๐ โ
โ0) |
6 | 3, 5 | reexpcld 14074 |
. 2
โข (๐ โ (๐พโ๐) โ โ) |
7 | | jm3.1.a |
. . 3
โข (๐ โ ๐ด โ
(โคโฅโ2)) |
8 | | eluzelre 12779 |
. . 3
โข (๐ด โ
(โคโฅโ2) โ ๐ด โ โ) |
9 | 7, 8 | syl 17 |
. 2
โข (๐ โ ๐ด โ โ) |
10 | | 2re 12232 |
. . . . . 6
โข 2 โ
โ |
11 | | remulcl 11141 |
. . . . . 6
โข ((2
โ โ โง ๐ด
โ โ) โ (2 ยท ๐ด) โ โ) |
12 | 10, 9, 11 | sylancr 588 |
. . . . 5
โข (๐ โ (2 ยท ๐ด) โ
โ) |
13 | 12, 3 | remulcld 11190 |
. . . 4
โข (๐ โ ((2 ยท ๐ด) ยท ๐พ) โ โ) |
14 | 3 | resqcld 14036 |
. . . 4
โข (๐ โ (๐พโ2) โ โ) |
15 | 13, 14 | resubcld 11588 |
. . 3
โข (๐ โ (((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ โ) |
16 | | 1re 11160 |
. . 3
โข 1 โ
โ |
17 | | resubcl 11470 |
. . 3
โข (((((2
ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ โ โง 1 โ
โ) โ ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1) โ
โ) |
18 | 15, 16, 17 | sylancl 587 |
. 2
โข (๐ โ ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1) โ
โ) |
19 | | jm3.1.d |
. . 3
โข (๐ โ (๐พ Yrm (๐ + 1)) โค ๐ด) |
20 | 7, 1, 4, 19 | jm3.1lem1 41384 |
. 2
โข (๐ โ (๐พโ๐) < ๐ด) |
21 | 9, 3 | remulcld 11190 |
. . . 4
โข (๐ โ (๐ด ยท ๐พ) โ โ) |
22 | | resubcl 11470 |
. . . . 5
โข ((๐พ โ โ โง 1 โ
โ) โ (๐พ โ
1) โ โ) |
23 | 3, 16, 22 | sylancl 587 |
. . . 4
โข (๐ โ (๐พ โ 1) โ โ) |
24 | 21, 23 | readdcld 11189 |
. . 3
โข (๐ โ ((๐ด ยท ๐พ) + (๐พ โ 1)) โ
โ) |
25 | | eluz2b1 12849 |
. . . . . . 7
โข (๐พ โ
(โคโฅโ2) โ (๐พ โ โค โง 1 < ๐พ)) |
26 | 25 | simprbi 498 |
. . . . . 6
โข (๐พ โ
(โคโฅโ2) โ 1 < ๐พ) |
27 | 1, 26 | syl 17 |
. . . . 5
โข (๐ โ 1 < ๐พ) |
28 | | eluz2nn 12814 |
. . . . . . . 8
โข (๐ด โ
(โคโฅโ2) โ ๐ด โ โ) |
29 | 7, 28 | syl 17 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
30 | 29 | nngt0d 12207 |
. . . . . 6
โข (๐ โ 0 < ๐ด) |
31 | | ltmulgt11 12020 |
. . . . . 6
โข ((๐ด โ โ โง ๐พ โ โ โง 0 <
๐ด) โ (1 < ๐พ โ ๐ด < (๐ด ยท ๐พ))) |
32 | 9, 3, 30, 31 | syl3anc 1372 |
. . . . 5
โข (๐ โ (1 < ๐พ โ ๐ด < (๐ด ยท ๐พ))) |
33 | 27, 32 | mpbid 231 |
. . . 4
โข (๐ โ ๐ด < (๐ด ยท ๐พ)) |
34 | | uz2m1nn 12853 |
. . . . . . 7
โข (๐พ โ
(โคโฅโ2) โ (๐พ โ 1) โ โ) |
35 | 1, 34 | syl 17 |
. . . . . 6
โข (๐ โ (๐พ โ 1) โ โ) |
36 | 35 | nnrpd 12960 |
. . . . 5
โข (๐ โ (๐พ โ 1) โ
โ+) |
37 | 21, 36 | ltaddrpd 12995 |
. . . 4
โข (๐ โ (๐ด ยท ๐พ) < ((๐ด ยท ๐พ) + (๐พ โ 1))) |
38 | 9, 21, 24, 33, 37 | lttrd 11321 |
. . 3
โข (๐ โ ๐ด < ((๐ด ยท ๐พ) + (๐พ โ 1))) |
39 | | peano2re 11333 |
. . . . . . 7
โข (๐พ โ โ โ (๐พ + 1) โ
โ) |
40 | 3, 39 | syl 17 |
. . . . . 6
โข (๐ โ (๐พ + 1) โ โ) |
41 | 40, 3 | remulcld 11190 |
. . . . 5
โข (๐ โ ((๐พ + 1) ยท ๐พ) โ โ) |
42 | | resubcl 11470 |
. . . . . . 7
โข (((๐ด ยท ๐พ) โ โ โง 1 โ โ)
โ ((๐ด ยท ๐พ) โ 1) โ
โ) |
43 | 21, 16, 42 | sylancl 587 |
. . . . . 6
โข (๐ โ ((๐ด ยท ๐พ) โ 1) โ
โ) |
44 | 43, 14 | resubcld 11588 |
. . . . 5
โข (๐ โ (((๐ด ยท ๐พ) โ 1) โ (๐พโ2)) โ โ) |
45 | 3 | recnd 11188 |
. . . . . . . . . 10
โข (๐ โ ๐พ โ โ) |
46 | 45 | exp1d 14052 |
. . . . . . . . 9
โข (๐ โ (๐พโ1) = ๐พ) |
47 | | eluz2nn 12814 |
. . . . . . . . . . . 12
โข (๐พ โ
(โคโฅโ2) โ ๐พ โ โ) |
48 | 1, 47 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐พ โ โ) |
49 | 48 | nnge1d 12206 |
. . . . . . . . . 10
โข (๐ โ 1 โค ๐พ) |
50 | | nnuz 12811 |
. . . . . . . . . . 11
โข โ =
(โคโฅโ1) |
51 | 4, 50 | eleqtrdi 2844 |
. . . . . . . . . 10
โข (๐ โ ๐ โ
(โคโฅโ1)) |
52 | 3, 49, 51 | leexp2ad 14163 |
. . . . . . . . 9
โข (๐ โ (๐พโ1) โค (๐พโ๐)) |
53 | 46, 52 | eqbrtrrd 5130 |
. . . . . . . 8
โข (๐ โ ๐พ โค (๐พโ๐)) |
54 | 3, 6, 9, 53, 20 | lelttrd 11318 |
. . . . . . 7
โข (๐ โ ๐พ < ๐ด) |
55 | | eluzelz 12778 |
. . . . . . . . 9
โข (๐พ โ
(โคโฅโ2) โ ๐พ โ โค) |
56 | 1, 55 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐พ โ โค) |
57 | | eluzelz 12778 |
. . . . . . . . 9
โข (๐ด โ
(โคโฅโ2) โ ๐ด โ โค) |
58 | 7, 57 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ด โ โค) |
59 | | zltp1le 12558 |
. . . . . . . 8
โข ((๐พ โ โค โง ๐ด โ โค) โ (๐พ < ๐ด โ (๐พ + 1) โค ๐ด)) |
60 | 56, 58, 59 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (๐พ < ๐ด โ (๐พ + 1) โค ๐ด)) |
61 | 54, 60 | mpbid 231 |
. . . . . 6
โข (๐ โ (๐พ + 1) โค ๐ด) |
62 | 48 | nngt0d 12207 |
. . . . . . 7
โข (๐ โ 0 < ๐พ) |
63 | | lemul1 12012 |
. . . . . . 7
โข (((๐พ + 1) โ โ โง ๐ด โ โ โง (๐พ โ โ โง 0 <
๐พ)) โ ((๐พ + 1) โค ๐ด โ ((๐พ + 1) ยท ๐พ) โค (๐ด ยท ๐พ))) |
64 | 40, 9, 3, 62, 63 | syl112anc 1375 |
. . . . . 6
โข (๐ โ ((๐พ + 1) โค ๐ด โ ((๐พ + 1) ยท ๐พ) โค (๐ด ยท ๐พ))) |
65 | 61, 64 | mpbid 231 |
. . . . 5
โข (๐ โ ((๐พ + 1) ยท ๐พ) โค (๐ด ยท ๐พ)) |
66 | 41, 21, 44, 65 | leadd1dd 11774 |
. . . 4
โข (๐ โ (((๐พ + 1) ยท ๐พ) + (((๐ด ยท ๐พ) โ 1) โ (๐พโ2))) โค ((๐ด ยท ๐พ) + (((๐ด ยท ๐พ) โ 1) โ (๐พโ2)))) |
67 | 21 | recnd 11188 |
. . . . . 6
โข (๐ โ (๐ด ยท ๐พ) โ โ) |
68 | 41, 14 | resubcld 11588 |
. . . . . . 7
โข (๐ โ (((๐พ + 1) ยท ๐พ) โ (๐พโ2)) โ โ) |
69 | 68 | recnd 11188 |
. . . . . 6
โข (๐ โ (((๐พ + 1) ยท ๐พ) โ (๐พโ2)) โ โ) |
70 | | 1cnd 11155 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
71 | 67, 69, 70 | addsub12d 11540 |
. . . . 5
โข (๐ โ ((๐ด ยท ๐พ) + ((((๐พ + 1) ยท ๐พ) โ (๐พโ2)) โ 1)) = ((((๐พ + 1) ยท ๐พ) โ (๐พโ2)) + ((๐ด ยท ๐พ) โ 1))) |
72 | 45, 70, 45 | adddird 11185 |
. . . . . . . . 9
โข (๐ โ ((๐พ + 1) ยท ๐พ) = ((๐พ ยท ๐พ) + (1 ยท ๐พ))) |
73 | 45 | sqvald 14054 |
. . . . . . . . 9
โข (๐ โ (๐พโ2) = (๐พ ยท ๐พ)) |
74 | 72, 73 | oveq12d 7376 |
. . . . . . . 8
โข (๐ โ (((๐พ + 1) ยท ๐พ) โ (๐พโ2)) = (((๐พ ยท ๐พ) + (1 ยท ๐พ)) โ (๐พ ยท ๐พ))) |
75 | 45, 45 | mulcld 11180 |
. . . . . . . . 9
โข (๐ โ (๐พ ยท ๐พ) โ โ) |
76 | | ax-1cn 11114 |
. . . . . . . . . 10
โข 1 โ
โ |
77 | | mulcl 11140 |
. . . . . . . . . 10
โข ((1
โ โ โง ๐พ
โ โ) โ (1 ยท ๐พ) โ โ) |
78 | 76, 45, 77 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ (1 ยท ๐พ) โ
โ) |
79 | 75, 78 | pncan2d 11519 |
. . . . . . . 8
โข (๐ โ (((๐พ ยท ๐พ) + (1 ยท ๐พ)) โ (๐พ ยท ๐พ)) = (1 ยท ๐พ)) |
80 | 45 | mulid2d 11178 |
. . . . . . . 8
โข (๐ โ (1 ยท ๐พ) = ๐พ) |
81 | 74, 79, 80 | 3eqtrd 2777 |
. . . . . . 7
โข (๐ โ (((๐พ + 1) ยท ๐พ) โ (๐พโ2)) = ๐พ) |
82 | 81 | oveq1d 7373 |
. . . . . 6
โข (๐ โ ((((๐พ + 1) ยท ๐พ) โ (๐พโ2)) โ 1) = (๐พ โ 1)) |
83 | 82 | oveq2d 7374 |
. . . . 5
โข (๐ โ ((๐ด ยท ๐พ) + ((((๐พ + 1) ยท ๐พ) โ (๐พโ2)) โ 1)) = ((๐ด ยท ๐พ) + (๐พ โ 1))) |
84 | 41 | recnd 11188 |
. . . . . 6
โข (๐ โ ((๐พ + 1) ยท ๐พ) โ โ) |
85 | 14 | recnd 11188 |
. . . . . 6
โข (๐ โ (๐พโ2) โ โ) |
86 | 43 | recnd 11188 |
. . . . . 6
โข (๐ โ ((๐ด ยท ๐พ) โ 1) โ
โ) |
87 | 84, 85, 86 | subadd23d 11539 |
. . . . 5
โข (๐ โ ((((๐พ + 1) ยท ๐พ) โ (๐พโ2)) + ((๐ด ยท ๐พ) โ 1)) = (((๐พ + 1) ยท ๐พ) + (((๐ด ยท ๐พ) โ 1) โ (๐พโ2)))) |
88 | 71, 83, 87 | 3eqtr3d 2781 |
. . . 4
โข (๐ โ ((๐ด ยท ๐พ) + (๐พ โ 1)) = (((๐พ + 1) ยท ๐พ) + (((๐ด ยท ๐พ) โ 1) โ (๐พโ2)))) |
89 | | 2cnd 12236 |
. . . . . . . . 9
โข (๐ โ 2 โ
โ) |
90 | 9 | recnd 11188 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
91 | 89, 90, 45 | mulassd 11183 |
. . . . . . . 8
โข (๐ โ ((2 ยท ๐ด) ยท ๐พ) = (2 ยท (๐ด ยท ๐พ))) |
92 | 67 | 2timesd 12401 |
. . . . . . . 8
โข (๐ โ (2 ยท (๐ด ยท ๐พ)) = ((๐ด ยท ๐พ) + (๐ด ยท ๐พ))) |
93 | 91, 92 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ ((2 ยท ๐ด) ยท ๐พ) = ((๐ด ยท ๐พ) + (๐ด ยท ๐พ))) |
94 | 93 | oveq1d 7373 |
. . . . . 6
โข (๐ โ (((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) = (((๐ด ยท ๐พ) + (๐ด ยท ๐พ)) โ (๐พโ2))) |
95 | 94 | oveq1d 7373 |
. . . . 5
โข (๐ โ ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1) = ((((๐ด ยท ๐พ) + (๐ด ยท ๐พ)) โ (๐พโ2)) โ 1)) |
96 | 21, 21 | readdcld 11189 |
. . . . . . 7
โข (๐ โ ((๐ด ยท ๐พ) + (๐ด ยท ๐พ)) โ โ) |
97 | 96 | recnd 11188 |
. . . . . 6
โข (๐ โ ((๐ด ยท ๐พ) + (๐ด ยท ๐พ)) โ โ) |
98 | 97, 85, 70 | sub32d 11549 |
. . . . 5
โข (๐ โ ((((๐ด ยท ๐พ) + (๐ด ยท ๐พ)) โ (๐พโ2)) โ 1) = ((((๐ด ยท ๐พ) + (๐ด ยท ๐พ)) โ 1) โ (๐พโ2))) |
99 | 67, 67, 70 | addsubassd 11537 |
. . . . . . 7
โข (๐ โ (((๐ด ยท ๐พ) + (๐ด ยท ๐พ)) โ 1) = ((๐ด ยท ๐พ) + ((๐ด ยท ๐พ) โ 1))) |
100 | 99 | oveq1d 7373 |
. . . . . 6
โข (๐ โ ((((๐ด ยท ๐พ) + (๐ด ยท ๐พ)) โ 1) โ (๐พโ2)) = (((๐ด ยท ๐พ) + ((๐ด ยท ๐พ) โ 1)) โ (๐พโ2))) |
101 | 67, 86, 85 | addsubassd 11537 |
. . . . . 6
โข (๐ โ (((๐ด ยท ๐พ) + ((๐ด ยท ๐พ) โ 1)) โ (๐พโ2)) = ((๐ด ยท ๐พ) + (((๐ด ยท ๐พ) โ 1) โ (๐พโ2)))) |
102 | 100, 101 | eqtrd 2773 |
. . . . 5
โข (๐ โ ((((๐ด ยท ๐พ) + (๐ด ยท ๐พ)) โ 1) โ (๐พโ2)) = ((๐ด ยท ๐พ) + (((๐ด ยท ๐พ) โ 1) โ (๐พโ2)))) |
103 | 95, 98, 102 | 3eqtrd 2777 |
. . . 4
โข (๐ โ ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1) = ((๐ด ยท ๐พ) + (((๐ด ยท ๐พ) โ 1) โ (๐พโ2)))) |
104 | 66, 88, 103 | 3brtr4d 5138 |
. . 3
โข (๐ โ ((๐ด ยท ๐พ) + (๐พ โ 1)) โค ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1)) |
105 | 9, 24, 18, 38, 104 | ltletrd 11320 |
. 2
โข (๐ โ ๐ด < ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1)) |
106 | 6, 9, 18, 20, 105 | lttrd 11321 |
1
โข (๐ โ (๐พโ๐) < ((((2 ยท ๐ด) ยท ๐พ) โ (๐พโ2)) โ 1)) |