prarloc - Intuitionistic Logic Explorer

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

Theorem prarloc 7766

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 7767 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 7740	. . . . . . 7 ⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥 ∈ Q 𝑥 ∈ 𝐿)
2		df-rex 2517	. . . . . . 7 ⊢ (∃𝑥 ∈ Q 𝑥 ∈ 𝐿 ↔ ∃𝑥(𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿))
3	1, 2	sylib 122	. . . . . 6 ⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥(𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿))
4	3	adantr 276	. . . . 5 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑥(𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿))
5		prmu 7741	. . . . . . 7 ⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑦 ∈ Q 𝑦 ∈ 𝑈)
6		df-rex 2517	. . . . . . 7 ⊢ (∃𝑦 ∈ Q 𝑦 ∈ 𝑈 ↔ ∃𝑦(𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈))
7	5, 6	sylib 122	. . . . . 6 ⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑦(𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈))
8	7	adantr 276	. . . . 5 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑦(𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈))
9		subhalfnqq 7677	. . . . . . . . 9 ⊢ (𝑃 ∈ Q → ∃𝑞 ∈ Q (𝑞 +_Q 𝑞) <_Q 𝑃)
10	9	adantl 277	. . . . . . . 8 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑞 ∈ Q (𝑞 +_Q 𝑞) <_Q 𝑃)
11		df-rex 2517	. . . . . . . 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 1955	. . . . . 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 1986	. . . . 5 ⊢ (∃𝑥∃𝑦∃𝑞((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ↔ (∃𝑥(𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ ∃𝑦(𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ∃𝑞((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))))
17	4, 8, 15, 16	syl3anbrc 1208	. . . 4 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑥∃𝑦∃𝑞((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))))
18		prarloclemarch2 7682	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ Q ∧ 𝑥 ∈ Q ∧ 𝑞 ∈ Q) → ∃𝑛 ∈ N (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))
19		df-rex 2517	. . . . . . . . . . . . . 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 1234	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑞 ∈ Q) → ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)))))
22	21	3adant1r 1258	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ Q ∧ 𝑞 ∈ Q) → ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)))))
23	22	3adant2r 1260	. . . . . . . . . 10 ⊢ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ 𝑞 ∈ Q) → ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)))))
24	23	3adant3r 1262	. . . . . . . . 9 ⊢ (((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃)) → ∃𝑛(𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)))))
25	24	3adant3l 1261	. . . . . . . 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 1955	. . . . . . 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 1650	. . . . 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 1649	. . . 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 1075	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → 𝑥 ∈ Q)
32		simp3rl 1097	. . . . . . . . . . 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 1098	. . . . . . . . . . 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 1204	. . . . . . . . 9 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → (𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))
37		simp3ll 1095	. . . . . . . . . . . 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 1076	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → 𝑥 ∈ 𝐿)
40		simprl 531	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → 𝑛 ∈ N)
41		simprrl 541	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → 1_o <_N 𝑛)
42		simprrr 542	. . . . . . . . . . . 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 1078	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → 𝑦 ∈ 𝑈)
44		prcunqu 7748	. . . . . . . . . . . . 13 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑦 ∈ 𝑈) → (𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)) → (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))
45	38, 43, 44	syl2anc 411	. . . . . . . . . . . 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 7764	. . . . . . . . . . 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 1294	. . . . . . . . . 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 2517	. . . . . . . . . 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 1955	. . . . . . . 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 541	. . . . . . . . . . . 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 2294	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) → (𝑎 ∈ 𝐿 ↔ (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∈ 𝐿))
56	55	anbi1d 465	. . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . 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 2936	. . . . . . . . . . . . 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 542	. . . . . . . . . . 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 2294	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) → (𝑏 ∈ 𝑈 ↔ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))
64	63	anbi2d 464	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) → ((𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈) ↔ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈)))
65	64	anbi2d 464	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) → ((𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)) ↔ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∈ 𝑈))))
66	65	anbi2d 464	. . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . 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 1873	. . . . . . . . . . . . 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 2936	. . . . . . . . . . . 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 1955	. . . . . . . . . . 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 1654	. . . . . . . . . 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 541	. . . . . . . . . . . . . 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 542	. . . . . . . . . . . . . . 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 1070	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑞 ∈ Q)
81		simprl3 1071	. . . . . . . . . . . . . . . 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 1069	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ 𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → 𝑥 ∈ Q)
84		simprrl 541	. . . . . . . . . . . . . . . 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 7765	. . . . . . . . . . . . . . 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 1272	. . . . . . . . . . . . . 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 571	. . . . . . . . . . 11 ⊢ (((𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ 𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞))) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈)))) → (𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
91	90	anasss 399	. . . . . . . . . 10 ⊢ ((𝑏 = (𝑥 +_Q ([⟨(𝑚 +_o 2_o), 1_o⟩] ~_Q ·_Q 𝑞)) ∧ (𝑎 = (𝑥 +_Q0 ([⟨𝑚, 1_o⟩] ~_Q0 ·_Q0 𝑞)) ∧ ((𝑥 ∈ Q ∧ 𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝑈))))) → (𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
92	91	2eximi 1650	. . . . . . . . 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 1647	. . . . . . 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 1945	. . . . 5 ⊢ (∃𝑞∃𝑛(((𝑥 ∈ Q ∧ 𝑥 ∈ 𝐿) ∧ (𝑦 ∈ Q ∧ 𝑦 ∈ 𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) ∧ (𝑞 ∈ Q ∧ (𝑞 +_Q 𝑞) <_Q 𝑃))) ∧ (𝑛 ∈ N ∧ (1_o <_N 𝑛 ∧ 𝑦 <_Q (𝑥 +_Q ([⟨𝑛, 1_o⟩] ~_Q ·_Q 𝑞))))) → ∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
97	96	exlimivv 1945	. . . 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 1712	. . 3 ⊢ (∃𝑏∃𝑎(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))) ↔ ∃𝑎∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
100	98, 99	sylib 122	. 2 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑎∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
101		19.42v 1955	. . . . 5 ⊢ (∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))) ↔ (𝑎 ∈ 𝐿 ∧ ∃𝑏(𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
102		df-rex 2517	. . . . . 6 ⊢ (∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃) ↔ ∃𝑏(𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃)))
103	102	anbi2i 457	. . . . 5 ⊢ ((𝑎 ∈ 𝐿 ∧ ∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃)) ↔ (𝑎 ∈ 𝐿 ∧ ∃𝑏(𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))))
104	101, 103	bitr4i 187	. . . 4 ⊢ (∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))) ↔ (𝑎 ∈ 𝐿 ∧ ∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃)))
105	104	exbii 1654	. . 3 ⊢ (∃𝑎∃𝑏(𝑎 ∈ 𝐿 ∧ (𝑏 ∈ 𝑈 ∧ 𝑏 <_Q (𝑎 +_Q 𝑃))) ↔ ∃𝑎(𝑎 ∈ 𝐿 ∧ ∃𝑏 ∈ 𝑈 𝑏 <_Q (𝑎 +_Q 𝑃)))
106		df-rex 2517	. . 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 1005 = wceq 1398 ∃wex 1541 ∈ wcel 2202 ∃wrex 2512 ⟨cop 3676 class class class wbr 4093 ωcom 4694 (class class class)co 6028 1_oc1o 6618 2_oc2o 6619 +_o coa 6622 [cec 6743 Ncnpi 7535 <_N clti 7538 ~_Q ceq 7542 Qcnq 7543 +_Q cplq 7545 ·_Q cmq 7546 <_Q cltq 7548 ~_Q0 ceq0 7549 +_Q0 cplq0 7552 ·_Q0 cmq0 7553 Pcnp 7554

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-nul 4220 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641 ax-iinf 4692

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-ral 2516 df-rex 2517 df-reu 2518 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-int 3934 df-iun 3977 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-eprel 4392 df-id 4396 df-po 4399 df-iso 4400 df-iord 4469 df-on 4471 df-suc 4474 df-iom 4695 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-ov 6031 df-oprab 6032 df-mpo 6033 df-1st 6312 df-2nd 6313 df-recs 6514 df-irdg 6579 df-1o 6625 df-2o 6626 df-oadd 6629 df-omul 6630 df-er 6745 df-ec 6747 df-qs 6751 df-ni 7567 df-pli 7568 df-mi 7569 df-lti 7570 df-plpq 7607 df-mpq 7608 df-enq 7610 df-nqqs 7611 df-plqqs 7612 df-mqqs 7613 df-1nqqs 7614 df-rq 7615 df-ltnqqs 7616 df-enq0 7687 df-nq0 7688 df-0nq0 7689 df-plq0 7690 df-mq0 7691 df-inp 7729

This theorem is referenced by: prarloc2 7767 addlocpr 7799 prmuloc 7829 ltaddpr 7860 ltexprlemloc 7870 ltexprlemrl 7873 ltexprlemru 7875

W3C validator