Step | Hyp | Ref
| Expression |
1 | | eqeq1 2737 |
. . . . . 6
โข (๐ = if(๐ โ โค, ๐, 1) โ (๐ = ((๐ ยท ๐ท) + ๐) โ if(๐ โ โค, ๐, 1) = ((๐ ยท ๐ท) + ๐))) |
2 | 1 | 3anbi3d 1443 |
. . . . 5
โข (๐ = if(๐ โ โค, ๐, 1) โ ((0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ (0 โค ๐ โง ๐ < (absโ๐ท) โง if(๐ โ โค, ๐, 1) = ((๐ ยท ๐ท) + ๐)))) |
3 | 2 | rexbidv 3172 |
. . . 4
โข (๐ = if(๐ โ โค, ๐, 1) โ (โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง if(๐ โ โค, ๐, 1) = ((๐ ยท ๐ท) + ๐)))) |
4 | 3 | reubidv 3370 |
. . 3
โข (๐ = if(๐ โ โค, ๐, 1) โ (โ!๐ โ โค โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ โ!๐ โ โค โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง if(๐ โ โค, ๐, 1) = ((๐ ยท ๐ท) + ๐)))) |
5 | | fveq2 6843 |
. . . . . . 7
โข (๐ท = if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ (absโ๐ท) = (absโif((๐ท โ โค โง ๐ท โ 0), ๐ท, 1))) |
6 | 5 | breq2d 5118 |
. . . . . 6
โข (๐ท = if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ (๐ < (absโ๐ท) โ ๐ < (absโif((๐ท โ โค โง ๐ท โ 0), ๐ท, 1)))) |
7 | | oveq2 7366 |
. . . . . . . 8
โข (๐ท = if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ (๐ ยท ๐ท) = (๐ ยท if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1))) |
8 | 7 | oveq1d 7373 |
. . . . . . 7
โข (๐ท = if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ ((๐ ยท ๐ท) + ๐) = ((๐ ยท if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1)) + ๐)) |
9 | 8 | eqeq2d 2744 |
. . . . . 6
โข (๐ท = if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ (if(๐ โ โค, ๐, 1) = ((๐ ยท ๐ท) + ๐) โ if(๐ โ โค, ๐, 1) = ((๐ ยท if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1)) + ๐))) |
10 | 6, 9 | 3anbi23d 1440 |
. . . . 5
โข (๐ท = if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ ((0 โค ๐ โง ๐ < (absโ๐ท) โง if(๐ โ โค, ๐, 1) = ((๐ ยท ๐ท) + ๐)) โ (0 โค ๐ โง ๐ < (absโif((๐ท โ โค โง ๐ท โ 0), ๐ท, 1)) โง if(๐ โ โค, ๐, 1) = ((๐ ยท if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1)) + ๐)))) |
11 | 10 | rexbidv 3172 |
. . . 4
โข (๐ท = if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ (โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง if(๐ โ โค, ๐, 1) = ((๐ ยท ๐ท) + ๐)) โ โ๐ โ โค (0 โค ๐ โง ๐ < (absโif((๐ท โ โค โง ๐ท โ 0), ๐ท, 1)) โง if(๐ โ โค, ๐, 1) = ((๐ ยท if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1)) + ๐)))) |
12 | 11 | reubidv 3370 |
. . 3
โข (๐ท = if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ (โ!๐ โ โค โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง if(๐ โ โค, ๐, 1) = ((๐ ยท ๐ท) + ๐)) โ โ!๐ โ โค โ๐ โ โค (0 โค ๐ โง ๐ < (absโif((๐ท โ โค โง ๐ท โ 0), ๐ท, 1)) โง if(๐ โ โค, ๐, 1) = ((๐ ยท if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1)) + ๐)))) |
13 | | 1z 12538 |
. . . . 5
โข 1 โ
โค |
14 | 13 | elimel 4556 |
. . . 4
โข if(๐ โ โค, ๐, 1) โ
โค |
15 | | simpl 484 |
. . . . 5
โข ((๐ท โ โค โง ๐ท โ 0) โ ๐ท โ
โค) |
16 | | eleq1 2822 |
. . . . 5
โข (๐ท = if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ (๐ท โ โค โ if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ โค)) |
17 | | eleq1 2822 |
. . . . 5
โข (1 =
if((๐ท โ โค โง
๐ท โ 0), ๐ท, 1) โ (1 โ โค
โ if((๐ท โ โค
โง ๐ท โ 0), ๐ท, 1) โ
โค)) |
18 | 15, 16, 17, 13 | elimdhyp 4557 |
. . . 4
โข if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ โค |
19 | | simpr 486 |
. . . . 5
โข ((๐ท โ โค โง ๐ท โ 0) โ ๐ท โ 0) |
20 | | neeq1 3003 |
. . . . 5
โข (๐ท = if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ (๐ท โ 0 โ if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ 0)) |
21 | | neeq1 3003 |
. . . . 5
โข (1 =
if((๐ท โ โค โง
๐ท โ 0), ๐ท, 1) โ (1 โ 0 โ
if((๐ท โ โค โง
๐ท โ 0), ๐ท, 1) โ 0)) |
22 | | ax-1ne0 11125 |
. . . . 5
โข 1 โ
0 |
23 | 19, 20, 21, 22 | elimdhyp 4557 |
. . . 4
โข if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โ 0 |
24 | | eqid 2733 |
. . . 4
โข {๐ โ โ0
โฃ if((๐ท โ
โค โง ๐ท โ 0),
๐ท, 1) โฅ (if(๐ โ โค, ๐, 1) โ ๐)} = {๐ โ โ0 โฃ if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1) โฅ (if(๐ โ โค, ๐, 1) โ ๐)} |
25 | 14, 18, 23, 24 | divalglem10 16289 |
. . 3
โข
โ!๐ โ
โค โ๐ โ
โค (0 โค ๐ โง
๐ < (absโif((๐ท โ โค โง ๐ท โ 0), ๐ท, 1)) โง if(๐ โ โค, ๐, 1) = ((๐ ยท if((๐ท โ โค โง ๐ท โ 0), ๐ท, 1)) + ๐)) |
26 | 4, 12, 25 | dedth2h 4546 |
. 2
โข ((๐ โ โค โง (๐ท โ โค โง ๐ท โ 0)) โ โ!๐ โ โค โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐))) |
27 | 26 | 3impb 1116 |
1
โข ((๐ โ โค โง ๐ท โ โค โง ๐ท โ 0) โ โ!๐ โ โค โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐))) |