Step | Hyp | Ref
| Expression |
1 | | pitore 7851 |
. . 3
โข (๐ โ N โ
โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ
โ) |
2 | | pitoregt0 7850 |
. . 3
โข (๐ โ N โ 0
<โ โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ,
0Rโฉ) |
3 | | axprecex 7881 |
. . 3
โข
((โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ โ
โง 0 <โ โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ) โ
โ๐ฆ โ โ (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1)) |
4 | 1, 2, 3 | syl2anc 411 |
. 2
โข (๐ โ N โ
โ๐ฆ โ โ (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1)) |
5 | | simprrr 540 |
. . . 4
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1) |
6 | | simprl 529 |
. . . . 5
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ ๐ฆ โ
โ) |
7 | 1 | adantr 276 |
. . . . . 6
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ
โ) |
8 | 2 | adantr 276 |
. . . . . 6
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ 0
<โ โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ,
0Rโฉ) |
9 | | rereceu 7890 |
. . . . . 6
โข
((โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ โ
โง 0 <โ โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ) โ
โ!๐ โ โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐) = 1) |
10 | 7, 8, 9 | syl2anc 411 |
. . . . 5
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ โ!๐ โ โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐) = 1) |
11 | | oveq2 5885 |
. . . . . . 7
โข (๐ = ๐ฆ โ (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐) = (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ)) |
12 | 11 | eqeq1d 2186 |
. . . . . 6
โข (๐ = ๐ฆ โ ((โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐) = 1 โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1)) |
13 | 12 | riota2 5855 |
. . . . 5
โข ((๐ฆ โ โ โง
โ!๐ โ โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐) = 1) โ
((โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1 โ
(โฉ๐ โ
โ (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐) = 1) = ๐ฆ)) |
14 | 6, 10, 13 | syl2anc 411 |
. . . 4
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
((โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1 โ
(โฉ๐ โ
โ (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐) = 1) = ๐ฆ)) |
15 | 5, 14 | mpbid 147 |
. . 3
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
(โฉ๐ โ
โ (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐) = 1) = ๐ฆ) |
16 | 5 | oveq2d 5893 |
. . . 4
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ)) = (โจ[โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
1)) |
17 | | axresscn 7861 |
. . . . . . . . . 10
โข โ
โ โ |
18 | 17, 7 | sselid 3155 |
. . . . . . . . 9
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ
โ) |
19 | | recnnre 7852 |
. . . . . . . . . . 11
โข (๐ โ N โ
โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ
โ) |
20 | 19 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ
โ) |
21 | 17, 20 | sselid 3155 |
. . . . . . . . 9
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ
โ) |
22 | | axmulcom 7872 |
. . . . . . . . 9
โข
((โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ โ
โง โจ[โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ โ)
โ (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ) =
(โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ,
0Rโฉ)) |
23 | 18, 21, 22 | syl2anc 411 |
. . . . . . . 8
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ) =
(โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ,
0Rโฉ)) |
24 | | recidpirq 7859 |
. . . . . . . . 9
โข (๐ โ N โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ) =
1) |
25 | 24 | adantr 276 |
. . . . . . . 8
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ) =
1) |
26 | 23, 25 | eqtr3d 2212 |
. . . . . . 7
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ) =
1) |
27 | 26 | oveq1d 5892 |
. . . . . 6
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
((โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ) ยท ๐ฆ) = (1 ยท ๐ฆ)) |
28 | 17, 6 | sselid 3155 |
. . . . . . 7
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ ๐ฆ โ
โ) |
29 | | axmulass 7874 |
. . . . . . 7
โข
((โจ[โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ โ
โง โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ โ
โง ๐ฆ โ โ)
โ ((โจ[โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ) ยท ๐ฆ) = (โจ[โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ))) |
30 | 21, 18, 28, 29 | syl3anc 1238 |
. . . . . 6
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
((โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ) ยท ๐ฆ) = (โจ[โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ))) |
31 | | ax1cn 7862 |
. . . . . . 7
โข 1 โ
โ |
32 | | axmulcom 7872 |
. . . . . . 7
โข ((1
โ โ โง ๐ฆ
โ โ) โ (1 ยท ๐ฆ) = (๐ฆ ยท 1)) |
33 | 31, 28, 32 | sylancr 414 |
. . . . . 6
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ (1 ยท
๐ฆ) = (๐ฆ ยท 1)) |
34 | 27, 30, 33 | 3eqtr3d 2218 |
. . . . 5
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ)) = (๐ฆ ยท 1)) |
35 | | ax1rid 7878 |
. . . . . 6
โข (๐ฆ โ โ โ (๐ฆ ยท 1) = ๐ฆ) |
36 | 6, 35 | syl 14 |
. . . . 5
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ (๐ฆ ยท 1) = ๐ฆ) |
37 | 34, 36 | eqtrd 2210 |
. . . 4
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท
(โจ[โจ(โจ{๐
โฃ ๐
<Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ)) = ๐ฆ) |
38 | | ax1rid 7878 |
. . . . 5
โข
(โจ[โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ โ โ
โ (โจ[โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท 1) =
โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ,
0Rโฉ) |
39 | 20, 38 | syl 14 |
. . . 4
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
(โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท 1) =
โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ,
0Rโฉ) |
40 | 16, 37, 39 | 3eqtr3d 2218 |
. . 3
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ ๐ฆ = โจ[โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ,
0Rโฉ) |
41 | 15, 40 | eqtrd 2210 |
. 2
โข ((๐ โ N โง
(๐ฆ โ โ โง (0
<โ ๐ฆ
โง (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐ฆ) = 1))) โ
(โฉ๐ โ
โ (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐) = 1) =
โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ,
0Rโฉ) |
42 | 4, 41 | rexlimddv 2599 |
1
โข (๐ โ N โ
(โฉ๐ โ
โ (โจ[โจ(โจ{๐ โฃ ๐ <Q [โจ๐, 1oโฉ]
~Q }, {๐ข โฃ [โจ๐, 1oโฉ]
~Q <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R , 0Rโฉ ยท ๐) = 1) =
โจ[โจ(โจ{๐
โฃ ๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ,
0Rโฉ) |