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

Theorem prarloc 6485
 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 6486 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 𝑚 𝑛 𝑞 x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prml 6459 . . . . . . 7 (⟨𝐿, 𝑈 Px Q x 𝐿)
2 df-rex 2306 . . . . . . 7 (x Q x 𝐿x(x Q x 𝐿))
31, 2sylib 127 . . . . . 6 (⟨𝐿, 𝑈 Px(x Q x 𝐿))
43adantr 261 . . . . 5 ((⟨𝐿, 𝑈 P 𝑃 Q) → x(x Q x 𝐿))
5 prmu 6460 . . . . . . 7 (⟨𝐿, 𝑈 Py Q y 𝑈)
6 df-rex 2306 . . . . . . 7 (y Q y 𝑈y(y Q y 𝑈))
75, 6sylib 127 . . . . . 6 (⟨𝐿, 𝑈 Py(y Q y 𝑈))
87adantr 261 . . . . 5 ((⟨𝐿, 𝑈 P 𝑃 Q) → y(y Q y 𝑈))
9 subhalfnqq 6397 . . . . . . . . 9 (𝑃 Q𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃)
109adantl 262 . . . . . . . 8 ((⟨𝐿, 𝑈 P 𝑃 Q) → 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃)
11 df-rex 2306 . . . . . . . 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 1783 . . . . . 6 (𝑞((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃)) ↔ ((⟨𝐿, 𝑈 P 𝑃 Q) 𝑞(𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃)))
1513, 14sylibr 137 . . . . 5 ((⟨𝐿, 𝑈 P 𝑃 Q) → 𝑞((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃)))
16 eeeanv 1805 . . . . 5 (xy𝑞((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) ↔ (x(x Q x 𝐿) y(y Q y 𝑈) 𝑞((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))))
174, 8, 15, 16syl3anbrc 1087 . . . 4 ((⟨𝐿, 𝑈 P 𝑃 Q) → xy𝑞((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))))
18 prarloclemarch2 6402 . . . . . . . . . . . . . 14 ((y Q x Q 𝑞 Q) → 𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))
19 df-rex 2306 . . . . . . . . . . . . . 14 (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))) ↔ 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
2018, 19sylib 127 . . . . . . . . . . . . 13 ((y Q x Q 𝑞 Q) → 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
21203com12 1107 . . . . . . . . . . . 12 ((x Q y Q 𝑞 Q) → 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
22213adant1r 1127 . . . . . . . . . . 11 (((x Q x 𝐿) y Q 𝑞 Q) → 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
23223adant2r 1129 . . . . . . . . . 10 (((x Q x 𝐿) (y Q y 𝑈) 𝑞 Q) → 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
24233adant3r 1131 . . . . . . . . 9 (((x Q x 𝐿) (y Q y 𝑈) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃)) → 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
25243adant3l 1130 . . . . . . . 8 (((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) → 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
2625ancli 306 . . . . . . 7 (((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) → (((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))))
27 19.42v 1783 . . . . . . 7 (𝑛(((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) ↔ (((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))))
2826, 27sylibr 137 . . . . . 6 (((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) → 𝑛(((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))))
29282eximi 1489 . . . . 5 (y𝑞((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) → y𝑞𝑛(((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))))
3029eximi 1488 . . . 4 (xy𝑞((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) → xy𝑞𝑛(((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))))
31 simpl1l 954 . . . . . . . . . 10 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → x Q)
32 simp3rl 976 . . . . . . . . . . 11 (((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) → 𝑞 Q)
3332adantr 261 . . . . . . . . . 10 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑞 Q)
34 simp3rr 977 . . . . . . . . . . 11 (((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) → (𝑞 +Q 𝑞) <Q 𝑃)
3534adantr 261 . . . . . . . . . 10 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → (𝑞 +Q 𝑞) <Q 𝑃)
3631, 33, 353jca 1083 . . . . . . . . 9 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → (x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))
37 simp3ll 974 . . . . . . . . . . . 12 (((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) → ⟨𝐿, 𝑈 P)
3837adantr 261 . . . . . . . . . . 11 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → ⟨𝐿, 𝑈 P)
39 simpl1r 955 . . . . . . . . . . 11 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → x 𝐿)
40 simprl 483 . . . . . . . . . . 11 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑛 N)
41 simprrl 491 . . . . . . . . . . 11 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 1𝑜 <N 𝑛)
42 simprrr 492 . . . . . . . . . . . 12 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))
43 simpl2r 957 . . . . . . . . . . . . 13 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → y 𝑈)
44 prcunqu 6467 . . . . . . . . . . . . 13 ((⟨𝐿, 𝑈 P y 𝑈) → (y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) → (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))
4538, 43, 44syl2anc 391 . . . . . . . . . . . 12 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → (y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) → (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))
4642, 45mpd 13 . . . . . . . . . . 11 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)
47 prarloclem 6483 . . . . . . . . . . 11 (((⟨𝐿, 𝑈 P x 𝐿) (𝑛 N 𝑞 Q 1𝑜 <N 𝑛) (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈) → 𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))
4838, 39, 40, 33, 41, 46, 47syl231anc 1154 . . . . . . . . . 10 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))
49 df-rex 2306 . . . . . . . . . 10 (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈) ↔ 𝑚(𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))
5048, 49sylib 127 . . . . . . . . 9 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑚(𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))
5136, 50jca 290 . . . . . . . 8 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) 𝑚(𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))))
52 19.42v 1783 . . . . . . . 8 (𝑚((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))) ↔ ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) 𝑚(𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))))
5351, 52sylibr 137 . . . . . . 7 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑚((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))))
54 simprrl 491 . . . . . . . . . . . 12 (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))) → (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿)
55 eleq1 2097 . . . . . . . . . . . . . . . . 17 (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → (𝑎 𝐿 ↔ (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿))
5655anbi1d 438 . . . . . . . . . . . . . . . 16 (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → ((𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈) ↔ ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))
5756anbi2d 437 . . . . . . . . . . . . . . 15 (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → ((𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)) ↔ (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))))
5857anbi2d 437 . . . . . . . . . . . . . 14 (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))) ↔ ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))))
5958ceqsexgv 2667 . . . . . . . . . . . . 13 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 → (𝑎(𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))) ↔ ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))))
6059biimprcd 149 . . . . . . . . . . . 12 (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))) → ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿𝑎(𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))))))
6154, 60mpd 13 . . . . . . . . . . 11 (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))) → 𝑎(𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))))
62 simprrr 492 . . . . . . . . . . 11 (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))) → (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)
63 eleq1 2097 . . . . . . . . . . . . . . . . . 18 (𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → (𝑏 𝑈 ↔ (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))
6463anbi2d 437 . . . . . . . . . . . . . . . . 17 (𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → ((𝑎 𝐿 𝑏 𝑈) ↔ (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))
6564anbi2d 437 . . . . . . . . . . . . . . . 16 (𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → ((𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)) ↔ (𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))))
6665anbi2d 437 . . . . . . . . . . . . . . 15 (𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))) ↔ ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))))
6766anbi2d 437 . . . . . . . . . . . . . 14 (𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → ((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) ↔ (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))))))
6867exbidv 1703 . . . . . . . . . . . . 13 (𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → (𝑎(𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) ↔ 𝑎(𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))))))
6968ceqsexgv 2667 . . . . . . . . . . . 12 ((x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈 → (𝑏(𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑎(𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))))) ↔ 𝑎(𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))))))
7069biimprcd 149 . . . . . . . . . . 11 (𝑎(𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))) → ((x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈𝑏(𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑎(𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))))))
7161, 62, 70sylc 56 . . . . . . . . . 10 (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))) → 𝑏(𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑎(𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))))))
72 19.42v 1783 . . . . . . . . . . 11 (𝑎(𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))))) ↔ (𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑎(𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))))))
7372exbii 1493 . . . . . . . . . 10 (𝑏𝑎(𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))))) ↔ 𝑏(𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑎(𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))))))
7471, 73sylibr 137 . . . . . . . . 9 (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))) → 𝑏𝑎(𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))))))
75 simprrl 491 . . . . . . . . . . . . . 14 (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))) → 𝑎 𝐿)
7675adantl 262 . . . . . . . . . . . . 13 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → 𝑎 𝐿)
77 simprrr 492 . . . . . . . . . . . . . . 15 (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))) → 𝑏 𝑈)
7877adantl 262 . . . . . . . . . . . . . 14 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → 𝑏 𝑈)
79 simpl 102 . . . . . . . . . . . . . . 15 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))))
80 simprl2 949 . . . . . . . . . . . . . . . 16 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → 𝑞 Q)
81 simprl3 950 . . . . . . . . . . . . . . . 16 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → (𝑞 +Q 𝑞) <Q 𝑃)
8280, 81jca 290 . . . . . . . . . . . . . . 15 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))
83 simprl1 948 . . . . . . . . . . . . . . . 16 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → x Q)
84 simprrl 491 . . . . . . . . . . . . . . . 16 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → 𝑚 𝜔)
8583, 84jca 290 . . . . . . . . . . . . . . 15 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → (x Q 𝑚 𝜔))
86 prarloclemcalc 6484 . . . . . . . . . . . . . . 15 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (x Q 𝑚 𝜔))) → 𝑏 <Q (𝑎 +Q 𝑃))
8779, 82, 85, 86syl12anc 1132 . . . . . . . . . . . . . 14 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → 𝑏 <Q (𝑎 +Q 𝑃))
8878, 87jca 290 . . . . . . . . . . . . 13 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
8976, 88jca 290 . . . . . . . . . . . 12 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → (𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
9089ancom1s 503 . . . . . . . . . . 11 (((𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → (𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
9190anasss 379 . . . . . . . . . 10 ((𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))))) → (𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
92912eximi 1489 . . . . . . . . 9 (𝑏𝑎(𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))))) → 𝑏𝑎(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
9374, 92syl 14 . . . . . . . 8 (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))) → 𝑏𝑎(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
9493exlimiv 1486 . . . . . . 7 (𝑚((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))) → 𝑏𝑎(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
9553, 94syl 14 . . . . . 6 ((((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑏𝑎(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
9695exlimivv 1773 . . . . 5 (𝑞𝑛(((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑏𝑎(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
9796exlimivv 1773 . . . 4 (xy𝑞𝑛(((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))) (𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))) → 𝑏𝑎(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
9817, 30, 973syl 17 . . 3 ((⟨𝐿, 𝑈 P 𝑃 Q) → 𝑏𝑎(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
99 excom 1551 . . 3 (𝑏𝑎(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))) ↔ 𝑎𝑏(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
10098, 99sylib 127 . 2 ((⟨𝐿, 𝑈 P 𝑃 Q) → 𝑎𝑏(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
101 19.42v 1783 . . . . 5 (𝑏(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))) ↔ (𝑎 𝐿 𝑏(𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
102 df-rex 2306 . . . . . 6 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃) ↔ 𝑏(𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
103102anbi2i 430 . . . . 5 ((𝑎 𝐿 𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃)) ↔ (𝑎 𝐿 𝑏(𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
104101, 103bitr4i 176 . . . 4 (𝑏(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))) ↔ (𝑎 𝐿 𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
105104exbii 1493 . . 3 (𝑎𝑏(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))) ↔ 𝑎(𝑎 𝐿 𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
106 df-rex 2306 . . 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 884   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ∃wrex 2301  ⟨cop 3370   class class class wbr 3755  𝜔com 4256  (class class class)co 5455  1𝑜c1o 5933  2𝑜c2o 5934   +𝑜 coa 5937  [cec 6040  Ncnpi 6256
 Copyright terms: Public domain W3C validator