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

Theorem prarloc 6357
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. (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 6331 . . . . . . 7 (⟨𝐿, 𝑈 Px Q x 𝐿)
2 df-rex 2290 . . . . . . 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 6332 . . . . . . 7 (⟨𝐿, 𝑈 Py Q y 𝑈)
6 df-rex 2290 . . . . . . 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 6271 . . . . . . . . 9 (𝑃 Q𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃)
109adantl 262 . . . . . . . 8 ((⟨𝐿, 𝑈 P 𝑃 Q) → 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃)
11 df-rex 2290 . . . . . . . 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 1768 . . . . . 6 (𝑞((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃)) ↔ ((⟨𝐿, 𝑈 P 𝑃 Q) 𝑞(𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃)))
1513, 14sylibr 137 . . . . 5 ((⟨𝐿, 𝑈 P 𝑃 Q) → 𝑞((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃)))
16 eeeanv 1790 . . . . 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 1075 . . . 4 ((⟨𝐿, 𝑈 P 𝑃 Q) → xy𝑞((x Q x 𝐿) (y Q y 𝑈) ((⟨𝐿, 𝑈 P 𝑃 Q) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃))))
18 prarloclemarch2 6276 . . . . . . . . . . . . . 14 ((y Q x Q 𝑞 Q) → 𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞))))
19 df-rex 2290 . . . . . . . . . . . . . 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 1094 . . . . . . . . . . . 12 ((x Q y Q 𝑞 Q) → 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
22213adant1r 1114 . . . . . . . . . . 11 (((x Q x 𝐿) y Q 𝑞 Q) → 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
23223adant2r 1116 . . . . . . . . . 10 (((x Q x 𝐿) (y Q y 𝑈) 𝑞 Q) → 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
24233adant3r 1118 . . . . . . . . 9 (((x Q x 𝐿) (y Q y 𝑈) (𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃)) → 𝑛(𝑛 N (1𝑜 <N 𝑛 y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)))))
25243adant3l 1117 . . . . . . . 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 1768 . . . . . . 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 1474 . . . . 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 1473 . . . 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 943 . . . . . . . . . 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 965 . . . . . . . . . . 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 966 . . . . . . . . . . 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 1069 . . . . . . . . 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 963 . . . . . . . . . . . 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 944 . . . . . . . . . . 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 471 . . . . . . . . . . 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 479 . . . . . . . . . . 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 480 . . . . . . . . . . . 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 946 . . . . . . . . . . . . 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 6339 . . . . . . . . . . . . 13 ((⟨𝐿, 𝑈 P y 𝑈) → (y <Q (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) → (x +Q ([⟨𝑛, 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))
4538, 43, 44syl2anc 393 . . . . . . . . . . . 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 6355 . . . . . . . . . . 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 1141 . . . . . . . . . 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 2290 . . . . . . . . . 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 1768 . . . . . . . 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 479 . . . . . . . . . . . 12 (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))) → (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿)
55 eleq1 2082 . . . . . . . . . . . . . . . . 17 (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → (𝑎 𝐿 ↔ (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿))
5655anbi1d 441 . . . . . . . . . . . . . . . 16 (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → ((𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈) ↔ ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))
5756anbi2d 440 . . . . . . . . . . . . . . 15 (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) → ((𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)) ↔ (𝑚 𝜔 ((x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))))
5857anbi2d 440 . . . . . . . . . . . . . 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 2650 . . . . . . . . . . . . 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 480 . . . . . . . . . . 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 2082 . . . . . . . . . . . . . . . . . 18 (𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → (𝑏 𝑈 ↔ (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))
6463anbi2d 440 . . . . . . . . . . . . . . . . 17 (𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → ((𝑎 𝐿 𝑏 𝑈) ↔ (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))
6564anbi2d 440 . . . . . . . . . . . . . . . 16 (𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → ((𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)) ↔ (𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈))))
6665anbi2d 440 . . . . . . . . . . . . . . 15 (𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) → (((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))) ↔ ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑈)))))
6766anbi2d 440 . . . . . . . . . . . . . 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 1688 . . . . . . . . . . . . 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 2650 . . . . . . . . . . . 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 1768 . . . . . . . . . . 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 1478 . . . . . . . . . 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 479 . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . 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 ax-ia1 99 . . . . . . . . . . . . . . 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 938 . . . . . . . . . . . . . . . 16 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → 𝑞 Q)
81 simprl3 939 . . . . . . . . . . . . . . . 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 937 . . . . . . . . . . . . . . . 16 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → x Q)
84 simprrl 479 . . . . . . . . . . . . . . . 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 6356 . . . . . . . . . . . . . . 15 (((𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) 𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞))) ((𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (x Q 𝑚 𝜔))) → 𝑏 <Q (𝑎 +Q 𝑃))
8779, 82, 85, 86syl12anc 1119 . . . . . . . . . . . . . 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 491 . . . . . . . . . . 11 (((𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) 𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞))) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈)))) → (𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
9190anasss 381 . . . . . . . . . 10 ((𝑏 = (x +Q ([⟨(𝑚 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑞)) (𝑎 = (x +Q0 ([⟨𝑚, 1𝑜⟩] ~Q0 ·Q0 𝑞)) ((x Q 𝑞 Q (𝑞 +Q 𝑞) <Q 𝑃) (𝑚 𝜔 (𝑎 𝐿 𝑏 𝑈))))) → (𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
92912eximi 1474 . . . . . . . . 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 1471 . . . . . . 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 1758 . . . . 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 1758 . . . 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 1536 . . 3 (𝑏𝑎(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))) ↔ 𝑎𝑏(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
10098, 99sylib 127 . 2 ((⟨𝐿, 𝑈 P 𝑃 Q) → 𝑎𝑏(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
101 19.42v 1768 . . . . 5 (𝑏(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))) ↔ (𝑎 𝐿 𝑏(𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
102 df-rex 2290 . . . . . 6 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃) ↔ 𝑏(𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
103102anbi2i 433 . . . . 5 ((𝑎 𝐿 𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃)) ↔ (𝑎 𝐿 𝑏(𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))))
104101, 103bitr4i 176 . . . 4 (𝑏(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))) ↔ (𝑎 𝐿 𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
105104exbii 1478 . . 3 (𝑎𝑏(𝑎 𝐿 (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))) ↔ 𝑎(𝑎 𝐿 𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃)))
106 df-rex 2290 . . 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 873   = wceq 1228  wex 1362   wcel 1374  wrex 2285  cop 3353   class class class wbr 3738  𝜔com 4240  (class class class)co 5436  1𝑜c1o 5909  2𝑜c2o 5910   +𝑜 coa 5913  [cec 6015  Ncnpi 6130   <N clti 6133   ~Q ceq 6137  Qcnq 6138   +Q cplq 6140   ·Q cmq 6141   <Q cltq 6143   ~Q0 ceq0 6144   +Q0 cplq0 6147   ·Q0 cmq0 6148  Pcnp 6149
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-13 1385  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-coll 3846  ax-sep 3849  ax-nul 3857  ax-pow 3901  ax-pr 3918  ax-un 4120  ax-setind 4204  ax-iinf 4238
This theorem depends on definitions:  df-bi 110  df-dc 734  df-3or 874  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2289  df-rex 2290  df-reu 2291  df-rab 2293  df-v 2537  df-sbc 2742  df-csb 2830  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-int 3590  df-iun 3633  df-br 3739  df-opab 3793  df-mpt 3794  df-tr 3829  df-eprel 4000  df-id 4004  df-po 4007  df-iso 4008  df-iord 4052  df-on 4054  df-suc 4057  df-iom 4241  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-rn 4283  df-res 4284  df-ima 4285  df-iota 4794  df-fun 4831  df-fn 4832  df-f 4833  df-f1 4834  df-fo 4835  df-f1o 4836  df-fv 4837  df-ov 5439  df-oprab 5440  df-mpt2 5441  df-1st 5690  df-2nd 5691  df-recs 5842  df-irdg 5878  df-1o 5916  df-2o 5917  df-oadd 5920  df-omul 5921  df-er 6017  df-ec 6019  df-qs 6023  df-ni 6164  df-pli 6165  df-mi 6166  df-lti 6167  df-plpq 6203  df-mpq 6204  df-enq 6206  df-nqqs 6207  df-plqqs 6208  df-mqqs 6209  df-1nqqs 6210  df-rq 6211  df-ltnqqs 6212  df-enq0 6279  df-nq0 6280  df-0nq0 6281  df-plq0 6282  df-mq0 6283  df-inp 6320
This theorem is referenced by:  prarloc2  6358  addlocpr  6391  prmuloc  6410  ltaddpr  6434  ltexprlemloc  6444  ltexprlemrl  6447  ltexprlemru  6449  addcanprleml  6451
  Copyright terms: Public domain W3C validator