Step | Hyp | Ref
| Expression |
1 | | df-nqqs 7346 |
. . 3
โข
Q = ((N ร N) /
~Q ) |
2 | | breq1 4006 |
. . . 4
โข
([โจ๐ฆ, ๐งโฉ]
~Q = ๐ด โ ([โจ๐ฆ, ๐งโฉ] ~Q
<Q [โจ๐ค, ๐ฃโฉ] ~Q โ
๐ด
<Q [โจ๐ค, ๐ฃโฉ] ~Q
)) |
3 | | oveq1 5881 |
. . . . . 6
โข
([โจ๐ฆ, ๐งโฉ]
~Q = ๐ด โ ([โจ๐ฆ, ๐งโฉ] ~Q
+Q ๐ฅ) = (๐ด +Q ๐ฅ)) |
4 | 3 | eqeq1d 2186 |
. . . . 5
โข
([โจ๐ฆ, ๐งโฉ]
~Q = ๐ด โ (([โจ๐ฆ, ๐งโฉ] ~Q
+Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q โ
(๐ด
+Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q
)) |
5 | 4 | rexbidv 2478 |
. . . 4
โข
([โจ๐ฆ, ๐งโฉ]
~Q = ๐ด โ (โ๐ฅ โ Q ([โจ๐ฆ, ๐งโฉ] ~Q
+Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q โ
โ๐ฅ โ
Q (๐ด
+Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q
)) |
6 | 2, 5 | imbi12d 234 |
. . 3
โข
([โจ๐ฆ, ๐งโฉ]
~Q = ๐ด โ (([โจ๐ฆ, ๐งโฉ] ~Q
<Q [โจ๐ค, ๐ฃโฉ] ~Q โ
โ๐ฅ โ
Q ([โจ๐ฆ,
๐งโฉ]
~Q +Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q ) โ
(๐ด
<Q [โจ๐ค, ๐ฃโฉ] ~Q โ
โ๐ฅ โ
Q (๐ด
+Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q
))) |
7 | | breq2 4007 |
. . . 4
โข
([โจ๐ค, ๐ฃโฉ]
~Q = ๐ต โ (๐ด <Q [โจ๐ค, ๐ฃโฉ] ~Q โ
๐ด
<Q ๐ต)) |
8 | | eqeq2 2187 |
. . . . 5
โข
([โจ๐ค, ๐ฃโฉ]
~Q = ๐ต โ ((๐ด +Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q โ
(๐ด
+Q ๐ฅ) = ๐ต)) |
9 | 8 | rexbidv 2478 |
. . . 4
โข
([โจ๐ค, ๐ฃโฉ]
~Q = ๐ต โ (โ๐ฅ โ Q (๐ด +Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q โ
โ๐ฅ โ
Q (๐ด
+Q ๐ฅ) = ๐ต)) |
10 | 7, 9 | imbi12d 234 |
. . 3
โข
([โจ๐ค, ๐ฃโฉ]
~Q = ๐ต โ ((๐ด <Q [โจ๐ค, ๐ฃโฉ] ~Q โ
โ๐ฅ โ
Q (๐ด
+Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q ) โ
(๐ด
<Q ๐ต โ โ๐ฅ โ Q (๐ด +Q ๐ฅ) = ๐ต))) |
11 | | ordpipqqs 7372 |
. . . 4
โข (((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ([โจ๐ฆ, ๐งโฉ] ~Q
<Q [โจ๐ค, ๐ฃโฉ] ~Q โ
(๐ฆ
ยทN ๐ฃ) <N (๐ง
ยทN ๐ค))) |
12 | | mulclpi 7326 |
. . . . . . . . 9
โข ((๐ฆ โ N โง
๐ฃ โ N)
โ (๐ฆ
ยทN ๐ฃ) โ N) |
13 | | mulclpi 7326 |
. . . . . . . . 9
โข ((๐ง โ N โง
๐ค โ N)
โ (๐ง
ยทN ๐ค) โ N) |
14 | 12, 13 | anim12i 338 |
. . . . . . . 8
โข (((๐ฆ โ N โง
๐ฃ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ((๐ฆ ยทN ๐ฃ) โ N โง
(๐ง
ยทN ๐ค) โ N)) |
15 | 14 | an42s 589 |
. . . . . . 7
โข (((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ((๐ฆ ยทN ๐ฃ) โ N โง
(๐ง
ยทN ๐ค) โ N)) |
16 | | ltexpi 7335 |
. . . . . . 7
โข (((๐ฆ
ยทN ๐ฃ) โ N โง (๐ง
ยทN ๐ค) โ N) โ ((๐ฆ
ยทN ๐ฃ) <N (๐ง
ยทN ๐ค) โ โ๐ข โ N ((๐ฆ ยทN ๐ฃ) +N
๐ข) = (๐ง ยทN ๐ค))) |
17 | 15, 16 | syl 14 |
. . . . . 6
โข (((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ((๐ฆ ยทN ๐ฃ) <N
(๐ง
ยทN ๐ค) โ โ๐ข โ N ((๐ฆ ยทN ๐ฃ) +N
๐ข) = (๐ง ยทN ๐ค))) |
18 | | df-rex 2461 |
. . . . . 6
โข
(โ๐ข โ
N ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค) โ โ๐ข(๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) |
19 | 17, 18 | bitrdi 196 |
. . . . 5
โข (((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ((๐ฆ ยทN ๐ฃ) <N
(๐ง
ยทN ๐ค) โ โ๐ข(๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค)))) |
20 | | simpll 527 |
. . . . . . . . . . . 12
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง ๐ข โ N) โ (๐ฆ โ N โง
๐ง โ
N)) |
21 | | simpr 110 |
. . . . . . . . . . . 12
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง ๐ข โ N) โ ๐ข โ
N) |
22 | | simpr 110 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ N โง
๐ง โ N)
โ ๐ง โ
N) |
23 | | simpr 110 |
. . . . . . . . . . . . . . 15
โข ((๐ค โ N โง
๐ฃ โ N)
โ ๐ฃ โ
N) |
24 | 22, 23 | anim12i 338 |
. . . . . . . . . . . . . 14
โข (((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ (๐ง โ N โง ๐ฃ โ
N)) |
25 | 24 | adantr 276 |
. . . . . . . . . . . . 13
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง ๐ข โ N) โ (๐ง โ N โง
๐ฃ โ
N)) |
26 | | mulclpi 7326 |
. . . . . . . . . . . . 13
โข ((๐ง โ N โง
๐ฃ โ N)
โ (๐ง
ยทN ๐ฃ) โ N) |
27 | 25, 26 | syl 14 |
. . . . . . . . . . . 12
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง ๐ข โ N) โ (๐ง
ยทN ๐ฃ) โ N) |
28 | 20, 21, 27 | jca32 310 |
. . . . . . . . . . 11
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง ๐ข โ N) โ ((๐ฆ โ N โง
๐ง โ N)
โง (๐ข โ
N โง (๐ง
ยทN ๐ฃ) โ N))) |
29 | 28 | adantrr 479 |
. . . . . . . . . 10
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ ((๐ฆ โ N โง ๐ง โ N) โง
(๐ข โ N
โง (๐ง
ยทN ๐ฃ) โ N))) |
30 | | addpipqqs 7368 |
. . . . . . . . . 10
โข (((๐ฆ โ N โง
๐ง โ N)
โง (๐ข โ
N โง (๐ง
ยทN ๐ฃ) โ N)) โ
([โจ๐ฆ, ๐งโฉ]
~Q +Q [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q ) = [โจ((๐ฆ ยทN (๐ง
ยทN ๐ฃ)) +N (๐ง
ยทN ๐ข)), (๐ง ยทN (๐ง
ยทN ๐ฃ))โฉ] ~Q
) |
31 | 29, 30 | syl 14 |
. . . . . . . . 9
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ ([โจ๐ฆ, ๐งโฉ] ~Q
+Q [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q ) = [โจ((๐ฆ ยทN (๐ง
ยทN ๐ฃ)) +N (๐ง
ยทN ๐ข)), (๐ง ยทN (๐ง
ยทN ๐ฃ))โฉ] ~Q
) |
32 | | simplll 533 |
. . . . . . . . . . . . . . 15
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ ๐ฆ โ N) |
33 | | simpllr 534 |
. . . . . . . . . . . . . . 15
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ ๐ง โ N) |
34 | | simplrr 536 |
. . . . . . . . . . . . . . 15
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ ๐ฃ โ N) |
35 | | mulcompig 7329 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ N โง
๐ โ N)
โ (๐
ยทN ๐) = (๐ ยทN ๐)) |
36 | 35 | adantl 277 |
. . . . . . . . . . . . . . 15
โข
(((((๐ฆ โ
N โง ๐ง
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โง
(๐ข โ N
โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โง (๐ โ N โง ๐ โ N)) โ
(๐
ยทN ๐) = (๐ ยทN ๐)) |
37 | | mulasspig 7330 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ N โง
๐ โ N
โง โ โ
N) โ ((๐
ยทN ๐) ยทN โ) = (๐ ยทN (๐
ยทN โ))) |
38 | 37 | adantl 277 |
. . . . . . . . . . . . . . 15
โข
(((((๐ฆ โ
N โง ๐ง
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โง
(๐ข โ N
โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โง (๐ โ N โง ๐ โ N โง
โ โ N))
โ ((๐
ยทN ๐) ยทN โ) = (๐ ยทN (๐
ยทN โ))) |
39 | 32, 33, 34, 36, 38 | caov12d 6055 |
. . . . . . . . . . . . . 14
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ (๐ฆ ยทN (๐ง
ยทN ๐ฃ)) = (๐ง ยทN (๐ฆ
ยทN ๐ฃ))) |
40 | 39 | oveq1d 5889 |
. . . . . . . . . . . . 13
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ ((๐ฆ ยทN (๐ง
ยทN ๐ฃ)) +N (๐ง
ยทN ๐ข)) = ((๐ง ยทN (๐ฆ
ยทN ๐ฃ)) +N (๐ง
ยทN ๐ข))) |
41 | 32, 34, 12 | syl2anc 411 |
. . . . . . . . . . . . . 14
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ (๐ฆ ยทN ๐ฃ) โ
N) |
42 | | simprl 529 |
. . . . . . . . . . . . . 14
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ ๐ข โ N) |
43 | | distrpig 7331 |
. . . . . . . . . . . . . 14
โข ((๐ง โ N โง
(๐ฆ
ยทN ๐ฃ) โ N โง ๐ข โ N) โ
(๐ง
ยทN ((๐ฆ ยทN ๐ฃ) +N
๐ข)) = ((๐ง ยทN (๐ฆ
ยทN ๐ฃ)) +N (๐ง
ยทN ๐ข))) |
44 | 33, 41, 42, 43 | syl3anc 1238 |
. . . . . . . . . . . . 13
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ (๐ง ยทN ((๐ฆ
ยทN ๐ฃ) +N ๐ข)) = ((๐ง ยทN (๐ฆ
ยทN ๐ฃ)) +N (๐ง
ยทN ๐ข))) |
45 | 40, 44 | eqtr4d 2213 |
. . . . . . . . . . . 12
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ ((๐ฆ ยทN (๐ง
ยทN ๐ฃ)) +N (๐ง
ยทN ๐ข)) = (๐ง ยทN ((๐ฆ
ยทN ๐ฃ) +N ๐ข))) |
46 | 45 | opeq1d 3784 |
. . . . . . . . . . 11
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ โจ((๐ฆ
ยทN (๐ง ยทN ๐ฃ)) +N
(๐ง
ยทN ๐ข)), (๐ง ยทN (๐ง
ยทN ๐ฃ))โฉ = โจ(๐ง ยทN ((๐ฆ
ยทN ๐ฃ) +N ๐ข)), (๐ง ยทN (๐ง
ยทN ๐ฃ))โฉ) |
47 | 46 | eceq1d 6570 |
. . . . . . . . . 10
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ [โจ((๐ฆ
ยทN (๐ง ยทN ๐ฃ)) +N
(๐ง
ยทN ๐ข)), (๐ง ยทN (๐ง
ยทN ๐ฃ))โฉ] ~Q =
[โจ(๐ง
ยทN ((๐ฆ ยทN ๐ฃ) +N
๐ข)), (๐ง ยทN (๐ง
ยทN ๐ฃ))โฉ] ~Q
) |
48 | | simpllr 534 |
. . . . . . . . . . . . 13
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง ๐ข โ N) โ ๐ง โ
N) |
49 | 12 | ad2ant2rl 511 |
. . . . . . . . . . . . . 14
โข (((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ (๐ฆ ยทN ๐ฃ) โ
N) |
50 | | addclpi 7325 |
. . . . . . . . . . . . . 14
โข (((๐ฆ
ยทN ๐ฃ) โ N โง ๐ข โ N) โ
((๐ฆ
ยทN ๐ฃ) +N ๐ข) โ
N) |
51 | 49, 50 | sylan 283 |
. . . . . . . . . . . . 13
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง ๐ข โ N) โ ((๐ฆ
ยทN ๐ฃ) +N ๐ข) โ
N) |
52 | 48, 51, 27 | 3jca 1177 |
. . . . . . . . . . . 12
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง ๐ข โ N) โ (๐ง โ N โง
((๐ฆ
ยทN ๐ฃ) +N ๐ข) โ N โง
(๐ง
ยทN ๐ฃ) โ N)) |
53 | 52 | adantrr 479 |
. . . . . . . . . . 11
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ (๐ง โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) โ N โง
(๐ง
ยทN ๐ฃ) โ N)) |
54 | | mulcanenqec 7384 |
. . . . . . . . . . 11
โข ((๐ง โ N โง
((๐ฆ
ยทN ๐ฃ) +N ๐ข) โ N โง
(๐ง
ยทN ๐ฃ) โ N) โ
[โจ(๐ง
ยทN ((๐ฆ ยทN ๐ฃ) +N
๐ข)), (๐ง ยทN (๐ง
ยทN ๐ฃ))โฉ] ~Q =
[โจ((๐ฆ
ยทN ๐ฃ) +N ๐ข), (๐ง ยทN ๐ฃ)โฉ]
~Q ) |
55 | 53, 54 | syl 14 |
. . . . . . . . . 10
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ [โจ(๐ง
ยทN ((๐ฆ ยทN ๐ฃ) +N
๐ข)), (๐ง ยทN (๐ง
ยทN ๐ฃ))โฉ] ~Q =
[โจ((๐ฆ
ยทN ๐ฃ) +N ๐ข), (๐ง ยทN ๐ฃ)โฉ]
~Q ) |
56 | 47, 55 | eqtrd 2210 |
. . . . . . . . 9
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ [โจ((๐ฆ
ยทN (๐ง ยทN ๐ฃ)) +N
(๐ง
ยทN ๐ข)), (๐ง ยทN (๐ง
ยทN ๐ฃ))โฉ] ~Q =
[โจ((๐ฆ
ยทN ๐ฃ) +N ๐ข), (๐ง ยทN ๐ฃ)โฉ]
~Q ) |
57 | | 3anass 982 |
. . . . . . . . . . . . . 14
โข ((๐ง โ N โง
๐ค โ N
โง ๐ฃ โ
N) โ (๐ง
โ N โง (๐ค โ N โง ๐ฃ โ
N))) |
58 | 57 | biimpri 133 |
. . . . . . . . . . . . 13
โข ((๐ง โ N โง
(๐ค โ N
โง ๐ฃ โ
N)) โ (๐ง
โ N โง ๐ค โ N โง ๐ฃ โ
N)) |
59 | 58 | adantll 476 |
. . . . . . . . . . . 12
โข (((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ (๐ง โ N โง ๐ค โ N โง
๐ฃ โ
N)) |
60 | 59 | anim1i 340 |
. . . . . . . . . . 11
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง ((๐ฆ ยทN ๐ฃ) +N
๐ข) = (๐ง ยทN ๐ค)) โ ((๐ง โ N โง ๐ค โ N โง
๐ฃ โ N)
โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) |
61 | 60 | adantrl 478 |
. . . . . . . . . 10
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ ((๐ง โ N โง ๐ค โ N โง
๐ฃ โ N)
โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) |
62 | | opeq1 3778 |
. . . . . . . . . . . 12
โข (((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค) โ โจ((๐ฆ
ยทN ๐ฃ) +N ๐ข), (๐ง ยทN ๐ฃ)โฉ = โจ(๐ง
ยทN ๐ค), (๐ง ยทN ๐ฃ)โฉ) |
63 | 62 | eceq1d 6570 |
. . . . . . . . . . 11
โข (((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค) โ [โจ((๐ฆ
ยทN ๐ฃ) +N ๐ข), (๐ง ยทN ๐ฃ)โฉ]
~Q = [โจ(๐ง ยทN ๐ค), (๐ง ยทN ๐ฃ)โฉ]
~Q ) |
64 | | mulcanenqec 7384 |
. . . . . . . . . . 11
โข ((๐ง โ N โง
๐ค โ N
โง ๐ฃ โ
N) โ [โจ(๐ง ยทN ๐ค), (๐ง ยทN ๐ฃ)โฉ]
~Q = [โจ๐ค, ๐ฃโฉ] ~Q
) |
65 | 63, 64 | sylan9eqr 2232 |
. . . . . . . . . 10
โข (((๐ง โ N โง
๐ค โ N
โง ๐ฃ โ
N) โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค)) โ [โจ((๐ฆ
ยทN ๐ฃ) +N ๐ข), (๐ง ยทN ๐ฃ)โฉ]
~Q = [โจ๐ค, ๐ฃโฉ] ~Q
) |
66 | 61, 65 | syl 14 |
. . . . . . . . 9
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ [โจ((๐ฆ
ยทN ๐ฃ) +N ๐ข), (๐ง ยทN ๐ฃ)โฉ]
~Q = [โจ๐ค, ๐ฃโฉ] ~Q
) |
67 | 31, 56, 66 | 3eqtrd 2214 |
. . . . . . . 8
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ ([โจ๐ฆ, ๐งโฉ] ~Q
+Q [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q ) = [โจ๐ค, ๐ฃโฉ] ~Q
) |
68 | 33, 34, 26 | syl2anc 411 |
. . . . . . . . . . 11
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ (๐ง ยทN ๐ฃ) โ
N) |
69 | | opelxpi 4658 |
. . . . . . . . . . . 12
โข ((๐ข โ N โง
(๐ง
ยทN ๐ฃ) โ N) โ โจ๐ข, (๐ง ยทN ๐ฃ)โฉ โ (N
ร N)) |
70 | | enqex 7358 |
. . . . . . . . . . . . 13
โข
~Q โ V |
71 | 70 | ecelqsi 6588 |
. . . . . . . . . . . 12
โข
(โจ๐ข, (๐ง
ยทN ๐ฃ)โฉ โ (N ร
N) โ [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q โ ((N ร N)
/ ~Q )) |
72 | 69, 71 | syl 14 |
. . . . . . . . . . 11
โข ((๐ข โ N โง
(๐ง
ยทN ๐ฃ) โ N) โ [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q โ ((N ร N)
/ ~Q )) |
73 | 42, 68, 72 | syl2anc 411 |
. . . . . . . . . 10
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q โ ((N ร N)
/ ~Q )) |
74 | 73, 1 | eleqtrrdi 2271 |
. . . . . . . . 9
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q โ Q) |
75 | | oveq2 5882 |
. . . . . . . . . . 11
โข (๐ฅ = [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q โ ([โจ๐ฆ, ๐งโฉ] ~Q
+Q ๐ฅ) = ([โจ๐ฆ, ๐งโฉ] ~Q
+Q [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q )) |
76 | 75 | eqeq1d 2186 |
. . . . . . . . . 10
โข (๐ฅ = [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q โ (([โจ๐ฆ, ๐งโฉ] ~Q
+Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q โ
([โจ๐ฆ, ๐งโฉ]
~Q +Q [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q ) = [โจ๐ค, ๐ฃโฉ] ~Q
)) |
77 | 76 | adantl 277 |
. . . . . . . . 9
โข
(((((๐ฆ โ
N โง ๐ง
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โง
(๐ข โ N
โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โง ๐ฅ = [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q ) โ (([โจ๐ฆ, ๐งโฉ] ~Q
+Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q โ
([โจ๐ฆ, ๐งโฉ]
~Q +Q [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q ) = [โจ๐ค, ๐ฃโฉ] ~Q
)) |
78 | 74, 77 | rspcedv 2845 |
. . . . . . . 8
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ (([โจ๐ฆ, ๐งโฉ] ~Q
+Q [โจ๐ข, (๐ง ยทN ๐ฃ)โฉ]
~Q ) = [โจ๐ค, ๐ฃโฉ] ~Q โ
โ๐ฅ โ
Q ([โจ๐ฆ,
๐งโฉ]
~Q +Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q
)) |
79 | 67, 78 | mpd 13 |
. . . . . . 7
โข ((((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค))) โ โ๐ฅ โ Q
([โจ๐ฆ, ๐งโฉ]
~Q +Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q
) |
80 | 79 | ex 115 |
. . . . . 6
โข (((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ((๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค)) โ โ๐ฅ โ Q
([โจ๐ฆ, ๐งโฉ]
~Q +Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q
)) |
81 | 80 | exlimdv 1819 |
. . . . 5
โข (((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ (โ๐ข(๐ข โ N โง ((๐ฆ
ยทN ๐ฃ) +N ๐ข) = (๐ง ยทN ๐ค)) โ โ๐ฅ โ Q
([โจ๐ฆ, ๐งโฉ]
~Q +Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q
)) |
82 | 19, 81 | sylbid 150 |
. . . 4
โข (((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ((๐ฆ ยทN ๐ฃ) <N
(๐ง
ยทN ๐ค) โ โ๐ฅ โ Q ([โจ๐ฆ, ๐งโฉ] ~Q
+Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q
)) |
83 | 11, 82 | sylbid 150 |
. . 3
โข (((๐ฆ โ N โง
๐ง โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ([โจ๐ฆ, ๐งโฉ] ~Q
<Q [โจ๐ค, ๐ฃโฉ] ~Q โ
โ๐ฅ โ
Q ([โจ๐ฆ,
๐งโฉ]
~Q +Q ๐ฅ) = [โจ๐ค, ๐ฃโฉ] ~Q
)) |
84 | 1, 6, 10, 83 | 2ecoptocl 6622 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
<Q ๐ต โ โ๐ฅ โ Q (๐ด +Q ๐ฅ) = ๐ต)) |
85 | | ltaddnq 7405 |
. . . . 5
โข ((๐ด โ Q โง
๐ฅ โ Q)
โ ๐ด
<Q (๐ด +Q ๐ฅ)) |
86 | | breq2 4007 |
. . . . 5
โข ((๐ด +Q
๐ฅ) = ๐ต โ (๐ด <Q (๐ด +Q
๐ฅ) โ ๐ด <Q ๐ต)) |
87 | 85, 86 | syl5ibcom 155 |
. . . 4
โข ((๐ด โ Q โง
๐ฅ โ Q)
โ ((๐ด
+Q ๐ฅ) = ๐ต โ ๐ด <Q ๐ต)) |
88 | 87 | rexlimdva 2594 |
. . 3
โข (๐ด โ Q โ
(โ๐ฅ โ
Q (๐ด
+Q ๐ฅ) = ๐ต โ ๐ด <Q ๐ต)) |
89 | 88 | adantr 276 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ (โ๐ฅ โ
Q (๐ด
+Q ๐ฅ) = ๐ต โ ๐ด <Q ๐ต)) |
90 | 84, 89 | impbid 129 |
1
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
<Q ๐ต โ โ๐ฅ โ Q (๐ด +Q ๐ฅ) = ๐ต)) |