Step | Hyp | Ref
| Expression |
1 | | divalglem8.4 |
. . . . . . . . . . . . 13
โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} |
2 | 1 | ssrab3 4081 |
. . . . . . . . . . . 12
โข ๐ โ
โ0 |
3 | | nn0sscn 12477 |
. . . . . . . . . . . 12
โข
โ0 โ โ |
4 | 2, 3 | sstri 3992 |
. . . . . . . . . . 11
โข ๐ โ
โ |
5 | 4 | sseli 3979 |
. . . . . . . . . 10
โข (๐ โ ๐ โ ๐ โ โ) |
6 | 4 | sseli 3979 |
. . . . . . . . . 10
โข (๐ โ ๐ โ ๐ โ โ) |
7 | | divalglem8.2 |
. . . . . . . . . . . . . 14
โข ๐ท โ โค |
8 | | divalglem8.3 |
. . . . . . . . . . . . . 14
โข ๐ท โ 0 |
9 | | nnabscl 15272 |
. . . . . . . . . . . . . 14
โข ((๐ท โ โค โง ๐ท โ 0) โ (absโ๐ท) โ
โ) |
10 | 7, 8, 9 | mp2an 691 |
. . . . . . . . . . . . 13
โข
(absโ๐ท) โ
โ |
11 | 10 | nnzi 12586 |
. . . . . . . . . . . 12
โข
(absโ๐ท) โ
โค |
12 | | zmulcl 12611 |
. . . . . . . . . . . 12
โข ((๐พ โ โค โง
(absโ๐ท) โ
โค) โ (๐พ ยท
(absโ๐ท)) โ
โค) |
13 | 11, 12 | mpan2 690 |
. . . . . . . . . . 11
โข (๐พ โ โค โ (๐พ ยท (absโ๐ท)) โ
โค) |
14 | 13 | zcnd 12667 |
. . . . . . . . . 10
โข (๐พ โ โค โ (๐พ ยท (absโ๐ท)) โ
โ) |
15 | | subadd 11463 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ โง (๐พ ยท (absโ๐ท)) โ โ) โ
((๐ โ ๐) = (๐พ ยท (absโ๐ท)) โ (๐ + (๐พ ยท (absโ๐ท))) = ๐)) |
16 | 5, 6, 14, 15 | syl3an 1161 |
. . . . . . . . 9
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐พ โ โค) โ ((๐ โ ๐) = (๐พ ยท (absโ๐ท)) โ (๐ + (๐พ ยท (absโ๐ท))) = ๐)) |
17 | 16 | 3com12 1124 |
. . . . . . . 8
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐พ โ โค) โ ((๐ โ ๐) = (๐พ ยท (absโ๐ท)) โ (๐ + (๐พ ยท (absโ๐ท))) = ๐)) |
18 | | eqcom 2740 |
. . . . . . . 8
โข ((๐ โ ๐) = (๐พ ยท (absโ๐ท)) โ (๐พ ยท (absโ๐ท)) = (๐ โ ๐)) |
19 | | eqcom 2740 |
. . . . . . . 8
โข ((๐ + (๐พ ยท (absโ๐ท))) = ๐ โ ๐ = (๐ + (๐พ ยท (absโ๐ท)))) |
20 | 17, 18, 19 | 3bitr3g 313 |
. . . . . . 7
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐พ โ โค) โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = (๐ + (๐พ ยท (absโ๐ท))))) |
21 | 20 | 3adant1r 1178 |
. . . . . 6
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐ โ ๐ โง ๐พ โ โค) โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = (๐ + (๐พ ยท (absโ๐ท))))) |
22 | 21 | 3adant2r 1180 |
. . . . 5
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = (๐ + (๐พ ยท (absโ๐ท))))) |
23 | | breq1 5152 |
. . . . . . . . . . . 12
โข (๐ง = ๐ โ (๐ง < (absโ๐ท) โ ๐ < (absโ๐ท))) |
24 | | eleq1 2822 |
. . . . . . . . . . . 12
โข (๐ง = ๐ โ (๐ง โ (0...((absโ๐ท) โ 1)) โ ๐ โ (0...((absโ๐ท) โ 1)))) |
25 | 23, 24 | imbi12d 345 |
. . . . . . . . . . 11
โข (๐ง = ๐ โ ((๐ง < (absโ๐ท) โ ๐ง โ (0...((absโ๐ท) โ 1))) โ (๐ < (absโ๐ท) โ ๐ โ (0...((absโ๐ท) โ 1))))) |
26 | 2 | sseli 3979 |
. . . . . . . . . . . . . . . 16
โข (๐ง โ ๐ โ ๐ง โ โ0) |
27 | | elnn0z 12571 |
. . . . . . . . . . . . . . . 16
โข (๐ง โ โ0
โ (๐ง โ โค
โง 0 โค ๐ง)) |
28 | 26, 27 | sylib 217 |
. . . . . . . . . . . . . . 15
โข (๐ง โ ๐ โ (๐ง โ โค โง 0 โค ๐ง)) |
29 | 28 | anim1i 616 |
. . . . . . . . . . . . . 14
โข ((๐ง โ ๐ โง ๐ง < (absโ๐ท)) โ ((๐ง โ โค โง 0 โค ๐ง) โง ๐ง < (absโ๐ท))) |
30 | | df-3an 1090 |
. . . . . . . . . . . . . 14
โข ((๐ง โ โค โง 0 โค
๐ง โง ๐ง < (absโ๐ท)) โ ((๐ง โ โค โง 0 โค ๐ง) โง ๐ง < (absโ๐ท))) |
31 | 29, 30 | sylibr 233 |
. . . . . . . . . . . . 13
โข ((๐ง โ ๐ โง ๐ง < (absโ๐ท)) โ (๐ง โ โค โง 0 โค ๐ง โง ๐ง < (absโ๐ท))) |
32 | | 0z 12569 |
. . . . . . . . . . . . . 14
โข 0 โ
โค |
33 | | elfzm11 13572 |
. . . . . . . . . . . . . 14
โข ((0
โ โค โง (absโ๐ท) โ โค) โ (๐ง โ (0...((absโ๐ท) โ 1)) โ (๐ง โ โค โง 0 โค ๐ง โง ๐ง < (absโ๐ท)))) |
34 | 32, 11, 33 | mp2an 691 |
. . . . . . . . . . . . 13
โข (๐ง โ (0...((absโ๐ท) โ 1)) โ (๐ง โ โค โง 0 โค
๐ง โง ๐ง < (absโ๐ท))) |
35 | 31, 34 | sylibr 233 |
. . . . . . . . . . . 12
โข ((๐ง โ ๐ โง ๐ง < (absโ๐ท)) โ ๐ง โ (0...((absโ๐ท) โ 1))) |
36 | 35 | ex 414 |
. . . . . . . . . . 11
โข (๐ง โ ๐ โ (๐ง < (absโ๐ท) โ ๐ง โ (0...((absโ๐ท) โ 1)))) |
37 | 25, 36 | vtoclga 3566 |
. . . . . . . . . 10
โข (๐ โ ๐ โ (๐ < (absโ๐ท) โ ๐ โ (0...((absโ๐ท) โ 1)))) |
38 | | eleq1 2822 |
. . . . . . . . . . 11
โข (๐ = (๐ + (๐พ ยท (absโ๐ท))) โ (๐ โ (0...((absโ๐ท) โ 1)) โ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
39 | 38 | biimpd 228 |
. . . . . . . . . 10
โข (๐ = (๐ + (๐พ ยท (absโ๐ท))) โ (๐ โ (0...((absโ๐ท) โ 1)) โ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
40 | 37, 39 | sylan9 509 |
. . . . . . . . 9
โข ((๐ โ ๐ โง ๐ = (๐ + (๐พ ยท (absโ๐ท)))) โ (๐ < (absโ๐ท) โ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
41 | 40 | impancom 453 |
. . . . . . . 8
โข ((๐ โ ๐ โง ๐ < (absโ๐ท)) โ (๐ = (๐ + (๐พ ยท (absโ๐ท))) โ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
42 | 41 | 3ad2ant2 1135 |
. . . . . . 7
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ (๐ = (๐ + (๐พ ยท (absโ๐ท))) โ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
43 | | breq1 5152 |
. . . . . . . . . . . . 13
โข (๐ง = ๐ โ (๐ง < (absโ๐ท) โ ๐ < (absโ๐ท))) |
44 | | eleq1 2822 |
. . . . . . . . . . . . 13
โข (๐ง = ๐ โ (๐ง โ (0...((absโ๐ท) โ 1)) โ ๐ โ (0...((absโ๐ท) โ 1)))) |
45 | 43, 44 | imbi12d 345 |
. . . . . . . . . . . 12
โข (๐ง = ๐ โ ((๐ง < (absโ๐ท) โ ๐ง โ (0...((absโ๐ท) โ 1))) โ (๐ < (absโ๐ท) โ ๐ โ (0...((absโ๐ท) โ 1))))) |
46 | 45, 36 | vtoclga 3566 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (๐ < (absโ๐ท) โ ๐ โ (0...((absโ๐ท) โ 1)))) |
47 | 46 | imp 408 |
. . . . . . . . . 10
โข ((๐ โ ๐ โง ๐ < (absโ๐ท)) โ ๐ โ (0...((absโ๐ท) โ 1))) |
48 | 7, 8 | divalglem7 16342 |
. . . . . . . . . 10
โข ((๐ โ (0...((absโ๐ท) โ 1)) โง ๐พ โ โค) โ (๐พ โ 0 โ ยฌ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
49 | 47, 48 | sylan 581 |
. . . . . . . . 9
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ (๐พ โ 0 โ ยฌ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
50 | 49 | 3adant2 1132 |
. . . . . . . 8
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ (๐พ โ 0 โ ยฌ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
51 | 50 | con2d 134 |
. . . . . . 7
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ ((๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)) โ ยฌ ๐พ โ 0)) |
52 | 42, 51 | syld 47 |
. . . . . 6
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ (๐ = (๐ + (๐พ ยท (absโ๐ท))) โ ยฌ ๐พ โ 0)) |
53 | | df-ne 2942 |
. . . . . . 7
โข (๐พ โ 0 โ ยฌ ๐พ = 0) |
54 | 53 | con2bii 358 |
. . . . . 6
โข (๐พ = 0 โ ยฌ ๐พ โ 0) |
55 | 52, 54 | syl6ibr 252 |
. . . . 5
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ (๐ = (๐ + (๐พ ยท (absโ๐ท))) โ ๐พ = 0)) |
56 | 22, 55 | sylbid 239 |
. . . 4
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐พ = 0)) |
57 | | oveq1 7416 |
. . . . . . . . . . 11
โข (๐พ = 0 โ (๐พ ยท (absโ๐ท)) = (0 ยท (absโ๐ท))) |
58 | 10 | nncni 12222 |
. . . . . . . . . . . 12
โข
(absโ๐ท) โ
โ |
59 | 58 | mul02i 11403 |
. . . . . . . . . . 11
โข (0
ยท (absโ๐ท)) =
0 |
60 | 57, 59 | eqtrdi 2789 |
. . . . . . . . . 10
โข (๐พ = 0 โ (๐พ ยท (absโ๐ท)) = 0) |
61 | 60 | eqeq1d 2735 |
. . . . . . . . 9
โข (๐พ = 0 โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ 0 = (๐ โ ๐))) |
62 | 61 | biimpac 480 |
. . . . . . . 8
โข (((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โง ๐พ = 0) โ 0 = (๐ โ ๐)) |
63 | | subeq0 11486 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ โ ๐) = 0 โ ๐ = ๐)) |
64 | 5, 6, 63 | syl2anr 598 |
. . . . . . . . 9
โข ((๐ โ ๐ โง ๐ โ ๐) โ ((๐ โ ๐) = 0 โ ๐ = ๐)) |
65 | | eqcom 2740 |
. . . . . . . . 9
โข ((๐ โ ๐) = 0 โ 0 = (๐ โ ๐)) |
66 | | eqcom 2740 |
. . . . . . . . 9
โข (๐ = ๐ โ ๐ = ๐) |
67 | 64, 65, 66 | 3bitr3g 313 |
. . . . . . . 8
โข ((๐ โ ๐ โง ๐ โ ๐) โ (0 = (๐ โ ๐) โ ๐ = ๐)) |
68 | 62, 67 | imbitrid 243 |
. . . . . . 7
โข ((๐ โ ๐ โง ๐ โ ๐) โ (((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โง ๐พ = 0) โ ๐ = ๐)) |
69 | 68 | ad2ant2r 746 |
. . . . . 6
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท))) โ (((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โง ๐พ = 0) โ ๐ = ๐)) |
70 | 69 | 3adant3 1133 |
. . . . 5
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ (((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โง ๐พ = 0) โ ๐ = ๐)) |
71 | 70 | expd 417 |
. . . 4
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ (๐พ = 0 โ ๐ = ๐))) |
72 | 56, 71 | mpdd 43 |
. . 3
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = ๐)) |
73 | 72 | 3expia 1122 |
. 2
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท))) โ (๐พ โ โค โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = ๐))) |
74 | 73 | an4s 659 |
1
โข (((๐ โ ๐ โง ๐ โ ๐) โง (๐ < (absโ๐ท) โง ๐ < (absโ๐ท))) โ (๐พ โ โค โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = ๐))) |