Let$$V'(x)=\#\{\phi(m) : 1\leq m\leq x\}$$and$$V(x)=\#\{\phi(m) \leq x : 1\leq m\}.$$ Does $\lim V(x)/V'(x)$ exist?

1True ↔2  ∃ L > 1,3    Filter.Tendsto4      (fun x => ↑{k | k ∈ Set.range Nat.totient ∧ ↑k ≤ x}.ncard / ↑(Nat.totient '' {m | 1 ≤ m ∧ ↑m ≤ x}).ncard)5      Filter.atTop (nhds L)