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

Theorem caucvgprprlemnkltj 6787
 Description: Lemma for caucvgprpr 6810. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.)
Hypotheses
Ref Expression
caucvgprpr.f (𝜑𝐹:NP)
caucvgprpr.cau (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
caucvgprprlemnkj.k (𝜑𝐾N)
caucvgprprlemnkj.j (𝜑𝐽N)
caucvgprprlemnkj.s (𝜑𝑆Q)
Assertion
Ref Expression
caucvgprprlemnkltj ((𝜑𝐾 <N 𝐽) → ¬ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩))
Distinct variable groups:   𝑘,𝐹,𝑛   𝐽,𝑝,𝑞   𝐾,𝑝,𝑞   𝐾,𝑙,𝑝   𝑢,𝐾,𝑞   𝑆,𝑝,𝑞   𝑘,𝑙,𝑛   𝑢,𝑘,𝑛
Allowed substitution hints:   𝜑(𝑢,𝑘,𝑛,𝑞,𝑝,𝑙)   𝑆(𝑢,𝑘,𝑛,𝑙)   𝐹(𝑢,𝑞,𝑝,𝑙)   𝐽(𝑢,𝑘,𝑛,𝑙)   𝐾(𝑘,𝑛)

Proof of Theorem caucvgprprlemnkltj
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltsopr 6694 . . . 4 <P Or P
2 ltrelpr 6603 . . . 4 <P ⊆ (P × P)
31, 2son2lpi 4721 . . 3 ¬ (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P (𝐹𝐽) ∧ (𝐹𝐽)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)
4 simprl 483 . . . . . . 7 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾))
5 caucvgprpr.f . . . . . . . . . 10 (𝜑𝐹:NP)
6 caucvgprpr.cau . . . . . . . . . 10 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
75, 6caucvgprprlemval 6786 . . . . . . . . 9 ((𝜑𝐾 <N 𝐽) → ((𝐹𝐾)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∧ (𝐹𝐽)<P ((𝐹𝐾) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)))
87simpld 105 . . . . . . . 8 ((𝜑𝐾 <N 𝐽) → (𝐹𝐾)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
98adantr 261 . . . . . . 7 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → (𝐹𝐾)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
101, 2sotri 4720 . . . . . . 7 (((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ (𝐹𝐾)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)) → (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
114, 9, 10syl2anc 391 . . . . . 6 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
12 ltaprg 6717 . . . . . . . 8 ((𝑓P𝑔PP) → (𝑓<P 𝑔 ↔ ( +P 𝑓)<P ( +P 𝑔)))
1312adantl 262 . . . . . . 7 ((((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) ∧ (𝑓P𝑔PP)) → (𝑓<P 𝑔 ↔ ( +P 𝑓)<P ( +P 𝑔)))
14 caucvgprprlemnkj.s . . . . . . . . 9 (𝜑𝑆Q)
1514ad2antrr 457 . . . . . . . 8 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → 𝑆Q)
16 nqprlu 6645 . . . . . . . 8 (𝑆Q → ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ ∈ P)
1715, 16syl 14 . . . . . . 7 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ ∈ P)
18 caucvgprprlemnkj.j . . . . . . . . 9 (𝜑𝐽N)
195, 18ffvelrnd 5303 . . . . . . . 8 (𝜑 → (𝐹𝐽) ∈ P)
2019ad2antrr 457 . . . . . . 7 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → (𝐹𝐽) ∈ P)
21 caucvgprprlemnkj.k . . . . . . . . 9 (𝜑𝐾N)
22 recnnpr 6646 . . . . . . . . 9 (𝐾N → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
2321, 22syl 14 . . . . . . . 8 (𝜑 → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
2423ad2antrr 457 . . . . . . 7 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
25 addcomprg 6676 . . . . . . . 8 ((𝑓P𝑔P) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
2625adantl 262 . . . . . . 7 ((((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) ∧ (𝑓P𝑔P)) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
2713, 17, 20, 24, 26caovord2d 5670 . . . . . 6 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P (𝐹𝐽) ↔ (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)))
2811, 27mpbird 156 . . . . 5 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P (𝐹𝐽))
29 recnnpr 6646 . . . . . . . . 9 (𝐽N → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
3018, 29syl 14 . . . . . . . 8 (𝜑 → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
3130ad2antrr 457 . . . . . . 7 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
32 ltaddpr 6695 . . . . . . 7 (((𝐹𝐽) ∈ P ∧ ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P) → (𝐹𝐽)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
3320, 31, 32syl2anc 391 . . . . . 6 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → (𝐹𝐽)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
34 simprr 484 . . . . . 6 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)
351, 2sotri 4720 . . . . . 6 (((𝐹𝐽)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩) → (𝐹𝐽)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)
3633, 34, 35syl2anc 391 . . . . 5 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → (𝐹𝐽)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)
3728, 36jca 290 . . . 4 (((𝜑𝐾 <N 𝐽) ∧ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P (𝐹𝐽) ∧ (𝐹𝐽)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩))
3837ex 108 . . 3 ((𝜑𝐾 <N 𝐽) → (((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩) → (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P (𝐹𝐽) ∧ (𝐹𝐽)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)))
393, 38mtoi 590 . 2 ((𝜑𝐾 <N 𝐽) → ¬ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩))
4014adantr 261 . . . . 5 ((𝜑𝐾 <N 𝐽) → 𝑆Q)
41 nnnq 6520 . . . . . . 7 (𝐾N → [⟨𝐾, 1𝑜⟩] ~QQ)
42 recclnq 6490 . . . . . . 7 ([⟨𝐾, 1𝑜⟩] ~QQ → (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) ∈ Q)
4321, 41, 423syl 17 . . . . . 6 (𝜑 → (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) ∈ Q)
4443adantr 261 . . . . 5 ((𝜑𝐾 <N 𝐽) → (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) ∈ Q)
45 addnqpr 6659 . . . . 5 ((𝑆Q ∧ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) ∈ Q) → ⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩ = (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
4640, 44, 45syl2anc 391 . . . 4 ((𝜑𝐾 <N 𝐽) → ⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩ = (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
4746breq1d 3774 . . 3 ((𝜑𝐾 <N 𝐽) → (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ↔ (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾)))
4847anbi1d 438 . 2 ((𝜑𝐾 <N 𝐽) → ((⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩) ↔ ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)))
4939, 48mtbird 598 1 ((𝜑𝐾 <N 𝐽) → ¬ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 885   = wceq 1243   ∈ wcel 1393  {cab 2026  ∀wral 2306  ⟨cop 3378   class class class wbr 3764  ⟶wf 4898  ‘cfv 4902  (class class class)co 5512  1𝑜c1o 5994  [cec 6104  Ncnpi 6370
 Copyright terms: Public domain W3C validator