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

Theorem prarloc 6601
 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 6602 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 6575 . . . . . . 7 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥Q 𝑥𝐿)
2 df-rex 2312 . . . . . . 7 (∃𝑥Q 𝑥𝐿 ↔ ∃𝑥(𝑥Q𝑥𝐿))
31, 2sylib 127 . . . . . 6 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥(𝑥Q𝑥𝐿))
43adantr 261 . . . . 5 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑥(𝑥Q𝑥𝐿))
5 prmu 6576 . . . . . . 7 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑦Q 𝑦𝑈)
6 df-rex 2312 . . . . . . 7 (∃𝑦Q 𝑦𝑈 ↔ ∃𝑦(𝑦Q𝑦𝑈))
75, 6sylib 127 . . . . . 6 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑦(𝑦Q𝑦𝑈))
87adantr 261 . . . . 5 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑦(𝑦Q𝑦𝑈))
9 subhalfnqq 6512 . . . . . . . . 9 (𝑃Q → ∃𝑞Q (𝑞 +Q 𝑞) <Q 𝑃)
109adantl 262 . . . . . . . 8 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑞Q (𝑞 +Q 𝑞) <Q 𝑃)
11 df-rex 2312 . . . . . . . 8 (∃𝑞Q (𝑞 +Q 𝑞) <Q 𝑃 ↔ ∃𝑞(𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))
1210, 11sylib 127 . . . . . . 7 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑞(𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))
1312ancli 306 . . . . . 6 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ ∃𝑞(𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)))
14 19.42v 1786 . . . . . 6 (∃𝑞((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)) ↔ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ ∃𝑞(𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)))
1513, 14sylibr 137 . . . . 5 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑞((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)))
16 eeeanv 1808 . . . . 5 (∃𝑥𝑦𝑞((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ↔ (∃𝑥(𝑥Q𝑥𝐿) ∧ ∃𝑦(𝑦Q𝑦𝑈) ∧ ∃𝑞((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))))
174, 8, 15, 16syl3anbrc 1088 . . . 4 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑥𝑦𝑞((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))))
18 prarloclemarch2 6517 . . . . . . . . . . . . . 14 ((𝑦Q𝑥Q𝑞Q) → ∃𝑛N (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))
19 df-rex 2312 . . . . . . . . . . . . . 14 (∃𝑛N (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))) ↔ ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
2018, 19sylib 127 . . . . . . . . . . . . 13 ((𝑦Q𝑥Q𝑞Q) → ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
21203com12 1108 . . . . . . . . . . . 12 ((𝑥Q𝑦Q𝑞Q) → ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
22213adant1r 1128 . . . . . . . . . . 11 (((𝑥Q𝑥𝐿) ∧ 𝑦Q𝑞Q) → ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
23223adant2r 1130 . . . . . . . . . 10 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ 𝑞Q) → ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
24233adant3r 1132 . . . . . . . . 9 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃)) → ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
25243adant3l 1131 . . . . . . . 8 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ∃𝑛(𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
2625ancli 306 . . . . . . 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 1786 . . . . . . 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 137 . . . . . 6 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ∃𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))))
29282eximi 1492 . . . . 5 (∃𝑦𝑞((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ∃𝑦𝑞𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))))
3029eximi 1491 . . . 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 955 . . . . . . . . . 10 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑥Q)
32 simp3rl 977 . . . . . . . . . . 11 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → 𝑞Q)
3332adantr 261 . . . . . . . . . 10 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑞Q)
34 simp3rr 978 . . . . . . . . . . 11 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → (𝑞 +Q 𝑞) <Q 𝑃)
3534adantr 261 . . . . . . . . . 10 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → (𝑞 +Q 𝑞) <Q 𝑃)
3631, 33, 353jca 1084 . . . . . . . . 9 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → (𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))
37 simp3ll 975 . . . . . . . . . . . 12 (((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) → ⟨𝐿, 𝑈⟩ ∈ P)
3837adantr 261 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → ⟨𝐿, 𝑈⟩ ∈ P)
39 simpl1r 956 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑥𝐿)
40 simprl 483 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑛N)
41 simprrl 491 . . . . . . . . . . 11 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 1𝑜 <N 𝑛)
42 simprrr 492 . . . . . . . . . . . 12 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))
43 simpl2r 958 . . . . . . . . . . . . 13 ((((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑦𝑈)
44 prcunqu 6583 . . . . . . . . . . . . 13 ((⟨𝐿, 𝑈⟩ ∈ P𝑦𝑈) → (𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) → (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))
4538, 43, 44syl2anc 391 . . . . . . . . . . . 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 6599 . . . . . . . . . . 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 1155 . . . . . . . . . 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 2312 . . . . . . . . . 10 (∃𝑚 ∈ ω ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈) ↔ ∃𝑚(𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))
5048, 49sylib 127 . . . . . . . . 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 290 . . . . . . . 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 1786 . . . . . . . 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 137 . . . . . . 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 491 . . . . . . . . . . . 12 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿)
55 eleq1 2100 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → (𝑎𝐿 ↔ (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿))
5655anbi1d 438 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → ((𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈) ↔ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))
5756anbi2d 437 . . . . . . . . . . . . . . 15 (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → ((𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)) ↔ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))
5857anbi2d 437 . . . . . . . . . . . . . 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 2673 . . . . . . . . . . . . 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 149 . . . . . . . . . . . 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 492 . . . . . . . . . . 11 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ ((𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∈ 𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))) → (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)
63 eleq1 2100 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → (𝑏𝑈 ↔ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))
6463anbi2d 437 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → ((𝑎𝐿𝑏𝑈) ↔ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))
6564anbi2d 437 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → ((𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)) ↔ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈))))
6665anbi2d 437 . . . . . . . . . . . . . . 15 (𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))) ↔ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿 ∧ (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∈ 𝑈)))))
6766anbi2d 437 . . . . . . . . . . . . . 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 1706 . . . . . . . . . . . . 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 2673 . . . . . . . . . . . 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 149 . . . . . . . . . . 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 56 . . . . . . . . . 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 1786 . . . . . . . . . . 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 1496 . . . . . . . . . 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 137 . . . . . . . . 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 491 . . . . . . . . . . . . . 14 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))) → 𝑎𝐿)
7675adantl 262 . . . . . . . . . . . . 13 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑎𝐿)
77 simprrr 492 . . . . . . . . . . . . . . 15 (((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))) → 𝑏𝑈)
7877adantl 262 . . . . . . . . . . . . . 14 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑏𝑈)
79 simpl 102 . . . . . . . . . . . . . . 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 950 . . . . . . . . . . . . . . . 16 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑞Q)
81 simprl3 951 . . . . . . . . . . . . . . . 16 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑞 +Q 𝑞) <Q 𝑃)
8280, 81jca 290 . . . . . . . . . . . . . . 15 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))
83 simprl1 949 . . . . . . . . . . . . . . . 16 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑥Q)
84 simprrl 491 . . . . . . . . . . . . . . . 16 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑚 ∈ ω)
8583, 84jca 290 . . . . . . . . . . . . . . 15 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑥Q𝑚 ∈ ω))
86 prarloclemcalc 6600 . . . . . . . . . . . . . . 15 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑥Q𝑚 ∈ ω))) → 𝑏 <Q (𝑎 +Q 𝑃))
8779, 82, 85, 86syl12anc 1133 . . . . . . . . . . . . . 14 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → 𝑏 <Q (𝑎 +Q 𝑃))
8878, 87jca 290 . . . . . . . . . . . . 13 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃)))
8976, 88jca 290 . . . . . . . . . . . 12 (((𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ 𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9089ancom1s 503 . . . . . . . . . . 11 (((𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ 𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞))) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈)))) → (𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9190anasss 379 . . . . . . . . . 10 ((𝑏 = (𝑥 +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) ∧ (𝑎 = (𝑥 +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ∧ ((𝑥Q𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃) ∧ (𝑚 ∈ ω ∧ (𝑎𝐿𝑏𝑈))))) → (𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
92912eximi 1492 . . . . . . . . 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 1489 . . . . . . 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 1776 . . . . 5 (∃𝑞𝑛(((𝑥Q𝑥𝐿) ∧ (𝑦Q𝑦𝑈) ∧ ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) ∧ (𝑞Q ∧ (𝑞 +Q 𝑞) <Q 𝑃))) ∧ (𝑛N ∧ (1𝑜 <N 𝑛𝑦 <Q (𝑥 +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → ∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
9796exlimivv 1776 . . . 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 1554 . . 3 (∃𝑏𝑎(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ ∃𝑎𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
10098, 99sylib 127 . 2 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑎𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
101 19.42v 1786 . . . . 5 (∃𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ (𝑎𝐿 ∧ ∃𝑏(𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
102 df-rex 2312 . . . . . 6 (∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃) ↔ ∃𝑏(𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃)))
103102anbi2i 430 . . . . 5 ((𝑎𝐿 ∧ ∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃)) ↔ (𝑎𝐿 ∧ ∃𝑏(𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))))
104101, 103bitr4i 176 . . . 4 (∃𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ (𝑎𝐿 ∧ ∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
105104exbii 1496 . . 3 (∃𝑎𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ ∃𝑎(𝑎𝐿 ∧ ∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
106 df-rex 2312 . . 3 (∃𝑎𝐿𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃) ↔ ∃𝑎(𝑎𝐿 ∧ ∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
107105, 106bitr4i 176 . 2 (∃𝑎𝑏(𝑎𝐿 ∧ (𝑏𝑈𝑏 <Q (𝑎 +Q 𝑃))) ↔ ∃𝑎𝐿𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃))
108100, 107sylib 127 1 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑎𝐿𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885   = wceq 1243  ∃wex 1381   ∈ wcel 1393  ∃wrex 2307  ⟨cop 3378   class class class wbr 3764  ωcom 4313  (class class class)co 5512  1𝑜c1o 5994  2𝑜c2o 5995   +𝑜 coa 5998  [cec 6104  Ncnpi 6370
 Copyright terms: Public domain W3C validator