Theorem caucvgprprlemnkeqj 7823

Description: Lemma for caucvgprpr 7845. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.)

Hypotheses

Ref	Expression
caucvgprpr.f	⊢ (𝜑 → 𝐹:N⟶P)
caucvgprpr.cau	⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))))
caucvgprprlemnkj.k	⊢ (𝜑 → 𝐾 ∈ N)
caucvgprprlemnkj.j	⊢ (𝜑 → 𝐽 ∈ N)
caucvgprprlemnkj.s	⊢ (𝜑 → 𝑆 ∈ Q)

Assertion

Ref	Expression
caucvgprprlemnkeqj	⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ¬ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩))

Distinct variable groups:   𝑘,𝐹,𝑛   𝐽,𝑝,𝑞   𝐾,𝑝,𝑞   𝑆,𝑝,𝑞

Allowed substitution hints:   𝜑(𝑢,𝑘,𝑛,𝑞,𝑝,𝑙)   𝑆(𝑢,𝑘,𝑛,𝑙)   𝐹(𝑢,𝑞,𝑝,𝑙)   𝐽(𝑢,𝑘,𝑛,𝑙)   𝐾(𝑢,𝑘,𝑛,𝑙)

Proof of Theorem caucvgprprlemnkeqj

Step	Hyp	Ref	Expression
1		ltsopr 7729	. . . 4 ⊢ <P Or P
2		ltrelpr 7638	. . . 4 ⊢ <P ⊆ (P × P)
3	1, 2	son2lpi 5088	. . 3 ⊢ ¬ ((𝐹‘𝐽)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ ∧ ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩<P (𝐹‘𝐽))
4		caucvgprpr.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:N⟶P)
5		caucvgprprlemnkj.j	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ N)
6	4, 5	ffvelcdmd 5729	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐽) ∈ P)
7	6	ad2antrr 488	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐾 = 𝐽) ∧ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) → (𝐹‘𝐽) ∈ P)
8	5	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → 𝐽 ∈ N)
9		nnnq 7555	. . . . . . . . . . 11 ⊢ (𝐽 ∈ N → [⟨𝐽, 1o⟩] ~Q ∈ Q)
10	8, 9	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → [⟨𝐽, 1o⟩] ~Q ∈ Q)
11		recclnq 7525	. . . . . . . . . 10 ⊢ ([⟨𝐽, 1o⟩] ~Q ∈ Q → (*Q‘[⟨𝐽, 1o⟩] ~Q ) ∈ Q)
12	10, 11	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → (*Q‘[⟨𝐽, 1o⟩] ~Q ) ∈ Q)
13		nqprlu 7680	. . . . . . . . 9 ⊢ ((*Q‘[⟨𝐽, 1o⟩] ~Q ) ∈ Q → ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
14	12, 13	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
15	14	adantr 276	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐾 = 𝐽) ∧ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
16		ltaddpr 7730	. . . . . . 7 ⊢ (((𝐹‘𝐽) ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩ ∈ P) → (𝐹‘𝐽)<P ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩))
17	7, 15, 16	syl2anc 411	. . . . . 6 ⊢ (((𝜑 ∧ 𝐾 = 𝐽) ∧ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) → (𝐹‘𝐽)<P ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩))
18		simprr 531	. . . . . 6 ⊢ (((𝜑 ∧ 𝐾 = 𝐽) ∧ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) → ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)
19	1, 2	sotri 5087	. . . . . 6 ⊢ (((𝐹‘𝐽)<P ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩) → (𝐹‘𝐽)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)
20	17, 18, 19	syl2anc 411	. . . . 5 ⊢ (((𝜑 ∧ 𝐾 = 𝐽) ∧ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) → (𝐹‘𝐽)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)
21		caucvgprprlemnkj.s	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ Q)
22	21	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → 𝑆 ∈ Q)
23		nqprlu 7680	. . . . . . . . 9 ⊢ (𝑆 ∈ Q → ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ ∈ P)
24	22, 23	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ ∈ P)
25		ltaddpr 7730	. . . . . . . 8 ⊢ ((⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩ ∈ P) → ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩<P (⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩))
26	24, 14, 25	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩<P (⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩))
27	26	adantr 276	. . . . . 6 ⊢ (((𝜑 ∧ 𝐾 = 𝐽) ∧ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩<P (⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩))
28		simprl 529	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐾 = 𝐽) ∧ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽))
29		addnqpr 7694	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Q ∧ (*Q‘[⟨𝐽, 1o⟩] ~Q ) ∈ Q) → ⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩ = (⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩))
30	22, 12, 29	syl2anc 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩ = (⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩))
31	30	breq1d 4061	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ↔ (⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹‘𝐽)))
32	31	adantr 276	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐾 = 𝐽) ∧ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) → (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ↔ (⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹‘𝐽)))
33	28, 32	mpbid 147	. . . . . 6 ⊢ (((𝜑 ∧ 𝐾 = 𝐽) ∧ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) → (⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹‘𝐽))
34	1, 2	sotri 5087	. . . . . 6 ⊢ ((⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩<P (⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩) ∧ (⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P (𝐹‘𝐽)) → ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩<P (𝐹‘𝐽))
35	27, 33, 34	syl2anc 411	. . . . 5 ⊢ (((𝜑 ∧ 𝐾 = 𝐽) ∧ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩<P (𝐹‘𝐽))
36	20, 35	jca 306	. . . 4 ⊢ (((𝜑 ∧ 𝐾 = 𝐽) ∧ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) → ((𝐹‘𝐽)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ ∧ ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩<P (𝐹‘𝐽)))
37	36	ex 115	. . 3 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ((⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩) → ((𝐹‘𝐽)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ ∧ ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩<P (𝐹‘𝐽))))
38	3, 37	mtoi 666	. 2 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ¬ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩))
39		opeq1 3825	. . . . . . . . . . 11 ⊢ (𝐾 = 𝐽 → ⟨𝐾, 1o⟩ = ⟨𝐽, 1o⟩)
40	39	eceq1d 6669	. . . . . . . . . 10 ⊢ (𝐾 = 𝐽 → [⟨𝐾, 1o⟩] ~Q = [⟨𝐽, 1o⟩] ~Q )
41	40	fveq2d 5593	. . . . . . . . 9 ⊢ (𝐾 = 𝐽 → (*Q‘[⟨𝐾, 1o⟩] ~Q ) = (*Q‘[⟨𝐽, 1o⟩] ~Q ))
42	41	oveq2d 5973	. . . . . . . 8 ⊢ (𝐾 = 𝐽 → (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) = (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )))
43	42	breq2d 4063	. . . . . . 7 ⊢ (𝐾 = 𝐽 → (𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) ↔ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))))
44	43	abbidv 2324	. . . . . 6 ⊢ (𝐾 = 𝐽 → {𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))} = {𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))})
45	42	breq1d 4061	. . . . . . 7 ⊢ (𝐾 = 𝐽 → ((𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞 ↔ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞))
46	45	abbidv 2324	. . . . . 6 ⊢ (𝐾 = 𝐽 → {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞} = {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞})
47	44, 46	opeq12d 3833	. . . . 5 ⊢ (𝐾 = 𝐽 → ⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩)
48		fveq2 5589	. . . . 5 ⊢ (𝐾 = 𝐽 → (𝐹‘𝐾) = (𝐹‘𝐽))
49	47, 48	breq12d 4064	. . . 4 ⊢ (𝐾 = 𝐽 → (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐾) ↔ ⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽)))
50	49	anbi1d 465	. . 3 ⊢ (𝐾 = 𝐽 → ((⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩) ↔ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)))
51	50	adantl 277	. 2 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ((⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩) ↔ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)))
52	38, 51	mtbird 675	1 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ¬ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1373   ∈ wcel 2177  {cab 2192  ∀wral 2485  ⟨cop 3641   class class class wbr 4051  ⟶wf 5276  ‘cfv 5280  (class class class)co 5957  1_oc1o 6508  [cec 6631  Ncnpi 7405   <_N clti 7408   ~_Q ceq 7412  Qcnq 7413   +_Q cplq 7415  *_Qcrq 7417   <_Q cltq 7418  Pcnp 7424   +_P cpp 7426  <_P cltp 7428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-coll 4167  ax-sep 4170  ax-nul 4178  ax-pow 4226  ax-pr 4261  ax-un 4488  ax-setind 4593  ax-iinf 4644

This theorem depends on definitions:  df-bi 117  df-dc 837  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-ral 2490  df-rex 2491  df-reu 2492  df-rab 2494  df-v 2775  df-sbc 3003  df-csb 3098  df-dif 3172  df-un 3174  df-in 3176  df-ss 3183  df-nul 3465  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-int 3892  df-iun 3935  df-br 4052  df-opab 4114  df-mpt 4115  df-tr 4151  df-eprel 4344  df-id 4348  df-po 4351  df-iso 4352  df-iord 4421  df-on 4423  df-suc 4426  df-iom 4647  df-xp 4689  df-rel 4690  df-cnv 4691  df-co 4692  df-dm 4693  df-rn 4694  df-res 4695  df-ima 4696  df-iota 5241  df-fun 5282  df-fn 5283  df-f 5284  df-f1 5285  df-fo 5286  df-f1o 5287  df-fv 5288  df-ov 5960  df-oprab 5961  df-mpo 5962  df-1st 6239  df-2nd 6240  df-recs 6404  df-irdg 6469  df-1o 6515  df-2o 6516  df-oadd 6519  df-omul 6520  df-er 6633  df-ec 6635  df-qs 6639  df-ni 7437  df-pli 7438  df-mi 7439  df-lti 7440  df-plpq 7477  df-mpq 7478  df-enq 7480  df-nqqs 7481  df-plqqs 7482  df-mqqs 7483  df-1nqqs 7484  df-rq 7485  df-ltnqqs 7486  df-enq0 7557  df-nq0 7558  df-0nq0 7559  df-plq0 7560  df-mq0 7561  df-inp 7599  df-iplp 7601  df-iltp 7603

This theorem is referenced by:  caucvgprprlemnkj  7825