prarloc - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > prarloc		GIF version

Theorem prarloc 7860

Description: A Dedekind cut is arithmetically located. Part of Proposition 11.15 of [BauerTaylor], p. 52, slightly modified. It states that given a tolerance 𝑃, there are elements of the lower and upper cut which are within that tolerance of each other.

Usually, proofs will be shorter if they use prarloc2 7861 instead. (Contributed by Jim Kingdon, 22-Oct-2019.)

**Assertion**
Ref	Expression
prarloc	⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑎 ∈ 𝐿 ∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃))

Distinct variable groups: 𝐿,𝑎,𝑏 𝑃,𝑎,𝑏 𝑈,𝑎,𝑏

Proof of Theorem prarloc Dummy variables 𝑚 𝑛 𝑞 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prml 7834	. . . . . . 7 ⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥 ∈ Q 𝑥 ∈ 𝐿)
2		df-rex 2534	. . . . . . 7 ⊢ (∃𝑥 ∈ Q 𝑥 ∈ 𝐿 ↔ ∃𝑥(𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿))
3	1, 2	sylib 122	. . . . . 6 ⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥(𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿))
4	3	adantr 276	. . . . 5 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑥(𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿))
5		prmu 7835	. . . . . . 7 ⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑦 ∈ Q 𝑦 ∈ 𝑈)
6		df-rex 2534	. . . . . . 7 ⊢ (∃𝑦 ∈ Q 𝑦 ∈ 𝑈 ↔ ∃𝑦(𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈))
7	5, 6	sylib 122	. . . . . 6 ⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑦(𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈))
8	7	adantr 276	. . . . 5 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑦(𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈))
9		subhalfnqq 7771	. . . . . . . . 9 ⊢ (𝑃 ∈ Q → ∃𝑞 ∈ Q (𝑞 +_Q 𝑞) <_Q 𝑃)
10	9	adantl 277	. . . . . . . 8 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑞 ∈ Q (𝑞 +_Q 𝑞) <_Q 𝑃)
11		df-rex 2534	. . . . . . . 8 ⊢ (∃𝑞 ∈ Q (𝑞 +_Q 𝑞) <_Q 𝑃 ↔ ∃𝑞(𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))
12	10, 11	sylib 122	. . . . . . 7 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑞(𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))
13	12	ancli 323	. . . . . 6 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ ∃𝑞(𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃)))
14		19.42v 1962	. . . . . 6 ⊢ (∃𝑞((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃)) ↔ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ ∃𝑞(𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃)))
15	13, 14	sylibr 134	. . . . 5 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑞((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃)))
16		eeeanv 1993	. . . . 5 ⊢ (∃𝑥∃𝑦∃𝑞((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ↔ (∃𝑥(𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ ∃𝑦(𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ∃𝑞((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))))
17	4, 8, 15, 16	syl3anbrc 1212	. . . 4 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑥∃𝑦∃𝑞((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))))
18		prarloclemarch2 7776	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ Q ∧ 𝑥 ∈ Q ∧ 𝑞 ∈ Q) → ∃𝑛 ∈ N (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))
19		df-rex 2534	. . . . . . . . . . . . . 14 ⊢ (∃𝑛 ∈ N (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))) ↔ ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)))))
20	18, 19	sylib 122	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ Q ∧ 𝑥 ∈ Q ∧ 𝑞 ∈ Q) → ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)))))
21	20	3com12 1238	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑞 ∈ Q) → ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)))))
22	21	3adant1r 1262	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ Q ∧ 𝑞 ∈ Q) → ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)))))
23	22	3adant2r 1264	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ 𝑞 ∈ Q) → ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)))))
24	23	3adant3r 1266	. . . . . . . . 9 ⊢ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃)) → ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)))))
25	24	3adant3l 1265	. . . . . . . 8 ⊢ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) → ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)))))
26	25	ancli 323	. . . . . . 7 ⊢ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) → (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))))
27		19.42v 1962	. . . . . . 7 ⊢ (∃𝑛(((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) ↔ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))))
28	26, 27	sylibr 134	. . . . . 6 ⊢ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) → ∃𝑛(((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))))
29	28	2eximi 1654	. . . . 5 ⊢ (∃𝑦∃𝑞((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) → ∃𝑦∃𝑞∃𝑛(((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))))
30	29	eximi 1653	. . . 4 ⊢ (∃𝑥∃𝑦∃𝑞((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) → ∃𝑥∃𝑦∃𝑞∃𝑛(((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))))
31		simpl1l 1079	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → 𝑥 ∈ Q)
32		simp3rl 1101	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) → 𝑞 ∈ Q)
33	32	adantr 276	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → 𝑞 ∈ Q)
34		simp3rr 1102	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) → (𝑞 +_Q 𝑞) <_Q 𝑃)
35	34	adantr 276	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → (𝑞 +_Q 𝑞) <_Q 𝑃)
36	31, 33, 35	3jca 1208	. . . . . . . . 9 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → (𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))
37		simp3ll 1099	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) → ⟨𝐿, 𝑈⟩ ∈ P)
38	37	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → ⟨𝐿, 𝑈⟩ ∈ P)
39		simpl1r 1080	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → 𝑥 ∈ 𝐿)
40		simprl 535	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → 𝑛 ∈ N)
41		simprrl 545	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → 1_o <_N 𝑛)
42		simprrr 546	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)))
43		simpl2r 1082	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → 𝑦 ∈ 𝑈)
44		prcunqu 7842	. . . . . . . . . . . . 13 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑦 ∈ 𝑈) → (𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)) → (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))
45	38, 43, 44	syl2anc 415	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → (𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)) → (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))
46	42, 45	mpd 13	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)
47		prarloclem 7858	. . . . . . . . . . 11 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑥 ∈ 𝐿) ∧ (𝑛 ∈ N ∧ 𝑞 ∈ Q ∧ 1_o <_N 𝑛) ∧ (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈) → ∃𝑚 ∈ ω ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))
48	38, 39, 40, 33, 41, 46, 47	syl231anc 1298	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → ∃𝑚 ∈ ω ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))
49		df-rex 2534	. . . . . . . . . 10 ⊢ (∃𝑚 ∈ ω ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈) ↔ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)))
50	48, 49	sylib 122	. . . . . . . . 9 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)))
51	36, 50	jca 306	. . . . . . . 8 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))))
52		19.42v 1962	. . . . . . . 8 ⊢ (∃𝑚((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))) ↔ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))))
53	51, 52	sylibr 134	. . . . . . 7 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → ∃𝑚((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))))
54		simprrl 545	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))) → (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿)
55		eleq1 2301	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) → (𝑎 ∈ 𝐿 ↔ (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿))
56	55	anbi1d 469	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) → ((𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈) ↔ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)))
57	56	anbi2d 468	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) → ((𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)) ↔ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))))
58	57	anbi2d 468	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) → (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))) ↔ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)))))
59	58	ceqsexgv 2955	. . . . . . . . . . . . 13 ⊢ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 → (∃𝑎(𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)))) ↔ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)))))
60	59	biimprcd 160	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))) → ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 → ∃𝑎(𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))))))
61	54, 60	mpd 13	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))) → ∃𝑎(𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)))))
62		simprrr 546	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))) → (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)
63		eleq1 2301	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) → (𝑏 ∈ 𝑈 ↔ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))
64	63	anbi2d 468	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) → ((𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈) ↔ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)))
65	64	anbi2d 468	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) → ((𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)) ↔ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))))
66	65	anbi2d 468	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) → (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))) ↔ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)))))
67	66	anbi2d 468	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) → ((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) ↔ (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))))))
68	67	exbidv 1878	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) → (∃𝑎(𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) ↔ ∃𝑎(𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))))))
69	68	ceqsexgv 2955	. . . . . . . . . . . 12 ⊢ ((𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈 → (∃𝑏(𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))) ↔ ∃𝑎(𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))))))
70	69	biimprcd 160	. . . . . . . . . . 11 ⊢ (∃𝑎(𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)))) → ((𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈 → ∃𝑏(𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))))))
71	61, 62, 70	sylc 62	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))) → ∃𝑏(𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))))
72		19.42v 1962	. . . . . . . . . . 11 ⊢ (∃𝑎(𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))) ↔ (𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))))
73	72	exbii 1658	. . . . . . . . . 10 ⊢ (∃𝑏∃𝑎(𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))) ↔ ∃𝑏(𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))))
74	71, 73	sylibr 134	. . . . . . . . 9 ⊢ (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))) → ∃𝑏∃𝑎(𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))))
75		simprrl 545	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))) → 𝑎 ∈ 𝐿)
76	75	adantl 277	. . . . . . . . . . . . 13 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑎 ∈ 𝐿)
77		simprrr 546	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))) → 𝑏 ∈ 𝑈)
78	77	adantl 277	. . . . . . . . . . . . . 14 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑏 ∈ 𝑈)
79		simpl 109	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))))
80		simprl2 1074	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑞 ∈ Q)
81		simprl3 1075	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑞 +_Q 𝑞) <_Q 𝑃)
82	80, 81	jca 306	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))
83		simprl1 1073	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑥 ∈ Q)
84		simprrl 545	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑚 ∈ ω)
85	83, 84	jca 306	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑥 ∈ Q ∧ 𝑚 ∈ ω))
86		prarloclemcalc 7859	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑥 ∈ Q ∧ 𝑚 ∈ ω))) → 𝑏 <_Q (𝑎 +_Q 𝑃))
87	79, 82, 85, 86	syl12anc 1276	. . . . . . . . . . . . . 14 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑏 <_Q (𝑎 +_Q 𝑃))
88	78, 87	jca 306	. . . . . . . . . . . . 13 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃)))
89	76, 88	jca 306	. . . . . . . . . . . 12 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
90	89	ancom1s 575	. . . . . . . . . . 11 ⊢ (((𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ 𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
91	90	anasss 403	. . . . . . . . . 10 ⊢ ((𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))) → (𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
92	91	2eximi 1654	. . . . . . . . 9 ⊢ (∃𝑏∃𝑎(𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
93	74, 92	syl 14	. . . . . . . 8 ⊢ (((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
94	93	exlimiv 1651	. . . . . . 7 ⊢ (∃𝑚((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
95	53, 94	syl 14	. . . . . 6 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
96	95	exlimivv 1952	. . . . 5 ⊢ (∃𝑞∃𝑛(((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
97	96	exlimivv 1952	. . . 4 ⊢ (∃𝑥∃𝑦∃𝑞∃𝑛(((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
98	17, 30, 97	3syl 17	. . 3 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
99		excom 1716	. . 3 ⊢ (∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))) ↔ ∃𝑎∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
100	98, 99	sylib 122	. 2 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑎∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
101		19.42v 1962	. . . . 5 ⊢ (∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))) ↔ (𝑎 ∈ 𝐿 ∧ ∃𝑏(𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
102		df-rex 2534	. . . . . 6 ⊢ (∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃) ↔ ∃𝑏(𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃)))
103	102	anbi2i 461	. . . . 5 ⊢ ((𝑎 ∈ 𝐿 ∧ ∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃)) ↔ (𝑎 ∈ 𝐿 ∧ ∃𝑏(𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
104	101, 103	bitr4i 187	. . . 4 ⊢ (∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))) ↔ (𝑎 ∈ 𝐿 ∧ ∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃)))
105	104	exbii 1658	. . 3 ⊢ (∃𝑎∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))) ↔ ∃𝑎(𝑎 ∈ 𝐿 ∧ ∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃)))
106		df-rex 2534	. . 3 ⊢ (∃𝑎 ∈ 𝐿 ∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃) ↔ ∃𝑎(𝑎 ∈ 𝐿 ∧ ∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃)))
107	105, 106	bitr4i 187	. 2 ⊢ (∃𝑎∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))) ↔ ∃𝑎 ∈ 𝐿 ∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃))
108	100, 107	sylib 122	1 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑎 ∈ 𝐿 ∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 1009 = wceq 1402 ∃wex 1545 ∈ wcel 2209 ∃wrex 2529 ⟨cop 3708 class class class wbr 4125 ωcom 4732 (class class class)co 6075 1_oc1o 6670 2_oc2o 6671 +_o coa 6674 [cec 6795 Ncnpi 7629 <_N clti 7632 ~_Q ceq 7636 Qcnq 7637 +_Q cplq 7639 ·_Q cmq 7640 <_Q cltq 7642 ~_Q0 ceq0 7643 +_Q0 cplq0 7646 ·_Q0 cmq0 7647 Pcnp 7648

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4241 ax-sep 4244 ax-nul 4254 ax-pow 4306 ax-pr 4341 ax-un 4573 ax-setind 4679 ax-iinf 4730

This theorem depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-ral 2533 df-rex 2534 df-reu 2535 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-pw 3687 df-sn 3711 df-pr 3712 df-op 3714 df-uni 3931 df-int 3966 df-iun 4009 df-br 4126 df-opab 4188 df-mpt 4189 df-tr 4225 df-eprel 4429 df-id 4433 df-po 4436 df-iso 4437 df-iord 4506 df-on 4508 df-suc 4511 df-iom 4733 df-xp 4775 df-rel 4776 df-cnv 4777 df-co 4778 df-dm 4779 df-rn 4780 df-res 4781 df-ima 4782 df-iota 5332 df-fun 5374 df-fn 5375 df-f 5376 df-f1 5377 df-fo 5378 df-f1o 5379 df-fv 5380 df-ov 6078 df-oprab 6079 df-mpo 6080 df-1st 6364 df-2nd 6365 df-recs 6566 df-irdg 6631 df-1o 6677 df-2o 6678 df-oadd 6681 df-omul 6682 df-er 6797 df-ec 6799 df-qs 6803 df-ni 7661 df-pli 7662 df-mi 7663 df-lti 7664 df-plpq 7701 df-mpq 7702 df-enq 7704 df-nqqs 7705 df-plqqs 7706 df-mqqs 7707 df-1nqqs 7708 df-rq 7709 df-ltnqqs 7710 df-enq0 7781 df-nq0 7782 df-0nq0 7783 df-plq0 7784 df-mq0 7785 df-inp 7823

This theorem is referenced by: prarloc2 7861 addlocpr 7893 prmuloc 7923 ltaddpr 7954 ltexprlemloc 7964 ltexprlemrl 7967 ltexprlemru 7969

W3C validator