Step | Hyp | Ref
| Expression |
1 | | sqdeccom12.a |
. . . . . . . . 9
โข ๐ด โ
โ0 |
2 | 1, 1 | nn0mulcli 12458 |
. . . . . . . 8
โข (๐ด ยท ๐ด) โ
โ0 |
3 | | 0nn0 12435 |
. . . . . . . 8
โข 0 โ
โ0 |
4 | 2, 3 | deccl 12640 |
. . . . . . 7
โข ;(๐ด ยท ๐ด)0 โ
โ0 |
5 | 4, 3 | deccl 12640 |
. . . . . 6
โข ;;(๐ด ยท ๐ด)00 โ
โ0 |
6 | 5 | nn0cni 12432 |
. . . . 5
โข ;;(๐ด ยท ๐ด)00 โ โ |
7 | | sqdeccom12.b |
. . . . . . . . 9
โข ๐ต โ
โ0 |
8 | 7, 7 | nn0mulcli 12458 |
. . . . . . . 8
โข (๐ต ยท ๐ต) โ
โ0 |
9 | 8, 3 | deccl 12640 |
. . . . . . 7
โข ;(๐ต ยท ๐ต)0 โ
โ0 |
10 | 9, 3 | deccl 12640 |
. . . . . 6
โข ;;(๐ต ยท ๐ต)00 โ
โ0 |
11 | 10 | nn0cni 12432 |
. . . . 5
โข ;;(๐ต ยท ๐ต)00 โ โ |
12 | 1 | nn0cni 12432 |
. . . . . 6
โข ๐ด โ โ |
13 | 12, 12 | mulcli 11169 |
. . . . 5
โข (๐ด ยท ๐ด) โ โ |
14 | 7 | nn0cni 12432 |
. . . . . 6
โข ๐ต โ โ |
15 | 14, 14 | mulcli 11169 |
. . . . 5
โข (๐ต ยท ๐ต) โ โ |
16 | | subadd4 11452 |
. . . . 5
โข (((;;(๐ด ยท ๐ด)00 โ โ โง ;;(๐ต ยท ๐ต)00 โ โ) โง ((๐ด ยท ๐ด) โ โ โง (๐ต ยท ๐ต) โ โ)) โ ((;;(๐ด ยท ๐ด)00 โ ;;(๐ต ยท ๐ต)00) โ ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) = ((;;(๐ด ยท ๐ด)00 + (๐ต ยท ๐ต)) โ (;;(๐ต ยท ๐ต)00 + (๐ด ยท ๐ด)))) |
17 | 6, 11, 13, 15, 16 | mp4an 692 |
. . . 4
โข ((;;(๐ด ยท ๐ด)00 โ ;;(๐ต ยท ๐ต)00) โ ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) = ((;;(๐ด ยท ๐ด)00 + (๐ต ยท ๐ต)) โ (;;(๐ต ยท ๐ต)00 + (๐ด ยท ๐ด))) |
18 | | eqid 2737 |
. . . . . 6
โข ;;(๐ด ยท ๐ด)00 = ;;(๐ด ยท ๐ด)00 |
19 | 15 | addid2i 11350 |
. . . . . 6
โข (0 +
(๐ต ยท ๐ต)) = (๐ต ยท ๐ต) |
20 | 4, 3, 8, 18, 19 | decaddi 12685 |
. . . . 5
โข (;;(๐ด ยท ๐ด)00 + (๐ต ยท ๐ต)) = ;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต) |
21 | | eqid 2737 |
. . . . . 6
โข ;;(๐ต ยท ๐ต)00 = ;;(๐ต ยท ๐ต)00 |
22 | 13 | addid2i 11350 |
. . . . . 6
โข (0 +
(๐ด ยท ๐ด)) = (๐ด ยท ๐ด) |
23 | 9, 3, 2, 21, 22 | decaddi 12685 |
. . . . 5
โข (;;(๐ต ยท ๐ต)00 + (๐ด ยท ๐ด)) = ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด) |
24 | 20, 23 | oveq12i 7374 |
. . . 4
โข ((;;(๐ด ยท ๐ด)00 + (๐ต ยท ๐ต)) โ (;;(๐ต ยท ๐ต)00 + (๐ด ยท ๐ด))) = (;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต) โ ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด)) |
25 | 17, 24 | eqtr2i 2766 |
. . 3
โข (;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต) โ ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด)) = ((;;(๐ด ยท ๐ด)00 โ ;;(๐ต ยท ๐ต)00) โ ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) |
26 | | eqid 2737 |
. . . . 5
โข ;;((๐ต ยท ๐ต) + (๐ด ยท ๐ด))(((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) + 0)((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) = ;;((๐ต ยท ๐ต) + (๐ด ยท ๐ด))(((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) + 0)((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) |
27 | 7, 1 | nn0mulcli 12458 |
. . . . . . . 8
โข (๐ต ยท ๐ด) โ
โ0 |
28 | 1, 7, 27 | numcl 12638 |
. . . . . . 7
โข ((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) โ
โ0 |
29 | 2, 28 | deccl 12640 |
. . . . . 6
โข ;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) โ
โ0 |
30 | | eqid 2737 |
. . . . . 6
โข ;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) = ;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) |
31 | | eqid 2737 |
. . . . . 6
โข ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด) = ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด) |
32 | | eqid 2737 |
. . . . . . 7
โข ;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) = ;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) |
33 | | eqid 2737 |
. . . . . . 7
โข ;(๐ต ยท ๐ต)0 = ;(๐ต ยท ๐ต)0 |
34 | 13, 15 | addcomi 11353 |
. . . . . . 7
โข ((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) = ((๐ต ยท ๐ต) + (๐ด ยท ๐ด)) |
35 | | eqid 2737 |
. . . . . . 7
โข (((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) + 0) = (((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) + 0) |
36 | 2, 28, 8, 3, 32, 33, 34, 35 | decadd 12679 |
. . . . . 6
โข (;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) + ;(๐ต ยท ๐ต)0) = ;((๐ต ยท ๐ต) + (๐ด ยท ๐ด))(((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) + 0) |
37 | 15, 13 | addcomi 11353 |
. . . . . 6
โข ((๐ต ยท ๐ต) + (๐ด ยท ๐ด)) = ((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) |
38 | 29, 8, 9, 2, 30, 31, 36, 37 | decadd 12679 |
. . . . 5
โข (;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) + ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด)) = ;;((๐ต ยท ๐ต) + (๐ด ยท ๐ด))(((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) + 0)((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) |
39 | 8, 28 | deccl 12640 |
. . . . . 6
โข ;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) โ
โ0 |
40 | | eqid 2737 |
. . . . . 6
โข ;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด) = ;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด) |
41 | | eqid 2737 |
. . . . . 6
โข ;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต) = ;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต) |
42 | | eqid 2737 |
. . . . . . 7
โข ;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) = ;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) |
43 | | eqid 2737 |
. . . . . . 7
โข ;(๐ด ยท ๐ด)0 = ;(๐ด ยท ๐ด)0 |
44 | | eqid 2737 |
. . . . . . 7
โข ((๐ต ยท ๐ต) + (๐ด ยท ๐ด)) = ((๐ต ยท ๐ต) + (๐ด ยท ๐ด)) |
45 | 8, 28, 2, 3, 42, 43, 44, 35 | decadd 12679 |
. . . . . 6
โข (;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) + ;(๐ด ยท ๐ด)0) = ;((๐ต ยท ๐ต) + (๐ด ยท ๐ด))(((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) + 0) |
46 | | eqid 2737 |
. . . . . 6
โข ((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) = ((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) |
47 | 39, 2, 4, 8, 40, 41, 45, 46 | decadd 12679 |
. . . . 5
โข (;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด) + ;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต)) = ;;((๐ต ยท ๐ต) + (๐ด ยท ๐ด))(((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) + 0)((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) |
48 | 26, 38, 47 | 3eqtr4i 2775 |
. . . 4
โข (;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) + ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด)) = (;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด) + ;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต)) |
49 | 29, 8 | deccl 12640 |
. . . . . 6
โข ;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) โ
โ0 |
50 | 49 | nn0cni 12432 |
. . . . 5
โข ;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) โ โ |
51 | 9, 2 | deccl 12640 |
. . . . . 6
โข ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด) โ
โ0 |
52 | 51 | nn0cni 12432 |
. . . . 5
โข ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด) โ โ |
53 | 39, 2 | deccl 12640 |
. . . . . 6
โข ;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด) โ
โ0 |
54 | 53 | nn0cni 12432 |
. . . . 5
โข ;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด) โ โ |
55 | 4, 8 | deccl 12640 |
. . . . . 6
โข ;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต) โ
โ0 |
56 | 55 | nn0cni 12432 |
. . . . 5
โข ;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต) โ โ |
57 | | addsubeq4com 40823 |
. . . . 5
โข (((;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) โ โ โง ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด) โ โ) โง (;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด) โ โ โง ;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต) โ โ)) โ ((;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) + ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด)) = (;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด) + ;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต)) โ (;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) โ ;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด)) = (;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต) โ ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด)))) |
58 | 50, 52, 54, 56, 57 | mp4an 692 |
. . . 4
โข ((;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) + ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด)) = (;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด) + ;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต)) โ (;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) โ ;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด)) = (;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต) โ ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด))) |
59 | 48, 58 | mpbi 229 |
. . 3
โข (;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) โ ;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด)) = (;;(๐ด ยท ๐ด)0(๐ต ยท ๐ต) โ ;;(๐ต ยท ๐ต)0(๐ด ยท ๐ด)) |
60 | | 10nn0 12643 |
. . . . . . 7
โข ;10 โ
โ0 |
61 | 60, 3 | deccl 12640 |
. . . . . 6
โข ;;100 โ โ0 |
62 | 61 | nn0cni 12432 |
. . . . 5
โข ;;100 โ โ |
63 | | ax-1cn 11116 |
. . . . 5
โข 1 โ
โ |
64 | 13, 15 | subcli 11484 |
. . . . 5
โข ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต)) โ โ |
65 | 62, 63, 64 | subdiri 11612 |
. . . 4
โข ((;;100 โ 1) ยท ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) = ((;;100
ยท ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) โ (1 ยท ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต)))) |
66 | 62, 13, 15 | subdii 11611 |
. . . . . 6
โข (;;100 ยท ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) = ((;;100
ยท (๐ด ยท ๐ด)) โ (;;100
ยท (๐ต ยท ๐ต))) |
67 | | eqid 2737 |
. . . . . . . 8
โข ;;100 = ;;100 |
68 | 2 | dec0u 12646 |
. . . . . . . 8
โข (;10 ยท (๐ด ยท ๐ด)) = ;(๐ด ยท ๐ด)0 |
69 | 13 | mul02i 11351 |
. . . . . . . 8
โข (0
ยท (๐ด ยท ๐ด)) = 0 |
70 | 2, 60, 3, 67, 68, 69 | decmul1 12689 |
. . . . . . 7
โข (;;100 ยท (๐ด ยท ๐ด)) = ;;(๐ด ยท ๐ด)00 |
71 | 8 | dec0u 12646 |
. . . . . . . 8
โข (;10 ยท (๐ต ยท ๐ต)) = ;(๐ต ยท ๐ต)0 |
72 | 15 | mul02i 11351 |
. . . . . . . 8
โข (0
ยท (๐ต ยท ๐ต)) = 0 |
73 | 8, 60, 3, 67, 71, 72 | decmul1 12689 |
. . . . . . 7
โข (;;100 ยท (๐ต ยท ๐ต)) = ;;(๐ต ยท ๐ต)00 |
74 | 70, 73 | oveq12i 7374 |
. . . . . 6
โข ((;;100 ยท (๐ด ยท ๐ด)) โ (;;100
ยท (๐ต ยท ๐ต))) = (;;(๐ด ยท ๐ด)00 โ ;;(๐ต ยท ๐ต)00) |
75 | 66, 74 | eqtri 2765 |
. . . . 5
โข (;;100 ยท ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) = (;;(๐ด ยท ๐ด)00 โ ;;(๐ต ยท ๐ต)00) |
76 | 64 | mulid2i 11167 |
. . . . 5
โข (1
ยท ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) = ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต)) |
77 | 75, 76 | oveq12i 7374 |
. . . 4
โข ((;;100 ยท ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) โ (1 ยท ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต)))) = ((;;(๐ด ยท ๐ด)00 โ ;;(๐ต ยท ๐ต)00) โ ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) |
78 | 65, 77 | eqtri 2765 |
. . 3
โข ((;;100 โ 1) ยท ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) = ((;;(๐ด ยท ๐ด)00 โ ;;(๐ต ยท ๐ต)00) โ ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) |
79 | 25, 59, 78 | 3eqtr4i 2775 |
. 2
โข (;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) โ ;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด)) = ((;;100
โ 1) ยท ((๐ด
ยท ๐ด) โ (๐ต ยท ๐ต))) |
80 | | eqid 2737 |
. . . 4
โข (๐ด ยท ๐ด) = (๐ด ยท ๐ด) |
81 | | eqid 2737 |
. . . 4
โข ((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) = ((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) |
82 | | eqid 2737 |
. . . 4
โข (๐ต ยท ๐ต) = (๐ต ยท ๐ต) |
83 | 1, 7, 1, 7, 80, 81, 82 | decpmulnc 40830 |
. . 3
โข (;๐ด๐ต ยท ;๐ด๐ต) = ;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) |
84 | 14, 12 | mulcli 11169 |
. . . . 5
โข (๐ต ยท ๐ด) โ โ |
85 | 12, 14 | mulcli 11169 |
. . . . 5
โข (๐ด ยท ๐ต) โ โ |
86 | 84, 85 | addcomi 11353 |
. . . 4
โข ((๐ต ยท ๐ด) + (๐ด ยท ๐ต)) = ((๐ด ยท ๐ต) + (๐ต ยท ๐ด)) |
87 | 7, 1, 7, 1, 82, 86, 80 | decpmulnc 40830 |
. . 3
โข (;๐ต๐ด ยท ;๐ต๐ด) = ;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด) |
88 | 83, 87 | oveq12i 7374 |
. 2
โข ((;๐ด๐ต ยท ;๐ด๐ต) โ (;๐ต๐ด ยท ;๐ต๐ด)) = (;;(๐ด ยท ๐ด)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ต ยท ๐ต) โ ;;(๐ต ยท ๐ต)((๐ด ยท ๐ต) + (๐ต ยท ๐ด))(๐ด ยท ๐ด)) |
89 | | 9nn0 12444 |
. . . . . 6
โข 9 โ
โ0 |
90 | 89, 89 | deccl 12640 |
. . . . 5
โข ;99 โ
โ0 |
91 | 90 | nn0cni 12432 |
. . . 4
โข ;99 โ โ |
92 | | 9p1e10 12627 |
. . . . . 6
โข (9 + 1) =
;10 |
93 | | eqid 2737 |
. . . . . 6
โข ;99 = ;99 |
94 | 89, 92, 93 | decsucc 12666 |
. . . . 5
โข (;99 + 1) = ;;100 |
95 | 91, 63, 94 | addcomli 11354 |
. . . 4
โข (1 +
;99) = ;;100 |
96 | 63, 91, 95 | mvlladdi 11426 |
. . 3
โข ;99 = (;;100
โ 1) |
97 | 96 | oveq1i 7372 |
. 2
โข (;99 ยท ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) = ((;;100
โ 1) ยท ((๐ด
ยท ๐ด) โ (๐ต ยท ๐ต))) |
98 | 79, 88, 97 | 3eqtr4i 2775 |
1
โข ((;๐ด๐ต ยท ;๐ด๐ต) โ (;๐ต๐ด ยท ;๐ต๐ด)) = (;99 ยท ((๐ด ยท ๐ด) โ (๐ต ยท ๐ต))) |