Proof of Theorem prarloclemlt
Step | Hyp | Ref
| Expression |
1 | | 2onn 6094 |
. . . . . . . . . . . 12
⊢
2𝑜 ∈ ω |
2 | | nnacl 6059 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧
2𝑜 ∈ ω) → (𝑦 +𝑜 2𝑜)
∈ ω) |
3 | 1, 2 | mpan2 401 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω → (𝑦 +𝑜
2𝑜) ∈ ω) |
4 | | nnaword1 6086 |
. . . . . . . . . . 11
⊢ (((𝑦 +𝑜
2𝑜) ∈ ω ∧ 𝑋 ∈ ω) → (𝑦 +𝑜 2𝑜)
⊆ ((𝑦
+𝑜 2𝑜) +𝑜 𝑋)) |
5 | 3, 4 | sylan 267 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ 𝑋 ∈ ω) → (𝑦 +𝑜
2𝑜) ⊆ ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)) |
6 | | 1onn 6093 |
. . . . . . . . . . . . . . 15
⊢
1𝑜 ∈ ω |
7 | 6 | elexi 2567 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ V |
8 | 7 | sucid 4154 |
. . . . . . . . . . . . 13
⊢
1𝑜 ∈ suc 1𝑜 |
9 | | df-2o 6002 |
. . . . . . . . . . . . 13
⊢
2𝑜 = suc 1𝑜 |
10 | 8, 9 | eleqtrri 2113 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ 2𝑜 |
11 | | nnaordi 6081 |
. . . . . . . . . . . . 13
⊢
((2𝑜 ∈ ω ∧ 𝑦 ∈ ω) →
(1𝑜 ∈ 2𝑜 → (𝑦 +𝑜 1𝑜)
∈ (𝑦
+𝑜 2𝑜))) |
12 | 1, 11 | mpan 400 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ω →
(1𝑜 ∈ 2𝑜 → (𝑦 +𝑜 1𝑜)
∈ (𝑦
+𝑜 2𝑜))) |
13 | 10, 12 | mpi 15 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω → (𝑦 +𝑜
1𝑜) ∈ (𝑦 +𝑜
2𝑜)) |
14 | 13 | adantr 261 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ 𝑋 ∈ ω) → (𝑦 +𝑜
1𝑜) ∈ (𝑦 +𝑜
2𝑜)) |
15 | 5, 14 | sseldd 2946 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧ 𝑋 ∈ ω) → (𝑦 +𝑜
1𝑜) ∈ ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)) |
16 | 15 | ancoms 255 |
. . . . . . . 8
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → (𝑦 +𝑜
1𝑜) ∈ ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)) |
17 | | 1pi 6413 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ N |
18 | | nnppipi 6441 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧
1𝑜 ∈ N) → (𝑦 +𝑜 1𝑜)
∈ N) |
19 | 17, 18 | mpan2 401 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ω → (𝑦 +𝑜
1𝑜) ∈ N) |
20 | 19 | adantl 262 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → (𝑦 +𝑜
1𝑜) ∈ N) |
21 | | o1p1e2 6048 |
. . . . . . . . . . . . . 14
⊢
(1𝑜 +𝑜 1𝑜) =
2𝑜 |
22 | | nnppipi 6441 |
. . . . . . . . . . . . . . 15
⊢
((1𝑜 ∈ ω ∧ 1𝑜
∈ N) → (1𝑜 +𝑜
1𝑜) ∈ N) |
23 | 6, 17, 22 | mp2an 402 |
. . . . . . . . . . . . . 14
⊢
(1𝑜 +𝑜 1𝑜)
∈ N |
24 | 21, 23 | eqeltrri 2111 |
. . . . . . . . . . . . 13
⊢
2𝑜 ∈ N |
25 | | nnppipi 6441 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ω ∧
2𝑜 ∈ N) → (𝑦 +𝑜 2𝑜)
∈ N) |
26 | 24, 25 | mpan2 401 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ω → (𝑦 +𝑜
2𝑜) ∈ N) |
27 | | pinn 6407 |
. . . . . . . . . . . 12
⊢ ((𝑦 +𝑜
2𝑜) ∈ N → (𝑦 +𝑜 2𝑜)
∈ ω) |
28 | 26, 27 | syl 14 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω → (𝑦 +𝑜
2𝑜) ∈ ω) |
29 | | nnacom 6063 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ω ∧ (𝑦 +𝑜
2𝑜) ∈ ω) → (𝑋 +𝑜 (𝑦 +𝑜
2𝑜)) = ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)) |
30 | 28, 29 | sylan2 270 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → (𝑋 +𝑜 (𝑦 +𝑜
2𝑜)) = ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)) |
31 | | nnppipi 6441 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ω ∧ (𝑦 +𝑜
2𝑜) ∈ N) → (𝑋 +𝑜 (𝑦 +𝑜
2𝑜)) ∈ N) |
32 | 26, 31 | sylan2 270 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → (𝑋 +𝑜 (𝑦 +𝑜
2𝑜)) ∈ N) |
33 | 30, 32 | eqeltrrd 2115 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → ((𝑦 +𝑜
2𝑜) +𝑜 𝑋) ∈ N) |
34 | | ltpiord 6417 |
. . . . . . . . 9
⊢ (((𝑦 +𝑜
1𝑜) ∈ N ∧ ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)
∈ N) → ((𝑦 +𝑜 1𝑜)
<N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)
↔ (𝑦
+𝑜 1𝑜) ∈ ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋))) |
35 | 20, 33, 34 | syl2anc 391 |
. . . . . . . 8
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → ((𝑦 +𝑜
1𝑜) <N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)
↔ (𝑦
+𝑜 1𝑜) ∈ ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋))) |
36 | 16, 35 | mpbird 156 |
. . . . . . 7
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → (𝑦 +𝑜
1𝑜) <N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)) |
37 | | mulidpi 6416 |
. . . . . . . . 9
⊢ ((𝑦 +𝑜
1𝑜) ∈ N → ((𝑦 +𝑜 1𝑜)
·N 1𝑜) = (𝑦 +𝑜
1𝑜)) |
38 | 20, 37 | syl 14 |
. . . . . . . 8
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → ((𝑦 +𝑜
1𝑜) ·N
1𝑜) = (𝑦
+𝑜 1𝑜)) |
39 | | mulcompig 6429 |
. . . . . . . . . 10
⊢ ((((𝑦 +𝑜
2𝑜) +𝑜 𝑋) ∈ N ∧
1𝑜 ∈ N) → (((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)
·N 1𝑜) =
(1𝑜 ·N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋))) |
40 | 33, 17, 39 | sylancl 392 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → (((𝑦 +𝑜
2𝑜) +𝑜 𝑋) ·N
1𝑜) = (1𝑜
·N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋))) |
41 | | mulidpi 6416 |
. . . . . . . . . 10
⊢ (((𝑦 +𝑜
2𝑜) +𝑜 𝑋) ∈ N → (((𝑦 +𝑜
2𝑜) +𝑜 𝑋) ·N
1𝑜) = ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)) |
42 | 33, 41 | syl 14 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → (((𝑦 +𝑜
2𝑜) +𝑜 𝑋) ·N
1𝑜) = ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)) |
43 | 40, 42 | eqtr3d 2074 |
. . . . . . . 8
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) →
(1𝑜 ·N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)) =
((𝑦 +𝑜
2𝑜) +𝑜 𝑋)) |
44 | 38, 43 | breq12d 3777 |
. . . . . . 7
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → (((𝑦 +𝑜
1𝑜) ·N
1𝑜) <N (1𝑜
·N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋))
↔ (𝑦
+𝑜 1𝑜) <N
((𝑦 +𝑜
2𝑜) +𝑜 𝑋))) |
45 | 36, 44 | mpbird 156 |
. . . . . 6
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → ((𝑦 +𝑜
1𝑜) ·N
1𝑜) <N (1𝑜
·N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋))) |
46 | | simpr 103 |
. . . . . . 7
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) → 𝑦 ∈
ω) |
47 | | ordpipqqs 6472 |
. . . . . . . . . 10
⊢ ((((𝑦 +𝑜
1𝑜) ∈ N ∧ 1𝑜
∈ N) ∧ (((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)
∈ N ∧ 1𝑜 ∈ N))
→ ([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q <Q [〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ↔ ((𝑦 +𝑜 1𝑜)
·N 1𝑜)
<N (1𝑜
·N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)))) |
48 | 17, 47 | mpanl2 411 |
. . . . . . . . 9
⊢ (((𝑦 +𝑜
1𝑜) ∈ N ∧ (((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)
∈ N ∧ 1𝑜 ∈ N))
→ ([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q <Q [〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ↔ ((𝑦 +𝑜 1𝑜)
·N 1𝑜)
<N (1𝑜
·N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)))) |
49 | 17, 48 | mpanr2 414 |
. . . . . . . 8
⊢ (((𝑦 +𝑜
1𝑜) ∈ N ∧ ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)
∈ N) → ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q <Q [〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ↔ ((𝑦 +𝑜 1𝑜)
·N 1𝑜)
<N (1𝑜
·N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)))) |
50 | 19, 49 | sylan 267 |
. . . . . . 7
⊢ ((𝑦 ∈ ω ∧ ((𝑦 +𝑜
2𝑜) +𝑜 𝑋) ∈ N) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q <Q [〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ↔ ((𝑦 +𝑜 1𝑜)
·N 1𝑜)
<N (1𝑜
·N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)))) |
51 | 46, 33, 50 | syl2anc 391 |
. . . . . 6
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q <Q [〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ↔ ((𝑦 +𝑜 1𝑜)
·N 1𝑜)
<N (1𝑜
·N ((𝑦 +𝑜 2𝑜)
+𝑜 𝑋)))) |
52 | 45, 51 | mpbird 156 |
. . . . 5
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) →
[〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q <Q [〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ) |
53 | 52 | adantlr 446 |
. . . 4
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
[〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q <Q [〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ) |
54 | | opelxpi 4376 |
. . . . . . . . 9
⊢ (((𝑦 +𝑜
1𝑜) ∈ N ∧ 1𝑜
∈ N) → 〈(𝑦 +𝑜
1𝑜), 1𝑜〉 ∈ (N
× N)) |
55 | 20, 17, 54 | sylancl 392 |
. . . . . . . 8
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) →
〈(𝑦
+𝑜 1𝑜), 1𝑜〉
∈ (N × N)) |
56 | | enqex 6458 |
. . . . . . . . 9
⊢
~Q ∈ V |
57 | 56 | ecelqsi 6160 |
. . . . . . . 8
⊢
(〈(𝑦
+𝑜 1𝑜), 1𝑜〉
∈ (N × N) → [〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ∈ ((N × N)
/ ~Q )) |
58 | 55, 57 | syl 14 |
. . . . . . 7
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) →
[〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ∈ ((N × N)
/ ~Q )) |
59 | | df-nqqs 6446 |
. . . . . . 7
⊢
Q = ((N × N) /
~Q ) |
60 | 58, 59 | syl6eleqr 2131 |
. . . . . 6
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) →
[〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ∈ Q) |
61 | 60 | adantlr 446 |
. . . . 5
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
[〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ∈ Q) |
62 | | opelxpi 4376 |
. . . . . . . . 9
⊢ ((((𝑦 +𝑜
2𝑜) +𝑜 𝑋) ∈ N ∧
1𝑜 ∈ N) → 〈((𝑦 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉 ∈ (N ×
N)) |
63 | 33, 17, 62 | sylancl 392 |
. . . . . . . 8
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) →
〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉
∈ (N × N)) |
64 | 56 | ecelqsi 6160 |
. . . . . . . 8
⊢
(〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉
∈ (N × N) → [〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ∈ ((N × N)
/ ~Q )) |
65 | 63, 64 | syl 14 |
. . . . . . 7
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) →
[〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ∈ ((N × N)
/ ~Q )) |
66 | 65, 59 | syl6eleqr 2131 |
. . . . . 6
⊢ ((𝑋 ∈ ω ∧ 𝑦 ∈ ω) →
[〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ∈ Q) |
67 | 66 | adantlr 446 |
. . . . 5
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
[〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ∈ Q) |
68 | | simplr3 948 |
. . . . 5
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → 𝑃 ∈
Q) |
69 | | ltmnqg 6499 |
. . . . 5
⊢
(([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ∈ Q ∧ [〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ∈ Q ∧ 𝑃 ∈ Q) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q <Q [〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ↔ (𝑃 ·Q
[〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ) <Q (𝑃 ·Q
[〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ))) |
70 | 61, 67, 68, 69 | syl3anc 1135 |
. . . 4
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q <Q [〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ↔ (𝑃 ·Q
[〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ) <Q (𝑃 ·Q
[〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ))) |
71 | 53, 70 | mpbid 135 |
. . 3
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝑃
·Q [〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ) <Q (𝑃 ·Q
[〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q )) |
72 | | mulcomnqg 6481 |
. . . . 5
⊢ ((𝑃 ∈ Q ∧
[〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ∈ Q) → (𝑃 ·Q
[〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ) = ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) |
73 | 68, 61, 72 | syl2anc 391 |
. . . 4
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝑃
·Q [〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ) = ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) |
74 | | mulcomnqg 6481 |
. . . . 5
⊢ ((𝑃 ∈ Q ∧
[〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ∈ Q) → (𝑃 ·Q
[〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ) = ([〈((𝑦 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q
·Q 𝑃)) |
75 | 68, 67, 74 | syl2anc 391 |
. . . 4
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝑃
·Q [〈((𝑦 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q ) = ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) |
76 | 73, 75 | breq12d 3777 |
. . 3
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝑃
·Q [〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ) <Q (𝑃 ·Q
[〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ) ↔ ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃) <Q
([〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃))) |
77 | 71, 76 | mpbid 135 |
. 2
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃) <Q
([〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) |
78 | | mulclnq 6474 |
. . . 4
⊢
(([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ∈ Q ∧ 𝑃 ∈ Q) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃) ∈
Q) |
79 | 61, 68, 78 | syl2anc 391 |
. . 3
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃) ∈
Q) |
80 | | mulclnq 6474 |
. . . 4
⊢
(([〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ∈ Q ∧ 𝑃 ∈ Q) →
([〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃) ∈
Q) |
81 | 67, 68, 80 | syl2anc 391 |
. . 3
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
([〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃) ∈
Q) |
82 | | simplr1 946 |
. . . 4
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
〈𝐿, 𝑈〉 ∈
P) |
83 | | simplr2 947 |
. . . 4
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → 𝐴 ∈ 𝐿) |
84 | | elprnql 6579 |
. . . 4
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴 ∈ 𝐿) → 𝐴 ∈ Q) |
85 | 82, 83, 84 | syl2anc 391 |
. . 3
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → 𝐴 ∈
Q) |
86 | | ltanqg 6498 |
. . 3
⊢
((([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃) ∈ Q ∧
([〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃) ∈ Q ∧
𝐴 ∈ Q)
→ (([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃) <Q
([〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃) ↔ (𝐴 +Q ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃))
<Q (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)))) |
87 | 79, 81, 85, 86 | syl3anc 1135 |
. 2
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
(([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃) <Q
([〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃) ↔ (𝐴 +Q ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃))
<Q (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)))) |
88 | 77, 87 | mpbid 135 |
1
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃))
<Q (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃))) |