Step | Hyp | Ref
| Expression |
1 | | peano2nn0 12458 |
. . . . 5
โข (๐พ โ โ0
โ (๐พ + 1) โ
โ0) |
2 | | vdwapval 16850 |
. . . . 5
โข (((๐พ + 1) โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ฅ โ (๐ด(APโ(๐พ + 1))๐ท) โ โ๐ โ (0...((๐พ + 1) โ 1))๐ฅ = (๐ด + (๐ ยท ๐ท)))) |
3 | 1, 2 | syl3an1 1164 |
. . . 4
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ฅ โ (๐ด(APโ(๐พ + 1))๐ท) โ โ๐ โ (0...((๐พ + 1) โ 1))๐ฅ = (๐ด + (๐ ยท ๐ท)))) |
4 | | simp1 1137 |
. . . . . . . . . . . . 13
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ ๐พ โ
โ0) |
5 | 4 | nn0cnd 12480 |
. . . . . . . . . . . 12
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ ๐พ โ
โ) |
6 | | ax-1cn 11114 |
. . . . . . . . . . . 12
โข 1 โ
โ |
7 | | pncan 11412 |
. . . . . . . . . . . 12
โข ((๐พ โ โ โง 1 โ
โ) โ ((๐พ + 1)
โ 1) = ๐พ) |
8 | 5, 6, 7 | sylancl 587 |
. . . . . . . . . . 11
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ ((๐พ + 1) โ 1)
= ๐พ) |
9 | 8 | oveq2d 7374 |
. . . . . . . . . 10
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (0...((๐พ + 1)
โ 1)) = (0...๐พ)) |
10 | 9 | eleq2d 2820 |
. . . . . . . . 9
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ โ
(0...((๐พ + 1) โ 1))
โ ๐ โ (0...๐พ))) |
11 | | nn0uz 12810 |
. . . . . . . . . . 11
โข
โ0 = (โคโฅโ0) |
12 | 4, 11 | eleqtrdi 2844 |
. . . . . . . . . 10
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ ๐พ โ
(โคโฅโ0)) |
13 | | elfzp12 13526 |
. . . . . . . . . 10
โข (๐พ โ
(โคโฅโ0) โ (๐ โ (0...๐พ) โ (๐ = 0 โจ ๐ โ ((0 + 1)...๐พ)))) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ โ (0...๐พ) โ (๐ = 0 โจ ๐ โ ((0 + 1)...๐พ)))) |
15 | 10, 14 | bitrd 279 |
. . . . . . . 8
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ โ
(0...((๐พ + 1) โ 1))
โ (๐ = 0 โจ ๐ โ ((0 + 1)...๐พ)))) |
16 | 15 | anbi1d 631 |
. . . . . . 7
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ ((๐ โ
(0...((๐พ + 1) โ 1))
โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โ ((๐ = 0 โจ ๐ โ ((0 + 1)...๐พ)) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))))) |
17 | | andir 1008 |
. . . . . . 7
โข (((๐ = 0 โจ ๐ โ ((0 + 1)...๐พ)) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โ ((๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โจ (๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))))) |
18 | 16, 17 | bitrdi 287 |
. . . . . 6
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ ((๐ โ
(0...((๐พ + 1) โ 1))
โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โ ((๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โจ (๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท)))))) |
19 | 18 | exbidv 1925 |
. . . . 5
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (โ๐(๐ โ (0...((๐พ + 1) โ 1)) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โ โ๐((๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โจ (๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท)))))) |
20 | | df-rex 3071 |
. . . . 5
โข
(โ๐ โ
(0...((๐พ + 1) โ
1))๐ฅ = (๐ด + (๐ ยท ๐ท)) โ โ๐(๐ โ (0...((๐พ + 1) โ 1)) โง ๐ฅ = (๐ด + (๐ ยท ๐ท)))) |
21 | | 19.43 1886 |
. . . . . 6
โข
(โ๐((๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โจ (๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท)))) โ (โ๐(๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โจ โ๐(๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))))) |
22 | 21 | bicomi 223 |
. . . . 5
โข
((โ๐(๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โจ โ๐(๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท)))) โ โ๐((๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โจ (๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))))) |
23 | 19, 20, 22 | 3bitr4g 314 |
. . . 4
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (โ๐ โ
(0...((๐พ + 1) โ
1))๐ฅ = (๐ด + (๐ ยท ๐ท)) โ (โ๐(๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โจ โ๐(๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท)))))) |
24 | 3, 23 | bitrd 279 |
. . 3
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ฅ โ (๐ด(APโ(๐พ + 1))๐ท) โ (โ๐(๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โจ โ๐(๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท)))))) |
25 | | nncn 12166 |
. . . . . . . . . . 11
โข (๐ท โ โ โ ๐ท โ
โ) |
26 | 25 | 3ad2ant3 1136 |
. . . . . . . . . 10
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ ๐ท โ
โ) |
27 | 26 | mul02d 11358 |
. . . . . . . . 9
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (0 ยท ๐ท) =
0) |
28 | 27 | oveq2d 7374 |
. . . . . . . 8
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ด + (0 ยท
๐ท)) = (๐ด + 0)) |
29 | | nncn 12166 |
. . . . . . . . . 10
โข (๐ด โ โ โ ๐ด โ
โ) |
30 | 29 | 3ad2ant2 1135 |
. . . . . . . . 9
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ ๐ด โ
โ) |
31 | 30 | addid1d 11360 |
. . . . . . . 8
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ด + 0) = ๐ด) |
32 | 28, 31 | eqtrd 2773 |
. . . . . . 7
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ด + (0 ยท
๐ท)) = ๐ด) |
33 | 32 | eqeq2d 2744 |
. . . . . 6
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ฅ = (๐ด + (0 ยท ๐ท)) โ ๐ฅ = ๐ด)) |
34 | | c0ex 11154 |
. . . . . . 7
โข 0 โ
V |
35 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ ยท ๐ท) = (0 ยท ๐ท)) |
36 | 35 | oveq2d 7374 |
. . . . . . . 8
โข (๐ = 0 โ (๐ด + (๐ ยท ๐ท)) = (๐ด + (0 ยท ๐ท))) |
37 | 36 | eqeq2d 2744 |
. . . . . . 7
โข (๐ = 0 โ (๐ฅ = (๐ด + (๐ ยท ๐ท)) โ ๐ฅ = (๐ด + (0 ยท ๐ท)))) |
38 | 34, 37 | ceqsexv 3493 |
. . . . . 6
โข
(โ๐(๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โ ๐ฅ = (๐ด + (0 ยท ๐ท))) |
39 | | velsn 4603 |
. . . . . 6
โข (๐ฅ โ {๐ด} โ ๐ฅ = ๐ด) |
40 | 33, 38, 39 | 3bitr4g 314 |
. . . . 5
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (โ๐(๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โ ๐ฅ โ {๐ด})) |
41 | | simpr 486 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ๐ โ ((0 + 1)...๐พ)) |
42 | | 0p1e1 12280 |
. . . . . . . . . . . . . . 15
โข (0 + 1) =
1 |
43 | 42 | oveq1i 7368 |
. . . . . . . . . . . . . 14
โข ((0 +
1)...๐พ) = (1...๐พ) |
44 | 41, 43 | eleqtrdi 2844 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ๐ โ (1...๐พ)) |
45 | | 1zzd 12539 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ 1 โ
โค) |
46 | 4 | adantr 482 |
. . . . . . . . . . . . . . 15
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ๐พ โ
โ0) |
47 | 46 | nn0zd 12530 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ๐พ โ
โค) |
48 | | elfzelz 13447 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((0 + 1)...๐พ) โ ๐ โ โค) |
49 | 48 | adantl 483 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ๐ โ
โค) |
50 | | fzsubel 13483 |
. . . . . . . . . . . . . 14
โข (((1
โ โค โง ๐พ
โ โค) โง (๐
โ โค โง 1 โ โค)) โ (๐ โ (1...๐พ) โ (๐ โ 1) โ ((1 โ 1)...(๐พ โ 1)))) |
51 | 45, 47, 49, 45, 50 | syl22anc 838 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ (๐ โ (1...๐พ) โ (๐ โ 1) โ ((1 โ 1)...(๐พ โ 1)))) |
52 | 44, 51 | mpbid 231 |
. . . . . . . . . . . 12
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ (๐ โ 1) โ ((1 โ
1)...(๐พ โ
1))) |
53 | | 1m1e0 12230 |
. . . . . . . . . . . . 13
โข (1
โ 1) = 0 |
54 | 53 | oveq1i 7368 |
. . . . . . . . . . . 12
โข ((1
โ 1)...(๐พ โ 1))
= (0...(๐พ โ
1)) |
55 | 52, 54 | eleqtrdi 2844 |
. . . . . . . . . . 11
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ (๐ โ 1) โ (0...(๐พ โ 1))) |
56 | 49 | zcnd 12613 |
. . . . . . . . . . . . . . . . 17
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ๐ โ
โ) |
57 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . 17
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ 1 โ
โ) |
58 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ๐ท โ
โ) |
59 | 56, 57, 58 | subdird 11617 |
. . . . . . . . . . . . . . . 16
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ((๐ โ 1) ยท ๐ท) = ((๐ ยท ๐ท) โ (1 ยท ๐ท))) |
60 | 58 | mulid2d 11178 |
. . . . . . . . . . . . . . . . 17
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ (1 ยท
๐ท) = ๐ท) |
61 | 60 | oveq2d 7374 |
. . . . . . . . . . . . . . . 16
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ((๐ ยท ๐ท) โ (1 ยท ๐ท)) = ((๐ ยท ๐ท) โ ๐ท)) |
62 | 59, 61 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ((๐ โ 1) ยท ๐ท) = ((๐ ยท ๐ท) โ ๐ท)) |
63 | 62 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ (๐ท + ((๐ โ 1) ยท ๐ท)) = (๐ท + ((๐ ยท ๐ท) โ ๐ท))) |
64 | 56, 58 | mulcld 11180 |
. . . . . . . . . . . . . . 15
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ (๐ ยท ๐ท) โ โ) |
65 | 58, 64 | pncan3d 11520 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ (๐ท + ((๐ ยท ๐ท) โ ๐ท)) = (๐ ยท ๐ท)) |
66 | 63, 65 | eqtr2d 2774 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ (๐ ยท ๐ท) = (๐ท + ((๐ โ 1) ยท ๐ท))) |
67 | 66 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ (๐ด + (๐ ยท ๐ท)) = (๐ด + (๐ท + ((๐ โ 1) ยท ๐ท)))) |
68 | 30 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ๐ด โ
โ) |
69 | | subcl 11405 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
1) โ โ) |
70 | 56, 6, 69 | sylancl 587 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ (๐ โ 1) โ
โ) |
71 | 70, 58 | mulcld 11180 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ((๐ โ 1) ยท ๐ท) โ
โ) |
72 | 68, 58, 71 | addassd 11182 |
. . . . . . . . . . . 12
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ ((๐ด + ๐ท) + ((๐ โ 1) ยท ๐ท)) = (๐ด + (๐ท + ((๐ โ 1) ยท ๐ท)))) |
73 | 67, 72 | eqtr4d 2776 |
. . . . . . . . . . 11
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ (๐ด + (๐ ยท ๐ท)) = ((๐ด + ๐ท) + ((๐ โ 1) ยท ๐ท))) |
74 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ = (๐ โ 1) โ (๐ ยท ๐ท) = ((๐ โ 1) ยท ๐ท)) |
75 | 74 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ = (๐ โ 1) โ ((๐ด + ๐ท) + (๐ ยท ๐ท)) = ((๐ด + ๐ท) + ((๐ โ 1) ยท ๐ท))) |
76 | 75 | rspceeqv 3596 |
. . . . . . . . . . 11
โข (((๐ โ 1) โ (0...(๐พ โ 1)) โง (๐ด + (๐ ยท ๐ท)) = ((๐ด + ๐ท) + ((๐ โ 1) ยท ๐ท))) โ โ๐ โ (0...(๐พ โ 1))(๐ด + (๐ ยท ๐ท)) = ((๐ด + ๐ท) + (๐ ยท ๐ท))) |
77 | 55, 73, 76 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ
โ๐ โ (0...(๐พ โ 1))(๐ด + (๐ ยท ๐ท)) = ((๐ด + ๐ท) + (๐ ยท ๐ท))) |
78 | | eqeq1 2737 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ด + (๐ ยท ๐ท)) โ (๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)) โ (๐ด + (๐ ยท ๐ท)) = ((๐ด + ๐ท) + (๐ ยท ๐ท)))) |
79 | 78 | rexbidv 3172 |
. . . . . . . . . 10
โข (๐ฅ = (๐ด + (๐ ยท ๐ท)) โ (โ๐ โ (0...(๐พ โ 1))๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)) โ โ๐ โ (0...(๐พ โ 1))(๐ด + (๐ ยท ๐ท)) = ((๐ด + ๐ท) + (๐ ยท ๐ท)))) |
80 | 77, 79 | syl5ibrcom 247 |
. . . . . . . . 9
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ ((0 +
1)...๐พ)) โ (๐ฅ = (๐ด + (๐ ยท ๐ท)) โ โ๐ โ (0...(๐พ โ 1))๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)))) |
81 | 80 | expimpd 455 |
. . . . . . . 8
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ ((๐ โ ((0 +
1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โ โ๐ โ (0...(๐พ โ 1))๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)))) |
82 | 81 | exlimdv 1937 |
. . . . . . 7
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (โ๐(๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โ โ๐ โ (0...(๐พ โ 1))๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)))) |
83 | | simpr 486 |
. . . . . . . . . . . 12
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ๐ โ (0...(๐พ โ 1))) |
84 | | 0zd 12516 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ 0 โ
โค) |
85 | 4 | adantr 482 |
. . . . . . . . . . . . . . 15
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ๐พ โ
โ0) |
86 | 85 | nn0zd 12530 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ๐พ โ
โค) |
87 | | peano2zm 12551 |
. . . . . . . . . . . . . 14
โข (๐พ โ โค โ (๐พ โ 1) โ
โค) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ (๐พ โ 1) โ
โค) |
89 | | elfzelz 13447 |
. . . . . . . . . . . . . 14
โข (๐ โ (0...(๐พ โ 1)) โ ๐ โ โค) |
90 | 89 | adantl 483 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ๐ โ
โค) |
91 | | 1zzd 12539 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ 1 โ
โค) |
92 | | fzaddel 13481 |
. . . . . . . . . . . . 13
โข (((0
โ โค โง (๐พ
โ 1) โ โค) โง (๐ โ โค โง 1 โ โค))
โ (๐ โ
(0...(๐พ โ 1)) โ
(๐ + 1) โ ((0 +
1)...((๐พ โ 1) +
1)))) |
93 | 84, 88, 90, 91, 92 | syl22anc 838 |
. . . . . . . . . . . 12
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ (๐ โ (0...(๐พ โ 1)) โ (๐ + 1) โ ((0 + 1)...((๐พ โ 1) + 1)))) |
94 | 83, 93 | mpbid 231 |
. . . . . . . . . . 11
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ (๐ + 1) โ ((0 + 1)...((๐พ โ 1) +
1))) |
95 | 85 | nn0cnd 12480 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ๐พ โ
โ) |
96 | | npcan 11415 |
. . . . . . . . . . . . 13
โข ((๐พ โ โ โง 1 โ
โ) โ ((๐พ โ
1) + 1) = ๐พ) |
97 | 95, 6, 96 | sylancl 587 |
. . . . . . . . . . . 12
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ((๐พ โ 1) + 1) = ๐พ) |
98 | 97 | oveq2d 7374 |
. . . . . . . . . . 11
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ((0 +
1)...((๐พ โ 1) + 1)) =
((0 + 1)...๐พ)) |
99 | 94, 98 | eleqtrd 2836 |
. . . . . . . . . 10
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ (๐ + 1) โ ((0 + 1)...๐พ)) |
100 | 30 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ๐ด โ
โ) |
101 | 26 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ๐ท โ
โ) |
102 | 90 | zcnd 12613 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ๐ โ
โ) |
103 | 102, 101 | mulcld 11180 |
. . . . . . . . . . . 12
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ (๐ ยท ๐ท) โ โ) |
104 | 100, 101,
103 | addassd 11182 |
. . . . . . . . . . 11
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ((๐ด + ๐ท) + (๐ ยท ๐ท)) = (๐ด + (๐ท + (๐ ยท ๐ท)))) |
105 | | 1cnd 11155 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ 1 โ
โ) |
106 | 102, 105,
101 | adddird 11185 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ((๐ + 1) ยท ๐ท) = ((๐ ยท ๐ท) + (1 ยท ๐ท))) |
107 | 101, 103 | addcomd 11362 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ (๐ท + (๐ ยท ๐ท)) = ((๐ ยท ๐ท) + ๐ท)) |
108 | 101 | mulid2d 11178 |
. . . . . . . . . . . . . . 15
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ (1 ยท
๐ท) = ๐ท) |
109 | 108 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ((๐ ยท ๐ท) + (1 ยท ๐ท)) = ((๐ ยท ๐ท) + ๐ท)) |
110 | 107, 109 | eqtr4d 2776 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ (๐ท + (๐ ยท ๐ท)) = ((๐ ยท ๐ท) + (1 ยท ๐ท))) |
111 | 106, 110 | eqtr4d 2776 |
. . . . . . . . . . . 12
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ((๐ + 1) ยท ๐ท) = (๐ท + (๐ ยท ๐ท))) |
112 | 111 | oveq2d 7374 |
. . . . . . . . . . 11
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ (๐ด + ((๐ + 1) ยท ๐ท)) = (๐ด + (๐ท + (๐ ยท ๐ท)))) |
113 | 104, 112 | eqtr4d 2776 |
. . . . . . . . . 10
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ ((๐ด + ๐ท) + (๐ ยท ๐ท)) = (๐ด + ((๐ + 1) ยท ๐ท))) |
114 | | ovex 7391 |
. . . . . . . . . . 11
โข (๐ + 1) โ V |
115 | | eleq1 2822 |
. . . . . . . . . . . 12
โข (๐ = (๐ + 1) โ (๐ โ ((0 + 1)...๐พ) โ (๐ + 1) โ ((0 + 1)...๐พ))) |
116 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ + 1) โ (๐ ยท ๐ท) = ((๐ + 1) ยท ๐ท)) |
117 | 116 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข (๐ = (๐ + 1) โ (๐ด + (๐ ยท ๐ท)) = (๐ด + ((๐ + 1) ยท ๐ท))) |
118 | 117 | eqeq2d 2744 |
. . . . . . . . . . . 12
โข (๐ = (๐ + 1) โ (((๐ด + ๐ท) + (๐ ยท ๐ท)) = (๐ด + (๐ ยท ๐ท)) โ ((๐ด + ๐ท) + (๐ ยท ๐ท)) = (๐ด + ((๐ + 1) ยท ๐ท)))) |
119 | 115, 118 | anbi12d 632 |
. . . . . . . . . . 11
โข (๐ = (๐ + 1) โ ((๐ โ ((0 + 1)...๐พ) โง ((๐ด + ๐ท) + (๐ ยท ๐ท)) = (๐ด + (๐ ยท ๐ท))) โ ((๐ + 1) โ ((0 + 1)...๐พ) โง ((๐ด + ๐ท) + (๐ ยท ๐ท)) = (๐ด + ((๐ + 1) ยท ๐ท))))) |
120 | 114, 119 | spcev 3564 |
. . . . . . . . . 10
โข (((๐ + 1) โ ((0 + 1)...๐พ) โง ((๐ด + ๐ท) + (๐ ยท ๐ท)) = (๐ด + ((๐ + 1) ยท ๐ท))) โ โ๐(๐ โ ((0 + 1)...๐พ) โง ((๐ด + ๐ท) + (๐ ยท ๐ท)) = (๐ด + (๐ ยท ๐ท)))) |
121 | 99, 113, 120 | syl2anc 585 |
. . . . . . . . 9
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ
โ๐(๐ โ ((0 + 1)...๐พ) โง ((๐ด + ๐ท) + (๐ ยท ๐ท)) = (๐ด + (๐ ยท ๐ท)))) |
122 | | eqeq1 2737 |
. . . . . . . . . . 11
โข (๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)) โ (๐ฅ = (๐ด + (๐ ยท ๐ท)) โ ((๐ด + ๐ท) + (๐ ยท ๐ท)) = (๐ด + (๐ ยท ๐ท)))) |
123 | 122 | anbi2d 630 |
. . . . . . . . . 10
โข (๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)) โ ((๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โ (๐ โ ((0 + 1)...๐พ) โง ((๐ด + ๐ท) + (๐ ยท ๐ท)) = (๐ด + (๐ ยท ๐ท))))) |
124 | 123 | exbidv 1925 |
. . . . . . . . 9
โข (๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)) โ (โ๐(๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โ โ๐(๐ โ ((0 + 1)...๐พ) โง ((๐ด + ๐ท) + (๐ ยท ๐ท)) = (๐ด + (๐ ยท ๐ท))))) |
125 | 121, 124 | syl5ibrcom 247 |
. . . . . . . 8
โข (((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โง ๐ โ (0...(๐พ โ 1))) โ (๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)) โ โ๐(๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))))) |
126 | 125 | rexlimdva 3149 |
. . . . . . 7
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (โ๐ โ
(0...(๐พ โ 1))๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)) โ โ๐(๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))))) |
127 | 82, 126 | impbid 211 |
. . . . . 6
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (โ๐(๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โ โ๐ โ (0...(๐พ โ 1))๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)))) |
128 | | nnaddcl 12181 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ท โ โ) โ (๐ด + ๐ท) โ โ) |
129 | 128 | 3adant1 1131 |
. . . . . . 7
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ด + ๐ท) โ
โ) |
130 | | vdwapval 16850 |
. . . . . . 7
โข ((๐พ โ โ0
โง (๐ด + ๐ท) โ โ โง ๐ท โ โ) โ (๐ฅ โ ((๐ด + ๐ท)(APโ๐พ)๐ท) โ โ๐ โ (0...(๐พ โ 1))๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)))) |
131 | 129, 130 | syld3an2 1412 |
. . . . . 6
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ฅ โ ((๐ด + ๐ท)(APโ๐พ)๐ท) โ โ๐ โ (0...(๐พ โ 1))๐ฅ = ((๐ด + ๐ท) + (๐ ยท ๐ท)))) |
132 | 127, 131 | bitr4d 282 |
. . . . 5
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (โ๐(๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โ ๐ฅ โ ((๐ด + ๐ท)(APโ๐พ)๐ท))) |
133 | 40, 132 | orbi12d 918 |
. . . 4
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ ((โ๐(๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โจ โ๐(๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท)))) โ (๐ฅ โ {๐ด} โจ ๐ฅ โ ((๐ด + ๐ท)(APโ๐พ)๐ท)))) |
134 | | elun 4109 |
. . . 4
โข (๐ฅ โ ({๐ด} โช ((๐ด + ๐ท)(APโ๐พ)๐ท)) โ (๐ฅ โ {๐ด} โจ ๐ฅ โ ((๐ด + ๐ท)(APโ๐พ)๐ท))) |
135 | 133, 134 | bitr4di 289 |
. . 3
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ ((โ๐(๐ = 0 โง ๐ฅ = (๐ด + (๐ ยท ๐ท))) โจ โ๐(๐ โ ((0 + 1)...๐พ) โง ๐ฅ = (๐ด + (๐ ยท ๐ท)))) โ ๐ฅ โ ({๐ด} โช ((๐ด + ๐ท)(APโ๐พ)๐ท)))) |
136 | 24, 135 | bitrd 279 |
. 2
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ฅ โ (๐ด(APโ(๐พ + 1))๐ท) โ ๐ฅ โ ({๐ด} โช ((๐ด + ๐ท)(APโ๐พ)๐ท)))) |
137 | 136 | eqrdv 2731 |
1
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ด(APโ(๐พ + 1))๐ท) = ({๐ด} โช ((๐ด + ๐ท)(APโ๐พ)๐ท))) |