Proof of Theorem pitonnlem1
Step | Hyp | Ref
| Expression |
1 | | df-1 6989 |
. 2
⊢ 1 =
〈1R,
0R〉 |
2 | | df-1r 6909 |
. . . 4
⊢
1R = [〈(1P
+P 1P),
1P〉] ~R |
3 | | df-i1p 6657 |
. . . . . . . 8
⊢
1P = 〈{𝑙 ∣ 𝑙 <Q
1Q}, {𝑢 ∣ 1Q
<Q 𝑢}〉 |
4 | | df-1nqqs 6541 |
. . . . . . . . . . 11
⊢
1Q = [〈1𝑜,
1𝑜〉] ~Q |
5 | 4 | breq2i 3793 |
. . . . . . . . . 10
⊢ (𝑙 <Q
1Q ↔ 𝑙 <Q
[〈1𝑜, 1𝑜〉]
~Q ) |
6 | 5 | abbii 2194 |
. . . . . . . . 9
⊢ {𝑙 ∣ 𝑙 <Q
1Q} = {𝑙 ∣ 𝑙 <Q
[〈1𝑜, 1𝑜〉]
~Q } |
7 | 4 | breq1i 3792 |
. . . . . . . . . 10
⊢
(1Q <Q 𝑢 ↔
[〈1𝑜, 1𝑜〉]
~Q <Q 𝑢) |
8 | 7 | abbii 2194 |
. . . . . . . . 9
⊢ {𝑢 ∣
1Q <Q 𝑢} = {𝑢 ∣ [〈1𝑜,
1𝑜〉] ~Q
<Q 𝑢} |
9 | 6, 8 | opeq12i 3575 |
. . . . . . . 8
⊢
〈{𝑙 ∣
𝑙
<Q 1Q}, {𝑢 ∣
1Q <Q 𝑢}〉 = 〈{𝑙 ∣ 𝑙 <Q
[〈1𝑜, 1𝑜〉]
~Q }, {𝑢 ∣ [〈1𝑜,
1𝑜〉] ~Q
<Q 𝑢}〉 |
10 | 3, 9 | eqtri 2101 |
. . . . . . 7
⊢
1P = 〈{𝑙 ∣ 𝑙 <Q
[〈1𝑜, 1𝑜〉]
~Q }, {𝑢 ∣ [〈1𝑜,
1𝑜〉] ~Q
<Q 𝑢}〉 |
11 | 10 | oveq1i 5542 |
. . . . . 6
⊢
(1P +P
1P) = (〈{𝑙 ∣ 𝑙 <Q
[〈1𝑜, 1𝑜〉]
~Q }, {𝑢 ∣ [〈1𝑜,
1𝑜〉] ~Q
<Q 𝑢}〉 +P
1P) |
12 | 11 | opeq1i 3573 |
. . . . 5
⊢
〈(1P +P
1P), 1P〉 =
〈(〈{𝑙 ∣
𝑙
<Q [〈1𝑜,
1𝑜〉] ~Q }, {𝑢 ∣ [〈1𝑜,
1𝑜〉] ~Q
<Q 𝑢}〉 +P
1P),
1P〉 |
13 | | eceq1 6164 |
. . . . 5
⊢
(〈(1P +P
1P), 1P〉 =
〈(〈{𝑙 ∣
𝑙
<Q [〈1𝑜,
1𝑜〉] ~Q }, {𝑢 ∣ [〈1𝑜,
1𝑜〉] ~Q
<Q 𝑢}〉 +P
1P), 1P〉 →
[〈(1P +P
1P), 1P〉]
~R = [〈(〈{𝑙 ∣ 𝑙 <Q
[〈1𝑜, 1𝑜〉]
~Q }, {𝑢 ∣ [〈1𝑜,
1𝑜〉] ~Q
<Q 𝑢}〉 +P
1P), 1P〉]
~R ) |
14 | 12, 13 | ax-mp 7 |
. . . 4
⊢
[〈(1P +P
1P), 1P〉]
~R = [〈(〈{𝑙 ∣ 𝑙 <Q
[〈1𝑜, 1𝑜〉]
~Q }, {𝑢 ∣ [〈1𝑜,
1𝑜〉] ~Q
<Q 𝑢}〉 +P
1P), 1P〉]
~R |
15 | 2, 14 | eqtri 2101 |
. . 3
⊢
1R = [〈(〈{𝑙 ∣ 𝑙 <Q
[〈1𝑜, 1𝑜〉]
~Q }, {𝑢 ∣ [〈1𝑜,
1𝑜〉] ~Q
<Q 𝑢}〉 +P
1P), 1P〉]
~R |
16 | 15 | opeq1i 3573 |
. 2
⊢
〈1R, 0R〉 =
〈[〈(〈{𝑙
∣ 𝑙
<Q [〈1𝑜,
1𝑜〉] ~Q }, {𝑢 ∣ [〈1𝑜,
1𝑜〉] ~Q
<Q 𝑢}〉 +P
1P), 1P〉]
~R ,
0R〉 |
17 | 1, 16 | eqtr2i 2102 |
1
⊢
〈[〈(〈{𝑙 ∣ 𝑙 <Q
[〈1𝑜, 1𝑜〉]
~Q }, {𝑢 ∣ [〈1𝑜,
1𝑜〉] ~Q
<Q 𝑢}〉 +P
1P), 1P〉]
~R , 0R〉 =
1 |