Step | Hyp | Ref
| Expression |
1 | | oveq2 7422 |
. . . . . . 7
โข (๐ = (๐ ยทs ๐) โ ( 1s /su
๐) = ( 1s
/su (๐
ยทs ๐))) |
2 | 1 | oveq2d 7430 |
. . . . . 6
โข (๐ = (๐ ยทs ๐) โ (๐ต๐น( 1s /su ๐)) = (๐ต๐น( 1s /su (๐ ยทs ๐)))) |
3 | 2 | eqeq2d 2738 |
. . . . 5
โข (๐ = (๐ ยทs ๐) โ ((๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) = (๐ต๐น( 1s /su ๐)) โ (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) = (๐ต๐น( 1s /su (๐ ยทs ๐))))) |
4 | | nnmulscl 28187 |
. . . . 5
โข ((๐ โ โs
โง ๐ โ
โs) โ (๐ ยทs ๐) โ
โs) |
5 | | 1sno 27734 |
. . . . . . . . 9
โข
1s โ No |
6 | 5 | a1i 11 |
. . . . . . . 8
โข ((๐ โ โs
โง ๐ โ
โs) โ 1s โ No
) |
7 | | nnsno 28170 |
. . . . . . . . 9
โข (๐ โ โs
โ ๐ โ No ) |
8 | 7 | adantr 480 |
. . . . . . . 8
โข ((๐ โ โs
โง ๐ โ
โs) โ ๐ โ No
) |
9 | | nnsno 28170 |
. . . . . . . . 9
โข (๐ โ โs
โ ๐ โ No ) |
10 | 9 | adantl 481 |
. . . . . . . 8
โข ((๐ โ โs
โง ๐ โ
โs) โ ๐ โ No
) |
11 | | nnne0s 28179 |
. . . . . . . . 9
โข (๐ โ โs
โ ๐ โ 0s
) |
12 | 11 | adantr 480 |
. . . . . . . 8
โข ((๐ โ โs
โง ๐ โ
โs) โ ๐ โ 0s ) |
13 | | nnne0s 28179 |
. . . . . . . . 9
โข (๐ โ โs
โ ๐ โ 0s
) |
14 | 13 | adantl 481 |
. . . . . . . 8
โข ((๐ โ โs
โง ๐ โ
โs) โ ๐ โ 0s ) |
15 | 6, 8, 6, 10, 12, 14 | divmuldivsd 28104 |
. . . . . . 7
โข ((๐ โ โs
โง ๐ โ
โs) โ (( 1s /su ๐) ยทs (
1s /su ๐)) = (( 1s ยทs
1s ) /su (๐ ยทs ๐))) |
16 | | mulsrid 27987 |
. . . . . . . . 9
โข (
1s โ No โ ( 1s
ยทs 1s ) = 1s ) |
17 | 5, 16 | ax-mp 5 |
. . . . . . . 8
โข (
1s ยทs 1s ) =
1s |
18 | 17 | oveq1i 7424 |
. . . . . . 7
โข ((
1s ยทs 1s ) /su (๐ ยทs ๐)) = ( 1s
/su (๐
ยทs ๐)) |
19 | 15, 18 | eqtrdi 2783 |
. . . . . 6
โข ((๐ โ โs
โง ๐ โ
โs) โ (( 1s /su ๐) ยทs (
1s /su ๐)) = ( 1s /su
(๐ ยทs
๐))) |
20 | 19 | oveq2d 7430 |
. . . . 5
โข ((๐ โ โs
โง ๐ โ
โs) โ (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) = (๐ต๐น( 1s /su (๐ ยทs ๐)))) |
21 | 3, 4, 20 | rspcedvdw 3610 |
. . . 4
โข ((๐ โ โs
โง ๐ โ
โs) โ โ๐ โ โs (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) = (๐ต๐น( 1s /su ๐))) |
22 | | eqeq1 2731 |
. . . . 5
โข (๐ด = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) โ (๐ด = (๐ต๐น( 1s /su ๐)) โ (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) = (๐ต๐น( 1s /su ๐)))) |
23 | 22 | rexbidv 3173 |
. . . 4
โข (๐ด = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) โ (โ๐ โ โs ๐ด = (๐ต๐น( 1s /su ๐)) โ โ๐ โ โs
(๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) = (๐ต๐น( 1s /su ๐)))) |
24 | 21, 23 | syl5ibrcom 246 |
. . 3
โข ((๐ โ โs
โง ๐ โ
โs) โ (๐ด = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) โ โ๐ โ โs ๐ด = (๐ต๐น( 1s /su ๐)))) |
25 | 24 | rexlimivv 3194 |
. 2
โข
(โ๐ โ
โs โ๐ โ โs ๐ด = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) โ โ๐ โ โs ๐ด = (๐ต๐น( 1s /su ๐))) |
26 | 5 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โs
โ 1s โ No ) |
27 | | nnsno 28170 |
. . . . . . . . 9
โข (๐ โ โs
โ ๐ โ No ) |
28 | | nnne0s 28179 |
. . . . . . . . 9
โข (๐ โ โs
โ ๐ โ 0s
) |
29 | 26, 27, 28 | divscld 28096 |
. . . . . . . 8
โข (๐ โ โs
โ ( 1s /su ๐) โ No
) |
30 | 29 | mulsridd 27988 |
. . . . . . 7
โข (๐ โ โs
โ (( 1s /su ๐) ยทs 1s ) = (
1s /su ๐)) |
31 | 30 | eqcomd 2733 |
. . . . . 6
โข (๐ โ โs
โ ( 1s /su ๐) = (( 1s /su ๐) ยทs
1s )) |
32 | 31 | oveq2d 7430 |
. . . . 5
โข (๐ โ โs
โ (๐ต๐น( 1s /su ๐)) = (๐ต๐น(( 1s /su ๐) ยทs
1s ))) |
33 | | 1nns 28189 |
. . . . . 6
โข
1s โ โs |
34 | | oveq2 7422 |
. . . . . . . . . 10
โข (๐ = ๐ โ ( 1s /su
๐) = ( 1s
/su ๐)) |
35 | 34 | oveq1d 7429 |
. . . . . . . . 9
โข (๐ = ๐ โ (( 1s /su
๐) ยทs (
1s /su ๐)) = (( 1s /su
๐) ยทs (
1s /su ๐))) |
36 | 35 | oveq2d 7430 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐)))) |
37 | 36 | eqeq2d 2738 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ต๐น( 1s /su ๐)) = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) โ (๐ต๐น( 1s /su ๐)) = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))))) |
38 | | oveq2 7422 |
. . . . . . . . . . 11
โข (๐ = 1s โ (
1s /su ๐) = ( 1s /su
1s )) |
39 | | divs1 28077 |
. . . . . . . . . . . 12
โข (
1s โ No โ ( 1s
/su 1s ) = 1s ) |
40 | 5, 39 | ax-mp 5 |
. . . . . . . . . . 11
โข (
1s /su 1s ) =
1s |
41 | 38, 40 | eqtrdi 2783 |
. . . . . . . . . 10
โข (๐ = 1s โ (
1s /su ๐) = 1s ) |
42 | 41 | oveq2d 7430 |
. . . . . . . . 9
โข (๐ = 1s โ ((
1s /su ๐) ยทs ( 1s
/su ๐)) = ((
1s /su ๐) ยทs 1s
)) |
43 | 42 | oveq2d 7430 |
. . . . . . . 8
โข (๐ = 1s โ (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) = (๐ต๐น(( 1s /su ๐) ยทs
1s ))) |
44 | 43 | eqeq2d 2738 |
. . . . . . 7
โข (๐ = 1s โ ((๐ต๐น( 1s /su ๐)) = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) โ (๐ต๐น( 1s /su ๐)) = (๐ต๐น(( 1s /su ๐) ยทs
1s )))) |
45 | 37, 44 | rspc2ev 3620 |
. . . . . 6
โข ((๐ โ โs
โง 1s โ โs โง (๐ต๐น( 1s /su ๐)) = (๐ต๐น(( 1s /su ๐) ยทs
1s ))) โ โ๐ โ โs โ๐ โ โs
(๐ต๐น( 1s /su ๐)) = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐)))) |
46 | 33, 45 | mp3an2 1446 |
. . . . 5
โข ((๐ โ โs
โง (๐ต๐น( 1s /su ๐)) = (๐ต๐น(( 1s /su ๐) ยทs
1s ))) โ โ๐ โ โs โ๐ โ โs
(๐ต๐น( 1s /su ๐)) = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐)))) |
47 | 32, 46 | mpdan 686 |
. . . 4
โข (๐ โ โs
โ โ๐ โ
โs โ๐ โ โs (๐ต๐น( 1s /su ๐)) = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐)))) |
48 | | eqeq1 2731 |
. . . . 5
โข (๐ด = (๐ต๐น( 1s /su ๐)) โ (๐ด = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) โ (๐ต๐น( 1s /su ๐)) = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))))) |
49 | 48 | 2rexbidv 3214 |
. . . 4
โข (๐ด = (๐ต๐น( 1s /su ๐)) โ (โ๐ โ โs
โ๐ โ
โs ๐ด =
(๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) โ โ๐ โ โs โ๐ โ โs
(๐ต๐น( 1s /su ๐)) = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))))) |
50 | 47, 49 | syl5ibrcom 246 |
. . 3
โข (๐ โ โs
โ (๐ด = (๐ต๐น( 1s /su ๐)) โ โ๐ โ โs
โ๐ โ
โs ๐ด =
(๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))))) |
51 | 50 | rexlimiv 3143 |
. 2
โข
(โ๐ โ
โs ๐ด =
(๐ต๐น( 1s /su ๐)) โ โ๐ โ โs
โ๐ โ
โs ๐ด =
(๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐)))) |
52 | 25, 51 | impbii 208 |
1
โข
(โ๐ โ
โs โ๐ โ โs ๐ด = (๐ต๐น(( 1s /su ๐) ยทs (
1s /su ๐))) โ โ๐ โ โs ๐ด = (๐ต๐น( 1s /su ๐))) |