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

Theorem caucvgprlemk 6821
 Description: Lemma for caucvgpr 6838. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.)
Hypotheses
Ref Expression
caucvgprlemk.jk (𝜑𝐽 <N 𝐾)
caucvgprlemk.jkq (𝜑 → (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑄)
Assertion
Ref Expression
caucvgprlemk (𝜑 → (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑄)

Proof of Theorem caucvgprlemk
StepHypRef Expression
1 caucvgprlemk.jk . . . 4 (𝜑𝐽 <N 𝐾)
2 ltrelpi 6480 . . . . . . 7 <N ⊆ (N × N)
32brel 4420 . . . . . 6 (𝐽 <N 𝐾 → (𝐽N𝐾N))
41, 3syl 14 . . . . 5 (𝜑 → (𝐽N𝐾N))
5 ltnnnq 6579 . . . . 5 ((𝐽N𝐾N) → (𝐽 <N 𝐾 ↔ [⟨𝐽, 1𝑜⟩] ~Q <Q [⟨𝐾, 1𝑜⟩] ~Q ))
64, 5syl 14 . . . 4 (𝜑 → (𝐽 <N 𝐾 ↔ [⟨𝐽, 1𝑜⟩] ~Q <Q [⟨𝐾, 1𝑜⟩] ~Q ))
71, 6mpbid 139 . . 3 (𝜑 → [⟨𝐽, 1𝑜⟩] ~Q <Q [⟨𝐾, 1𝑜⟩] ~Q )
8 ltrnqi 6577 . . 3 ([⟨𝐽, 1𝑜⟩] ~Q <Q [⟨𝐾, 1𝑜⟩] ~Q → (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ))
97, 8syl 14 . 2 (𝜑 → (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ))
10 caucvgprlemk.jkq . 2 (𝜑 → (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑄)
11 ltsonq 6554 . . 3 <Q Or Q
12 ltrelnq 6521 . . 3 <Q ⊆ (Q × Q)
1311, 12sotri 4748 . 2 (((*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) ∧ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑄) → (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑄)
149, 10, 13syl2anc 397 1 (𝜑 → (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑄)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   ∈ wcel 1409  ⟨cop 3406   class class class wbr 3792  ‘cfv 4930  1𝑜c1o 6025  [cec 6135  Ncnpi 6428
 Copyright terms: Public domain W3C validator