Step | Hyp | Ref
| Expression |
1 | | oveq2 7414 |
. . . 4
โข (๐ฅ = โ
โ (๐ต +o ๐ฅ) = (๐ต +o โ
)) |
2 | 1 | oveq2d 7422 |
. . 3
โข (๐ฅ = โ
โ (๐ด โo (๐ต +o ๐ฅ)) = (๐ด โo (๐ต +o โ
))) |
3 | | oveq2 7414 |
. . . 4
โข (๐ฅ = โ
โ (๐ด โo ๐ฅ) = (๐ด โo
โ
)) |
4 | 3 | oveq2d 7422 |
. . 3
โข (๐ฅ = โ
โ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ)) = ((๐ด โo ๐ต) ยทo (๐ด โo
โ
))) |
5 | 2, 4 | eqeq12d 2749 |
. 2
โข (๐ฅ = โ
โ ((๐ด โo (๐ต +o ๐ฅ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ)) โ (๐ด โo (๐ต +o โ
)) = ((๐ด โo ๐ต) ยทo (๐ด โo
โ
)))) |
6 | | oveq2 7414 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ต +o ๐ฅ) = (๐ต +o ๐ฆ)) |
7 | 6 | oveq2d 7422 |
. . 3
โข (๐ฅ = ๐ฆ โ (๐ด โo (๐ต +o ๐ฅ)) = (๐ด โo (๐ต +o ๐ฆ))) |
8 | | oveq2 7414 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ด โo ๐ฅ) = (๐ด โo ๐ฆ)) |
9 | 8 | oveq2d 7422 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) |
10 | 7, 9 | eqeq12d 2749 |
. 2
โข (๐ฅ = ๐ฆ โ ((๐ด โo (๐ต +o ๐ฅ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ)) โ (๐ด โo (๐ต +o ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)))) |
11 | | oveq2 7414 |
. . . 4
โข (๐ฅ = suc ๐ฆ โ (๐ต +o ๐ฅ) = (๐ต +o suc ๐ฆ)) |
12 | 11 | oveq2d 7422 |
. . 3
โข (๐ฅ = suc ๐ฆ โ (๐ด โo (๐ต +o ๐ฅ)) = (๐ด โo (๐ต +o suc ๐ฆ))) |
13 | | oveq2 7414 |
. . . 4
โข (๐ฅ = suc ๐ฆ โ (๐ด โo ๐ฅ) = (๐ด โo suc ๐ฆ)) |
14 | 13 | oveq2d 7422 |
. . 3
โข (๐ฅ = suc ๐ฆ โ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ)) = ((๐ด โo ๐ต) ยทo (๐ด โo suc ๐ฆ))) |
15 | 12, 14 | eqeq12d 2749 |
. 2
โข (๐ฅ = suc ๐ฆ โ ((๐ด โo (๐ต +o ๐ฅ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ)) โ (๐ด โo (๐ต +o suc ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo suc ๐ฆ)))) |
16 | | oveq2 7414 |
. . . 4
โข (๐ฅ = ๐ถ โ (๐ต +o ๐ฅ) = (๐ต +o ๐ถ)) |
17 | 16 | oveq2d 7422 |
. . 3
โข (๐ฅ = ๐ถ โ (๐ด โo (๐ต +o ๐ฅ)) = (๐ด โo (๐ต +o ๐ถ))) |
18 | | oveq2 7414 |
. . . 4
โข (๐ฅ = ๐ถ โ (๐ด โo ๐ฅ) = (๐ด โo ๐ถ)) |
19 | 18 | oveq2d 7422 |
. . 3
โข (๐ฅ = ๐ถ โ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ))) |
20 | 17, 19 | eqeq12d 2749 |
. 2
โข (๐ฅ = ๐ถ โ ((๐ด โo (๐ต +o ๐ฅ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ)) โ (๐ด โo (๐ต +o ๐ถ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ)))) |
21 | | oeoalem.1 |
. . . . 5
โข ๐ด โ On |
22 | | oeoalem.3 |
. . . . 5
โข ๐ต โ On |
23 | | oecl 8534 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โo ๐ต) โ On) |
24 | 21, 22, 23 | mp2an 691 |
. . . 4
โข (๐ด โo ๐ต) โ On |
25 | | om1 8539 |
. . . 4
โข ((๐ด โo ๐ต) โ On โ ((๐ด โo ๐ต) ยทo
1o) = (๐ด
โo ๐ต)) |
26 | 24, 25 | ax-mp 5 |
. . 3
โข ((๐ด โo ๐ต) ยทo
1o) = (๐ด
โo ๐ต) |
27 | | oe0 8519 |
. . . . 5
โข (๐ด โ On โ (๐ด โo โ
) =
1o) |
28 | 21, 27 | ax-mp 5 |
. . . 4
โข (๐ด โo โ
) =
1o |
29 | 28 | oveq2i 7417 |
. . 3
โข ((๐ด โo ๐ต) ยทo (๐ด โo โ
)) =
((๐ด โo
๐ต) ยทo
1o) |
30 | | oa0 8513 |
. . . . 5
โข (๐ต โ On โ (๐ต +o โ
) = ๐ต) |
31 | 22, 30 | ax-mp 5 |
. . . 4
โข (๐ต +o โ
) = ๐ต |
32 | 31 | oveq2i 7417 |
. . 3
โข (๐ด โo (๐ต +o โ
)) =
(๐ด โo ๐ต) |
33 | 26, 29, 32 | 3eqtr4ri 2772 |
. 2
โข (๐ด โo (๐ต +o โ
)) =
((๐ด โo
๐ต) ยทo
(๐ด โo
โ
)) |
34 | | oasuc 8521 |
. . . . . . . 8
โข ((๐ต โ On โง ๐ฆ โ On) โ (๐ต +o suc ๐ฆ) = suc (๐ต +o ๐ฆ)) |
35 | 34 | oveq2d 7422 |
. . . . . . 7
โข ((๐ต โ On โง ๐ฆ โ On) โ (๐ด โo (๐ต +o suc ๐ฆ)) = (๐ด โo suc (๐ต +o ๐ฆ))) |
36 | | oacl 8532 |
. . . . . . . 8
โข ((๐ต โ On โง ๐ฆ โ On) โ (๐ต +o ๐ฆ) โ On) |
37 | | oesuc 8524 |
. . . . . . . 8
โข ((๐ด โ On โง (๐ต +o ๐ฆ) โ On) โ (๐ด โo suc (๐ต +o ๐ฆ)) = ((๐ด โo (๐ต +o ๐ฆ)) ยทo ๐ด)) |
38 | 21, 36, 37 | sylancr 588 |
. . . . . . 7
โข ((๐ต โ On โง ๐ฆ โ On) โ (๐ด โo suc (๐ต +o ๐ฆ)) = ((๐ด โo (๐ต +o ๐ฆ)) ยทo ๐ด)) |
39 | 35, 38 | eqtrd 2773 |
. . . . . 6
โข ((๐ต โ On โง ๐ฆ โ On) โ (๐ด โo (๐ต +o suc ๐ฆ)) = ((๐ด โo (๐ต +o ๐ฆ)) ยทo ๐ด)) |
40 | 22, 39 | mpan 689 |
. . . . 5
โข (๐ฆ โ On โ (๐ด โo (๐ต +o suc ๐ฆ)) = ((๐ด โo (๐ต +o ๐ฆ)) ยทo ๐ด)) |
41 | | oveq1 7413 |
. . . . 5
โข ((๐ด โo (๐ต +o ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)) โ ((๐ด โo (๐ต +o ๐ฆ)) ยทo ๐ด) = (((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)) ยทo ๐ด)) |
42 | 40, 41 | sylan9eq 2793 |
. . . 4
โข ((๐ฆ โ On โง (๐ด โo (๐ต +o ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) โ (๐ด โo (๐ต +o suc ๐ฆ)) = (((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)) ยทo ๐ด)) |
43 | | oecl 8534 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ฆ โ On) โ (๐ด โo ๐ฆ) โ On) |
44 | | omass 8577 |
. . . . . . . . 9
โข (((๐ด โo ๐ต) โ On โง (๐ด โo ๐ฆ) โ On โง ๐ด โ On) โ (((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)) ยทo ๐ด) = ((๐ด โo ๐ต) ยทo ((๐ด โo ๐ฆ) ยทo ๐ด))) |
45 | 24, 21, 44 | mp3an13 1453 |
. . . . . . . 8
โข ((๐ด โo ๐ฆ) โ On โ (((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)) ยทo ๐ด) = ((๐ด โo ๐ต) ยทo ((๐ด โo ๐ฆ) ยทo ๐ด))) |
46 | 43, 45 | syl 17 |
. . . . . . 7
โข ((๐ด โ On โง ๐ฆ โ On) โ (((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)) ยทo ๐ด) = ((๐ด โo ๐ต) ยทo ((๐ด โo ๐ฆ) ยทo ๐ด))) |
47 | | oesuc 8524 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ฆ โ On) โ (๐ด โo suc ๐ฆ) = ((๐ด โo ๐ฆ) ยทo ๐ด)) |
48 | 47 | oveq2d 7422 |
. . . . . . 7
โข ((๐ด โ On โง ๐ฆ โ On) โ ((๐ด โo ๐ต) ยทo (๐ด โo suc ๐ฆ)) = ((๐ด โo ๐ต) ยทo ((๐ด โo ๐ฆ) ยทo ๐ด))) |
49 | 46, 48 | eqtr4d 2776 |
. . . . . 6
โข ((๐ด โ On โง ๐ฆ โ On) โ (((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)) ยทo ๐ด) = ((๐ด โo ๐ต) ยทo (๐ด โo suc ๐ฆ))) |
50 | 21, 49 | mpan 689 |
. . . . 5
โข (๐ฆ โ On โ (((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)) ยทo ๐ด) = ((๐ด โo ๐ต) ยทo (๐ด โo suc ๐ฆ))) |
51 | 50 | adantr 482 |
. . . 4
โข ((๐ฆ โ On โง (๐ด โo (๐ต +o ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) โ (((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)) ยทo ๐ด) = ((๐ด โo ๐ต) ยทo (๐ด โo suc ๐ฆ))) |
52 | 42, 51 | eqtrd 2773 |
. . 3
โข ((๐ฆ โ On โง (๐ด โo (๐ต +o ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) โ (๐ด โo (๐ต +o suc ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo suc ๐ฆ))) |
53 | 52 | ex 414 |
. 2
โข (๐ฆ โ On โ ((๐ด โo (๐ต +o ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)) โ (๐ด โo (๐ต +o suc ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo suc ๐ฆ)))) |
54 | | vex 3479 |
. . . . . . . 8
โข ๐ฅ โ V |
55 | | oalim 8529 |
. . . . . . . . 9
โข ((๐ต โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โ (๐ต +o ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ต +o ๐ฆ)) |
56 | 22, 55 | mpan 689 |
. . . . . . . 8
โข ((๐ฅ โ V โง Lim ๐ฅ) โ (๐ต +o ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ต +o ๐ฆ)) |
57 | 54, 56 | mpan 689 |
. . . . . . 7
โข (Lim
๐ฅ โ (๐ต +o ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ต +o ๐ฆ)) |
58 | 57 | oveq2d 7422 |
. . . . . 6
โข (Lim
๐ฅ โ (๐ด โo (๐ต +o ๐ฅ)) = (๐ด โo โช ๐ฆ โ ๐ฅ (๐ต +o ๐ฆ))) |
59 | | limord 6422 |
. . . . . . . . . 10
โข (Lim
๐ฅ โ Ord ๐ฅ) |
60 | | ordelon 6386 |
. . . . . . . . . 10
โข ((Ord
๐ฅ โง ๐ฆ โ ๐ฅ) โ ๐ฆ โ On) |
61 | 59, 60 | sylan 581 |
. . . . . . . . 9
โข ((Lim
๐ฅ โง ๐ฆ โ ๐ฅ) โ ๐ฆ โ On) |
62 | 22, 61, 36 | sylancr 588 |
. . . . . . . 8
โข ((Lim
๐ฅ โง ๐ฆ โ ๐ฅ) โ (๐ต +o ๐ฆ) โ On) |
63 | 62 | ralrimiva 3147 |
. . . . . . 7
โข (Lim
๐ฅ โ โ๐ฆ โ ๐ฅ (๐ต +o ๐ฆ) โ On) |
64 | | 0ellim 6425 |
. . . . . . . 8
โข (Lim
๐ฅ โ โ
โ
๐ฅ) |
65 | 64 | ne0d 4335 |
. . . . . . 7
โข (Lim
๐ฅ โ ๐ฅ โ โ
) |
66 | | vex 3479 |
. . . . . . . . 9
โข ๐ค โ V |
67 | | oeoalem.2 |
. . . . . . . . . . 11
โข โ
โ ๐ด |
68 | | oelim 8531 |
. . . . . . . . . . 11
โข (((๐ด โ On โง (๐ค โ V โง Lim ๐ค)) โง โ
โ ๐ด) โ (๐ด โo ๐ค) = โช ๐ง โ ๐ค (๐ด โo ๐ง)) |
69 | 67, 68 | mpan2 690 |
. . . . . . . . . 10
โข ((๐ด โ On โง (๐ค โ V โง Lim ๐ค)) โ (๐ด โo ๐ค) = โช ๐ง โ ๐ค (๐ด โo ๐ง)) |
70 | 21, 69 | mpan 689 |
. . . . . . . . 9
โข ((๐ค โ V โง Lim ๐ค) โ (๐ด โo ๐ค) = โช ๐ง โ ๐ค (๐ด โo ๐ง)) |
71 | 66, 70 | mpan 689 |
. . . . . . . 8
โข (Lim
๐ค โ (๐ด โo ๐ค) = โช ๐ง โ ๐ค (๐ด โo ๐ง)) |
72 | | oewordi 8588 |
. . . . . . . . . . 11
โข (((๐ง โ On โง ๐ค โ On โง ๐ด โ On) โง โ
โ
๐ด) โ (๐ง โ ๐ค โ (๐ด โo ๐ง) โ (๐ด โo ๐ค))) |
73 | 67, 72 | mpan2 690 |
. . . . . . . . . 10
โข ((๐ง โ On โง ๐ค โ On โง ๐ด โ On) โ (๐ง โ ๐ค โ (๐ด โo ๐ง) โ (๐ด โo ๐ค))) |
74 | 21, 73 | mp3an3 1451 |
. . . . . . . . 9
โข ((๐ง โ On โง ๐ค โ On) โ (๐ง โ ๐ค โ (๐ด โo ๐ง) โ (๐ด โo ๐ค))) |
75 | 74 | 3impia 1118 |
. . . . . . . 8
โข ((๐ง โ On โง ๐ค โ On โง ๐ง โ ๐ค) โ (๐ด โo ๐ง) โ (๐ด โo ๐ค)) |
76 | 71, 75 | onoviun 8340 |
. . . . . . 7
โข ((๐ฅ โ V โง โ๐ฆ โ ๐ฅ (๐ต +o ๐ฆ) โ On โง ๐ฅ โ โ
) โ (๐ด โo โช ๐ฆ โ ๐ฅ (๐ต +o ๐ฆ)) = โช
๐ฆ โ ๐ฅ (๐ด โo (๐ต +o ๐ฆ))) |
77 | 54, 63, 65, 76 | mp3an2i 1467 |
. . . . . 6
โข (Lim
๐ฅ โ (๐ด โo โช ๐ฆ โ ๐ฅ (๐ต +o ๐ฆ)) = โช
๐ฆ โ ๐ฅ (๐ด โo (๐ต +o ๐ฆ))) |
78 | 58, 77 | eqtrd 2773 |
. . . . 5
โข (Lim
๐ฅ โ (๐ด โo (๐ต +o ๐ฅ)) = โช
๐ฆ โ ๐ฅ (๐ด โo (๐ต +o ๐ฆ))) |
79 | | iuneq2 5016 |
. . . . 5
โข
(โ๐ฆ โ
๐ฅ (๐ด โo (๐ต +o ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)) โ โช
๐ฆ โ ๐ฅ (๐ด โo (๐ต +o ๐ฆ)) = โช
๐ฆ โ ๐ฅ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) |
80 | 78, 79 | sylan9eq 2793 |
. . . 4
โข ((Lim
๐ฅ โง โ๐ฆ โ ๐ฅ (๐ด โo (๐ต +o ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) โ (๐ด โo (๐ต +o ๐ฅ)) = โช
๐ฆ โ ๐ฅ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) |
81 | | oelim 8531 |
. . . . . . . . . 10
โข (((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง โ
โ ๐ด) โ (๐ด โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) |
82 | 67, 81 | mpan2 690 |
. . . . . . . . 9
โข ((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โ (๐ด โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) |
83 | 21, 82 | mpan 689 |
. . . . . . . 8
โข ((๐ฅ โ V โง Lim ๐ฅ) โ (๐ด โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) |
84 | 54, 83 | mpan 689 |
. . . . . . 7
โข (Lim
๐ฅ โ (๐ด โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) |
85 | 84 | oveq2d 7422 |
. . . . . 6
โข (Lim
๐ฅ โ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ)) = ((๐ด โo ๐ต) ยทo โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ))) |
86 | 21, 61, 43 | sylancr 588 |
. . . . . . . 8
โข ((Lim
๐ฅ โง ๐ฆ โ ๐ฅ) โ (๐ด โo ๐ฆ) โ On) |
87 | 86 | ralrimiva 3147 |
. . . . . . 7
โข (Lim
๐ฅ โ โ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ On) |
88 | | omlim 8530 |
. . . . . . . . . 10
โข (((๐ด โo ๐ต) โ On โง (๐ค โ V โง Lim ๐ค)) โ ((๐ด โo ๐ต) ยทo ๐ค) = โช ๐ง โ ๐ค ((๐ด โo ๐ต) ยทo ๐ง)) |
89 | 24, 88 | mpan 689 |
. . . . . . . . 9
โข ((๐ค โ V โง Lim ๐ค) โ ((๐ด โo ๐ต) ยทo ๐ค) = โช ๐ง โ ๐ค ((๐ด โo ๐ต) ยทo ๐ง)) |
90 | 66, 89 | mpan 689 |
. . . . . . . 8
โข (Lim
๐ค โ ((๐ด โo ๐ต) ยทo ๐ค) = โช ๐ง โ ๐ค ((๐ด โo ๐ต) ยทo ๐ง)) |
91 | | omwordi 8568 |
. . . . . . . . . 10
โข ((๐ง โ On โง ๐ค โ On โง (๐ด โo ๐ต) โ On) โ (๐ง โ ๐ค โ ((๐ด โo ๐ต) ยทo ๐ง) โ ((๐ด โo ๐ต) ยทo ๐ค))) |
92 | 24, 91 | mp3an3 1451 |
. . . . . . . . 9
โข ((๐ง โ On โง ๐ค โ On) โ (๐ง โ ๐ค โ ((๐ด โo ๐ต) ยทo ๐ง) โ ((๐ด โo ๐ต) ยทo ๐ค))) |
93 | 92 | 3impia 1118 |
. . . . . . . 8
โข ((๐ง โ On โง ๐ค โ On โง ๐ง โ ๐ค) โ ((๐ด โo ๐ต) ยทo ๐ง) โ ((๐ด โo ๐ต) ยทo ๐ค)) |
94 | 90, 93 | onoviun 8340 |
. . . . . . 7
โข ((๐ฅ โ V โง โ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ On โง ๐ฅ โ โ
) โ ((๐ด โo ๐ต) ยทo โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) = โช
๐ฆ โ ๐ฅ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) |
95 | 54, 87, 65, 94 | mp3an2i 1467 |
. . . . . 6
โข (Lim
๐ฅ โ ((๐ด โo ๐ต) ยทo โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) = โช
๐ฆ โ ๐ฅ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) |
96 | 85, 95 | eqtrd 2773 |
. . . . 5
โข (Lim
๐ฅ โ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ)) = โช ๐ฆ โ ๐ฅ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) |
97 | 96 | adantr 482 |
. . . 4
โข ((Lim
๐ฅ โง โ๐ฆ โ ๐ฅ (๐ด โo (๐ต +o ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) โ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ)) = โช
๐ฆ โ ๐ฅ ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) |
98 | 80, 97 | eqtr4d 2776 |
. . 3
โข ((Lim
๐ฅ โง โ๐ฆ โ ๐ฅ (๐ด โo (๐ต +o ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ))) โ (๐ด โo (๐ต +o ๐ฅ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ))) |
99 | 98 | ex 414 |
. 2
โข (Lim
๐ฅ โ (โ๐ฆ โ ๐ฅ (๐ด โo (๐ต +o ๐ฆ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฆ)) โ (๐ด โo (๐ต +o ๐ฅ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ฅ)))) |
100 | 5, 10, 15, 20, 33, 53, 99 | tfinds 7846 |
1
โข (๐ถ โ On โ (๐ด โo (๐ต +o ๐ถ)) = ((๐ด โo ๐ต) ยทo (๐ด โo ๐ถ))) |