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

Theorem caucvgprprlemval 6992
Description: Lemma for caucvgprpr 7016. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.)
Hypotheses
Ref Expression
caucvgprpr.f (𝜑𝐹:NP)
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 𝑢}⟩))))
Assertion
Ref Expression
caucvgprprlemval ((𝜑𝐴 <N 𝐵) → ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)))
Distinct variable groups:   𝐴,𝑙   𝑢,𝐴   𝐴,𝑝,𝑙   𝐴,𝑞,𝑢   𝑘,𝐹,𝑛   𝑘,𝑙,𝑛   𝑢,𝑘,𝑛
Allowed substitution hints:   𝜑(𝑢,𝑘,𝑛,𝑞,𝑝,𝑙)   𝐴(𝑘,𝑛)   𝐵(𝑢,𝑘,𝑛,𝑞,𝑝,𝑙)   𝐹(𝑢,𝑞,𝑝,𝑙)

Proof of Theorem caucvgprprlemval
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelpi 6628 . . . . 5 <N ⊆ (N × N)
21brel 4438 . . . 4 (𝐴 <N 𝐵 → (𝐴N𝐵N))
32adantl 271 . . 3 ((𝜑𝐴 <N 𝐵) → (𝐴N𝐵N))
4 caucvgprpr.f . . . . 5 (𝜑𝐹:NP)
5 caucvgprpr.cau . . . . 5 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
64, 5caucvgprprlemcbv 6991 . . . 4 (𝜑 → ∀𝑎N𝑏N (𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
76adantr 270 . . 3 ((𝜑𝐴 <N 𝐵) → ∀𝑎N𝑏N (𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
8 simpr 108 . . 3 ((𝜑𝐴 <N 𝐵) → 𝐴 <N 𝐵)
9 breq1 3808 . . . . 5 (𝑎 = 𝐴 → (𝑎 <N 𝑏𝐴 <N 𝑏))
10 fveq2 5229 . . . . . . 7 (𝑎 = 𝐴 → (𝐹𝑎) = (𝐹𝐴))
11 opeq1 3590 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → ⟨𝑎, 1𝑜⟩ = ⟨𝐴, 1𝑜⟩)
1211eceq1d 6229 . . . . . . . . . . . 12 (𝑎 = 𝐴 → [⟨𝑎, 1𝑜⟩] ~Q = [⟨𝐴, 1𝑜⟩] ~Q )
1312fveq2d 5233 . . . . . . . . . . 11 (𝑎 = 𝐴 → (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ))
1413breq2d 3817 . . . . . . . . . 10 (𝑎 = 𝐴 → (𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) ↔ 𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )))
1514abbidv 2200 . . . . . . . . 9 (𝑎 = 𝐴 → {𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )} = {𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )})
1613breq1d 3815 . . . . . . . . . 10 (𝑎 = 𝐴 → ((*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢 ↔ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢))
1716abbidv 2200 . . . . . . . . 9 (𝑎 = 𝐴 → {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢} = {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢})
1815, 17opeq12d 3598 . . . . . . . 8 (𝑎 = 𝐴 → ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ = ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)
1918oveq2d 5579 . . . . . . 7 (𝑎 = 𝐴 → ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))
2010, 19breq12d 3818 . . . . . 6 (𝑎 = 𝐴 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝐴)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
2110, 18oveq12d 5581 . . . . . . 7 (𝑎 = 𝐴 → ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))
2221breq2d 3817 . . . . . 6 (𝑎 = 𝐴 → ((𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝑏)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
2320, 22anbi12d 457 . . . . 5 (𝑎 = 𝐴 → (((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)) ↔ ((𝐹𝐴)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
249, 23imbi12d 232 . . . 4 (𝑎 = 𝐴 → ((𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))) ↔ (𝐴 <N 𝑏 → ((𝐹𝐴)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))))
25 breq2 3809 . . . . 5 (𝑏 = 𝐵 → (𝐴 <N 𝑏𝐴 <N 𝐵))
26 fveq2 5229 . . . . . . . 8 (𝑏 = 𝐵 → (𝐹𝑏) = (𝐹𝐵))
2726oveq1d 5578 . . . . . . 7 (𝑏 = 𝐵 → ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))
2827breq2d 3817 . . . . . 6 (𝑏 = 𝐵 → ((𝐹𝐴)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
2926breq1d 3815 . . . . . 6 (𝑏 = 𝐵 → ((𝐹𝑏)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
3028, 29anbi12d 457 . . . . 5 (𝑏 = 𝐵 → (((𝐹𝐴)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)) ↔ ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
3125, 30imbi12d 232 . . . 4 (𝑏 = 𝐵 → ((𝐴 <N 𝑏 → ((𝐹𝐴)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))) ↔ (𝐴 <N 𝐵 → ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))))
3224, 31rspc2v 2721 . . 3 ((𝐴N𝐵N) → (∀𝑎N𝑏N (𝑎 <N 𝑏 → ((𝐹𝑎)<P ((𝐹𝑏) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑏)<P ((𝐹𝑎) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑎, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))) → (𝐴 <N 𝐵 → ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))))
333, 7, 8, 32syl3c 62 . 2 ((𝜑𝐴 <N 𝐵) → ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)))
34 breq1 3808 . . . . . . 7 (𝑙 = 𝑝 → (𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) ↔ 𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )))
3534cbvabv 2206 . . . . . 6 {𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )} = {𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}
36 breq2 3809 . . . . . . 7 (𝑢 = 𝑞 → ((*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢 ↔ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞))
3736cbvabv 2206 . . . . . 6 {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢} = {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}
3835, 37opeq12i 3595 . . . . 5 ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ = ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩
3938oveq2i 5574 . . . 4 ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝐵) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)
4039breq2i 3813 . . 3 ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
4138oveq2i 5574 . . . 4 ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) = ((𝐹𝐴) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)
4241breq2i 3813 . . 3 ((𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ↔ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
4340, 42anbi12i 448 . 2 (((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)) ↔ ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)))
4433, 43sylib 120 1 ((𝜑𝐴 <N 𝐵) → ((𝐹𝐴)<P ((𝐹𝐵) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∧ (𝐹𝐵)<P ((𝐹𝐴) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐴, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1285  wcel 1434  {cab 2069  wral 2353  cop 3419   class class class wbr 3805  wf 4948  cfv 4952  (class class class)co 5563  1𝑜c1o 6078  [cec 6191  Ncnpi 6576   <N clti 6579   ~Q ceq 6583  *Qcrq 6588   <Q cltq 6589  Pcnp 6595   +P cpp 6597  <P cltp 6599
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-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-pow 3968  ax-pr 3992
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2612  df-un 2986  df-in 2988  df-ss 2995  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-br 3806  df-opab 3860  df-xp 4397  df-cnv 4399  df-dm 4401  df-rn 4402  df-res 4403  df-ima 4404  df-iota 4917  df-fv 4960  df-ov 5566  df-ec 6195  df-lti 6611
This theorem is referenced by:  caucvgprprlemnkltj  6993  caucvgprprlemnjltk  6995  caucvgprprlemnbj  6997
  Copyright terms: Public domain W3C validator