Metamath Proof Explorer

Theorem monotuz

Description: A function defined on an upper set of integers which increases at every adjacent pair is globally strictly monotonic by induction. (Contributed by Stefan O'Rear, 24-Sep-2014)

Ref Expression
Hypotheses monotuz.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐻 ) → 𝐹 < 𝐺 )
monotuz.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) → 𝐶 ∈ ℝ )
monotuz.3 ⊢ 𝐻 = ( ℤ≥ ‘ 𝐼 )
monotuz.4 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → 𝐶 = 𝐺 )
monotuz.5 ⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐹 )
monotuz.6 ⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐷 )
monotuz.7 ⊢ ( 𝑥 = 𝐵 → 𝐶 = 𝐸 )
Assertion monotuz ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ) → ( 𝐴 < 𝐵 ↔ 𝐷 < 𝐸 ) )

Proof

Step Hyp Ref Expression
1 monotuz.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐻 ) → 𝐹 < 𝐺 )
2 monotuz.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) → 𝐶 ∈ ℝ )
3 monotuz.3 ⊢ 𝐻 = ( ℤ≥ ‘ 𝐼 )
4 monotuz.4 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → 𝐶 = 𝐺 )
5 monotuz.5 ⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐹 )
6 monotuz.6 ⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐷 )
7 monotuz.7 ⊢ ( 𝑥 = 𝐵 → 𝐶 = 𝐸 )
8 csbeq1 ⊢ ( 𝑎 = 𝑏 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 )
9 csbeq1 ⊢ ( 𝑎 = 𝐴 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
10 csbeq1 ⊢ ( 𝑎 = 𝐵 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑥 ⦌ 𝐶 )
11 uzssz ⊢ ( ℤ≥ ‘ 𝐼 ) ⊆ ℤ
12 zssre ⊢ ℤ ⊆ ℝ
13 11 12 sstri ⊢ ( ℤ≥ ‘ 𝐼 ) ⊆ ℝ
14 3 13 eqsstri ⊢ 𝐻 ⊆ ℝ
15 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑎 ∈ 𝐻 )
16 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶
17 16 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ ℝ
18 15 17 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ ℝ )
19 eleq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ∈ 𝐻 ↔ 𝑎 ∈ 𝐻 ) )
20 19 anbi2d ⊢ ( 𝑥 = 𝑎 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) ↔ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ) )
21 csbeq1a ⊢ ( 𝑥 = 𝑎 → 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
22 21 eleq1d ⊢ ( 𝑥 = 𝑎 → ( 𝐶 ∈ ℝ ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ ℝ ) )
23 20 22 imbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) → 𝐶 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ ℝ ) ) )
24 18 23 2 chvarfv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ ℝ )
25 simpl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑎 < 𝑏 ) → ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) )
26 25 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑎 < 𝑏 ) → ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) )
27 3 11 eqsstri ⊢ 𝐻 ⊆ ℤ
28 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 ∈ 𝐻 )
29 27 28 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 ∈ ℤ )
30 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑎 < 𝑏 ) → 𝑏 ∈ 𝐻 )
31 27 30 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑎 < 𝑏 ) → 𝑏 ∈ ℤ )
32 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑎 < 𝑏 ) → 𝑎 < 𝑏 )
33 csbeq1 ⊢ ( 𝑐 = ( 𝑎 + 1 ) → ⦋ 𝑐 / 𝑥 ⦌ 𝐶 = ⦋ ( 𝑎 + 1 ) / 𝑥 ⦌ 𝐶 )
34 33 breq2d ⊢ ( 𝑐 = ( 𝑎 + 1 ) → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑎 + 1 ) / 𝑥 ⦌ 𝐶 ) )
35 34 imbi2d ⊢ ( 𝑐 = ( 𝑎 + 1 ) → ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑎 + 1 ) / 𝑥 ⦌ 𝐶 ) ) )
36 csbeq1 ⊢ ( 𝑐 = 𝑑 → ⦋ 𝑐 / 𝑥 ⦌ 𝐶 = ⦋ 𝑑 / 𝑥 ⦌ 𝐶 )
37 36 breq2d ⊢ ( 𝑐 = 𝑑 → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) )
38 37 imbi2d ⊢ ( 𝑐 = 𝑑 → ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) ) )
39 csbeq1 ⊢ ( 𝑐 = ( 𝑑 + 1 ) → ⦋ 𝑐 / 𝑥 ⦌ 𝐶 = ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 )
40 39 breq2d ⊢ ( 𝑐 = ( 𝑑 + 1 ) → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 ) )
41 40 imbi2d ⊢ ( 𝑐 = ( 𝑑 + 1 ) → ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 ) ) )
42 csbeq1 ⊢ ( 𝑐 = 𝑏 → ⦋ 𝑐 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 )
43 42 breq2d ⊢ ( 𝑐 = 𝑏 → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑏 / 𝑥 ⦌ 𝐶 ) )
44 43 imbi2d ⊢ ( 𝑐 = 𝑏 → ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑏 / 𝑥 ⦌ 𝐶 ) ) )
45 eleq1 ⊢ ( 𝑦 = 𝑎 → ( 𝑦 ∈ 𝐻 ↔ 𝑎 ∈ 𝐻 ) )
46 45 anbi2d ⊢ ( 𝑦 = 𝑎 → ( ( 𝜑 ∧ 𝑦 ∈ 𝐻 ) ↔ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ) )
47 vex ⊢ 𝑦 ∈ V
48 47 5 csbie ⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = 𝐹
49 csbeq1 ⊢ ( 𝑦 = 𝑎 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
50 48 49 eqtr3id ⊢ ( 𝑦 = 𝑎 → 𝐹 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
51 ovex ⊢ ( 𝑦 + 1 ) ∈ V
52 51 4 csbie ⊢ ⦋ ( 𝑦 + 1 ) / 𝑥 ⦌ 𝐶 = 𝐺
53 oveq1 ⊢ ( 𝑦 = 𝑎 → ( 𝑦 + 1 ) = ( 𝑎 + 1 ) )
54 53 csbeq1d ⊢ ( 𝑦 = 𝑎 → ⦋ ( 𝑦 + 1 ) / 𝑥 ⦌ 𝐶 = ⦋ ( 𝑎 + 1 ) / 𝑥 ⦌ 𝐶 )
55 52 54 eqtr3id ⊢ ( 𝑦 = 𝑎 → 𝐺 = ⦋ ( 𝑎 + 1 ) / 𝑥 ⦌ 𝐶 )
56 50 55 breq12d ⊢ ( 𝑦 = 𝑎 → ( 𝐹 < 𝐺 ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑎 + 1 ) / 𝑥 ⦌ 𝐶 ) )
57 46 56 imbi12d ⊢ ( 𝑦 = 𝑎 → ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐻 ) → 𝐹 < 𝐺 ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑎 + 1 ) / 𝑥 ⦌ 𝐶 ) ) )
58 57 1 vtoclg ⊢ ( 𝑎 ∈ ℤ → ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑎 + 1 ) / 𝑥 ⦌ 𝐶 ) )
59 24 3ad2ant2 ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ ℝ )
60 simp2l ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → 𝜑 )
61 zre ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℝ )
62 61 3ad2ant1 ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) → 𝑎 ∈ ℝ )
63 zre ⊢ ( 𝑑 ∈ ℤ → 𝑑 ∈ ℝ )
64 63 3ad2ant2 ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) → 𝑑 ∈ ℝ )
65 simp3 ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) → 𝑎 < 𝑑 )
66 62 64 65 ltled ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) → 𝑎 ≤ 𝑑 )
67 66 3ad2ant1 ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → 𝑎 ≤ 𝑑 )
68 simp11 ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → 𝑎 ∈ ℤ )
69 simp12 ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → 𝑑 ∈ ℤ )
70 eluz ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( 𝑑 ∈ ( ℤ≥ ‘ 𝑎 ) ↔ 𝑎 ≤ 𝑑 ) )
71 68 69 70 syl2anc ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → ( 𝑑 ∈ ( ℤ≥ ‘ 𝑎 ) ↔ 𝑎 ≤ 𝑑 ) )
72 67 71 mpbird ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → 𝑑 ∈ ( ℤ≥ ‘ 𝑎 ) )
73 simp2r ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → 𝑎 ∈ 𝐻 )
74 73 3 eleqtrdi ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → 𝑎 ∈ ( ℤ≥ ‘ 𝐼 ) )
75 uztrn ⊢ ( ( 𝑑 ∈ ( ℤ≥ ‘ 𝑎 ) ∧ 𝑎 ∈ ( ℤ≥ ‘ 𝐼 ) ) → 𝑑 ∈ ( ℤ≥ ‘ 𝐼 ) )
76 72 74 75 syl2anc ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → 𝑑 ∈ ( ℤ≥ ‘ 𝐼 ) )
77 76 3 eleqtrrdi ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → 𝑑 ∈ 𝐻 )
78 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑑 ∈ 𝐻 )
79 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑑 / 𝑥 ⦌ 𝐶
80 79 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ∈ ℝ
81 78 80 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑑 ∈ 𝐻 ) → ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ∈ ℝ )
82 eleq1 ⊢ ( 𝑥 = 𝑑 → ( 𝑥 ∈ 𝐻 ↔ 𝑑 ∈ 𝐻 ) )
83 82 anbi2d ⊢ ( 𝑥 = 𝑑 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) ↔ ( 𝜑 ∧ 𝑑 ∈ 𝐻 ) ) )
84 csbeq1a ⊢ ( 𝑥 = 𝑑 → 𝐶 = ⦋ 𝑑 / 𝑥 ⦌ 𝐶 )
85 84 eleq1d ⊢ ( 𝑥 = 𝑑 → ( 𝐶 ∈ ℝ ↔ ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ∈ ℝ ) )
86 83 85 imbi12d ⊢ ( 𝑥 = 𝑑 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) → 𝐶 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑑 ∈ 𝐻 ) → ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ∈ ℝ ) ) )
87 81 86 2 chvarfv ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐻 ) → ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ∈ ℝ )
88 60 77 87 syl2anc ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ∈ ℝ )
89 peano2uz ⊢ ( 𝑑 ∈ ( ℤ≥ ‘ 𝐼 ) → ( 𝑑 + 1 ) ∈ ( ℤ≥ ‘ 𝐼 ) )
90 76 89 syl ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → ( 𝑑 + 1 ) ∈ ( ℤ≥ ‘ 𝐼 ) )
91 90 3 eleqtrrdi ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → ( 𝑑 + 1 ) ∈ 𝐻 )
92 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑑 + 1 ) ∈ 𝐻 )
93 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶
94 93 nfel1 ⊢ Ⅎ 𝑥 ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 ∈ ℝ
95 92 94 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 𝑑 + 1 ) ∈ 𝐻 ) → ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 ∈ ℝ )
96 ovex ⊢ ( 𝑑 + 1 ) ∈ V
97 eleq1 ⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( 𝑥 ∈ 𝐻 ↔ ( 𝑑 + 1 ) ∈ 𝐻 ) )
98 97 anbi2d ⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) ↔ ( 𝜑 ∧ ( 𝑑 + 1 ) ∈ 𝐻 ) ) )
99 csbeq1a ⊢ ( 𝑥 = ( 𝑑 + 1 ) → 𝐶 = ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 )
100 99 eleq1d ⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( 𝐶 ∈ ℝ ↔ ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 ∈ ℝ ) )
101 98 100 imbi12d ⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) → 𝐶 ∈ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝑑 + 1 ) ∈ 𝐻 ) → ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 ∈ ℝ ) ) )
102 95 96 101 2 vtoclf ⊢ ( ( 𝜑 ∧ ( 𝑑 + 1 ) ∈ 𝐻 ) → ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 ∈ ℝ )
103 60 91 102 syl2anc ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 ∈ ℝ )
104 simp3 ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 )
105 nfv ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑑 ∈ 𝐻 ) → ⦋ 𝑑 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 )
106 eleq1 ⊢ ( 𝑦 = 𝑑 → ( 𝑦 ∈ 𝐻 ↔ 𝑑 ∈ 𝐻 ) )
107 106 anbi2d ⊢ ( 𝑦 = 𝑑 → ( ( 𝜑 ∧ 𝑦 ∈ 𝐻 ) ↔ ( 𝜑 ∧ 𝑑 ∈ 𝐻 ) ) )
108 csbeq1 ⊢ ( 𝑦 = 𝑑 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ 𝑑 / 𝑥 ⦌ 𝐶 )
109 48 108 eqtr3id ⊢ ( 𝑦 = 𝑑 → 𝐹 = ⦋ 𝑑 / 𝑥 ⦌ 𝐶 )
110 oveq1 ⊢ ( 𝑦 = 𝑑 → ( 𝑦 + 1 ) = ( 𝑑 + 1 ) )
111 110 csbeq1d ⊢ ( 𝑦 = 𝑑 → ⦋ ( 𝑦 + 1 ) / 𝑥 ⦌ 𝐶 = ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 )
112 52 111 eqtr3id ⊢ ( 𝑦 = 𝑑 → 𝐺 = ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 )
113 109 112 breq12d ⊢ ( 𝑦 = 𝑑 → ( 𝐹 < 𝐺 ↔ ⦋ 𝑑 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 ) )
114 107 113 imbi12d ⊢ ( 𝑦 = 𝑑 → ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐻 ) → 𝐹 < 𝐺 ) ↔ ( ( 𝜑 ∧ 𝑑 ∈ 𝐻 ) → ⦋ 𝑑 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 ) ) )
115 105 114 1 chvarfv ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐻 ) → ⦋ 𝑑 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 )
116 60 77 115 syl2anc ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → ⦋ 𝑑 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 )
117 59 88 103 104 116 lttrd ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) ∧ ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 )
118 117 3exp ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) → ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 ) ) )
119 118 a2d ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 𝑎 < 𝑑 ) → ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑑 / 𝑥 ⦌ 𝐶 ) → ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ ( 𝑑 + 1 ) / 𝑥 ⦌ 𝐶 ) ) )
120 35 38 41 44 58 119 uzind2 ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑎 < 𝑏 ) → ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑏 / 𝑥 ⦌ 𝐶 ) )
121 29 31 32 120 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑎 < 𝑏 ) → ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑏 / 𝑥 ⦌ 𝐶 ) )
122 26 121 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) ∧ 𝑎 < 𝑏 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑏 / 𝑥 ⦌ 𝐶 )
123 122 ex ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → ( 𝑎 < 𝑏 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 < ⦋ 𝑏 / 𝑥 ⦌ 𝐶 ) )
124 8 9 10 14 24 123 ltord1 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ) → ( 𝐴 < 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 < ⦋ 𝐵 / 𝑥 ⦌ 𝐶 ) )
125 nfcvd ⊢ ( 𝐴 ∈ 𝐻 → Ⅎ 𝑥 𝐷 )
126 125 6 csbiegf ⊢ ( 𝐴 ∈ 𝐻 → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐷 )
127 nfcvd ⊢ ( 𝐵 ∈ 𝐻 → Ⅎ 𝑥 𝐸 )
128 127 7 csbiegf ⊢ ( 𝐵 ∈ 𝐻 → ⦋ 𝐵 / 𝑥 ⦌ 𝐶 = 𝐸 )
129 126 128 breqan12d ⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 < ⦋ 𝐵 / 𝑥 ⦌ 𝐶 ↔ 𝐷 < 𝐸 ) )
130 129 adantl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ) → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 < ⦋ 𝐵 / 𝑥 ⦌ 𝐶 ↔ 𝐷 < 𝐸 ) )
131 124 130 bitrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ) → ( 𝐴 < 𝐵 ↔ 𝐷 < 𝐸 ) )