Theorem caucvgprprlemaddq 7211

Description: Lemma for caucvgprpr 7215. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 5-Jun-2021.)

Hypotheses

Ref	Expression
caucvgprpr.f	⊢ (𝜑 → 𝐹:N⟶P)
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 𝑢}⟩))))
caucvgprpr.bnd	⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚))
caucvgprpr.lim	⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩
caucvgprprlemaddq.x	⊢ (𝜑 → 𝑋 ∈ P)
caucvgprprlemaddq.q	⊢ (𝜑 → 𝑄 ∈ P)
caucvgprprlemaddq.ex	⊢ (𝜑 → ∃𝑟 ∈ N (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))

Assertion

Ref	Expression
caucvgprprlemaddq	⊢ (𝜑 → 𝑋<P (𝐿 +P 𝑄))

Distinct variable groups:   𝐴,𝑚   𝑚,𝐹   𝐴,𝑟,𝑚   𝐹,𝑙,𝑟,𝑢,𝑘,𝑛   𝑘,𝐿   𝑄,𝑟   𝑋,𝑟   𝑝,𝑙,𝑞,𝑟,𝑢   𝜑,𝑟   𝑘,𝑝,𝑞

Allowed substitution hints:   𝜑(𝑢,𝑘,𝑚,𝑛,𝑞,𝑝,𝑙)   𝐴(𝑢,𝑘,𝑛,𝑞,𝑝,𝑙)   𝑄(𝑢,𝑘,𝑚,𝑛,𝑞,𝑝,𝑙)   𝐹(𝑞,𝑝)   𝐿(𝑢,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝑋(𝑢,𝑘,𝑚,𝑛,𝑞,𝑝,𝑙)

Proof of Theorem caucvgprprlemaddq

Dummy variables 𝑏 𝑓 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		caucvgprprlemaddq.ex	. 2 ⊢ (𝜑 → ∃𝑟 ∈ N (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))
2		nfv 1464	. . 3 ⊢ Ⅎ𝑟𝜑
3		nfcv 2225	. . . 4 ⊢ Ⅎ𝑟𝑋
4		nfcv 2225	. . . 4 ⊢ Ⅎ𝑟<P
5		caucvgprpr.lim	. . . . . 6 ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩
6		nfre1 2415	. . . . . . . 8 ⊢ Ⅎ𝑟∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)
7		nfcv 2225	. . . . . . . 8 ⊢ Ⅎ𝑟Q
8	6, 7	nfrabxy 2543	. . . . . . 7 ⊢ Ⅎ𝑟{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}
9		nfre1 2415	. . . . . . . 8 ⊢ Ⅎ𝑟∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩
10	9, 7	nfrabxy 2543	. . . . . . 7 ⊢ Ⅎ𝑟{𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}
11	8, 10	nfop 3621	. . . . . 6 ⊢ Ⅎ𝑟⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩
12	5, 11	nfcxfr 2222	. . . . 5 ⊢ Ⅎ𝑟𝐿
13		nfcv 2225	. . . . 5 ⊢ Ⅎ𝑟 +P
14		nfcv 2225	. . . . 5 ⊢ Ⅎ𝑟𝑄
15	12, 13, 14	nfov 5636	. . . 4 ⊢ Ⅎ𝑟(𝐿 +P 𝑄)
16	3, 4, 15	nfbr 3864	. . 3 ⊢ Ⅎ𝑟 𝑋<P (𝐿 +P 𝑄)
17		caucvgprpr.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:N⟶P)
18	17	ad2antrr 472	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → 𝐹:N⟶P)
19		caucvgprpr.cau	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
20	19	ad2antrr 472	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
21		simpr 108	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → 𝑏 ∈ N)
22		simplrl 502	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → 𝑟 ∈ N)
23	18, 20, 21, 22	caucvgprprlemnbj 7196	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → ¬ (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)<P (𝐹‘𝑟))
24	18, 21	ffvelrnd 5398	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → (𝐹‘𝑏) ∈ P)
25		recnnpr 7051	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ N → ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ ∈ P)
26	25	adantl 271	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ ∈ P)
27		addclpr 7040	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑏) ∈ P ∧ ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ ∈ P) → ((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∈ P)
28	24, 26, 27	syl2anc 403	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → ((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∈ P)
29		recnnpr 7051	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ N → ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ ∈ P)
30	22, 29	syl 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ ∈ P)
31		caucvgprprlemaddq.q	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄 ∈ P)
32	31	ad2antrr 472	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → 𝑄 ∈ P)
33		addassprg 7082	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∈ P ∧ ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ ∈ P ∧ 𝑄 ∈ P) → ((((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P 𝑄) = (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 𝑄)))
34	28, 30, 32, 33	syl3anc 1172	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → ((((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P 𝑄) = (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 𝑄)))
35	34	breq1d 3830	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → (((((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P 𝑄)<P ((𝐹‘𝑟) +P 𝑄) ↔ (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 𝑄))<P ((𝐹‘𝑟) +P 𝑄)))
36		ltaprg 7122	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P (ℎ +P 𝑔)))
37	36	adantl 271	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P)) → (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P (ℎ +P 𝑔)))
38		addclpr 7040	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∈ P ∧ ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ ∈ P) → (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∈ P)
39	28, 30, 38	syl2anc 403	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∈ P)
40	18, 22	ffvelrnd 5398	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → (𝐹‘𝑟) ∈ P)
41		addcomprg 7081	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
42	41	adantl 271	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P)) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
43	37, 39, 40, 32, 42	caovord2d 5771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → ((((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)<P (𝐹‘𝑟) ↔ ((((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P 𝑄)<P ((𝐹‘𝑟) +P 𝑄)))
44		addcomprg 7081	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ P ∧ ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ ∈ P) → (𝑄 +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = (⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 𝑄))
45	32, 30, 44	syl2anc 403	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → (𝑄 +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = (⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 𝑄))
46	45	oveq2d 5629	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (𝑄 +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)) = (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 𝑄)))
47	46	breq1d 3830	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → ((((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (𝑄 +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))<P ((𝐹‘𝑟) +P 𝑄) ↔ (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 𝑄))<P ((𝐹‘𝑟) +P 𝑄)))
48	35, 43, 47	3bitr4rd 219	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → ((((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (𝑄 +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))<P ((𝐹‘𝑟) +P 𝑄) ↔ (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)<P (𝐹‘𝑟)))
49	23, 48	mtbird 631	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ 𝑏 ∈ N) → ¬ (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (𝑄 +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))<P ((𝐹‘𝑟) +P 𝑄))
50	49	nrexdv 2462	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → ¬ ∃𝑏 ∈ N (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (𝑄 +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))<P ((𝐹‘𝑟) +P 𝑄))
51		breq1 3823	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑙 → (𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) ↔ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )))
52	51	cbvabv 2208	. . . . . . . . . . . . 13 ⊢ {𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )} = {𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}
53		breq2 3824	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑢 → ((*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞 ↔ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢))
54	53	cbvabv 2208	. . . . . . . . . . . . 13 ⊢ {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞} = {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}
55	52, 54	opeq12i 3610	. . . . . . . . . . . 12 ⊢ ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ = ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩
56	55	oveq2i 5624	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑏) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) = ((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)
57		breq1 3823	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑙 → (𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) ↔ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )))
58	57	cbvabv 2208	. . . . . . . . . . . . 13 ⊢ {𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )} = {𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}
59		breq2 3824	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑢 → ((*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞 ↔ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢))
60	59	cbvabv 2208	. . . . . . . . . . . . 13 ⊢ {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞} = {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}
61	58, 60	opeq12i 3610	. . . . . . . . . . . 12 ⊢ ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ = ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩
62	61	oveq2i 5624	. . . . . . . . . . 11 ⊢ (𝑄 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) = (𝑄 +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)
63	56, 62	oveq12i 5625	. . . . . . . . . 10 ⊢ (((𝐹‘𝑏) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P (𝑄 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)) = (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (𝑄 +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))
64	63	breq1i 3827	. . . . . . . . 9 ⊢ ((((𝐹‘𝑏) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P (𝑄 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))<P ((𝐹‘𝑟) +P 𝑄) ↔ (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (𝑄 +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))<P ((𝐹‘𝑟) +P 𝑄))
65	64	rexbii 2381	. . . . . . . 8 ⊢ (∃𝑏 ∈ N (((𝐹‘𝑏) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P (𝑄 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))<P ((𝐹‘𝑟) +P 𝑄) ↔ ∃𝑏 ∈ N (((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) +P (𝑄 +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))<P ((𝐹‘𝑟) +P 𝑄))
66	50, 65	sylnibr 635	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → ¬ ∃𝑏 ∈ N (((𝐹‘𝑏) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P (𝑄 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))<P ((𝐹‘𝑟) +P 𝑄))
67	17	adantr 270	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → 𝐹:N⟶P)
68	19	adantr 270	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
69		caucvgprpr.bnd	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚))
70	69	adantr 270	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚))
71	31	adantr 270	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → 𝑄 ∈ P)
72		simprl 498	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → 𝑟 ∈ N)
73	67, 68, 70, 5, 71, 72	caucvgprprlemexb 7210	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → (((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄) → ∃𝑏 ∈ N (((𝐹‘𝑏) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P (𝑄 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))<P ((𝐹‘𝑟) +P 𝑄)))
74	66, 73	mtod 622	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → ¬ ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))
75		simprr 499	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))
76		caucvgprprlemaddq.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ P)
77	76	adantr 270	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → 𝑋 ∈ P)
78		recnnpr 7051	. . . . . . . . . 10 ⊢ (𝑟 ∈ N → ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
79	72, 78	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
80		addclpr 7040	. . . . . . . . 9 ⊢ ((𝑋 ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P) → (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
81	77, 79, 80	syl2anc 403	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
82	67, 72	ffvelrnd 5398	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → (𝐹‘𝑟) ∈ P)
83		addclpr 7040	. . . . . . . . 9 ⊢ (((𝐹‘𝑟) ∈ P ∧ 𝑄 ∈ P) → ((𝐹‘𝑟) +P 𝑄) ∈ P)
84	82, 71, 83	syl2anc 403	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → ((𝐹‘𝑟) +P 𝑄) ∈ P)
85	17, 19, 69, 5	caucvgprprlemcl 7207	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ P)
86	85	adantr 270	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → 𝐿 ∈ P)
87		addclpr 7040	. . . . . . . . . 10 ⊢ ((𝐿 ∈ P ∧ 𝑄 ∈ P) → (𝐿 +P 𝑄) ∈ P)
88	86, 71, 87	syl2anc 403	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → (𝐿 +P 𝑄) ∈ P)
89		addclpr 7040	. . . . . . . . 9 ⊢ (((𝐿 +P 𝑄) ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P) → ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
90	88, 79, 89	syl2anc 403	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
91		ltsopr 7099	. . . . . . . . 9 ⊢ <P Or P
92		sowlin 4121	. . . . . . . . 9 ⊢ ((<P Or P ∧ ((𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P ∧ ((𝐹‘𝑟) +P 𝑄) ∈ P ∧ ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P)) → ((𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄) → ((𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∨ ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))))
93	91, 92	mpan 415	. . . . . . . 8 ⊢ (((𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P ∧ ((𝐹‘𝑟) +P 𝑄) ∈ P ∧ ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P) → ((𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄) → ((𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∨ ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))))
94	81, 84, 90, 93	syl3anc 1172	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → ((𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄) → ((𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∨ ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))))
95	75, 94	mpd 13	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → ((𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∨ ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄)))
96	74, 95	ecased 1283	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
97	36	adantl 271	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P)) → (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P (ℎ +P 𝑔)))
98	41	adantl 271	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P)) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
99	97, 77, 88, 79, 98	caovord2d 5771	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → (𝑋<P (𝐿 +P 𝑄) ↔ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)))
100	96, 99	mpbird 165	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ N ∧ (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))) → 𝑋<P (𝐿 +P 𝑄))
101	100	exp32 357	. . 3 ⊢ (𝜑 → (𝑟 ∈ N → ((𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄) → 𝑋<P (𝐿 +P 𝑄))))
102	2, 16, 101	rexlimd 2482	. 2 ⊢ (𝜑 → (∃𝑟 ∈ N (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄) → 𝑋<P (𝐿 +P 𝑄)))
103	1, 102	mpd 13	1 ⊢ (𝜑 → 𝑋<P (𝐿 +P 𝑄))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   ∨ wo 662   ∧ w3a 922   = wceq 1287   ∈ wcel 1436  {cab 2071  ∀wral 2355  ∃wrex 2356  {crab 2359  ⟨cop 3434   class class class wbr 3820   Or wor 4096  ⟶wf 4977  ‘cfv 4981  (class class class)co 5613  1_𝑜c1o 6128  [cec 6242  Ncnpi 6775   <_N clti 6778   ~_Q ceq 6782  Qcnq 6783   +_Q cplq 6785  *_Qcrq 6787   <_Q cltq 6788  Pcnp 6794   +_P cpp 6796  <_P cltp 6798

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3929  ax-sep 3932  ax-nul 3940  ax-pow 3984  ax-pr 4010  ax-un 4234  ax-setind 4326  ax-iinf 4376

This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-int 3672  df-iun 3715  df-br 3821  df-opab 3875  df-mpt 3876  df-tr 3912  df-eprel 4090  df-id 4094  df-po 4097  df-iso 4098  df-iord 4167  df-on 4169  df-suc 4172  df-iom 4379  df-xp 4417  df-rel 4418  df-cnv 4419  df-co 4420  df-dm 4421  df-rn 4422  df-res 4423  df-ima 4424  df-iota 4946  df-fun 4983  df-fn 4984  df-f 4985  df-f1 4986  df-fo 4987  df-f1o 4988  df-fv 4989  df-ov 5616  df-oprab 5617  df-mpt2 5618  df-1st 5868  df-2nd 5869  df-recs 6024  df-irdg 6089  df-1o 6135  df-2o 6136  df-oadd 6139  df-omul 6140  df-er 6244  df-ec 6246  df-qs 6250  df-ni 6807  df-pli 6808  df-mi 6809  df-lti 6810  df-plpq 6847  df-mpq 6848  df-enq 6850  df-nqqs 6851  df-plqqs 6852  df-mqqs 6853  df-1nqqs 6854  df-rq 6855  df-ltnqqs 6856  df-enq0 6927  df-nq0 6928  df-0nq0 6929  df-plq0 6930  df-mq0 6931  df-inp 6969  df-iplp 6971  df-iltp 6973

This theorem is referenced by:  caucvgprprlem1  7212