Proof of Theorem prarloclem3step
Step | Hyp | Ref
| Expression |
1 | | nfv 1461 |
. . 3
⊢
Ⅎ𝑦(𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) |
2 | | nfre1 2407 |
. . 3
⊢
Ⅎ𝑦∃𝑦 ∈ ω ((𝐴 +Q0
([〈𝑦,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) |
3 | | prarloclemlo 6684 |
. . . . 5
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿 → (((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)))) |
4 | | prarloclemup 6685 |
. . . . 5
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q
([〈((𝑦
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈 → (((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)))) |
5 | | prarloclemlt 6683 |
. . . . . 6
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃))
<Q (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃))) |
6 | | prloc 6681 |
. . . . . . . . 9
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ (𝐴
+Q ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃))
<Q (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃))) → ((𝐴 +Q ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿 ∨ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
7 | 6 | ex 113 |
. . . . . . . 8
⊢
(〈𝐿, 𝑈〉 ∈ P
→ ((𝐴
+Q ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃))
<Q (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) → ((𝐴 +Q ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿 ∨ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
8 | 7 | 3ad2ant1 959 |
. . . . . . 7
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q) → ((𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃))
<Q (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) → ((𝐴 +Q ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿 ∨ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
9 | 8 | ad2antlr 472 |
. . . . . 6
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃))
<Q (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) → ((𝐴 +Q ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿 ∨ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
10 | 5, 9 | mpd 13 |
. . . . 5
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿 ∨ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
11 | 3, 4, 10 | mpjaod 670 |
. . . 4
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (((𝐴 +Q0
([〈𝑦,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
12 | 11 | ex 113 |
. . 3
⊢ ((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) → (𝑦 ∈ ω → (((𝐴 +Q0
([〈𝑦,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)))) |
13 | 1, 2, 12 | rexlimd 2474 |
. 2
⊢ ((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) →
(∃𝑦 ∈ ω
((𝐴
+Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
14 | 13 | imp 122 |
1
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ ∃𝑦 ∈ ω ((𝐴 +Q0
([〈𝑦,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |