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

Theorem prarloc 7423
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 7424 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.
StepHypRef Expression
1 prml 7397 . . . . . . 7 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥Q 𝑥𝐿)
2 df-rex 2441 . . . . . . 7 (∃𝑥Q 𝑥𝐿 ↔ ∃𝑥(𝑥Q𝑥𝐿))
31, 2sylib 121 . . . . . 6 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥(𝑥Q𝑥𝐿))
43adantr 274 . . . . 5 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑥(𝑥Q𝑥𝐿))
5 prmu 7398 . . . . . . 7 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑦Q 𝑦𝑈)
6 df-rex 2441 . . . . . . 7 (∃𝑦Q 𝑦𝑈 ↔ ∃𝑦(𝑦Q𝑦𝑈))
75, 6sylib 121 . . . . . 6 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑦(𝑦Q𝑦𝑈))
87adantr 274 . . . . 5 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑦(𝑦Q𝑦𝑈))
9 subhalfnqq 7334 . . . . . . . . 9 (𝑃Q → ∃𝑞Q (𝑞 +Q 𝑞) <Q 𝑃)
109adantl 275 . . . . . . . 8 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑞Q (𝑞 +Q 𝑞) <Q 𝑃)
11 df-rex 2441 . . . . . . . 8 (∃𝑞Q (𝑞 +Q 𝑞) <Q 𝑃 ↔ ∃𝑞(𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))
1210, 11sylib 121 . . . . . . 7 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑞(𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))
1312ancli 321 . . . . . 6 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ ∃𝑞(𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)))
14 19.42v 1886 . . . . . 6 (∃𝑞((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)) ↔ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ ∃𝑞(𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)))
1513, 14sylibr 133 . . . . 5 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑞((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)))
16 eeeanv 1913 . . . . 5 (∃𝑥𝑦𝑞((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ↔ (∃𝑥(𝑥Q𝑥𝐿) ∧ ∃𝑦(𝑦Q𝑦𝑈) ∧ ∃𝑞((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))))
174, 8, 15, 16syl3anbrc 1166 . . . 4 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑥𝑦𝑞((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))))
18 prarloclemarch2 7339 . . . . . . . . . . . . . 14 ((𝑦Q𝑥Q𝑞Q) → ∃𝑛N (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))
19 df-rex 2441 . . . . . . . . . . . . . 14 (∃𝑛N (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))) ↔ ∃𝑛(𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)))))
2018, 19sylib 121 . . . . . . . . . . . . 13 ((𝑦Q𝑥Q𝑞Q) → ∃𝑛(𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)))))
21203com12 1189 . . . . . . . . . . . 12 ((𝑥Q𝑦Q𝑞Q) → ∃𝑛(𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)))))
22213adant1r 1213 . . . . . . . . . . 11 (((𝑥Q𝑥𝐿) ∧ 𝑦Q𝑞Q) → ∃𝑛(𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)))))
23223adant2r 1215 . . . . . . . . . 10 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ 𝑞Q) → ∃𝑛(𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)))))
24233adant3r 1217 . . . . . . . . 9 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)) → ∃𝑛(𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)))))
25243adant3l 1216 . . . . . . . 8 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ∃𝑛(𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)))))
2625ancli 321 . . . . . . 7 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ ∃𝑛(𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))))
27 19.42v 1886 . . . . . . 7 (∃𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) ↔ (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ ∃𝑛(𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))))
2826, 27sylibr 133 . . . . . 6 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ∃𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))))
29282eximi 1581 . . . . 5 (∃𝑦𝑞((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ∃𝑦𝑞𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))))
3029eximi 1580 . . . 4 (∃𝑥𝑦𝑞((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ∃𝑥𝑦𝑞𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))))
31 simpl1l 1033 . . . . . . . . . 10 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → 𝑥Q)
32 simp3rl 1055 . . . . . . . . . . 11 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → 𝑞Q)
3332adantr 274 . . . . . . . . . 10 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → 𝑞Q)
34 simp3rr 1056 . . . . . . . . . . 11 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → (𝑞 +Q 𝑞) <Q 𝑃)
3534adantr 274 . . . . . . . . . 10 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → (𝑞 +Q 𝑞) <Q 𝑃)
3631, 33, 353jca 1162 . . . . . . . . 9 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → (𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))
37 simp3ll 1053 . . . . . . . . . . . 12 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ⟨𝐿, 𝑈⟩ ∈ P)
3837adantr 274 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → ⟨𝐿, 𝑈⟩ ∈ P)
39 simpl1r 1034 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → 𝑥𝐿)
40 simprl 521 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → 𝑛N)
41 simprrl 529 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → 1o <N 𝑛)
42 simprrr 530 . . . . . . . . . . . 12 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → 𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)))
43 simpl2r 1036 . . . . . . . . . . . . 13 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → 𝑦𝑈)
44 prcunqu 7405 . . . . . . . . . . . . 13 ((⟨𝐿, 𝑈⟩ ∈ P𝑦𝑈) → (𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)) → (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))
4538, 43, 44syl2anc 409 . . . . . . . . . . . 12 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → (𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)) → (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))
4642, 45mpd 13 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)
47 prarloclem 7421 . . . . . . . . . . 11 (((⟨𝐿, 𝑈⟩ ∈ P𝑥𝐿) ∧ (𝑛N𝑞Q ∧ 1o <N 𝑛) ∧ (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈) → ∃𝑚 ∈ ω ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))
4838, 39, 40, 33, 41, 46, 47syl231anc 1240 . . . . . . . . . 10 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → ∃𝑚 ∈ ω ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))
49 df-rex 2441 . . . . . . . . . 10 (∃𝑚 ∈ ω ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈) ↔ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))
5048, 49sylib 121 . . . . . . . . 9 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))
5136, 50jca 304 . . . . . . . 8 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))
52 19.42v 1886 . . . . . . . 8 (∃𝑚((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) ↔ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))
5351, 52sylibr 133 . . . . . . 7 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → ∃𝑚((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))
54 simprrl 529 . . . . . . . . . . . 12 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿)
55 eleq1 2220 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) → (𝑎𝐿 ↔ (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿))
5655anbi1d 461 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) → ((𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈) ↔ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))
5756anbi2d 460 . . . . . . . . . . . . . . 15 (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) → ((𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)) ↔ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))
5857anbi2d 460 . . . . . . . . . . . . . 14 (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) → (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) ↔ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))))
5958ceqsexgv 2841 . . . . . . . . . . . . 13 ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 → (∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))) ↔ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))))
6059biimprcd 159 . . . . . . . . . . . 12 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 → ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))))
6154, 60mpd 13 . . . . . . . . . . 11 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))))
62 simprrr 530 . . . . . . . . . . 11 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)
63 eleq1 2220 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) → (𝑏𝑈 ↔ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))
6463anbi2d 460 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) → ((𝑎𝐿𝑏𝑈) ↔ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))
6564anbi2d 460 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) → ((𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)) ↔ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))
6665anbi2d 460 . . . . . . . . . . . . . . 15 (𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) → (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))) ↔ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))))
6766anbi2d 460 . . . . . . . . . . . . . 14 (𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) → ((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) ↔ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))))
6867exbidv 1805 . . . . . . . . . . . . 13 (𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) → (∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) ↔ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))))
6968ceqsexgv 2841 . . . . . . . . . . . 12 ((𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈 → (∃𝑏(𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))) ↔ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))))
7069biimprcd 159 . . . . . . . . . . 11 (∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))) → ((𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈 → ∃𝑏(𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))))))
7161, 62, 70sylc 62 . . . . . . . . . 10 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → ∃𝑏(𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))))
72 19.42v 1886 . . . . . . . . . . 11 (∃𝑎(𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))) ↔ (𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))))
7372exbii 1585 . . . . . . . . . 10 (∃𝑏𝑎(𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))) ↔ ∃𝑏(𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))))
7471, 73sylibr 133 . . . . . . . . 9 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → ∃𝑏𝑎(𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))))
75 simprrl 529 . . . . . . . . . . . . . 14 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))) → 𝑎𝐿)
7675adantl 275 . . . . . . . . . . . . 13 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑎𝐿)
77 simprrr 530 . . . . . . . . . . . . . . 15 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))) → 𝑏𝑈)
7877adantl 275 . . . . . . . . . . . . . 14 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑏𝑈)
79 simpl 108 . . . . . . . . . . . . . . 15 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))))
80 simprl2 1028 . . . . . . . . . . . . . . . 16 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑞Q)
81 simprl3 1029 . . . . . . . . . . . . . . . 16 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑞 +Q 𝑞) <Q 𝑃)
8280, 81jca 304 . . . . . . . . . . . . . . 15 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))
83 simprl1 1027 . . . . . . . . . . . . . . . 16 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑥Q)
84 simprrl 529 . . . . . . . . . . . . . . . 16 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑚 ∈ ω)
8583, 84jca 304 . . . . . . . . . . . . . . 15 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑥Q𝑚 ∈ ω))
86 prarloclemcalc 7422 . . . . . . . . . . . . . . 15 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑥Q𝑚 ∈ ω))) → 𝑏 <Q (𝑎 +Q 𝑃))
8779, 82, 85, 86syl12anc 1218 . . . . . . . . . . . . . 14 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑏 <Q (𝑎 +Q 𝑃))
8878, 87jca 304 . . . . . . . . . . . . 13 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃)))
8976, 88jca 304 . . . . . . . . . . . 12 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9089ancom1s 559 . . . . . . . . . . 11 (((𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∧ 𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9190anasss 397 . . . . . . . . . 10 ((𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))) → (𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
92912eximi 1581 . . . . . . . . 9 (∃𝑏𝑎(𝑏 = (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9374, 92syl 14 . . . . . . . 8 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9493exlimiv 1578 . . . . . . 7 (∃𝑚((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1o⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +o 2o), 1o⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9553, 94syl 14 . . . . . 6 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9695exlimivv 1876 . . . . 5 (∃𝑞𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9796exlimivv 1876 . . . 4 (∃𝑥𝑦𝑞𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1o <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1o⟩] ~Q ·Q 𝑞))))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9817, 30, 973syl 17 . . 3 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
99 excom 1644 . . 3 (∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ ∃𝑎𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
10098, 99sylib 121 . 2 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑎𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
101 19.42v 1886 . . . . 5 (∃𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ (𝑎𝐿 ∧ ∃𝑏(𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
102 df-rex 2441 . . . . . 6 (∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃) ↔ ∃𝑏(𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃)))
103102anbi2i 453 . . . . 5 ((𝑎𝐿 ∧ ∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃)) ↔ (𝑎𝐿 ∧ ∃𝑏(𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
104101, 103bitr4i 186 . . . 4 (∃𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ (𝑎𝐿 ∧ ∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
105104exbii 1585 . . 3 (∃𝑎𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ ∃𝑎(𝑎𝐿 ∧ ∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
106 df-rex 2441 . . 3 (∃𝑎𝐿𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃) ↔ ∃𝑎(𝑎𝐿 ∧ ∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
107105, 106bitr4i 186 . 2 (∃𝑎𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ ∃𝑎𝐿𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃))
108100, 107sylib 121 1 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑎𝐿𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 963   = wceq 1335  wex 1472  wcel 2128  wrex 2436  cop 3563   class class class wbr 3965  ωcom 4549  (class class class)co 5824  1oc1o 6356  2oc2o 6357   +o coa 6360  [cec 6478  Ncnpi 7192   <N clti 7195   ~Q ceq 7199  Qcnq 7200   +Q cplq 7202   ·Q cmq 7203   <Q cltq 7205   ~Q0 ceq0 7206   +Q0 cplq0 7209   ·Q0 cmq0 7210  Pcnp 7211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4496  ax-iinf 4547
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-eprel 4249  df-id 4253  df-po 4256  df-iso 4257  df-iord 4326  df-on 4328  df-suc 4331  df-iom 4550  df-xp 4592  df-rel 4593  df-cnv 4594  df-co 4595  df-dm 4596  df-rn 4597  df-res 4598  df-ima 4599  df-iota 5135  df-fun 5172  df-fn 5173  df-f 5174  df-f1 5175  df-fo 5176  df-f1o 5177  df-fv 5178  df-ov 5827  df-oprab 5828  df-mpo 5829  df-1st 6088  df-2nd 6089  df-recs 6252  df-irdg 6317  df-1o 6363  df-2o 6364  df-oadd 6367  df-omul 6368  df-er 6480  df-ec 6482  df-qs 6486  df-ni 7224  df-pli 7225  df-mi 7226  df-lti 7227  df-plpq 7264  df-mpq 7265  df-enq 7267  df-nqqs 7268  df-plqqs 7269  df-mqqs 7270  df-1nqqs 7271  df-rq 7272  df-ltnqqs 7273  df-enq0 7344  df-nq0 7345  df-0nq0 7346  df-plq0 7347  df-mq0 7348  df-inp 7386
This theorem is referenced by:  prarloc2  7424  addlocpr  7456  prmuloc  7486  ltaddpr  7517  ltexprlemloc  7527  ltexprlemrl  7530  ltexprlemru  7532
  Copyright terms: Public domain W3C validator