Proof of Theorem prarloclemup
Step | Hyp | Ref
| Expression |
1 | | simpllr 500 |
. . 3
⊢
(((((𝑋 ∈
ω ∧ (〈𝐿,
𝑈〉 ∈
P ∧ 𝐴
∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧
𝑦 ∈ ω) ∧
(𝐴
+Q ([〈((𝑦 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈) ∧ ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) → 𝑦 ∈ ω) |
2 | | simprl 497 |
. . 3
⊢
(((((𝑋 ∈
ω ∧ (〈𝐿,
𝑈〉 ∈
P ∧ 𝐴
∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧
𝑦 ∈ ω) ∧
(𝐴
+Q ([〈((𝑦 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈) ∧ ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) → (𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿) |
3 | | simplr 496 |
. . 3
⊢
(((((𝑋 ∈
ω ∧ (〈𝐿,
𝑈〉 ∈
P ∧ 𝐴
∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧
𝑦 ∈ ω) ∧
(𝐴
+Q ([〈((𝑦 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈) ∧ ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) → (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) |
4 | | rspe 2412 |
. . 3
⊢ ((𝑦 ∈ ω ∧ ((𝐴 +Q0
([〈𝑦,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
5 | 1, 2, 3, 4 | syl12anc 1167 |
. 2
⊢
(((((𝑋 ∈
ω ∧ (〈𝐿,
𝑈〉 ∈
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 𝑃)) ∈ 𝑈)) |
6 | 5 | exp31 356 |
1
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ 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 𝑃)) ∈ 𝑈)))) |