caucvgprlemnkj - Intuitionistic Logic Explorer

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

Theorem caucvgprlemnkj 7474

Description: Lemma for caucvgpr 7490. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.)

**Hypotheses**
Ref	Expression
caucvgpr.f	⊢ (𝜑 → 𝐹:N⟶Q)
caucvgpr.cau	⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <_N 𝑘 → ((𝐹‘𝑛) <_Q ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑘) <_Q ((𝐹‘𝑛) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )))))
caucvgprlemnkj.k	⊢ (𝜑 → 𝐾 ∈ N)
caucvgprlemnkj.j	⊢ (𝜑 → 𝐽 ∈ N)
caucvgprlemnkj.s	⊢ (𝜑 → 𝑆 ∈ Q)

**Assertion**
Ref	Expression
caucvgprlemnkj	⊢ (𝜑 → ¬ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆))

Distinct variable group: 𝑘,𝐹,𝑛 Allowed substitution hints: 𝜑(𝑘,𝑛) 𝑆(𝑘,𝑛) 𝐽(𝑘,𝑛) 𝐾(𝑘,𝑛)

Proof of Theorem caucvgprlemnkj Dummy variables 𝑎 𝑏 𝑓 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltsonq 7206	. . . 4 ⊢ <_Q Or Q
2		ltrelnq 7173	. . . 4 ⊢ <_Q ⊆ (Q × Q)
3	1, 2	son2lpi 4935	. . 3 ⊢ ¬ (𝑆 <_Q (𝐹‘𝐽) ∧ (𝐹‘𝐽) <_Q 𝑆)
4		simprl 520	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (𝑆 +_Q (*_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾))
5		caucvgpr.cau	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <_N 𝑘 → ((𝐹‘𝑛) <_Q ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑘) <_Q ((𝐹‘𝑛) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )))))
6		breq1 3932	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑎 → (𝑛 <_N 𝑘 ↔ 𝑎 <_N 𝑘))
7		fveq2 5421	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑎 → (𝐹‘𝑛) = (𝐹‘𝑎))
8		opeq1 3705	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑎 → ⟨𝑛, 1_o⟩ = ⟨𝑎, 1_o⟩)
9	8	eceq1d 6465	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑎 → [⟨𝑛, 1_o⟩] ~_Q = [⟨𝑎, 1_o⟩] ~_Q )
10	9	fveq2d 5425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑎 → (_Q‘[⟨𝑛, 1_o⟩] ~_Q ) = (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))
11	10	oveq2d 5790	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑎 → ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )) = ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))
12	7, 11	breq12d 3942	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑎 → ((𝐹‘𝑛) <_Q ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )) ↔ (𝐹‘𝑎) <_Q ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))))
13	7, 10	oveq12d 5792	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑎 → ((𝐹‘𝑛) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )) = ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))
14	13	breq2d 3941	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑎 → ((𝐹‘𝑘) <_Q ((𝐹‘𝑛) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )) ↔ (𝐹‘𝑘) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))))
15	12, 14	anbi12d 464	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑎 → (((𝐹‘𝑛) <_Q ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑘) <_Q ((𝐹‘𝑛) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q ))) ↔ ((𝐹‘𝑎) <_Q ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑘) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))))
16	6, 15	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑎 → ((𝑛 <_N 𝑘 → ((𝐹‘𝑛) <_Q ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑘) <_Q ((𝐹‘𝑛) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )))) ↔ (𝑎 <_N 𝑘 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑘) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))))))
17		breq2 3933	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑏 → (𝑎 <_N 𝑘 ↔ 𝑎 <_N 𝑏))
18		fveq2 5421	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑏 → (𝐹‘𝑘) = (𝐹‘𝑏))
19	18	oveq1d 5789	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑏 → ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) = ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))
20	19	breq2d 3941	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑏 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ↔ (𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))))
21	18	breq1d 3939	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑏 → ((𝐹‘𝑘) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ↔ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))))
22	20, 21	anbi12d 464	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑏 → (((𝐹‘𝑎) <_Q ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑘) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))) ↔ ((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))))
23	17, 22	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑏 → ((𝑎 <_N 𝑘 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑘) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))) ↔ (𝑎 <_N 𝑏 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))))))
24	16, 23	cbvral2v 2665	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <_N 𝑘 → ((𝐹‘𝑛) <_Q ((𝐹‘𝑘) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑘) <_Q ((𝐹‘𝑛) +_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )))) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑎 <_N 𝑏 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))))
25	5, 24	sylib 121	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑎 <_N 𝑏 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))))
26		caucvgprlemnkj.k	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ N)
27		caucvgprlemnkj.j	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ N)
28		breq1 3932	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝐾 → (𝑎 <_N 𝑏 ↔ 𝐾 <_N 𝑏))
29		fveq2 5421	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝐾 → (𝐹‘𝑎) = (𝐹‘𝐾))
30		opeq1 3705	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝐾 → ⟨𝑎, 1_o⟩ = ⟨𝐾, 1_o⟩)
31	30	eceq1d 6465	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝐾 → [⟨𝑎, 1_o⟩] ~_Q = [⟨𝐾, 1_o⟩] ~_Q )
32	31	fveq2d 5425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝐾 → (_Q‘[⟨𝑎, 1_o⟩] ~_Q ) = (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))
33	32	oveq2d 5790	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝐾 → ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) = ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )))
34	29, 33	breq12d 3942	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝐾 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ↔ (𝐹‘𝐾) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))))
35	29, 32	oveq12d 5792	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝐾 → ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) = ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )))
36	35	breq2d 3941	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝐾 → ((𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ↔ (𝐹‘𝑏) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))))
37	34, 36	anbi12d 464	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝐾 → (((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))) ↔ ((𝐹‘𝐾) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )))))
38	28, 37	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝐾 → ((𝑎 <_N 𝑏 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))) ↔ (𝐾 <_N 𝑏 → ((𝐹‘𝐾) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))))))
39		breq2 3933	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝐽 → (𝐾 <_N 𝑏 ↔ 𝐾 <_N 𝐽))
40		fveq2 5421	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝐽 → (𝐹‘𝑏) = (𝐹‘𝐽))
41	40	oveq1d 5789	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝐽 → ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) = ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )))
42	41	breq2d 3941	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝐽 → ((𝐹‘𝐾) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ↔ (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))))
43	40	breq1d 3939	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝐽 → ((𝐹‘𝑏) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ↔ (𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))))
44	42, 43	anbi12d 464	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝐽 → (((𝐹‘𝐾) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))) ↔ ((𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ∧ (𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )))))
45	39, 44	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝐽 → ((𝐾 <_N 𝑏 → ((𝐹‘𝐾) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )))) ↔ (𝐾 <_N 𝐽 → ((𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ∧ (𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))))))
46	38, 45	rspc2v 2802	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ N ∧ 𝐽 ∈ N) → (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑎 <_N 𝑏 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))) → (𝐾 <_N 𝐽 → ((𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ∧ (𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))))))
47	26, 27, 46	syl2anc 408	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑎 <_N 𝑏 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))) → (𝐾 <_N 𝐽 → ((𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ∧ (𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))))))
48	25, 47	mpd 13	. . . . . . . . . 10 ⊢ (𝜑 → (𝐾 <_N 𝐽 → ((𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ∧ (𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )))))
49	48	imp 123	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐾 <_N 𝐽) → ((𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ∧ (𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))))
50	49	simpld 111	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐾 <_N 𝐽) → (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (*_Q‘[⟨𝐾, 1_o⟩] ~_Q )))
51	50	adantr 274	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (*_Q‘[⟨𝐾, 1_o⟩] ~_Q )))
52	1, 2	sotri 4934	. . . . . . 7 ⊢ (((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))) → (𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )))
53	4, 51, 52	syl2anc 408	. . . . . 6 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )))
54		ltanqg 7208	. . . . . . . 8 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → (𝑓 <_Q 𝑔 ↔ (ℎ +_Q 𝑓) <_Q (ℎ +_Q 𝑔)))
55	54	adantl 275	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q)) → (𝑓 <_Q 𝑔 ↔ (ℎ +_Q 𝑓) <_Q (ℎ +_Q 𝑔)))
56		caucvgprlemnkj.s	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ Q)
57	56	ad2antrr 479	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → 𝑆 ∈ Q)
58		caucvgpr.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:N⟶Q)
59	58, 27	ffvelrnd 5556	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐽) ∈ Q)
60	59	ad2antrr 479	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (𝐹‘𝐽) ∈ Q)
61		nnnq 7230	. . . . . . . . 9 ⊢ (𝐾 ∈ N → [⟨𝐾, 1_o⟩] ~_Q ∈ Q)
62		recclnq 7200	. . . . . . . . 9 ⊢ ([⟨𝐾, 1_o⟩] ~_Q ∈ Q → (*_Q‘[⟨𝐾, 1_o⟩] ~_Q ) ∈ Q)
63	26, 61, 62	3syl 17	. . . . . . . 8 ⊢ (𝜑 → (*_Q‘[⟨𝐾, 1_o⟩] ~_Q ) ∈ Q)
64	63	ad2antrr 479	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (*_Q‘[⟨𝐾, 1_o⟩] ~_Q ) ∈ Q)
65		addcomnqg 7189	. . . . . . . 8 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q) → (𝑓 +_Q 𝑔) = (𝑔 +_Q 𝑓))
66	65	adantl 275	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q)) → (𝑓 +_Q 𝑔) = (𝑔 +_Q 𝑓))
67	55, 57, 60, 64, 66	caovord2d 5940	. . . . . 6 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (𝑆 <_Q (𝐹‘𝐽) ↔ (𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q ))))
68	53, 67	mpbird 166	. . . . 5 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → 𝑆 <_Q (𝐹‘𝐽))
69		nnnq 7230	. . . . . . . . 9 ⊢ (𝐽 ∈ N → [⟨𝐽, 1_o⟩] ~_Q ∈ Q)
70		recclnq 7200	. . . . . . . . 9 ⊢ ([⟨𝐽, 1_o⟩] ~_Q ∈ Q → (*_Q‘[⟨𝐽, 1_o⟩] ~_Q ) ∈ Q)
71	27, 69, 70	3syl 17	. . . . . . . 8 ⊢ (𝜑 → (*_Q‘[⟨𝐽, 1_o⟩] ~_Q ) ∈ Q)
72	71	ad2antrr 479	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (*_Q‘[⟨𝐽, 1_o⟩] ~_Q ) ∈ Q)
73		ltaddnq 7215	. . . . . . 7 ⊢ (((𝐹‘𝐽) ∈ Q ∧ (_Q‘[⟨𝐽, 1_o⟩] ~_Q ) ∈ Q) → (𝐹‘𝐽) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
74	60, 72, 73	syl2anc 408	. . . . . 6 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (𝐹‘𝐽) <_Q ((𝐹‘𝐽) +_Q (*_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
75		simprr 521	. . . . . 6 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → ((𝐹‘𝐽) +_Q (*_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)
76	1, 2	sotri 4934	. . . . . 6 ⊢ (((𝐹‘𝐽) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆) → (𝐹‘𝐽) <_Q 𝑆)
77	74, 75, 76	syl2anc 408	. . . . 5 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (𝐹‘𝐽) <_Q 𝑆)
78	68, 77	jca 304	. . . 4 ⊢ (((𝜑 ∧ 𝐾 <_N 𝐽) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (𝑆 <_Q (𝐹‘𝐽) ∧ (𝐹‘𝐽) <_Q 𝑆))
79	78	ex 114	. . 3 ⊢ ((𝜑 ∧ 𝐾 <_N 𝐽) → (((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆) → (𝑆 <_Q (𝐹‘𝐽) ∧ (𝐹‘𝐽) <_Q 𝑆)))
80	3, 79	mtoi 653	. 2 ⊢ ((𝜑 ∧ 𝐾 <_N 𝐽) → ¬ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆))
81	1, 2	son2lpi 4935	. . 3 ⊢ ¬ (((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆 ∧ 𝑆 <_Q ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
82		opeq1 3705	. . . . . . . . . . . 12 ⊢ (𝐾 = 𝐽 → ⟨𝐾, 1_o⟩ = ⟨𝐽, 1_o⟩)
83	82	eceq1d 6465	. . . . . . . . . . 11 ⊢ (𝐾 = 𝐽 → [⟨𝐾, 1_o⟩] ~_Q = [⟨𝐽, 1_o⟩] ~_Q )
84	83	fveq2d 5425	. . . . . . . . . 10 ⊢ (𝐾 = 𝐽 → (_Q‘[⟨𝐾, 1_o⟩] ~_Q ) = (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))
85	84	oveq2d 5790	. . . . . . . . 9 ⊢ (𝐾 = 𝐽 → (𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) = (𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
86		fveq2 5421	. . . . . . . . 9 ⊢ (𝐾 = 𝐽 → (𝐹‘𝐾) = (𝐹‘𝐽))
87	85, 86	breq12d 3942	. . . . . . . 8 ⊢ (𝐾 = 𝐽 → ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ↔ (𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐽)))
88	87	anbi1d 460	. . . . . . 7 ⊢ (𝐾 = 𝐽 → (((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆) ↔ ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)))
89	88	adantl 275	. . . . . 6 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → (((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆) ↔ ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)))
90	54	adantl 275	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q)) → (𝑓 <_Q 𝑔 ↔ (ℎ +_Q 𝑓) <_Q (ℎ +_Q 𝑔)))
91		addclnq 7183	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Q ∧ (_Q‘[⟨𝐽, 1_o⟩] ~_Q ) ∈ Q) → (𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∈ Q)
92	56, 71, 91	syl2anc 408	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 +_Q (*_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∈ Q)
93	65	adantl 275	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q)) → (𝑓 +_Q 𝑔) = (𝑔 +_Q 𝑓))
94	90, 92, 59, 71, 93	caovord2d 5940	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐽) ↔ ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))))
95	94	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐽) ↔ ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))))
96	95	anbi1d 460	. . . . . 6 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → (((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐽) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆) ↔ (((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)))
97	89, 96	bitrd 187	. . . . 5 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → (((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆) ↔ (((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)))
98	1, 2	sotri 4934	. . . . 5 ⊢ ((((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆) → ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)
99	97, 98	syl6bi 162	. . . 4 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → (((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆) → ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆))
100		ltaddnq 7215	. . . . . . 7 ⊢ ((𝑆 ∈ Q ∧ (_Q‘[⟨𝐽, 1_o⟩] ~_Q ) ∈ Q) → 𝑆 <_Q (𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
101	56, 71, 100	syl2anc 408	. . . . . 6 ⊢ (𝜑 → 𝑆 <_Q (𝑆 +_Q (*_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
102		ltaddnq 7215	. . . . . . 7 ⊢ (((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∈ Q ∧ (_Q‘[⟨𝐽, 1_o⟩] ~_Q ) ∈ Q) → (𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (*_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
103	92, 71, 102	syl2anc 408	. . . . . 6 ⊢ (𝜑 → (𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (*_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
104	1, 2	sotri 4934	. . . . . 6 ⊢ ((𝑆 <_Q (𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ (𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))) → 𝑆 <_Q ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
105	101, 103, 104	syl2anc 408	. . . . 5 ⊢ (𝜑 → 𝑆 <_Q ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
106	105	adantr 274	. . . 4 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → 𝑆 <_Q ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
107	99, 106	jctird 315	. . 3 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → (((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆) → (((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆 ∧ 𝑆 <_Q ((𝑆 +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))))
108	81, 107	mtoi 653	. 2 ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ¬ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆))
109	1, 2	son2lpi 4935	. . 3 ⊢ ¬ (𝑆 <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)
110	56	ad2antrr 479	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐽 <_N 𝐾) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → 𝑆 ∈ Q)
111	63	ad2antrr 479	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐽 <_N 𝐾) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (*_Q‘[⟨𝐾, 1_o⟩] ~_Q ) ∈ Q)
112		ltaddnq 7215	. . . . . . 7 ⊢ ((𝑆 ∈ Q ∧ (_Q‘[⟨𝐾, 1_o⟩] ~_Q ) ∈ Q) → 𝑆 <_Q (𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )))
113	110, 111, 112	syl2anc 408	. . . . . 6 ⊢ (((𝜑 ∧ 𝐽 <_N 𝐾) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → 𝑆 <_Q (𝑆 +_Q (*_Q‘[⟨𝐾, 1_o⟩] ~_Q )))
114		simprl 520	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐽 <_N 𝐾) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (𝑆 +_Q (*_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾))
115		breq1 3932	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝐽 → (𝑎 <_N 𝑏 ↔ 𝐽 <_N 𝑏))
116		fveq2 5421	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝐽 → (𝐹‘𝑎) = (𝐹‘𝐽))
117		opeq1 3705	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝐽 → ⟨𝑎, 1_o⟩ = ⟨𝐽, 1_o⟩)
118	117	eceq1d 6465	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝐽 → [⟨𝑎, 1_o⟩] ~_Q = [⟨𝐽, 1_o⟩] ~_Q )
119	118	fveq2d 5425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝐽 → (_Q‘[⟨𝑎, 1_o⟩] ~_Q ) = (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))
120	119	oveq2d 5790	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝐽 → ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) = ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
121	116, 120	breq12d 3942	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝐽 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ↔ (𝐹‘𝐽) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))))
122	116, 119	oveq12d 5792	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝐽 → ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) = ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
123	122	breq2d 3941	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝐽 → ((𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ↔ (𝐹‘𝑏) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))))
124	121, 123	anbi12d 464	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝐽 → (((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))) ↔ ((𝐹‘𝐽) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))))
125	115, 124	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝐽 → ((𝑎 <_N 𝑏 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))) ↔ (𝐽 <_N 𝑏 → ((𝐹‘𝐽) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))))))
126		breq2 3933	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝐾 → (𝐽 <_N 𝑏 ↔ 𝐽 <_N 𝐾))
127		fveq2 5421	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝐾 → (𝐹‘𝑏) = (𝐹‘𝐾))
128	127	oveq1d 5789	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝐾 → ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) = ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
129	128	breq2d 3941	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝐾 → ((𝐹‘𝐽) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ↔ (𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))))
130	127	breq1d 3939	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝐾 → ((𝐹‘𝑏) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ↔ (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))))
131	129, 130	anbi12d 464	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝐾 → (((𝐹‘𝐽) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))) ↔ ((𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))))
132	126, 131	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝐾 → ((𝐽 <_N 𝑏 → ((𝐹‘𝐽) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))) ↔ (𝐽 <_N 𝐾 → ((𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))))))
133	125, 132	rspc2v 2802	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑎 <_N 𝑏 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))) → (𝐽 <_N 𝐾 → ((𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))))))
134	27, 26, 133	syl2anc 408	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑎 <_N 𝑏 → ((𝐹‘𝑎) <_Q ((𝐹‘𝑏) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ∧ (𝐹‘𝑏) <_Q ((𝐹‘𝑎) +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )))) → (𝐽 <_N 𝐾 → ((𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))))))
135	25, 134	mpd 13	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 <_N 𝐾 → ((𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))))
136	135	imp 123	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐽 <_N 𝐾) → ((𝐹‘𝐽) <_Q ((𝐹‘𝐾) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))))
137	136	simprd 113	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐽 <_N 𝐾) → (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (*_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
138	137	adantr 274	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐽 <_N 𝐾) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (*_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
139	1, 2	sotri 4934	. . . . . . 7 ⊢ (((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ (𝐹‘𝐾) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))) → (𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
140	114, 138, 139	syl2anc 408	. . . . . 6 ⊢ (((𝜑 ∧ 𝐽 <_N 𝐾) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
141	1, 2	sotri 4934	. . . . . 6 ⊢ ((𝑆 <_Q (𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) ∧ (𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q ))) → 𝑆 <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
142	113, 140, 141	syl2anc 408	. . . . 5 ⊢ (((𝜑 ∧ 𝐽 <_N 𝐾) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → 𝑆 <_Q ((𝐹‘𝐽) +_Q (*_Q‘[⟨𝐽, 1_o⟩] ~_Q )))
143		simprr 521	. . . . 5 ⊢ (((𝜑 ∧ 𝐽 <_N 𝐾) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → ((𝐹‘𝐽) +_Q (*_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)
144	142, 143	jca 304	. . . 4 ⊢ (((𝜑 ∧ 𝐽 <_N 𝐾) ∧ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)) → (𝑆 <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆))
145	144	ex 114	. . 3 ⊢ ((𝜑 ∧ 𝐽 <_N 𝐾) → (((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆) → (𝑆 <_Q ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆)))
146	109, 145	mtoi 653	. 2 ⊢ ((𝜑 ∧ 𝐽 <_N 𝐾) → ¬ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆))
147		pitri3or 7130	. . 3 ⊢ ((𝐾 ∈ N ∧ 𝐽 ∈ N) → (𝐾 <_N 𝐽 ∨ 𝐾 = 𝐽 ∨ 𝐽 <_N 𝐾))
148	26, 27, 147	syl2anc 408	. 2 ⊢ (𝜑 → (𝐾 <_N 𝐽 ∨ 𝐾 = 𝐽 ∨ 𝐽 <_N 𝐾))
149	80, 108, 146, 148	mpjao3dan 1285	1 ⊢ (𝜑 → ¬ ((𝑆 +_Q (_Q‘[⟨𝐾, 1_o⟩] ~_Q )) <_Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +_Q (_Q‘[⟨𝐽, 1_o⟩] ~_Q )) <_Q 𝑆))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ w3o 961 ∧ w3a 962 = wceq 1331 ∈ wcel 1480 ∀wral 2416 ⟨cop 3530 class class class wbr 3929 ⟶wf 5119 ‘cfv 5123 (class class class)co 5774 1_oc1o 6306 [cec 6427 Ncnpi 7080 <_N clti 7083 ~_Q ceq 7087 Qcnq 7088 +_Q cplq 7090 *_Qcrq 7092 <_Q cltq 7093

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-coll 4043 ax-sep 4046 ax-nul 4054 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-iinf 4502

This theorem depends on definitions: df-bi 116 df-dc 820 df-3or 963 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-ral 2421 df-rex 2422 df-reu 2423 df-rab 2425 df-v 2688 df-sbc 2910 df-csb 3004 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-nul 3364 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-int 3772 df-iun 3815 df-br 3930 df-opab 3990 df-mpt 3991 df-tr 4027 df-eprel 4211 df-id 4215 df-po 4218 df-iso 4219 df-iord 4288 df-on 4290 df-suc 4293 df-iom 4505 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-rn 4550 df-res 4551 df-ima 4552 df-iota 5088 df-fun 5125 df-fn 5126 df-f 5127 df-f1 5128 df-fo 5129 df-f1o 5130 df-fv 5131 df-ov 5777 df-oprab 5778 df-mpo 5779 df-1st 6038 df-2nd 6039 df-recs 6202 df-irdg 6267 df-1o 6313 df-oadd 6317 df-omul 6318 df-er 6429 df-ec 6431 df-qs 6435 df-ni 7112 df-pli 7113 df-mi 7114 df-lti 7115 df-plpq 7152 df-mpq 7153 df-enq 7155 df-nqqs 7156 df-plqqs 7157 df-mqqs 7158 df-1nqqs 7159 df-rq 7160 df-ltnqqs 7161

This theorem is referenced by: caucvgprlemdisj 7482

W3C validator