Step | Hyp | Ref
| Expression |
1 | | 2sqlem6.1 |
. 2
โข (๐ โ ๐ด โ โ) |
2 | | 2sqlem6.2 |
. . 3
โข (๐ โ ๐ต โ โ) |
3 | | 2sqlem6.3 |
. . 3
โข (๐ โ โ๐ โ โ (๐ โฅ ๐ต โ ๐ โ ๐)) |
4 | | breq2 5110 |
. . . . . . 7
โข (๐ฅ = 1 โ (๐ โฅ ๐ฅ โ ๐ โฅ 1)) |
5 | 4 | imbi1d 342 |
. . . . . 6
โข (๐ฅ = 1 โ ((๐ โฅ ๐ฅ โ ๐ โ ๐) โ (๐ โฅ 1 โ ๐ โ ๐))) |
6 | 5 | ralbidv 3175 |
. . . . 5
โข (๐ฅ = 1 โ (โ๐ โ โ (๐ โฅ ๐ฅ โ ๐ โ ๐) โ โ๐ โ โ (๐ โฅ 1 โ ๐ โ ๐))) |
7 | | oveq2 7366 |
. . . . . . . 8
โข (๐ฅ = 1 โ (๐ ยท ๐ฅ) = (๐ ยท 1)) |
8 | 7 | eleq1d 2823 |
. . . . . . 7
โข (๐ฅ = 1 โ ((๐ ยท ๐ฅ) โ ๐ โ (๐ ยท 1) โ ๐)) |
9 | 8 | imbi1d 342 |
. . . . . 6
โข (๐ฅ = 1 โ (((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐) โ ((๐ ยท 1) โ ๐ โ ๐ โ ๐))) |
10 | 9 | ralbidv 3175 |
. . . . 5
โข (๐ฅ = 1 โ (โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท 1) โ ๐ โ ๐ โ ๐))) |
11 | 6, 10 | imbi12d 345 |
. . . 4
โข (๐ฅ = 1 โ ((โ๐ โ โ (๐ โฅ ๐ฅ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐)) โ (โ๐ โ โ (๐ โฅ 1 โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท 1) โ ๐ โ ๐ โ ๐)))) |
12 | | breq2 5110 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐ฆ)) |
13 | 12 | imbi1d 342 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ((๐ โฅ ๐ฅ โ ๐ โ ๐) โ (๐ โฅ ๐ฆ โ ๐ โ ๐))) |
14 | 13 | ralbidv 3175 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (โ๐ โ โ (๐ โฅ ๐ฅ โ ๐ โ ๐) โ โ๐ โ โ (๐ โฅ ๐ฆ โ ๐ โ ๐))) |
15 | | oveq2 7366 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ (๐ ยท ๐ฅ) = (๐ ยท ๐ฆ)) |
16 | 15 | eleq1d 2823 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ ((๐ ยท ๐ฅ) โ ๐ โ (๐ ยท ๐ฆ) โ ๐)) |
17 | 16 | imbi1d 342 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐) โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐))) |
18 | 17 | ralbidv 3175 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐))) |
19 | 14, 18 | imbi12d 345 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((โ๐ โ โ (๐ โฅ ๐ฅ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐)) โ (โ๐ โ โ (๐ โฅ ๐ฆ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)))) |
20 | | breq2 5110 |
. . . . . . 7
โข (๐ฅ = ๐ง โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐ง)) |
21 | 20 | imbi1d 342 |
. . . . . 6
โข (๐ฅ = ๐ง โ ((๐ โฅ ๐ฅ โ ๐ โ ๐) โ (๐ โฅ ๐ง โ ๐ โ ๐))) |
22 | 21 | ralbidv 3175 |
. . . . 5
โข (๐ฅ = ๐ง โ (โ๐ โ โ (๐ โฅ ๐ฅ โ ๐ โ ๐) โ โ๐ โ โ (๐ โฅ ๐ง โ ๐ โ ๐))) |
23 | | oveq2 7366 |
. . . . . . . 8
โข (๐ฅ = ๐ง โ (๐ ยท ๐ฅ) = (๐ ยท ๐ง)) |
24 | 23 | eleq1d 2823 |
. . . . . . 7
โข (๐ฅ = ๐ง โ ((๐ ยท ๐ฅ) โ ๐ โ (๐ ยท ๐ง) โ ๐)) |
25 | 24 | imbi1d 342 |
. . . . . 6
โข (๐ฅ = ๐ง โ (((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐) โ ((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐))) |
26 | 25 | ralbidv 3175 |
. . . . 5
โข (๐ฅ = ๐ง โ (โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐))) |
27 | 22, 26 | imbi12d 345 |
. . . 4
โข (๐ฅ = ๐ง โ ((โ๐ โ โ (๐ โฅ ๐ฅ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐)) โ (โ๐ โ โ (๐ โฅ ๐ง โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐)))) |
28 | | breq2 5110 |
. . . . . . 7
โข (๐ฅ = (๐ฆ ยท ๐ง) โ (๐ โฅ ๐ฅ โ ๐ โฅ (๐ฆ ยท ๐ง))) |
29 | 28 | imbi1d 342 |
. . . . . 6
โข (๐ฅ = (๐ฆ ยท ๐ง) โ ((๐ โฅ ๐ฅ โ ๐ โ ๐) โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐))) |
30 | 29 | ralbidv 3175 |
. . . . 5
โข (๐ฅ = (๐ฆ ยท ๐ง) โ (โ๐ โ โ (๐ โฅ ๐ฅ โ ๐ โ ๐) โ โ๐ โ โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐))) |
31 | | oveq2 7366 |
. . . . . . . 8
โข (๐ฅ = (๐ฆ ยท ๐ง) โ (๐ ยท ๐ฅ) = (๐ ยท (๐ฆ ยท ๐ง))) |
32 | 31 | eleq1d 2823 |
. . . . . . 7
โข (๐ฅ = (๐ฆ ยท ๐ง) โ ((๐ ยท ๐ฅ) โ ๐ โ (๐ ยท (๐ฆ ยท ๐ง)) โ ๐)) |
33 | 32 | imbi1d 342 |
. . . . . 6
โข (๐ฅ = (๐ฆ ยท ๐ง) โ (((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐) โ ((๐ ยท (๐ฆ ยท ๐ง)) โ ๐ โ ๐ โ ๐))) |
34 | 33 | ralbidv 3175 |
. . . . 5
โข (๐ฅ = (๐ฆ ยท ๐ง) โ (โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท (๐ฆ ยท ๐ง)) โ ๐ โ ๐ โ ๐))) |
35 | 30, 34 | imbi12d 345 |
. . . 4
โข (๐ฅ = (๐ฆ ยท ๐ง) โ ((โ๐ โ โ (๐ โฅ ๐ฅ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐)) โ (โ๐ โ โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท (๐ฆ ยท ๐ง)) โ ๐ โ ๐ โ ๐)))) |
36 | | breq2 5110 |
. . . . . . 7
โข (๐ฅ = ๐ต โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐ต)) |
37 | 36 | imbi1d 342 |
. . . . . 6
โข (๐ฅ = ๐ต โ ((๐ โฅ ๐ฅ โ ๐ โ ๐) โ (๐ โฅ ๐ต โ ๐ โ ๐))) |
38 | 37 | ralbidv 3175 |
. . . . 5
โข (๐ฅ = ๐ต โ (โ๐ โ โ (๐ โฅ ๐ฅ โ ๐ โ ๐) โ โ๐ โ โ (๐ โฅ ๐ต โ ๐ โ ๐))) |
39 | | oveq2 7366 |
. . . . . . . 8
โข (๐ฅ = ๐ต โ (๐ ยท ๐ฅ) = (๐ ยท ๐ต)) |
40 | 39 | eleq1d 2823 |
. . . . . . 7
โข (๐ฅ = ๐ต โ ((๐ ยท ๐ฅ) โ ๐ โ (๐ ยท ๐ต) โ ๐)) |
41 | 40 | imbi1d 342 |
. . . . . 6
โข (๐ฅ = ๐ต โ (((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐) โ ((๐ ยท ๐ต) โ ๐ โ ๐ โ ๐))) |
42 | 41 | ralbidv 3175 |
. . . . 5
โข (๐ฅ = ๐ต โ (โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ต) โ ๐ โ ๐ โ ๐))) |
43 | 38, 42 | imbi12d 345 |
. . . 4
โข (๐ฅ = ๐ต โ ((โ๐ โ โ (๐ โฅ ๐ฅ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐)) โ (โ๐ โ โ (๐ โฅ ๐ต โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ต) โ ๐ โ ๐ โ ๐)))) |
44 | | nncn 12162 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
45 | 44 | mulid1d 11173 |
. . . . . . . 8
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
46 | 45 | eleq1d 2823 |
. . . . . . 7
โข (๐ โ โ โ ((๐ ยท 1) โ ๐ โ ๐ โ ๐)) |
47 | 46 | biimpd 228 |
. . . . . 6
โข (๐ โ โ โ ((๐ ยท 1) โ ๐ โ ๐ โ ๐)) |
48 | 47 | rgen 3067 |
. . . . 5
โข
โ๐ โ
โ ((๐ ยท 1)
โ ๐ โ ๐ โ ๐) |
49 | 48 | a1i 11 |
. . . 4
โข
(โ๐ โ
โ (๐ โฅ 1 โ
๐ โ ๐) โ โ๐ โ โ ((๐ ยท 1) โ ๐ โ ๐ โ ๐)) |
50 | | breq1 5109 |
. . . . . . 7
โข (๐ = ๐ฅ โ (๐ โฅ ๐ฅ โ ๐ฅ โฅ ๐ฅ)) |
51 | | eleq1 2826 |
. . . . . . 7
โข (๐ = ๐ฅ โ (๐ โ ๐ โ ๐ฅ โ ๐)) |
52 | 50, 51 | imbi12d 345 |
. . . . . 6
โข (๐ = ๐ฅ โ ((๐ โฅ ๐ฅ โ ๐ โ ๐) โ (๐ฅ โฅ ๐ฅ โ ๐ฅ โ ๐))) |
53 | 52 | rspcv 3578 |
. . . . 5
โข (๐ฅ โ โ โ
(โ๐ โ โ
(๐ โฅ ๐ฅ โ ๐ โ ๐) โ (๐ฅ โฅ ๐ฅ โ ๐ฅ โ ๐))) |
54 | | prmz 16552 |
. . . . . . 7
โข (๐ฅ โ โ โ ๐ฅ โ
โค) |
55 | | iddvds 16153 |
. . . . . . 7
โข (๐ฅ โ โค โ ๐ฅ โฅ ๐ฅ) |
56 | 54, 55 | syl 17 |
. . . . . 6
โข (๐ฅ โ โ โ ๐ฅ โฅ ๐ฅ) |
57 | | 2sq.1 |
. . . . . . . . . 10
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) |
58 | | simprl 770 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง ๐ฅ โ ๐) โง (๐ โ โ โง (๐ ยท ๐ฅ) โ ๐)) โ ๐ โ โ) |
59 | | simpll 766 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง ๐ฅ โ ๐) โง (๐ โ โ โง (๐ ยท ๐ฅ) โ ๐)) โ ๐ฅ โ โ) |
60 | | simprr 772 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง ๐ฅ โ ๐) โง (๐ โ โ โง (๐ ยท ๐ฅ) โ ๐)) โ (๐ ยท ๐ฅ) โ ๐) |
61 | | simplr 768 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง ๐ฅ โ ๐) โง (๐ โ โ โง (๐ ยท ๐ฅ) โ ๐)) โ ๐ฅ โ ๐) |
62 | 57, 58, 59, 60, 61 | 2sqlem5 26773 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง ๐ฅ โ ๐) โง (๐ โ โ โง (๐ ยท ๐ฅ) โ ๐)) โ ๐ โ ๐) |
63 | 62 | expr 458 |
. . . . . . . 8
โข (((๐ฅ โ โ โง ๐ฅ โ ๐) โง ๐ โ โ) โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐)) |
64 | 63 | ralrimiva 3144 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฅ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐)) |
65 | 64 | ex 414 |
. . . . . 6
โข (๐ฅ โ โ โ (๐ฅ โ ๐ โ โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐))) |
66 | 56, 65 | embantd 59 |
. . . . 5
โข (๐ฅ โ โ โ ((๐ฅ โฅ ๐ฅ โ ๐ฅ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐))) |
67 | 53, 66 | syld 47 |
. . . 4
โข (๐ฅ โ โ โ
(โ๐ โ โ
(๐ โฅ ๐ฅ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฅ) โ ๐ โ ๐ โ ๐))) |
68 | | anim12 808 |
. . . . 5
โข
(((โ๐ โ
โ (๐ โฅ ๐ฆ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง (โ๐ โ โ (๐ โฅ ๐ง โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐))) โ ((โ๐ โ โ (๐ โฅ ๐ฆ โ ๐ โ ๐) โง โ๐ โ โ (๐ โฅ ๐ง โ ๐ โ ๐)) โ (โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐) โง โ๐ โ โ ((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐)))) |
69 | | simpr 486 |
. . . . . . . . . . . . . 14
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ ๐ โ
โ) |
70 | | eluzelz 12774 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ
(โคโฅโ2) โ ๐ฆ โ โค) |
71 | 70 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ ๐ฆ โ
โค) |
72 | | eluzelz 12774 |
. . . . . . . . . . . . . . 15
โข (๐ง โ
(โคโฅโ2) โ ๐ง โ โค) |
73 | 72 | ad2antlr 726 |
. . . . . . . . . . . . . 14
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ ๐ง โ
โค) |
74 | | euclemma 16590 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ฆ โ โค โง ๐ง โ โค) โ (๐ โฅ (๐ฆ ยท ๐ง) โ (๐ โฅ ๐ฆ โจ ๐ โฅ ๐ง))) |
75 | 69, 71, 73, 74 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ (๐ โฅ (๐ฆ ยท ๐ง) โ (๐ โฅ ๐ฆ โจ ๐ โฅ ๐ง))) |
76 | 75 | imbi1d 342 |
. . . . . . . . . . . 12
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ ((๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐) โ ((๐ โฅ ๐ฆ โจ ๐ โฅ ๐ง) โ ๐ โ ๐))) |
77 | | jaob 961 |
. . . . . . . . . . . 12
โข (((๐ โฅ ๐ฆ โจ ๐ โฅ ๐ง) โ ๐ โ ๐) โ ((๐ โฅ ๐ฆ โ ๐ โ ๐) โง (๐ โฅ ๐ง โ ๐ โ ๐))) |
78 | 76, 77 | bitrdi 287 |
. . . . . . . . . . 11
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ ((๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐) โ ((๐ โฅ ๐ฆ โ ๐ โ ๐) โง (๐ โฅ ๐ง โ ๐ โ ๐)))) |
79 | 78 | ralbidva 3173 |
. . . . . . . . . 10
โข ((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โ (โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐) โ โ๐ โ โ ((๐ โฅ ๐ฆ โ ๐ โ ๐) โง (๐ โฅ ๐ง โ ๐ โ ๐)))) |
80 | | r19.26 3115 |
. . . . . . . . . 10
โข
(โ๐ โ
โ ((๐ โฅ ๐ฆ โ ๐ โ ๐) โง (๐ โฅ ๐ง โ ๐ โ ๐)) โ (โ๐ โ โ (๐ โฅ ๐ฆ โ ๐ โ ๐) โง โ๐ โ โ (๐ โฅ ๐ง โ ๐ โ ๐))) |
81 | 79, 80 | bitrdi 287 |
. . . . . . . . 9
โข ((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โ (โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐) โ (โ๐ โ โ (๐ โฅ ๐ฆ โ ๐ โ ๐) โง โ๐ โ โ (๐ โฅ ๐ง โ ๐ โ ๐)))) |
82 | 81 | biimpa 478 |
. . . . . . . 8
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โ (โ๐ โ โ (๐ โฅ ๐ฆ โ ๐ โ ๐) โง โ๐ โ โ (๐ โฅ ๐ง โ ๐ โ ๐))) |
83 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ ยท ๐ฆ) = (๐ ยท ๐ฆ)) |
84 | 83 | eleq1d 2823 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐ ยท ๐ฆ) โ ๐ โ (๐ ยท ๐ฆ) โ ๐)) |
85 | | eleq1 2826 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ โ ๐ โ ๐ โ ๐)) |
86 | 84, 85 | imbi12d 345 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐) โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐))) |
87 | 86 | cbvralvw 3226 |
. . . . . . . . . 10
โข
(โ๐ โ
โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) |
88 | 44 | adantl 483 |
. . . . . . . . . . . . . . 15
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ ๐ โ โ) |
89 | | uzssz 12785 |
. . . . . . . . . . . . . . . . 17
โข
(โคโฅโ2) โ โค |
90 | | zsscn 12508 |
. . . . . . . . . . . . . . . . 17
โข โค
โ โ |
91 | 89, 90 | sstri 3954 |
. . . . . . . . . . . . . . . 16
โข
(โคโฅโ2) โ โ |
92 | | simpll 766 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โ ๐ฆ โ
(โคโฅโ2)) |
93 | 92 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ ๐ฆ โ
(โคโฅโ2)) |
94 | 91, 93 | sselid 3943 |
. . . . . . . . . . . . . . 15
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ ๐ฆ โ โ) |
95 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โ ๐ง โ
(โคโฅโ2)) |
96 | 95 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ ๐ง โ
(โคโฅโ2)) |
97 | 91, 96 | sselid 3943 |
. . . . . . . . . . . . . . 15
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ ๐ง โ โ) |
98 | | mul32 11322 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ฆ โ โ โง ๐ง โ โ) โ ((๐ ยท ๐ฆ) ยท ๐ง) = ((๐ ยท ๐ง) ยท ๐ฆ)) |
99 | | mulass 11140 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ฆ โ โ โง ๐ง โ โ) โ ((๐ ยท ๐ฆ) ยท ๐ง) = (๐ ยท (๐ฆ ยท ๐ง))) |
100 | 98, 99 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ฆ โ โ โง ๐ง โ โ) โ ((๐ ยท ๐ง) ยท ๐ฆ) = (๐ ยท (๐ฆ ยท ๐ง))) |
101 | 88, 94, 97, 100 | syl3anc 1372 |
. . . . . . . . . . . . . 14
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ ((๐ ยท ๐ง) ยท ๐ฆ) = (๐ ยท (๐ฆ ยท ๐ง))) |
102 | 101 | eleq1d 2823 |
. . . . . . . . . . . . 13
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ (((๐ ยท ๐ง) ยท ๐ฆ) โ ๐ โ (๐ ยท (๐ฆ ยท ๐ง)) โ ๐)) |
103 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ ๐ โ โ) |
104 | | eluz2nn 12810 |
. . . . . . . . . . . . . . . 16
โข (๐ง โ
(โคโฅโ2) โ ๐ง โ โ) |
105 | 96, 104 | syl 17 |
. . . . . . . . . . . . . . 15
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ ๐ง โ โ) |
106 | 103, 105 | nnmulcld 12207 |
. . . . . . . . . . . . . 14
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ (๐ ยท ๐ง) โ โ) |
107 | | simplr 768 |
. . . . . . . . . . . . . 14
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) |
108 | | oveq1 7365 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ ยท ๐ง) โ (๐ ยท ๐ฆ) = ((๐ ยท ๐ง) ยท ๐ฆ)) |
109 | 108 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ ยท ๐ง) โ ((๐ ยท ๐ฆ) โ ๐ โ ((๐ ยท ๐ง) ยท ๐ฆ) โ ๐)) |
110 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ ยท ๐ง) โ (๐ โ ๐ โ (๐ ยท ๐ง) โ ๐)) |
111 | 109, 110 | imbi12d 345 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ ยท ๐ง) โ (((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐) โ (((๐ ยท ๐ง) ยท ๐ฆ) โ ๐ โ (๐ ยท ๐ง) โ ๐))) |
112 | 111 | rspcv 3578 |
. . . . . . . . . . . . . 14
โข ((๐ ยท ๐ง) โ โ โ (โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐) โ (((๐ ยท ๐ง) ยท ๐ฆ) โ ๐ โ (๐ ยท ๐ง) โ ๐))) |
113 | 106, 107,
112 | sylc 65 |
. . . . . . . . . . . . 13
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ (((๐ ยท ๐ง) ยท ๐ฆ) โ ๐ โ (๐ ยท ๐ง) โ ๐)) |
114 | 102, 113 | sylbird 260 |
. . . . . . . . . . . 12
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ ((๐ ยท (๐ฆ ยท ๐ง)) โ ๐ โ (๐ ยท ๐ง) โ ๐)) |
115 | 114 | imim1d 82 |
. . . . . . . . . . 11
โข
(((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง ๐ โ โ) โ (((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐) โ ((๐ ยท (๐ฆ ยท ๐ง)) โ ๐ โ ๐ โ ๐))) |
116 | 115 | ralimdva 3165 |
. . . . . . . . . 10
โข ((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โ (โ๐ โ โ ((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท (๐ฆ ยท ๐ง)) โ ๐ โ ๐ โ ๐))) |
117 | 87, 116 | sylan2b 595 |
. . . . . . . . 9
โข ((((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โง โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โ (โ๐ โ โ ((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท (๐ฆ ยท ๐ง)) โ ๐ โ ๐ โ ๐))) |
118 | 117 | expimpd 455 |
. . . . . . . 8
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โ ((โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐) โง โ๐ โ โ ((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐)) โ โ๐ โ โ ((๐ ยท (๐ฆ ยท ๐ง)) โ ๐ โ ๐ โ ๐))) |
119 | 82, 118 | embantd 59 |
. . . . . . 7
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐)) โ (((โ๐ โ โ (๐ โฅ ๐ฆ โ ๐ โ ๐) โง โ๐ โ โ (๐ โฅ ๐ง โ ๐ โ ๐)) โ (โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐) โง โ๐ โ โ ((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐))) โ โ๐ โ โ ((๐ ยท (๐ฆ ยท ๐ง)) โ ๐ โ ๐ โ ๐))) |
120 | 119 | ex 414 |
. . . . . 6
โข ((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โ (โ๐ โ
โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐) โ (((โ๐ โ โ (๐ โฅ ๐ฆ โ ๐ โ ๐) โง โ๐ โ โ (๐ โฅ ๐ง โ ๐ โ ๐)) โ (โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐) โง โ๐ โ โ ((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐))) โ โ๐ โ โ ((๐ ยท (๐ฆ ยท ๐ง)) โ ๐ โ ๐ โ ๐)))) |
121 | 120 | com23 86 |
. . . . 5
โข ((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โ (((โ๐ โ
โ (๐ โฅ ๐ฆ โ ๐ โ ๐) โง โ๐ โ โ (๐ โฅ ๐ง โ ๐ โ ๐)) โ (โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐) โง โ๐ โ โ ((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐))) โ (โ๐ โ โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท (๐ฆ ยท ๐ง)) โ ๐ โ ๐ โ ๐)))) |
122 | 68, 121 | syl5 34 |
. . . 4
โข ((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โ (((โ๐ โ
โ (๐ โฅ ๐ฆ โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ฆ) โ ๐ โ ๐ โ ๐)) โง (โ๐ โ โ (๐ โฅ ๐ง โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ง) โ ๐ โ ๐ โ ๐))) โ (โ๐ โ โ (๐ โฅ (๐ฆ ยท ๐ง) โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท (๐ฆ ยท ๐ง)) โ ๐ โ ๐ โ ๐)))) |
123 | 11, 19, 27, 35, 43, 49, 67, 122 | prmind 16563 |
. . 3
โข (๐ต โ โ โ
(โ๐ โ โ
(๐ โฅ ๐ต โ ๐ โ ๐) โ โ๐ โ โ ((๐ ยท ๐ต) โ ๐ โ ๐ โ ๐))) |
124 | 2, 3, 123 | sylc 65 |
. 2
โข (๐ โ โ๐ โ โ ((๐ ยท ๐ต) โ ๐ โ ๐ โ ๐)) |
125 | | 2sqlem6.4 |
. 2
โข (๐ โ (๐ด ยท ๐ต) โ ๐) |
126 | | oveq1 7365 |
. . . . 5
โข (๐ = ๐ด โ (๐ ยท ๐ต) = (๐ด ยท ๐ต)) |
127 | 126 | eleq1d 2823 |
. . . 4
โข (๐ = ๐ด โ ((๐ ยท ๐ต) โ ๐ โ (๐ด ยท ๐ต) โ ๐)) |
128 | | eleq1 2826 |
. . . 4
โข (๐ = ๐ด โ (๐ โ ๐ โ ๐ด โ ๐)) |
129 | 127, 128 | imbi12d 345 |
. . 3
โข (๐ = ๐ด โ (((๐ ยท ๐ต) โ ๐ โ ๐ โ ๐) โ ((๐ด ยท ๐ต) โ ๐ โ ๐ด โ ๐))) |
130 | 129 | rspcv 3578 |
. 2
โข (๐ด โ โ โ
(โ๐ โ โ
((๐ ยท ๐ต) โ ๐ โ ๐ โ ๐) โ ((๐ด ยท ๐ต) โ ๐ โ ๐ด โ ๐))) |
131 | 1, 124, 125, 130 | syl3c 66 |
1
โข (๐ โ ๐ด โ ๐) |