Step | Hyp | Ref
| Expression |
1 | | df-3an 1090 |
. . . . . . . . 9
โข ((0 โค
๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ ((0 โค ๐ โง ๐ < (absโ๐ท)) โง ๐ = ((๐ ยท ๐ท) + ๐))) |
2 | 1 | rexbii 3094 |
. . . . . . . 8
โข
(โ๐ โ
โค (0 โค ๐ โง
๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ โ๐ โ โค ((0 โค ๐ โง ๐ < (absโ๐ท)) โง ๐ = ((๐ ยท ๐ท) + ๐))) |
3 | | r19.42v 3184 |
. . . . . . . 8
โข
(โ๐ โ
โค ((0 โค ๐ โง
๐ < (absโ๐ท)) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ ((0 โค ๐ โง ๐ < (absโ๐ท)) โง โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐))) |
4 | 2, 3 | bitri 275 |
. . . . . . 7
โข
(โ๐ โ
โค (0 โค ๐ โง
๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ ((0 โค ๐ โง ๐ < (absโ๐ท)) โง โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐))) |
5 | | zsubcl 12550 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โ ๐) โ โค) |
6 | | divides 16143 |
. . . . . . . . . . . 12
โข ((๐ท โ โค โง (๐ โ ๐) โ โค) โ (๐ท โฅ (๐ โ ๐) โ โ๐ โ โค (๐ ยท ๐ท) = (๐ โ ๐))) |
7 | 5, 6 | sylan2 594 |
. . . . . . . . . . 11
โข ((๐ท โ โค โง (๐ โ โค โง ๐ โ โค)) โ (๐ท โฅ (๐ โ ๐) โ โ๐ โ โค (๐ ยท ๐ท) = (๐ โ ๐))) |
8 | 7 | 3impb 1116 |
. . . . . . . . . 10
โข ((๐ท โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ท โฅ (๐ โ ๐) โ โ๐ โ โค (๐ ยท ๐ท) = (๐ โ ๐))) |
9 | 8 | 3com12 1124 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ท โ โค โง ๐ โ โค) โ (๐ท โฅ (๐ โ ๐) โ โ๐ โ โค (๐ ยท ๐ท) = (๐ โ ๐))) |
10 | | zcn 12509 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ ๐ โ
โ) |
11 | | zcn 12509 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ ๐ โ
โ) |
12 | | zmulcl 12557 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐ท โ โค) โ (๐ ยท ๐ท) โ โค) |
13 | 12 | zcnd 12613 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ท โ โค) โ (๐ ยท ๐ท) โ โ) |
14 | | subadd 11409 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ โง (๐ ยท ๐ท) โ โ) โ ((๐ โ ๐) = (๐ ยท ๐ท) โ (๐ + (๐ ยท ๐ท)) = ๐)) |
15 | 10, 11, 13, 14 | syl3an 1161 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐ โ โค โง (๐ โ โค โง ๐ท โ โค)) โ ((๐ โ ๐) = (๐ ยท ๐ท) โ (๐ + (๐ ยท ๐ท)) = ๐)) |
16 | | addcom 11346 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง (๐ ยท ๐ท) โ โ) โ (๐ + (๐ ยท ๐ท)) = ((๐ ยท ๐ท) + ๐)) |
17 | 11, 13, 16 | syl2an 597 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง (๐ โ โค โง ๐ท โ โค)) โ (๐ + (๐ ยท ๐ท)) = ((๐ ยท ๐ท) + ๐)) |
18 | 17 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ โ โค โง (๐ โ โค โง ๐ท โ โค)) โ (๐ + (๐ ยท ๐ท)) = ((๐ ยท ๐ท) + ๐)) |
19 | 18 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐ โ โค โง (๐ โ โค โง ๐ท โ โค)) โ ((๐ + (๐ ยท ๐ท)) = ๐ โ ((๐ ยท ๐ท) + ๐) = ๐)) |
20 | 15, 19 | bitrd 279 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ๐ โ โค โง (๐ โ โค โง ๐ท โ โค)) โ ((๐ โ ๐) = (๐ ยท ๐ท) โ ((๐ ยท ๐ท) + ๐) = ๐)) |
21 | | eqcom 2740 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ ๐) = (๐ ยท ๐ท) โ (๐ ยท ๐ท) = (๐ โ ๐)) |
22 | | eqcom 2740 |
. . . . . . . . . . . . . . . 16
โข (((๐ ยท ๐ท) + ๐) = ๐ โ ๐ = ((๐ ยท ๐ท) + ๐)) |
23 | 20, 21, 22 | 3bitr3g 313 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ๐ โ โค โง (๐ โ โค โง ๐ท โ โค)) โ ((๐ ยท ๐ท) = (๐ โ ๐) โ ๐ = ((๐ ยท ๐ท) + ๐))) |
24 | 23 | 3expia 1122 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ โ โค โง ๐ท โ โค) โ ((๐ ยท ๐ท) = (๐ โ ๐) โ ๐ = ((๐ ยท ๐ท) + ๐)))) |
25 | 24 | expcomd 418 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ (๐ท โ โค โ (๐ โ โค โ ((๐ ยท ๐ท) = (๐ โ ๐) โ ๐ = ((๐ ยท ๐ท) + ๐))))) |
26 | 25 | 3impia 1118 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค โง ๐ท โ โค) โ (๐ โ โค โ ((๐ ยท ๐ท) = (๐ โ ๐) โ ๐ = ((๐ ยท ๐ท) + ๐)))) |
27 | 26 | imp 408 |
. . . . . . . . . . 11
โข (((๐ โ โค โง ๐ โ โค โง ๐ท โ โค) โง ๐ โ โค) โ ((๐ ยท ๐ท) = (๐ โ ๐) โ ๐ = ((๐ ยท ๐ท) + ๐))) |
28 | 27 | rexbidva 3170 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ท โ โค) โ
(โ๐ โ โค
(๐ ยท ๐ท) = (๐ โ ๐) โ โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐))) |
29 | 28 | 3com23 1127 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ท โ โค โง ๐ โ โค) โ
(โ๐ โ โค
(๐ ยท ๐ท) = (๐ โ ๐) โ โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐))) |
30 | 9, 29 | bitrd 279 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ท โ โค โง ๐ โ โค) โ (๐ท โฅ (๐ โ ๐) โ โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐))) |
31 | 30 | anbi2d 630 |
. . . . . . 7
โข ((๐ โ โค โง ๐ท โ โค โง ๐ โ โค) โ (((0
โค ๐ โง ๐ < (absโ๐ท)) โง ๐ท โฅ (๐ โ ๐)) โ ((0 โค ๐ โง ๐ < (absโ๐ท)) โง โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐)))) |
32 | 4, 31 | bitr4id 290 |
. . . . . 6
โข ((๐ โ โค โง ๐ท โ โค โง ๐ โ โค) โ
(โ๐ โ โค (0
โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ ((0 โค ๐ โง ๐ < (absโ๐ท)) โง ๐ท โฅ (๐ โ ๐)))) |
33 | | anass 470 |
. . . . . 6
โข (((0 โค
๐ โง ๐ < (absโ๐ท)) โง ๐ท โฅ (๐ โ ๐)) โ (0 โค ๐ โง (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐)))) |
34 | 32, 33 | bitrdi 287 |
. . . . 5
โข ((๐ โ โค โง ๐ท โ โค โง ๐ โ โค) โ
(โ๐ โ โค (0
โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ (0 โค ๐ โง (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐))))) |
35 | 34 | 3expa 1119 |
. . . 4
โข (((๐ โ โค โง ๐ท โ โค) โง ๐ โ โค) โ
(โ๐ โ โค (0
โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ (0 โค ๐ โง (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐))))) |
36 | 35 | reubidva 3368 |
. . 3
โข ((๐ โ โค โง ๐ท โ โค) โ
(โ!๐ โ โค
โ๐ โ โค (0
โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ โ!๐ โ โค (0 โค ๐ โง (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐))))) |
37 | | elnn0z 12517 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ โ โค
โง 0 โค ๐)) |
38 | 37 | anbi1i 625 |
. . . . . 6
โข ((๐ โ โ0
โง (๐ <
(absโ๐ท) โง ๐ท โฅ (๐ โ ๐))) โ ((๐ โ โค โง 0 โค ๐) โง (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐)))) |
39 | | anass 470 |
. . . . . 6
โข (((๐ โ โค โง 0 โค
๐) โง (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐))) โ (๐ โ โค โง (0 โค ๐ โง (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐))))) |
40 | 38, 39 | bitri 275 |
. . . . 5
โข ((๐ โ โ0
โง (๐ <
(absโ๐ท) โง ๐ท โฅ (๐ โ ๐))) โ (๐ โ โค โง (0 โค ๐ โง (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐))))) |
41 | 40 | eubii 2580 |
. . . 4
โข
(โ!๐(๐ โ โ0
โง (๐ <
(absโ๐ท) โง ๐ท โฅ (๐ โ ๐))) โ โ!๐(๐ โ โค โง (0 โค ๐ โง (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐))))) |
42 | | df-reu 3353 |
. . . 4
โข
(โ!๐ โ
โ0 (๐ <
(absโ๐ท) โง ๐ท โฅ (๐ โ ๐)) โ โ!๐(๐ โ โ0 โง (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐)))) |
43 | | df-reu 3353 |
. . . 4
โข
(โ!๐ โ
โค (0 โค ๐ โง
(๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐))) โ โ!๐(๐ โ โค โง (0 โค ๐ โง (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐))))) |
44 | 41, 42, 43 | 3bitr4ri 304 |
. . 3
โข
(โ!๐ โ
โค (0 โค ๐ โง
(๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐))) โ โ!๐ โ โ0 (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐))) |
45 | 36, 44 | bitrdi 287 |
. 2
โข ((๐ โ โค โง ๐ท โ โค) โ
(โ!๐ โ โค
โ๐ โ โค (0
โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ โ!๐ โ โ0 (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐)))) |
46 | 45 | 3adant3 1133 |
1
โข ((๐ โ โค โง ๐ท โ โค โง ๐ท โ 0) โ (โ!๐ โ โค โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ โ!๐ โ โ0 (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐)))) |