Theorem caucvgprprlemnkeqj 7714

Description: Lemma for caucvgprpr 7736. 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 7620	. . . 4 ⊢ <P Or P
2		ltrelpr 7529	. . . 4 ⊢ <P ⊆ (P × P)
3	1, 2	son2lpi 5040	. . 3 ⊢ ¬ ((𝐹‘𝐽)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ ∧ ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩<P (𝐹‘𝐽))
4		caucvgprpr.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:N⟶P)
5		caucvgprprlemnkj.j	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ N)
6	4, 5	ffvelcdmd 5669	. . . . . . . 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 7446	. . . . . . . . . . 11 ⊢ (𝐽 ∈ N → [⟨𝐽, 1o⟩] ~Q ∈ Q)
10	8, 9	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → [⟨𝐽, 1o⟩] ~Q ∈ Q)
11		recclnq 7416	. . . . . . . . . 10 ⊢ ([⟨𝐽, 1o⟩] ~Q ∈ Q → (*Q‘[⟨𝐽, 1o⟩] ~Q ) ∈ Q)
12	10, 11	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → (*Q‘[⟨𝐽, 1o⟩] ~Q ) ∈ Q)
13		nqprlu 7571	. . . . . . . . 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 7621	. . . . . . 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 5039	. . . . . 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 7571	. . . . . . . . 9 ⊢ (𝑆 ∈ Q → ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ ∈ P)
24	22, 23	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩ ∈ P)
25		ltaddpr 7621	. . . . . . . 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 7585	. . . . . . . . . 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 4028	. . . . . . . 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 5039	. . . . . 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 665	. 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 3793	. . . . . . . . . . 11 ⊢ (𝐾 = 𝐽 → ⟨𝐾, 1o⟩ = ⟨𝐽, 1o⟩)
40	39	eceq1d 6590	. . . . . . . . . 10 ⊢ (𝐾 = 𝐽 → [⟨𝐾, 1o⟩] ~Q = [⟨𝐽, 1o⟩] ~Q )
41	40	fveq2d 5535	. . . . . . . . 9 ⊢ (𝐾 = 𝐽 → (*Q‘[⟨𝐾, 1o⟩] ~Q ) = (*Q‘[⟨𝐽, 1o⟩] ~Q ))
42	41	oveq2d 5908	. . . . . . . 8 ⊢ (𝐾 = 𝐽 → (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) = (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )))
43	42	breq2d 4030	. . . . . . 7 ⊢ (𝐾 = 𝐽 → (𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) ↔ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))))
44	43	abbidv 2307	. . . . . 6 ⊢ (𝐾 = 𝐽 → {𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))} = {𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))})
45	42	breq1d 4028	. . . . . . 7 ⊢ (𝐾 = 𝐽 → ((𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞 ↔ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞))
46	45	abbidv 2307	. . . . . 6 ⊢ (𝐾 = 𝐽 → {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞} = {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞})
47	44, 46	opeq12d 3801	. . . . 5 ⊢ (𝐾 = 𝐽 → ⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑞}⟩)
48		fveq2 5531	. . . . 5 ⊢ (𝐾 = 𝐽 → (𝐹‘𝐾) = (𝐹‘𝐽))
49	47, 48	breq12d 4031	. . . 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 674	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 1364   ∈ wcel 2160  {cab 2175  ∀wral 2468  ⟨cop 3610   class class class wbr 4018  ⟶wf 5228  ‘cfv 5232  (class class class)co 5892  1_oc1o 6429  [cec 6552  Ncnpi 7296   <_N clti 7299   ~_Q ceq 7303  Qcnq 7304   +_Q cplq 7306  *_Qcrq 7308   <_Q cltq 7309  Pcnp 7315   +_P cpp 7317  <_P cltp 7319

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-iinf 4602

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-eprel 4304  df-id 4308  df-po 4311  df-iso 4312  df-iord 4381  df-on 4383  df-suc 4386  df-iom 4605  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5234  df-fn 5235  df-f 5236  df-f1 5237  df-fo 5238  df-f1o 5239  df-fv 5240  df-ov 5895  df-oprab 5896  df-mpo 5897  df-1st 6160  df-2nd 6161  df-recs 6325  df-irdg 6390  df-1o 6436  df-2o 6437  df-oadd 6440  df-omul 6441  df-er 6554  df-ec 6556  df-qs 6560  df-ni 7328  df-pli 7329  df-mi 7330  df-lti 7331  df-plpq 7368  df-mpq 7369  df-enq 7371  df-nqqs 7372  df-plqqs 7373  df-mqqs 7374  df-1nqqs 7375  df-rq 7376  df-ltnqqs 7377  df-enq0 7448  df-nq0 7449  df-0nq0 7450  df-plq0 7451  df-mq0 7452  df-inp 7490  df-iplp 7492  df-iltp 7494

This theorem is referenced by:  caucvgprprlemnkj  7716