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

Theorem prarloc 7041
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 7042 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 7015 . . . . . . 7 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥Q 𝑥𝐿)
2 df-rex 2365 . . . . . . 7 (∃𝑥Q 𝑥𝐿 ↔ ∃𝑥(𝑥Q𝑥𝐿))
31, 2sylib 120 . . . . . 6 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥(𝑥Q𝑥𝐿))
43adantr 270 . . . . 5 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑥(𝑥Q𝑥𝐿))
5 prmu 7016 . . . . . . 7 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑦Q 𝑦𝑈)
6 df-rex 2365 . . . . . . 7 (∃𝑦Q 𝑦𝑈 ↔ ∃𝑦(𝑦Q𝑦𝑈))
75, 6sylib 120 . . . . . 6 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑦(𝑦Q𝑦𝑈))
87adantr 270 . . . . 5 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑦(𝑦Q𝑦𝑈))
9 subhalfnqq 6952 . . . . . . . . 9 (𝑃Q → ∃𝑞Q (𝑞 +Q 𝑞) <Q 𝑃)
109adantl 271 . . . . . . . 8 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑞Q (𝑞 +Q 𝑞) <Q 𝑃)
11 df-rex 2365 . . . . . . . 8 (∃𝑞Q (𝑞 +Q 𝑞) <Q 𝑃 ↔ ∃𝑞(𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))
1210, 11sylib 120 . . . . . . 7 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑞(𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))
1312ancli 316 . . . . . 6 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ ∃𝑞(𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)))
14 19.42v 1834 . . . . . 6 (∃𝑞((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)) ↔ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ ∃𝑞(𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)))
1513, 14sylibr 132 . . . . 5 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑞((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)))
16 eeeanv 1856 . . . . 5 (∃𝑥𝑦𝑞((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ↔ (∃𝑥(𝑥Q𝑥𝐿) ∧ ∃𝑦(𝑦Q𝑦𝑈) ∧ ∃𝑞((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))))
174, 8, 15, 16syl3anbrc 1127 . . . 4 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑥𝑦𝑞((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))))
18 prarloclemarch2 6957 . . . . . . . . . . . . . 14 ((𝑦Q𝑥Q𝑞Q) → ∃𝑛N (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))
19 df-rex 2365 . . . . . . . . . . . . . 14 (∃𝑛N (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))) ↔ ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
2018, 19sylib 120 . . . . . . . . . . . . 13 ((𝑦Q𝑥Q𝑞Q) → ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
21203com12 1147 . . . . . . . . . . . 12 ((𝑥Q𝑦Q𝑞Q) → ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
22213adant1r 1167 . . . . . . . . . . 11 (((𝑥Q𝑥𝐿) ∧ 𝑦Q𝑞Q) → ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
23223adant2r 1169 . . . . . . . . . 10 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ 𝑞Q) → ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
24233adant3r 1171 . . . . . . . . 9 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)) → ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
25243adant3l 1170 . . . . . . . 8 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
2625ancli 316 . . . . . . 7 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))))
27 19.42v 1834 . . . . . . 7 (∃𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) ↔ (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))))
2826, 27sylibr 132 . . . . . 6 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ∃𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))))
29282eximi 1537 . . . . 5 (∃𝑦𝑞((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ∃𝑦𝑞𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))))
3029eximi 1536 . . . 4 (∃𝑥𝑦𝑞((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ∃𝑥𝑦𝑞𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))))
31 simpl1l 994 . . . . . . . . . 10 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑥Q)
32 simp3rl 1016 . . . . . . . . . . 11 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → 𝑞Q)
3332adantr 270 . . . . . . . . . 10 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑞Q)
34 simp3rr 1017 . . . . . . . . . . 11 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → (𝑞 +Q 𝑞) <Q 𝑃)
3534adantr 270 . . . . . . . . . 10 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → (𝑞 +Q 𝑞) <Q 𝑃)
3631, 33, 353jca 1123 . . . . . . . . 9 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → (𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))
37 simp3ll 1014 . . . . . . . . . . . 12 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ⟨𝐿, 𝑈⟩ ∈ P)
3837adantr 270 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → ⟨𝐿, 𝑈⟩ ∈ P)
39 simpl1r 995 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑥𝐿)
40 simprl 498 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑛N)
41 simprrl 506 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 1𝑜 <N 𝑛)
42 simprrr 507 . . . . . . . . . . . 12 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))
43 simpl2r 997 . . . . . . . . . . . . 13 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑦𝑈)
44 prcunqu 7023 . . . . . . . . . . . . 13 ((⟨𝐿, 𝑈⟩ ∈ P𝑦𝑈) → (𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) → (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))
4538, 43, 44syl2anc 403 . . . . . . . . . . . 12 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → (𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) → (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))
4642, 45mpd 13 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)
47 prarloclem 7039 . . . . . . . . . . 11 (((⟨𝐿, 𝑈⟩ ∈ P𝑥𝐿) ∧ (𝑛N𝑞Q ∧ 1𝑜 <N 𝑛) ∧ (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈) → ∃𝑚 ∈ ω ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))
4838, 39, 40, 33, 41, 46, 47syl231anc 1194 . . . . . . . . . 10 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → ∃𝑚 ∈ ω ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))
49 df-rex 2365 . . . . . . . . . 10 (∃𝑚 ∈ ω ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈) ↔ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))
5048, 49sylib 120 . . . . . . . . 9 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))
5136, 50jca 300 . . . . . . . 8 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))
52 19.42v 1834 . . . . . . . 8 (∃𝑚((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) ↔ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))
5351, 52sylibr 132 . . . . . . 7 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → ∃𝑚((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))
54 simprrl 506 . . . . . . . . . . . 12 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿)
55 eleq1 2150 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → (𝑎𝐿 ↔ (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿))
5655anbi1d 453 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → ((𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈) ↔ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))
5756anbi2d 452 . . . . . . . . . . . . . . 15 (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → ((𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)) ↔ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))
5857anbi2d 452 . . . . . . . . . . . . . 14 (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) ↔ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))))
5958ceqsexgv 2744 . . . . . . . . . . . . 13 ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 → (∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))) ↔ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))))
6059biimprcd 158 . . . . . . . . . . . 12 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 → ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))))
6154, 60mpd 13 . . . . . . . . . . 11 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))))
62 simprrr 507 . . . . . . . . . . 11 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)
63 eleq1 2150 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → (𝑏𝑈 ↔ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))
6463anbi2d 452 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → ((𝑎𝐿𝑏𝑈) ↔ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))
6564anbi2d 452 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → ((𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)) ↔ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))
6665anbi2d 452 . . . . . . . . . . . . . . 15 (𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))) ↔ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))))
6766anbi2d 452 . . . . . . . . . . . . . 14 (𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → ((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) ↔ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))))
6867exbidv 1753 . . . . . . . . . . . . 13 (𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → (∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) ↔ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))))
6968ceqsexgv 2744 . . . . . . . . . . . 12 ((𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈 → (∃𝑏(𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))) ↔ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))))
7069biimprcd 158 . . . . . . . . . . 11 (∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))) → ((𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈 → ∃𝑏(𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))))))
7161, 62, 70sylc 61 . . . . . . . . . 10 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → ∃𝑏(𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))))
72 19.42v 1834 . . . . . . . . . . 11 (∃𝑎(𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))) ↔ (𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))))
7372exbii 1541 . . . . . . . . . 10 (∃𝑏𝑎(𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))) ↔ ∃𝑏(𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ ∃𝑎(𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))))
7471, 73sylibr 132 . . . . . . . . 9 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → ∃𝑏𝑎(𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))))
75 simprrl 506 . . . . . . . . . . . . . 14 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))) → 𝑎𝐿)
7675adantl 271 . . . . . . . . . . . . 13 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑎𝐿)
77 simprrr 507 . . . . . . . . . . . . . . 15 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))) → 𝑏𝑈)
7877adantl 271 . . . . . . . . . . . . . 14 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑏𝑈)
79 simpl 107 . . . . . . . . . . . . . . 15 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))))
80 simprl2 989 . . . . . . . . . . . . . . . 16 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑞Q)
81 simprl3 990 . . . . . . . . . . . . . . . 16 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑞 +Q 𝑞) <Q 𝑃)
8280, 81jca 300 . . . . . . . . . . . . . . 15 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))
83 simprl1 988 . . . . . . . . . . . . . . . 16 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑥Q)
84 simprrl 506 . . . . . . . . . . . . . . . 16 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑚 ∈ ω)
8583, 84jca 300 . . . . . . . . . . . . . . 15 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑥Q𝑚 ∈ ω))
86 prarloclemcalc 7040 . . . . . . . . . . . . . . 15 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑥Q𝑚 ∈ ω))) → 𝑏 <Q (𝑎 +Q 𝑃))
8779, 82, 85, 86syl12anc 1172 . . . . . . . . . . . . . 14 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑏 <Q (𝑎 +Q 𝑃))
8878, 87jca 300 . . . . . . . . . . . . 13 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃)))
8976, 88jca 300 . . . . . . . . . . . 12 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9089ancom1s 536 . . . . . . . . . . 11 (((𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ 𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9190anasss 391 . . . . . . . . . 10 ((𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))) → (𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
92912eximi 1537 . . . . . . . . 9 (∃𝑏𝑎(𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9374, 92syl 14 . . . . . . . 8 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9493exlimiv 1534 . . . . . . 7 (∃𝑚((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9553, 94syl 14 . . . . . 6 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9695exlimivv 1824 . . . . 5 (∃𝑞𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9796exlimivv 1824 . . . 4 (∃𝑥𝑦𝑞𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9817, 30, 973syl 17 . . 3 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
99 excom 1599 . . 3 (∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ ∃𝑎𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
10098, 99sylib 120 . 2 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑎𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
101 19.42v 1834 . . . . 5 (∃𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ (𝑎𝐿 ∧ ∃𝑏(𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
102 df-rex 2365 . . . . . 6 (∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃) ↔ ∃𝑏(𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃)))
103102anbi2i 445 . . . . 5 ((𝑎𝐿 ∧ ∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃)) ↔ (𝑎𝐿 ∧ ∃𝑏(𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
104101, 103bitr4i 185 . . . 4 (∃𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ (𝑎𝐿 ∧ ∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
105104exbii 1541 . . 3 (∃𝑎𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ ∃𝑎(𝑎𝐿 ∧ ∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
106 df-rex 2365 . . 3 (∃𝑎𝐿𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃) ↔ ∃𝑎(𝑎𝐿 ∧ ∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
107105, 106bitr4i 185 . 2 (∃𝑎𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ ∃𝑎𝐿𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃))
108100, 107sylib 120 1 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑎𝐿𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 924   = wceq 1289  wex 1426  wcel 1438  wrex 2360  cop 3444   class class class wbr 3837  ωcom 4395  (class class class)co 5634  1𝑜c1o 6156  2𝑜c2o 6157   +𝑜 coa 6160  [cec 6270  Ncnpi 6810   <N clti 6813   ~Q ceq 6817  Qcnq 6818   +Q cplq 6820   ·Q cmq 6821   <Q cltq 6823   ~Q0 ceq0 6824   +Q0 cplq0 6827   ·Q0 cmq0 6828  Pcnp 6829
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3946  ax-sep 3949  ax-nul 3957  ax-pow 4001  ax-pr 4027  ax-un 4251  ax-setind 4343  ax-iinf 4393
This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2839  df-csb 2932  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-int 3684  df-iun 3727  df-br 3838  df-opab 3892  df-mpt 3893  df-tr 3929  df-eprel 4107  df-id 4111  df-po 4114  df-iso 4115  df-iord 4184  df-on 4186  df-suc 4189  df-iom 4396  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-f1 5007  df-fo 5008  df-f1o 5009  df-fv 5010  df-ov 5637  df-oprab 5638  df-mpt2 5639  df-1st 5893  df-2nd 5894  df-recs 6052  df-irdg 6117  df-1o 6163  df-2o 6164  df-oadd 6167  df-omul 6168  df-er 6272  df-ec 6274  df-qs 6278  df-ni 6842  df-pli 6843  df-mi 6844  df-lti 6845  df-plpq 6882  df-mpq 6883  df-enq 6885  df-nqqs 6886  df-plqqs 6887  df-mqqs 6888  df-1nqqs 6889  df-rq 6890  df-ltnqqs 6891  df-enq0 6962  df-nq0 6963  df-0nq0 6964  df-plq0 6965  df-mq0 6966  df-inp 7004
This theorem is referenced by:  prarloc2  7042  addlocpr  7074  prmuloc  7104  ltaddpr  7135  ltexprlemloc  7145  ltexprlemrl  7148  ltexprlemru  7150
  Copyright terms: Public domain W3C validator