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

Theorem caucvgprlemladdrl 6649
Description: Lemma for caucvgpr 6653. Adding 𝑆 after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.)
Hypotheses
Ref Expression
caucvgpr.f (φ𝐹:NQ)
caucvgpr.cau (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))
caucvgpr.bnd (φ𝑗 N A <Q (𝐹𝑗))
caucvgpr.lim 𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩
caucvgprlemladd.s (φ𝑆 Q)
Assertion
Ref Expression
caucvgprlemladdrl (φ → {𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆)} ⊆ (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)))
Distinct variable groups:   A,𝑗   𝑗,𝐹,u,𝑙   𝑛,𝐹,𝑘   𝑘,𝐿,𝑗   𝑆,𝑙,u,𝑗   𝑗,𝑘,𝑆
Allowed substitution hints:   φ(u,𝑗,𝑘,𝑛,𝑙)   A(u,𝑘,𝑛,𝑙)   𝑆(𝑛)   𝐿(u,𝑛,𝑙)

Proof of Theorem caucvgprlemladdrl
Dummy variables 𝑟 f g 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 3540 . . . . . . . . 9 (𝑗 = 𝑎 → ⟨𝑗, 1𝑜⟩ = ⟨𝑎, 1𝑜⟩)
21eceq1d 6078 . . . . . . . 8 (𝑗 = 𝑎 → [⟨𝑗, 1𝑜⟩] ~Q = [⟨𝑎, 1𝑜⟩] ~Q )
32fveq2d 5125 . . . . . . 7 (𝑗 = 𝑎 → (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))
43oveq2d 5471 . . . . . 6 (𝑗 = 𝑎 → (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) = (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )))
5 fveq2 5121 . . . . . . 7 (𝑗 = 𝑎 → (𝐹𝑗) = (𝐹𝑎))
65oveq1d 5470 . . . . . 6 (𝑗 = 𝑎 → ((𝐹𝑗) +Q 𝑆) = ((𝐹𝑎) +Q 𝑆))
74, 6breq12d 3768 . . . . 5 (𝑗 = 𝑎 → ((𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆) ↔ (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)))
87cbvrexv 2528 . . . 4 (𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆) ↔ 𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆))
98a1i 9 . . 3 (𝑙 Q → (𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆) ↔ 𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)))
109rabbiia 2541 . 2 {𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆)} = {𝑙 Q𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)}
11 oveq1 5462 . . . . . . 7 (𝑙 = 𝑟 → (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) = (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )))
1211breq1d 3765 . . . . . 6 (𝑙 = 𝑟 → ((𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆) ↔ (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)))
1312rexbidv 2321 . . . . 5 (𝑙 = 𝑟 → (𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆) ↔ 𝑎 N (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)))
1413elrab 2692 . . . 4 (𝑟 {𝑙 Q𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)} ↔ (𝑟 Q 𝑎 N (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)))
15 caucvgpr.f . . . . . . . . . . . . . . 15 (φ𝐹:NQ)
1615ad4antr 463 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → 𝐹:NQ)
17 caucvgpr.cau . . . . . . . . . . . . . . 15 (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))
1817ad4antr 463 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → 𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))
19 simpr 103 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → 𝑏 N)
20 simpllr 486 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → 𝑎 N)
2116, 18, 19, 20caucvgprlemnbj 6638 . . . . . . . . . . . . 13 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ¬ (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q (𝐹𝑎))
2215ad3antrrr 461 . . . . . . . . . . . . . . . . . 18 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝐹:NQ)
2322ffvelrnda 5245 . . . . . . . . . . . . . . . . 17 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (𝐹𝑏) Q)
24 nnnq 6405 . . . . . . . . . . . . . . . . . 18 (𝑏 N → [⟨𝑏, 1𝑜⟩] ~Q Q)
25 recclnq 6376 . . . . . . . . . . . . . . . . . 18 ([⟨𝑏, 1𝑜⟩] ~Q Q → (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) Q)
2619, 24, 253syl 17 . . . . . . . . . . . . . . . . 17 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) Q)
27 addclnq 6359 . . . . . . . . . . . . . . . . 17 (((𝐹𝑏) Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) Q) → ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) Q)
2823, 26, 27syl2anc 391 . . . . . . . . . . . . . . . 16 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) Q)
29 nnnq 6405 . . . . . . . . . . . . . . . . 17 (𝑎 N → [⟨𝑎, 1𝑜⟩] ~Q Q)
30 recclnq 6376 . . . . . . . . . . . . . . . . 17 ([⟨𝑎, 1𝑜⟩] ~Q Q → (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q)
3120, 29, 303syl 17 . . . . . . . . . . . . . . . 16 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q)
32 caucvgprlemladd.s . . . . . . . . . . . . . . . . 17 (φ𝑆 Q)
3332ad4antr 463 . . . . . . . . . . . . . . . 16 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → 𝑆 Q)
34 addassnqg 6366 . . . . . . . . . . . . . . . 16 ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q 𝑆 Q) → ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) +Q 𝑆) = (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆)))
3528, 31, 33, 34syl3anc 1134 . . . . . . . . . . . . . . 15 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) +Q 𝑆) = (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆)))
3635breq1d 3765 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) +Q 𝑆) <Q ((𝐹𝑎) +Q 𝑆) ↔ (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆)) <Q ((𝐹𝑎) +Q 𝑆)))
37 ltanqg 6384 . . . . . . . . . . . . . . . 16 ((f Q g Q Q) → (f <Q g ↔ ( +Q f) <Q ( +Q g)))
3837adantl 262 . . . . . . . . . . . . . . 15 ((((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) (f Q g Q Q)) → (f <Q g ↔ ( +Q f) <Q ( +Q g)))
39 addclnq 6359 . . . . . . . . . . . . . . . 16 ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q) → (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) Q)
4028, 31, 39syl2anc 391 . . . . . . . . . . . . . . 15 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) Q)
4116, 20ffvelrnd 5246 . . . . . . . . . . . . . . 15 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (𝐹𝑎) Q)
42 addcomnqg 6365 . . . . . . . . . . . . . . . 16 ((f Q g Q) → (f +Q g) = (g +Q f))
4342adantl 262 . . . . . . . . . . . . . . 15 ((((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) (f Q g Q)) → (f +Q g) = (g +Q f))
4438, 40, 41, 33, 43caovord2d 5612 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q (𝐹𝑎) ↔ ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) +Q 𝑆) <Q ((𝐹𝑎) +Q 𝑆)))
45 addcomnqg 6365 . . . . . . . . . . . . . . . . 17 ((𝑆 Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q) → (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) = ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆))
4633, 31, 45syl2anc 391 . . . . . . . . . . . . . . . 16 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) = ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆))
4746oveq2d 5471 . . . . . . . . . . . . . . 15 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) = (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆)))
4847breq1d 3765 . . . . . . . . . . . . . 14 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆) ↔ (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) +Q 𝑆)) <Q ((𝐹𝑎) +Q 𝑆)))
4936, 44, 483bitr4rd 210 . . . . . . . . . . . . 13 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆) ↔ (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q (𝐹𝑎)))
5021, 49mtbird 597 . . . . . . . . . . . 12 (((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) 𝑏 N) → ¬ (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆))
5150nrexdv 2406 . . . . . . . . . . 11 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ¬ 𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆))
5251intnand 839 . . . . . . . . . 10 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ¬ (((𝐹𝑎) +Q 𝑆) Q 𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆)))
5317ad3antrrr 461 . . . . . . . . . . . . 13 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))
54 caucvgpr.bnd . . . . . . . . . . . . . . 15 (φ𝑗 N A <Q (𝐹𝑗))
55 fveq2 5121 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑏 → (𝐹𝑗) = (𝐹𝑏))
5655breq2d 3767 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑏 → (A <Q (𝐹𝑗) ↔ A <Q (𝐹𝑏)))
5756cbvralv 2527 . . . . . . . . . . . . . . 15 (𝑗 N A <Q (𝐹𝑗) ↔ 𝑏 N A <Q (𝐹𝑏))
5854, 57sylib 127 . . . . . . . . . . . . . 14 (φ𝑏 N A <Q (𝐹𝑏))
5958ad3antrrr 461 . . . . . . . . . . . . 13 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝑏 N A <Q (𝐹𝑏))
60 caucvgpr.lim . . . . . . . . . . . . . 14 𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩
61 opeq1 3540 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑏 → ⟨𝑗, 1𝑜⟩ = ⟨𝑏, 1𝑜⟩)
6261eceq1d 6078 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑏 → [⟨𝑗, 1𝑜⟩] ~Q = [⟨𝑏, 1𝑜⟩] ~Q )
6362fveq2d 5125 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑏 → (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))
6463oveq2d 5471 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑏 → (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) = (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )))
6564, 55breq12d 3768 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑏 → ((𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗) ↔ (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝐹𝑏)))
6665cbvrexv 2528 . . . . . . . . . . . . . . . . 17 (𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗) ↔ 𝑏 N (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝐹𝑏))
6766a1i 9 . . . . . . . . . . . . . . . 16 (𝑙 Q → (𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗) ↔ 𝑏 N (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝐹𝑏)))
6867rabbiia 2541 . . . . . . . . . . . . . . 15 {𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)} = {𝑙 Q𝑏 N (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝐹𝑏)}
6955, 63oveq12d 5473 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑏 → ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) = ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )))
7069breq1d 3765 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑏 → (((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u ↔ ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q u))
7170cbvrexv 2528 . . . . . . . . . . . . . . . . 17 (𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u𝑏 N ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q u)
7271a1i 9 . . . . . . . . . . . . . . . 16 (u Q → (𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u𝑏 N ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q u))
7372rabbiia 2541 . . . . . . . . . . . . . . 15 {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u} = {u Q𝑏 N ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q u}
7468, 73opeq12i 3545 . . . . . . . . . . . . . 14 ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩ = ⟨{𝑙 Q𝑏 N (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝐹𝑏)}, {u Q𝑏 N ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q u}⟩
7560, 74eqtri 2057 . . . . . . . . . . . . 13 𝐿 = ⟨{𝑙 Q𝑏 N (𝑙 +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q (𝐹𝑏)}, {u Q𝑏 N ((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) <Q u}⟩
7632ad3antrrr 461 . . . . . . . . . . . . . 14 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝑆 Q)
7729, 30syl 14 . . . . . . . . . . . . . . 15 (𝑎 N → (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q)
7877ad2antlr 458 . . . . . . . . . . . . . 14 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q)
79 addclnq 6359 . . . . . . . . . . . . . 14 ((𝑆 Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) Q) → (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) Q)
8076, 78, 79syl2anc 391 . . . . . . . . . . . . 13 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) Q)
8122, 53, 59, 75, 80caucvgprlemladdfu 6648 . . . . . . . . . . . 12 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) ⊆ {u Q𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q u})
8281sseld 2938 . . . . . . . . . . 11 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (((𝐹𝑎) +Q 𝑆) (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) → ((𝐹𝑎) +Q 𝑆) {u Q𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q u}))
83 breq2 3759 . . . . . . . . . . . . 13 (u = ((𝐹𝑎) +Q 𝑆) → ((((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q u ↔ (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆)))
8483rexbidv 2321 . . . . . . . . . . . 12 (u = ((𝐹𝑎) +Q 𝑆) → (𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q u𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆)))
8584elrab 2692 . . . . . . . . . . 11 (((𝐹𝑎) +Q 𝑆) {u Q𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q u} ↔ (((𝐹𝑎) +Q 𝑆) Q 𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆)))
8682, 85syl6ib 150 . . . . . . . . . 10 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (((𝐹𝑎) +Q 𝑆) (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) → (((𝐹𝑎) +Q 𝑆) Q 𝑏 N (((𝐹𝑏) +Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )) +Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))) <Q ((𝐹𝑎) +Q 𝑆))))
8752, 86mtod 588 . . . . . . . . 9 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ¬ ((𝐹𝑎) +Q 𝑆) (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)))
8815, 17, 54, 60caucvgprlemcl 6647 . . . . . . . . . . . 12 (φ𝐿 P)
8988ad3antrrr 461 . . . . . . . . . . 11 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝐿 P)
90 nqprlu 6530 . . . . . . . . . . . 12 ((𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) Q → ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩ P)
9180, 90syl 14 . . . . . . . . . . 11 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩ P)
92 addclpr 6520 . . . . . . . . . . 11 ((𝐿 P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩ P) → (𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩) P)
9389, 91, 92syl2anc 391 . . . . . . . . . 10 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩) P)
94 prop 6458 . . . . . . . . . . 11 ((𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩) P → ⟨(1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)), (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩))⟩ P)
95 prloc 6474 . . . . . . . . . . 11 ((⟨(1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)), (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩))⟩ P (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ((𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) ((𝐹𝑎) +Q 𝑆) (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩))))
9694, 95sylan 267 . . . . . . . . . 10 (((𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩) P (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ((𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) ((𝐹𝑎) +Q 𝑆) (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩))))
9793, 96sylancom 397 . . . . . . . . 9 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ((𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) ((𝐹𝑎) +Q 𝑆) (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩))))
9887, 97ecased 1238 . . . . . . . 8 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)))
99 simpllr 486 . . . . . . . . 9 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝑟 Q)
10089, 76, 99, 78cauappcvgprlemcan 6616 . . . . . . . 8 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → ((𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ))}, {u ∣ (𝑆 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q u}⟩)) ↔ 𝑟 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩))))
10198, 100mpbid 135 . . . . . . 7 ((((φ 𝑟 Q) 𝑎 N) (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝑟 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)))
102101ex 108 . . . . . 6 (((φ 𝑟 Q) 𝑎 N) → ((𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆) → 𝑟 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩))))
103102rexlimdva 2427 . . . . 5 ((φ 𝑟 Q) → (𝑎 N (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆) → 𝑟 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩))))
104103expimpd 345 . . . 4 (φ → ((𝑟 Q 𝑎 N (𝑟 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)) → 𝑟 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩))))
10514, 104syl5bi 141 . . 3 (φ → (𝑟 {𝑙 Q𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)} → 𝑟 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩))))
106105ssrdv 2945 . 2 (φ → {𝑙 Q𝑎 N (𝑙 +Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )) <Q ((𝐹𝑎) +Q 𝑆)} ⊆ (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)))
10710, 106syl5eqss 2983 1 (φ → {𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆)} ⊆ (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   wo 628   w3a 884   = wceq 1242   wcel 1390  {cab 2023  wral 2300  wrex 2301  {crab 2304  wss 2911  cop 3370   class class class wbr 3755  wf 4841  cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  1𝑜c1o 5933  [cec 6040  Ncnpi 6256   <N clti 6259   ~Q ceq 6263  Qcnq 6264   +Q cplq 6266  *Qcrq 6268   <Q cltq 6269  Pcnp 6275   +P cpp 6277
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254
This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-eprel 4017  df-id 4021  df-po 4024  df-iso 4025  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-1o 5940  df-2o 5941  df-oadd 5944  df-omul 5945  df-er 6042  df-ec 6044  df-qs 6048  df-ni 6288  df-pli 6289  df-mi 6290  df-lti 6291  df-plpq 6328  df-mpq 6329  df-enq 6331  df-nqqs 6332  df-plqqs 6333  df-mqqs 6334  df-1nqqs 6335  df-rq 6336  df-ltnqqs 6337  df-enq0 6407  df-nq0 6408  df-0nq0 6409  df-plq0 6410  df-mq0 6411  df-inp 6449  df-iplp 6451  df-iltp 6453
This theorem is referenced by:  caucvgprlem1  6650
  Copyright terms: Public domain W3C validator