Step | Hyp | Ref
| Expression |
1 | | divalglem8.4 |
. . . . . . . . . . . . 13
โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} |
2 | 1 | ssrab3 4079 |
. . . . . . . . . . . 12
โข ๐ โ
โ0 |
3 | | nn0sscn 12481 |
. . . . . . . . . . . 12
โข
โ0 โ โ |
4 | 2, 3 | sstri 3990 |
. . . . . . . . . . 11
โข ๐ โ
โ |
5 | 4 | sseli 3977 |
. . . . . . . . . 10
โข (๐ โ ๐ โ ๐ โ โ) |
6 | 4 | sseli 3977 |
. . . . . . . . . 10
โข (๐ โ ๐ โ ๐ โ โ) |
7 | | divalglem8.2 |
. . . . . . . . . . . . . 14
โข ๐ท โ โค |
8 | | divalglem8.3 |
. . . . . . . . . . . . . 14
โข ๐ท โ 0 |
9 | | nnabscl 15276 |
. . . . . . . . . . . . . 14
โข ((๐ท โ โค โง ๐ท โ 0) โ (absโ๐ท) โ
โ) |
10 | 7, 8, 9 | mp2an 688 |
. . . . . . . . . . . . 13
โข
(absโ๐ท) โ
โ |
11 | 10 | nnzi 12590 |
. . . . . . . . . . . 12
โข
(absโ๐ท) โ
โค |
12 | | zmulcl 12615 |
. . . . . . . . . . . 12
โข ((๐พ โ โค โง
(absโ๐ท) โ
โค) โ (๐พ ยท
(absโ๐ท)) โ
โค) |
13 | 11, 12 | mpan2 687 |
. . . . . . . . . . 11
โข (๐พ โ โค โ (๐พ ยท (absโ๐ท)) โ
โค) |
14 | 13 | zcnd 12671 |
. . . . . . . . . 10
โข (๐พ โ โค โ (๐พ ยท (absโ๐ท)) โ
โ) |
15 | | subadd 11467 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ โง (๐พ ยท (absโ๐ท)) โ โ) โ
((๐ โ ๐) = (๐พ ยท (absโ๐ท)) โ (๐ + (๐พ ยท (absโ๐ท))) = ๐)) |
16 | 5, 6, 14, 15 | syl3an 1158 |
. . . . . . . . 9
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐พ โ โค) โ ((๐ โ ๐) = (๐พ ยท (absโ๐ท)) โ (๐ + (๐พ ยท (absโ๐ท))) = ๐)) |
17 | 16 | 3com12 1121 |
. . . . . . . 8
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐พ โ โค) โ ((๐ โ ๐) = (๐พ ยท (absโ๐ท)) โ (๐ + (๐พ ยท (absโ๐ท))) = ๐)) |
18 | | eqcom 2737 |
. . . . . . . 8
โข ((๐ โ ๐) = (๐พ ยท (absโ๐ท)) โ (๐พ ยท (absโ๐ท)) = (๐ โ ๐)) |
19 | | eqcom 2737 |
. . . . . . . 8
โข ((๐ + (๐พ ยท (absโ๐ท))) = ๐ โ ๐ = (๐ + (๐พ ยท (absโ๐ท)))) |
20 | 17, 18, 19 | 3bitr3g 312 |
. . . . . . 7
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐พ โ โค) โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = (๐ + (๐พ ยท (absโ๐ท))))) |
21 | 20 | 3adant1r 1175 |
. . . . . 6
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐ โ ๐ โง ๐พ โ โค) โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = (๐ + (๐พ ยท (absโ๐ท))))) |
22 | 21 | 3adant2r 1177 |
. . . . 5
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = (๐ + (๐พ ยท (absโ๐ท))))) |
23 | | breq1 5150 |
. . . . . . . . . . . 12
โข (๐ง = ๐ โ (๐ง < (absโ๐ท) โ ๐ < (absโ๐ท))) |
24 | | eleq1 2819 |
. . . . . . . . . . . 12
โข (๐ง = ๐ โ (๐ง โ (0...((absโ๐ท) โ 1)) โ ๐ โ (0...((absโ๐ท) โ 1)))) |
25 | 23, 24 | imbi12d 343 |
. . . . . . . . . . 11
โข (๐ง = ๐ โ ((๐ง < (absโ๐ท) โ ๐ง โ (0...((absโ๐ท) โ 1))) โ (๐ < (absโ๐ท) โ ๐ โ (0...((absโ๐ท) โ 1))))) |
26 | 2 | sseli 3977 |
. . . . . . . . . . . . . . . 16
โข (๐ง โ ๐ โ ๐ง โ โ0) |
27 | | elnn0z 12575 |
. . . . . . . . . . . . . . . 16
โข (๐ง โ โ0
โ (๐ง โ โค
โง 0 โค ๐ง)) |
28 | 26, 27 | sylib 217 |
. . . . . . . . . . . . . . 15
โข (๐ง โ ๐ โ (๐ง โ โค โง 0 โค ๐ง)) |
29 | 28 | anim1i 613 |
. . . . . . . . . . . . . 14
โข ((๐ง โ ๐ โง ๐ง < (absโ๐ท)) โ ((๐ง โ โค โง 0 โค ๐ง) โง ๐ง < (absโ๐ท))) |
30 | | df-3an 1087 |
. . . . . . . . . . . . . 14
โข ((๐ง โ โค โง 0 โค
๐ง โง ๐ง < (absโ๐ท)) โ ((๐ง โ โค โง 0 โค ๐ง) โง ๐ง < (absโ๐ท))) |
31 | 29, 30 | sylibr 233 |
. . . . . . . . . . . . 13
โข ((๐ง โ ๐ โง ๐ง < (absโ๐ท)) โ (๐ง โ โค โง 0 โค ๐ง โง ๐ง < (absโ๐ท))) |
32 | | 0z 12573 |
. . . . . . . . . . . . . 14
โข 0 โ
โค |
33 | | elfzm11 13576 |
. . . . . . . . . . . . . 14
โข ((0
โ โค โง (absโ๐ท) โ โค) โ (๐ง โ (0...((absโ๐ท) โ 1)) โ (๐ง โ โค โง 0 โค ๐ง โง ๐ง < (absโ๐ท)))) |
34 | 32, 11, 33 | mp2an 688 |
. . . . . . . . . . . . 13
โข (๐ง โ (0...((absโ๐ท) โ 1)) โ (๐ง โ โค โง 0 โค
๐ง โง ๐ง < (absโ๐ท))) |
35 | 31, 34 | sylibr 233 |
. . . . . . . . . . . 12
โข ((๐ง โ ๐ โง ๐ง < (absโ๐ท)) โ ๐ง โ (0...((absโ๐ท) โ 1))) |
36 | 35 | ex 411 |
. . . . . . . . . . 11
โข (๐ง โ ๐ โ (๐ง < (absโ๐ท) โ ๐ง โ (0...((absโ๐ท) โ 1)))) |
37 | 25, 36 | vtoclga 3565 |
. . . . . . . . . 10
โข (๐ โ ๐ โ (๐ < (absโ๐ท) โ ๐ โ (0...((absโ๐ท) โ 1)))) |
38 | | eleq1 2819 |
. . . . . . . . . . 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 506 |
. . . . . . . . 9
โข ((๐ โ ๐ โง ๐ = (๐ + (๐พ ยท (absโ๐ท)))) โ (๐ < (absโ๐ท) โ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
41 | 40 | impancom 450 |
. . . . . . . 8
โข ((๐ โ ๐ โง ๐ < (absโ๐ท)) โ (๐ = (๐ + (๐พ ยท (absโ๐ท))) โ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
42 | 41 | 3ad2ant2 1132 |
. . . . . . 7
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ (๐ = (๐ + (๐พ ยท (absโ๐ท))) โ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
43 | | breq1 5150 |
. . . . . . . . . . . . 13
โข (๐ง = ๐ โ (๐ง < (absโ๐ท) โ ๐ < (absโ๐ท))) |
44 | | eleq1 2819 |
. . . . . . . . . . . . 13
โข (๐ง = ๐ โ (๐ง โ (0...((absโ๐ท) โ 1)) โ ๐ โ (0...((absโ๐ท) โ 1)))) |
45 | 43, 44 | imbi12d 343 |
. . . . . . . . . . . 12
โข (๐ง = ๐ โ ((๐ง < (absโ๐ท) โ ๐ง โ (0...((absโ๐ท) โ 1))) โ (๐ < (absโ๐ท) โ ๐ โ (0...((absโ๐ท) โ 1))))) |
46 | 45, 36 | vtoclga 3565 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (๐ < (absโ๐ท) โ ๐ โ (0...((absโ๐ท) โ 1)))) |
47 | 46 | imp 405 |
. . . . . . . . . 10
โข ((๐ โ ๐ โง ๐ < (absโ๐ท)) โ ๐ โ (0...((absโ๐ท) โ 1))) |
48 | 7, 8 | divalglem7 16346 |
. . . . . . . . . 10
โข ((๐ โ (0...((absโ๐ท) โ 1)) โง ๐พ โ โค) โ (๐พ โ 0 โ ยฌ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
49 | 47, 48 | sylan 578 |
. . . . . . . . 9
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ (๐พ โ 0 โ ยฌ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
50 | 49 | 3adant2 1129 |
. . . . . . . 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 2939 |
. . . . . . 7
โข (๐พ โ 0 โ ยฌ ๐พ = 0) |
54 | 53 | con2bii 356 |
. . . . . 6
โข (๐พ = 0 โ ยฌ ๐พ โ 0) |
55 | 52, 54 | imbitrrdi 251 |
. . . . 5
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ (๐ = (๐ + (๐พ ยท (absโ๐ท))) โ ๐พ = 0)) |
56 | 22, 55 | sylbid 239 |
. . . 4
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐พ = 0)) |
57 | | oveq1 7418 |
. . . . . . . . . . 11
โข (๐พ = 0 โ (๐พ ยท (absโ๐ท)) = (0 ยท (absโ๐ท))) |
58 | 10 | nncni 12226 |
. . . . . . . . . . . 12
โข
(absโ๐ท) โ
โ |
59 | 58 | mul02i 11407 |
. . . . . . . . . . 11
โข (0
ยท (absโ๐ท)) =
0 |
60 | 57, 59 | eqtrdi 2786 |
. . . . . . . . . 10
โข (๐พ = 0 โ (๐พ ยท (absโ๐ท)) = 0) |
61 | 60 | eqeq1d 2732 |
. . . . . . . . 9
โข (๐พ = 0 โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ 0 = (๐ โ ๐))) |
62 | 61 | biimpac 477 |
. . . . . . . 8
โข (((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โง ๐พ = 0) โ 0 = (๐ โ ๐)) |
63 | | subeq0 11490 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ โ ๐) = 0 โ ๐ = ๐)) |
64 | 5, 6, 63 | syl2anr 595 |
. . . . . . . . 9
โข ((๐ โ ๐ โง ๐ โ ๐) โ ((๐ โ ๐) = 0 โ ๐ = ๐)) |
65 | | eqcom 2737 |
. . . . . . . . 9
โข ((๐ โ ๐) = 0 โ 0 = (๐ โ ๐)) |
66 | | eqcom 2737 |
. . . . . . . . 9
โข (๐ = ๐ โ ๐ = ๐) |
67 | 64, 65, 66 | 3bitr3g 312 |
. . . . . . . 8
โข ((๐ โ ๐ โง ๐ โ ๐) โ (0 = (๐ โ ๐) โ ๐ = ๐)) |
68 | 62, 67 | imbitrid 243 |
. . . . . . 7
โข ((๐ โ ๐ โง ๐ โ ๐) โ (((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โง ๐พ = 0) โ ๐ = ๐)) |
69 | 68 | ad2ant2r 743 |
. . . . . 6
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท))) โ (((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โง ๐พ = 0) โ ๐ = ๐)) |
70 | 69 | 3adant3 1130 |
. . . . 5
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ (((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โง ๐พ = 0) โ ๐ = ๐)) |
71 | 70 | expd 414 |
. . . 4
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ (๐พ = 0 โ ๐ = ๐))) |
72 | 56, 71 | mpdd 43 |
. . 3
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท)) โง ๐พ โ โค) โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = ๐)) |
73 | 72 | 3expia 1119 |
. 2
โข (((๐ โ ๐ โง ๐ < (absโ๐ท)) โง (๐ โ ๐ โง ๐ < (absโ๐ท))) โ (๐พ โ โค โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = ๐))) |
74 | 73 | an4s 656 |
1
โข (((๐ โ ๐ โง ๐ โ ๐) โง (๐ < (absโ๐ท) โง ๐ < (absโ๐ท))) โ (๐พ โ โค โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = ๐))) |